Object/Class

ap.terfor.conjunctions

Conjunction

Related Docs: class Conjunction | package conjunctions

Permalink

object Conjunction

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By inheritance
Inherited
  1. Conjunction
  2. AnyRef
  3. Any
  1. Hide All
  2. Show all
Visibility
  1. Public
  2. All

Value Members

  1. final def !=(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  4. val FALSE: Conjunction

    Permalink
  5. val TRUE: Conjunction

    Permalink
  6. def apply(quans: Seq[Quantifier], arithConj: ArithConj, predConj: PredConj, negatedConjs: NegatedConjunctions, order: TermOrder): Conjunction

    Permalink

    Create a Conjunction from an arbitrary collection of formulas.

    Create a Conjunction from an arbitrary collection of formulas. It is required that all given formulas are sorted by the specified order.

  7. def apply(quans: Seq[Quantifier], formulas: Iterable[Formula], order: TermOrder): Conjunction

    Permalink
  8. def apply(quans: Seq[Quantifier], formulas: Iterator[Formula], order: TermOrder): Conjunction

    Permalink
  9. def apply(quans: Seq[Quantifier], formulas: Iterator[Formula], logger: ComputationLogger, order: TermOrder): Conjunction

    Permalink

    Create a Conjunction from an arbitrary collection of formulas.

    Create a Conjunction from an arbitrary collection of formulas. It is required that all given formulas are sorted by the specified order.

  10. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  11. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  12. def collectQuantifiers(f: Formula): Set[Quantifier]

    Permalink

    Default: divisibility is not counted (but we count immediately preceeding quantifiers)

  13. def collectQuantifiers(f: Formula, divCollector: (Conjunction) ⇒ Set[Quantifier]): Set[Quantifier]

    Permalink

    Determine the quantifiers that occur in a formula.

    Determine the quantifiers that occur in a formula. Because there are different points of view, a function can be given as parameter that determines whether (quantified) divisibility/indivisibility statements are counted as quantifiers

  14. def compare(c1: Conjunction, c2: Conjunction, order: TermOrder): Int

    Permalink

    Rudimentary sorting of conjunctions.

    Rudimentary sorting of conjunctions. TODO: improve this (a lot)

  15. def conj(f: Formula, order: TermOrder): Conjunction

    Permalink
  16. def conj(formulas: Iterable[Formula], order: TermOrder): Conjunction

    Permalink
  17. def conj(formulas: Iterator[Formula], order: TermOrder): Conjunction

    Permalink

    Compute a conjunction from an arbitrary set of formulas

  18. def conjOrdering(order: TermOrder): Ordering[Conjunction]

    Permalink

    Rudimentary sorting of conjunctions.

    Rudimentary sorting of conjunctions. TODO: improve this (a lot)

  19. def createFromNormalised(quans: Seq[Quantifier], arithConj: ArithConj, predConj: PredConj, negatedConjs: NegatedConjunctions, order: TermOrder): Conjunction

    Permalink

    Create a Conjunction from different parts that are already normalised.

    Create a Conjunction from different parts that are already normalised. This primarily means that negatedConjs must not contain any conjunctions that are just literals, and that quantifiers are pulled out completely if the conjunction only has a single conjunct.

  20. def disj(formulas: Iterable[Conjunction], order: TermOrder): Conjunction

    Permalink
  21. def disj(formulas: Iterator[Conjunction], order: TermOrder): Conjunction

    Permalink
  22. def disjFor(formulas: Iterable[Formula], order: TermOrder): Conjunction

    Permalink
  23. def disjFor(formulas: Iterator[Formula], order: TermOrder): Conjunction

    Permalink

    Compute a disjunction from an arbitrary set of formulas

  24. final def eq(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  25. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  26. def eqv(for1: Formula, for2: Formula, order: TermOrder): Conjunction

    Permalink

    Form the equivalence between two formulas

  27. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  28. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
  29. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  30. def implies(for1: Formula, for2: Formula, order: TermOrder): Conjunction

    Permalink

    Form the implication between two formulas

  31. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  32. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  33. def negate(f: Formula, order: TermOrder): Conjunction

    Permalink

    Negate a formula

  34. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
  35. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
  36. def quantify(quan: Quantifier, constants: Seq[ConstantTerm], f: Formula, order: TermOrder): Conjunction

    Permalink

    Quantify a number of constants in a formula, i.e., replace the constants with variables and add quantifiers

  37. def quantify(quans: Seq[Quantifier], f: Formula, order: TermOrder): Conjunction

    Permalink

    Quantify a formula

  38. def reverseConjOrdering(order: TermOrder): Ordering[Conjunction]

    Permalink

    Rudimentary reverse sorting of conjunctions.

    Rudimentary reverse sorting of conjunctions. TODO: improve this (a lot)

  39. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef
  40. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any
  41. final def wait(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  42. final def wait(arg0: Long, arg1: Int): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  43. final def wait(arg0: Long): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped