Packages

class Conjunction extends Formula with SortedWithOrder[Conjunction]

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

Linear Supertypes
SortedWithOrder[Conjunction], Sorted[Conjunction], Formula, TerFor, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Conjunction
  2. SortedWithOrder
  3. Sorted
  4. Formula
  5. TerFor
  6. AnyRef
  7. 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. def &(that: Conjunction)(implicit newOrder: TermOrder): Conjunction
  4. def --(that: Conjunction): Conjunction
  5. def <=>(that: Conjunction)(implicit newOrder: TermOrder): Conjunction
  6. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  7. def ==>(that: Conjunction)(implicit newOrder: TermOrder): Conjunction
  8. val arithConj: ArithConj
  9. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  10. lazy val boundVariables: Set[VariableTerm]
  11. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
  12. lazy val constants: Set[ConstantTerm]
    Definition Classes
    Conjunction → SortedWithOrder → TerFor
  13. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  14. def equals(that: Any): Boolean
    Definition Classes
    Conjunction → AnyRef → Any
  15. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  16. lazy val groundAtoms: Set[Atom]
    Definition Classes
    Conjunction → Formula
  17. def hashCode(): Int
    Definition Classes
    Conjunction → AnyRef → Any
  18. def implies(that: Conjunction): Boolean
  19. def instantiate(terms: Seq[Term])(implicit newOrder: TermOrder): Conjunction

    Instantiate the outermost quantifiers with the given terms, starting with the innermost quantifier to be instantiated

  20. def isArithLiteral: Boolean

    Return whether this conjunction actually only is a single arithmetic literal (a single, unquantified (in)equation, inequality)

  21. def isDivisibility: Boolean

    Return whether this is a divisibility judgement EX (n*_0 + t = 0)

  22. def isDivisionFormula: Option[(LinearCombination, LinearCombination, Conjunction)]

    "Division quantifiers" of the form EX ( n*_0 + t >= 0 & -n*_0 - t - m >= 0 & phi ) where 0 <= m < n .

    "Division quantifiers" of the form EX ( n*_0 + t >= 0 & -n*_0 - t - m >= 0 & phi ) where 0 <= m < n .

    The result of this test is a triple (n*_0 + t, -n*_0 - t - m, phi), or None if the formula is not of the guarded quantifier shape

  23. def isDivisionFormulaHelp: Option[(LinearCombination, LinearCombination, InEqConj)]
  24. def isExactDivisionFormula: Option[(LinearCombination, Conjunction)]

    "Exact division quantifiers" of the form EX ( n*_0 + t = 0 & phi) where 0 < n .

    "Exact division quantifiers" of the form EX ( n*_0 + t = 0 & phi) where 0 < n .

    The result of this test is a pair (n*_0 + t, phi), or None if the formula is not of the guarded quantifier shape

  25. def isExactDivisionFormulaHelp: Option[(LinearCombination, EquationConj)]
  26. def isFalse: Boolean

    The only allow case of false is when arithConj is false and everything else is empty.

    The only allow case of false is when arithConj is false and everything else is empty.

    Definition Classes
    Conjunction → Formula
  27. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  28. def isLiteral: Boolean

    Return whether this conjunction actually only is a single literal (a single, unquantified (in)equation, inequality or predicate literal)

  29. def isNegatedConjunction: Boolean

    Return whether this conjunction actually is the negation of a single conjunction

  30. def isNonDivisibility: Boolean

    Return whether this is a negated divisibility judgement ALL (n*_0 + t != 0)

  31. def isProperDivisibility: Boolean

    Assuming that this formula is a divisibility or non-divisibility statement, check whether the divisibility is proper (i.e., not of the form ALL (1*_0 + t != 0))

  32. def isPurelyNegated: Boolean

    Return whether this conjunction only contains negated sub-conjunctions

  33. def isQuantifiedDivisibility: Boolean

    Return whether this is a divisibility judgement EX (n*_0 + t = 0), possibly underneath quantifiers

  34. def isQuantifiedDivisionFormula: Option[(LinearCombination, LinearCombination, Conjunction)]
  35. def isQuantifiedExactDivisionFormula: Option[(LinearCombination, Conjunction)]
  36. def isQuantifiedNegatedConjunction: Boolean

    Return whether this conjunction actually is the negation of a single conjunction

  37. def isQuantifiedNonDivisibility: Boolean

    Return whether this is a negated divisibility judgement ALL (n*_0 + t != 0), possibly underneath quantifiers

  38. def isSortedBy(otherOrder: TermOrder): Boolean
    Definition Classes
    SortedWithOrder → Sorted
  39. def isTrue: Boolean

    Return true if this formula is obviously always true

    Return true if this formula is obviously always true

    Definition Classes
    Conjunction → Formula
  40. def iterator: Iterator[Conjunction]
  41. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  42. def negate: Conjunction
  43. val negatedConjs: NegatedConjunctions
  44. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  45. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  46. def opCount: Int
  47. val order: TermOrder
    Definition Classes
    Conjunction → SortedWithOrder
  48. val predConj: PredConj
  49. lazy val predicates: Set[Predicate]
    Definition Classes
    Conjunction → SortedWithOrder → TerFor
  50. val quans: Seq[Quantifier]
  51. def remove(that: Conjunction, logger: ComputationLogger): Conjunction
  52. def size: Int
  53. def sortBy(newOrder: TermOrder): Conjunction

    Re-sort an object with a new TermOrder.

    Re-sort an object with a new TermOrder. It is guaranteed that the result isSortedBy(order)

    Definition Classes
    Conjunction → Sorted
  54. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  55. def toString(): String
    Definition Classes
    Conjunction → AnyRef → Any
  56. def unary_!: Conjunction
  57. def unquantify(num: Int): Conjunction

    Remove the num outermost quantifiers of this Conjunction, without changing the matrix of the formula

  58. def updateArithConj(ac: ArithConj)(implicit newOrder: TermOrder): Conjunction

    Update the arithmetic parts of this conjunction (without changing anything else apart from the TermOrder)

  59. def updateInEqs(newEqs: InEqConj)(implicit newOrder: TermOrder): Conjunction

    Update the inequalities of this conjunction (without changing anything else apart from the TermOrder)

  60. def updateNegatedConjs(newNegConjs: NegatedConjunctions)(implicit newOrder: TermOrder): Conjunction

    Update the inequalities of this conjunction (without changing anything else apart from the TermOrder)

  61. def updateNegativeEqs(newEqs: NegEquationConj)(implicit newOrder: TermOrder): Conjunction

    Update the negative equations of this conjunction (without changing anything else apart from the TermOrder)

  62. def updatePositiveEqs(newEqs: EquationConj)(implicit newOrder: TermOrder): Conjunction

    Update the positive equations of this conjunction (without changing anything else apart from the TermOrder)

  63. def updatePredConj(pc: PredConj)(implicit newOrder: TermOrder): Conjunction

    Update the predicate parts of this conjunction (without changing anything else apart from the TermOrder)

  64. lazy val variables: Set[VariableTerm]
    Definition Classes
    Conjunction → TerFor
  65. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  66. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  67. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  68. def |(that: Conjunction)(implicit newOrder: TermOrder): Conjunction

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 SortedWithOrder[Conjunction]

Inherited from Sorted[Conjunction]

Inherited from Formula

Inherited from TerFor

Inherited from AnyRef

Inherited from Any

Ungrouped