Package

ap.terfor

conjunctions

Permalink

package conjunctions

Visibility
  1. Public
  2. All

Type Members

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

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

    Permalink
    Attributes
    protected
  3. abstract class ConjunctEliminator extends AnyRef

    Permalink

    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]

    Permalink

    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]

    Permalink
  6. sealed abstract class LazyConjunction extends AnyRef

    Permalink

    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

    Permalink
    Attributes
    protected
  8. class NegatedConjunctions extends Formula with SortedWithOrder[NegatedConjunctions] with IndexedSeq[Conjunction]

    Permalink

    Class for representing a conjunction of negated Conjunctions.

    Class for representing a conjunction of negated Conjunctions.

  9. sealed abstract class Quantifier extends AnyRef

    Permalink
  10. class ReduceWithConjunction extends AnyRef

    Permalink
  11. abstract class ReducerPlugin extends AnyRef

    Permalink

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

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

  12. abstract class ReducerPluginFactory extends AnyRef

    Permalink

    Factory to construct new reducer plugins.

  13. class SeqReducerPlugin extends ReducerPlugin

    Permalink

    Reducer plugin that sequentially applies a list of plugins.

  14. class SeqReducerPluginFactory extends ReducerPluginFactory

    Permalink
  15. class SubsumptionRemover extends AnyRef

    Permalink

    Naive version of a subsumption test

Value Members

  1. object ConjunctEliminator

    Permalink
  2. object Conjunction

    Permalink
  3. object IdentityReducerPlugin extends ReducerPlugin

    Permalink

    Reducer plugin that always just returns unchanged formulas.

  4. object IdentityReducerPluginFactory extends ReducerPluginFactory

    Permalink
  5. object IterativeClauseMatcher

    Permalink
  6. object LazyConjunction

    Permalink
  7. object NegatedConjunctions

    Permalink
  8. object Quantifier

    Permalink
  9. object ReduceWithConjunction

    Permalink
  10. object ReducerPlugin

    Permalink
  11. object SeqReducerPluginFactory

    Permalink

Ungrouped