Class/Object

ap.terfor.conjunctions

Conjunction

Related Docs: object Conjunction | package conjunctions

Permalink

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

Value Members

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

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

    Permalink
    Definition Classes
    AnyRef → Any
  3. def &(that: Conjunction)(implicit newOrder: TermOrder): Conjunction

    Permalink
  4. def --(that: Conjunction): Conjunction

    Permalink
  5. def <=>(that: Conjunction)(implicit newOrder: TermOrder): Conjunction

    Permalink
  6. final def ==(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  7. def ==>(that: Conjunction)(implicit newOrder: TermOrder): Conjunction

    Permalink
  8. val arithConj: ArithConj

    Permalink
  9. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  10. lazy val boundVariables: Set[VariableTerm]

    Permalink
  11. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @throws( ... )
  12. lazy val constants: Set[ConstantTerm]

    Permalink
    Definition Classes
    ConjunctionSortedWithOrderTerFor
  13. final def eq(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  14. def equals(that: Any): Boolean

    Permalink
    Definition Classes
    Conjunction → AnyRef → Any
  15. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()
  16. lazy val groundAtoms: Set[Atom]

    Permalink
    Definition Classes
    ConjunctionFormula
  17. def hashCode(): Int

    Permalink
    Definition Classes
    Conjunction → AnyRef → Any
  18. def implies(that: Conjunction): Boolean

    Permalink
  19. def instantiate(terms: Seq[Term])(implicit newOrder: TermOrder): Conjunction

    Permalink

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

  20. def isArithLiteral: Boolean

    Permalink

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

  21. def isDivisibility: Boolean

    Permalink

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

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

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

    Permalink

    "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)]

    Permalink
  24. def isExactDivisionFormula: Option[(LinearCombination, Conjunction)]

    Permalink

    "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)]

    Permalink
  26. def isFalse: Boolean

    Permalink

    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
    ConjunctionFormula
  27. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  28. def isLiteral: Boolean

    Permalink

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

  29. def isNegatedConjunction: Boolean

    Permalink

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

  30. def isNonDivisibility: Boolean

    Permalink

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

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

  31. def isProperDivisibility: Boolean

    Permalink

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

    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

    Permalink

    Return whether this conjunction only contains negated sub-conjunctions

  33. def isQuantifiedDivisibility: Boolean

    Permalink

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

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

  34. def isQuantifiedDivisionFormula: Option[(LinearCombination, LinearCombination, Conjunction)]

    Permalink
  35. def isQuantifiedExactDivisionFormula: Option[(LinearCombination, Conjunction)]

    Permalink
  36. def isQuantifiedNegatedConjunction: Boolean

    Permalink

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

  37. def isQuantifiedNonDivisibility: Boolean

    Permalink

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

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

  38. def isSortedBy(otherOrder: TermOrder): Boolean

    Permalink
    Definition Classes
    SortedWithOrderSorted
  39. def isTrue: Boolean

    Permalink

    Return true if this formula is obviously always true

    Return true if this formula is obviously always true

    Definition Classes
    ConjunctionFormula
  40. def iterator: Iterator[Conjunction]

    Permalink
  41. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  42. def negate: Conjunction

    Permalink
  43. val negatedConjs: NegatedConjunctions

    Permalink
  44. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()
  45. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()
  46. def opCount: Int

    Permalink
  47. val order: TermOrder

    Permalink
    Definition Classes
    ConjunctionSortedWithOrder
  48. val predConj: PredConj

    Permalink
  49. lazy val predicates: Set[Predicate]

    Permalink
    Definition Classes
    ConjunctionSortedWithOrderTerFor
  50. val quans: Seq[Quantifier]

    Permalink
  51. def remove(that: Conjunction, logger: ComputationLogger): Conjunction

    Permalink
  52. def size: Int

    Permalink
  53. def sortBy(newOrder: TermOrder): Conjunction

    Permalink

    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
    ConjunctionSorted
  54. final def synchronized[T0](arg0: ⇒ T0): T0

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

    Permalink
    Definition Classes
    Conjunction → AnyRef → Any
  56. def unary_!: Conjunction

    Permalink
  57. def unquantify(num: Int): Conjunction

    Permalink

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

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

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

    Permalink

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

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

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

    Permalink

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

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

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

    Permalink

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

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

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

    Permalink

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

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

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

    Permalink

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

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

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

    Permalink

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

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

  64. lazy val variables: Set[VariableTerm]

    Permalink
    Definition Classes
    ConjunctionTerFor
  65. final def wait(arg0: Long, arg1: Int): Unit

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

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  67. final def wait(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  68. def |(that: Conjunction)(implicit newOrder: TermOrder): Conjunction

    Permalink

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

Inherited from Sorted[Conjunction]

Inherited from Formula

Inherited from TerFor

Inherited from AnyRef

Inherited from Any

Ungrouped