Packages

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

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##: Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. val FALSE: Conjunction
  5. val TRUE: Conjunction
  6. def apply(quans: Seq[Quantifier], arithConj: ArithConj, predConj: PredConj, negatedConjs: NegatedConjunctions, order: TermOrder): Conjunction

    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
  8. def apply(quans: Seq[Quantifier], formulas: Iterator[Formula], order: TermOrder): Conjunction
  9. def apply(quans: Seq[Quantifier], formulas: Iterator[Formula], logger: ComputationLogger, order: TermOrder): Conjunction

    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
    Definition Classes
    Any
  11. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
  12. def collectQuantifiers(f: Formula): Set[Quantifier]

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

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

    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

    Rudimentary sorting of conjunctions.

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

  15. def conj(f: Formula, order: TermOrder): Conjunction
  16. def conj(formulas: Iterable[Formula], order: TermOrder): Conjunction
  17. def conj(formulas: Iterator[Formula], order: TermOrder): Conjunction

    Compute a conjunction from an arbitrary set of formulas

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

    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

    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
  21. def disj(formulas: Iterator[Conjunction], order: TermOrder): Conjunction
  22. def disjFor(formulas: Iterable[Formula], order: TermOrder): Conjunction
  23. def disjFor(formulas: Iterator[Formula], order: TermOrder): Conjunction

    Compute a disjunction from an arbitrary set of formulas

  24. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  25. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  26. def eqv(for1: Formula, for2: Formula, order: TermOrder): Conjunction

    Form the equivalence between two formulas

  27. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  28. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  29. def implies(for1: Formula, for2: Formula, order: TermOrder): Conjunction

    Form the implication between two formulas

  30. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  31. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  32. def negate(f: Formula, order: TermOrder): Conjunction

    Negate a formula

  33. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  34. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  35. def quantify(quan: Quantifier, constants: Seq[ConstantTerm], f: Formula, order: TermOrder): Conjunction

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

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

    Quantify a formula

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

    Rudimentary reverse sorting of conjunctions.

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

  38. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  39. def toString(): String
    Definition Classes
    AnyRef → Any
  40. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  41. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  42. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable]) @Deprecated
    Deprecated

    (Since version 9)

Inherited from AnyRef

Inherited from Any

Ungrouped