Type Members

1.  class ArithConj extends Formula with SortedWithOrder[ArithConj]

   The class for a conjunction of equations, negated equations and inequalities

2.  case class ElimPredModelElement(_preds: Set[Predicate]) extends ModelElement with Product with Serializable

   Class for storing information about eliminated predicates, without giving a precise description how their value can be reconstructed.

   Class for storing information about eliminated predicates, without giving a precise description how their value can be reconstructed. This is currently used for "abbreviations", which are eliminated from proof branches when it becomes clear that they will never be expanded.

3.  case class EqModelElement(eqs: EquationConj, _cs: Set[ConstantTerm]) extends ModelElement with Product with Serializable

   Class for creating models (assignments of integer literals to constants) of Formula, for certain special cases.

   Class for creating models (assignments of integer literals to constants) of Formula, for certain special cases. This class is used in EliminateFactsTask

4.  case class EquivModelElement(booleanAssignments: Seq[(Atom, Conjunction)]) extends ModelElement with Product with Serializable

   Class for creating models that assign truth values to Boolean variables.

5.  case class InNegEqModelElement(ac: ArithConj, _cs: Set[ConstantTerm]) extends ModelElement with Product with Serializable

   Class for creating models (assignments of integer literals to constants) of Formula, for certain special cases.

   Class for creating models (assignments of integer literals to constants) of Formula, for certain special cases. This class is used in EliminateFactsTask

6.  sealed abstract class ModelElement extends AnyRef

   Class for creating models (assignments of integer literals to constants, and boolean variables to truth values) of Formula, for certain special cases.

   Class for creating models (assignments of integer literals to constants, and boolean variables to truth values) of Formula, for certain special cases. This class is used in EliminateFactsTask

7.  case class ReducableModelElement(f: Conjunction, _cs: Set[ConstantTerm], reducerSettings: ReducerSettings) extends ModelElement with Product with Serializable

   Class for creating models based on formulas from which a reducer is able to extract an assignment.

8.  class ReduceWithAC extends AnyRef