A | |
| ARITH [Infsys] |
Abstract interface of an inference system for arithmetic theories
as an extension of the
Infsys.EQ signature.
|
D | |
| DEP [Solution] |
Iterators over dependency index.
|
E | |
| EQ [Infsys] |
Abstract interface of an inference system for equality theories.
|
| EXT [Solution] |
An equality theory is specified by means of its name
th,, a term map f a for replacing uninterpreted positions x of a
with f x and canonizing the resulting term in theory th., side effects when updating and restricting solution sets.
|
L | |
| LEVEL [Infsys] |
Specification of tracer for inference system.
|
O | |
| OPS [Can] |
Operations for canonizable theories.
|
R | |
| Rat [Euclid] |
The argument signature of the functor
Euclid.Make
May only be instantiated with a structure isomorphic to
the rationals.
|
S | |
| S [Euclid] |
Input signature of the functor
Euclid.Make.
|
| SET [Solution] |
Signature for equality sets.
|
| SET0 [Solution] |
Solution set without field extension.
|
| SIG [Acsym] |
Specification of a signature
th with one binary,
associative-commutative (AC) function symbol f.
|
| SIG [Ac] |
Specification of a signature
th with one binary,
associative-commutative (AC) function symbol f.
|
T | |
| T [Shostak] |
A Shostak theory
th is specified by means of a replacement map f a for replacing uninterpreted
subterms of a with f a and canonizing the result, and, a solver solve. , an extended canonizer map f a for replacing uninterpreted
positions x of a with f b followed by canonization in the
given theory, and, a branching function disjunction. If disjunction always returns Not_found,
then th is also said to be a convex Shostak theory.
|
| T [Can] |
A canonizable and ground confluent theory
th is specified
by means of a replacement map f a for replacing uninterpreted
subterms of a with f a and canonizing the result,, a theory-specific canonizer;, chainings functions of_var_equal, of_var_diseq, of_var_diseq
for keeping equality sets ground confluent by triggering inference rules
on pure equalities, variable equalities, and variable disequalities, respectively; and, a branching function disjunction.
|
| TERM [Acsym] |
Canonizer and iterators for AC theories.
|
| TERM [Ac] |
Canonizer and iterators for AC theories.
|