Theory solver for algebraic data-types.
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