theories
Theory solver for algebraic data-types.
Theory representing the SMT-LIB semantics of division and modulo by zero.
Theory representing the SMT-LIB semantics of division and modulo by zero. According to SMT-LIB, division is a total function, and division by zero has to be represented as a unary uninterpreted function.
Theory of extensional arrays.
A theory for explicitly enumerating all values of integer terms.
A theory for explicitly enumerating all values of integer
terms. The proof procedure that will take care of the splitting
will be given the priority specified by
splitterCost. The splitting of the value range of
terms will initially be binary; once the range of possible values
of a term has been narrowed down to at most
completeSplitBound values, in a single step the range
will be split into all individual values.
Trait for theories providing general, non-linear multiplication.
Simple implementation of an array theory.
trait for representing signature and axioms of theories, e.g., the theory of arrays.
trait for representing signature and axioms of theories, e.g., the theory of arrays. This is used to make sure that theory symbols are unique.
Interface to construct theory objects with complex parameters.
Class to find out which theories where used in a given set of formulae/expressions
Multiplication by means of axioms describing shift-and-add
A dummy theory that represents the functional consistency axioms for functional predicates.
Non-linear arithmetic, support for general multiplication
Temporary hack to track incompleteness of theory implementations.
Bit-vectors and modular arithmetic
Class for keeping track of instantiated theories.
Package object making available some of the objects in sub-packages