TheorySort
Related Doc:
package Theory
Extract constructor terms from a model.
Extract constructor terms from a model. Such terms will always be
encoded as integers, and integers can have different meaning
depending on the considered sort. Each sort can add the terms
representing a model to the assignment
map. Alternatively, a sort can add indexes to the
definedTerms set to indicate a particular index is
defined by a model, but the corresponding constructor term is not
available yet because it refers to other terms that are not yet
available.
The cardinality of sorts with fixed-size, finite domain.
The cardinality of sorts with fixed-size, finite domain.
Terms representing elements of the sort.
Terms representing elements of the sort.
Constraints defining the range of the sort.
Constraints defining the range of the sort.
Query the theory that the sort belongs to.
Higher-order syntax for universal quantifiers.
Higher-order syntax for universal quantifiers. This makes it possible
to write a quantifier as
Sort.all((a, b, c, d, e) => phi(a, b, c, d, e)).
Higher-order syntax for universal quantifiers.
Higher-order syntax for universal quantifiers. This makes it possible
to write a quantifier as
Sort.all((a, b, c, d) => phi(a, b, c, d)).
Higher-order syntax for universal quantifiers.
Higher-order syntax for universal quantifiers. This makes it possible
to write a quantifier as
Sort.all((a, b, c) => phi(a, b, c)).
Higher-order syntax for universal quantifiers.
Higher-order syntax for universal quantifiers. This makes it possible
to write a quantifier as Sort.all((a, b) => phi(a, b)).
Higher-order syntax for universal quantifiers.
Higher-order syntax for universal quantifiers. This makes it possible
to write a quantifier as Sort.all(a => phi(a)).
Add an existential quantifier for the variable with de Bruijn index 0, together with a guard representing this sort.
Add an existential quantifier for the variable with de Bruijn index 0, together with a guard representing this sort.
Extract a term representation of some value in the sort.
Extract a term representation of some value in the sort.
The variable with given de Bruijn index and this sort.
The variable with given de Bruijn index and this sort.
Extract a term representation of some value in the sort.
Extract a term representation of some value in the sort. This method can be overwritten in sub-classes to decode in a sort-specific way
Higher-order syntax for epsilon-expressions.
Higher-order syntax for epsilon-expressions. This makes it possible
to write things like Sort.eps(a => phi(a)).
Generate an epsilon-expression.
Generate an epsilon-expression.
Higher-order syntax for existential quantifiers.
Higher-order syntax for existential quantifiers. This makes it possible
to write a quantifier as
Sort.ex((a, b, c, d, e) => phi(a, b, c, d, e)).
Higher-order syntax for existential quantifiers.
Higher-order syntax for existential quantifiers. This makes it possible
to write a quantifier as
Sort.ex((a, b, c, d) => phi(a, b, c, d)).
Higher-order syntax for existential quantifiers.
Higher-order syntax for existential quantifiers. This makes it possible
to write a quantifier as
Sort.ex((a, b, c) => phi(a, b, c)).
Higher-order syntax for existential quantifiers.
Higher-order syntax for existential quantifiers. This makes it possible
to write a quantifier as Sort.ex((a, b) => phi(a, b)).
Higher-order syntax for existential quantifiers.
Higher-order syntax for existential quantifiers. This makes it possible
to write a quantifier as Sort.ex(a => phi(a)).
Add an existential quantifier for the variable with de Bruijn index 0, together with a guard representing this sort.
Add an existential quantifier for the variable with de Bruijn index 0, together with a guard representing this sort.
Allocation of a new constant with this sort.
Allocation of a new constant with this sort.
A witness term proving that the sort is inhabited.
A witness term proving that the sort is inhabited.
(Since version ) see corresponding Javadoc for more information.
Trait for sorts that belong to a specific theory.