theories

Type Members

1. class ADT extends SMTLinearisableTheory

   

   Theory solver for algebraic data-types.

2. abstract class AbstractSaturationProcedure extends Theory

   

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

4. type ExtArray = theories.arrays.ExtArray

   

   Extensional arrays

5. type Heap = theories.heaps.Heap

   

   Heaps

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

7. trait MulTheory extends Theory

   

   Trait for theories providing general, non-linear multiplication.

8. abstract class SaturationProcedure extends AbstractSaturationProcedure

   

   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.

9. type SimpleArray = theories.arrays.SimpleArray

   

   Untyped arrays

10. abstract class TermBasedSaturationProcedure extends AbstractSaturationProcedure

    

    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 version of a saturation procedure only supports rules whose application points can be specified using a fixed-arity vector of terms, for instance the arguments of certain atoms occurring in a proof goal. The procedure takes simplification of terms occurring in the proof goal into account. It is defined in such a way that application points that occur repeatedly can also lead to repeated application of the rule. Application points are handled by a single task (with priority basePriority) added to the task queue, which will always pick the application point with the highest priority and apply the defined handler to it. The flag priorityUpdates enables continuous updates of the priority of application points.

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

12. abstract class TheoryBuilder extends AnyRef

    

    Interface to construct theory objects with complex parameters.

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

    

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