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
    @HotSpotIntrinsicCandidate() @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. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()

  28. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()

  29. def implies(for1: Formula, for2: Formula, order: TermOrder): Conjunction

    Permalink

    Form the implication between two formulas

  30. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any

  31. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef

  32. def negate(f: Formula, order: TermOrder): Conjunction

    Permalink

    Negate a formula

  33. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()

  34. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()

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

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

    Permalink

    Quantify a formula

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

    Permalink

    Rudimentary reverse sorting of conjunctions.

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

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

    Permalink
    Definition Classes
    AnyRef

  39. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any

  40. final def wait(arg0: Long, arg1: Int): Unit

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

  41. final def wait(arg0: Long): Unit

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

  42. final def wait(): Unit

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

Deprecated Value Members

  1. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
    Deprecated

    (Since version ) see corresponding Javadoc for more information.

Inherited from AnyRef

Inherited from Any

Ungrouped