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.
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