theories

Type Members

1. class ADT extends SMTLinearisableTheory

   

   Theory solver for algebraic data-types.

2. class DivZero extends Theory

   

   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.

3. type ExtArray = theories.arrays.ExtArray

   

   Extensional arrays

4. class Heap extends SMTLinearisableTheory

   

5. class IntValueEnumTheory extends Theory

   

   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. In order to initiate splitting, literals IntValueEnumTheory.enumPred(t) have to be added to a proof goal.

6. trait MulTheory extends Theory

   

   Trait for theories providing general, non-linear multiplication.

7. abstract class SaturationProcedure extends Theory

   

   Class to simplify the implementation of saturation procedures as part of theory plugins.

   Class to simplify the implementation of saturation procedures as part of theory plugins. A saturation procedure is a procedure waiting for patterns to occur in a proof goal (e.g., formulas of a certain shape), and can apply proof rules for every such occurrence. Saturation will be implemented by adding tasks to the task queue of every goal, so that the prover can globally schedule the different rules to be applied.

   This procedure does not take into account that applications points might get rewritten during the proof process; e.g., a variable x could turn into y when the equation x = y appears. In such cases, the saturation rule could get applied repeatedly for the same point.

8. type SimpleArray = theories.arrays.SimpleArray

   

   Untyped arrays

9. trait Theory extends AnyRef

   

   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.

10. abstract class TheoryBuilder extends AnyRef

    

    Interface to construct theory objects with complex parameters.

11. class TheoryCollector extends CollectingVisitor[Unit, Unit] with Cloneable

    

    Class to find out which theories where used in a given set of formulae/expressions