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