ap.theories.bitvectors.ModuloArithmetic
ModSort
Related Doc:
package ModuloArithmetic
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.
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 variable with given de Bruijn index and this sort.
The variable with given de Bruijn index and this sort.
The cardinality of sorts with fixed-size, finite domain.
Extract a term representation of some value in the sort.
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.
Terms representing elements of the sort.
Constraints defining the range of the 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.
Modulo sorts, representing the interval
[lower, upper]with wrap-around arithmetic.