Type Members

1.  case class AndLazyConjunction(left: LazyConjunction, right: LazyConjunction, newOrder: TermOrder) extends LazyConjunction with Iterable[Formula] with Product with Serializable

   Attributes

   protected

2.  case class AtomicLazyConjunction(form: Formula, newOrder: TermOrder) extends LazyConjunction with Product with Serializable

   Attributes

   protected

3.  abstract class ConjunctEliminator extends AnyRef

   Class for removing irrelevant conjuncts from a conjunction (like equations that have been applied to all other formulas)

4.  class Conjunction extends Formula with SortedWithOrder[Conjunction]

   Class for representing (possibly quantified) conjunctions of arithmetic literal (equations, inequalities), predicate literals and negated Conjunctions.

   Class for representing (possibly quantified) conjunctions of arithmetic literal (equations, inequalities), predicate literals and negated Conjunctions. quans describes how the lowest quans.size variables are quantified in the conjunction (quans(0)) is responsible for VariableTerm(0) and is the innermost quantifier, etc).

5.  class IterativeClauseMatcher extends Sorted[IterativeClauseMatcher]
6.  sealed abstract class LazyConjunction extends AnyRef

   A lazy version of conjunctions.

   A lazy version of conjunctions. This class can be useful when recursively constructing large formulae, since the number of invocations of methods of the class Conjunction is reduced.

7.  case class NegLazyConjunction(conj: LazyConjunction) extends LazyConjunction with Product with Serializable

   Attributes

   protected

8.  class NegatedConjunctions extends Formula with SortedWithOrder[NegatedConjunctions] with IndexedSeq[Conjunction]

   Class for representing a conjunction of negated Conjunctions.

9.  sealed abstract class Quantifier extends AnyRef
10.  class ReduceWithConjunction extends AnyRef
11.  abstract class ReducerPlugin extends AnyRef

    Interface for plugins that can be added to the ReduceWithConjunction class.

12.  abstract class ReducerPluginFactory extends AnyRef

    Factory to construct new reducer plugins.

13.  class SeqReducerPlugin extends ReducerPlugin

    Reducer plugin that sequentially applies a list of plugins.

14.  class SeqReducerPluginFactory extends ReducerPluginFactory
15.  class SubsumptionRemover extends AnyRef

    Naive version of a subsumption test