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
    @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. def finalize(): Unit

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

    Permalink
    Definition Classes
    AnyRef → Any
  17. lazy val groundAtoms: Set[Atom]

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

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

    Permalink
  20. 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

  21. def isArithLiteral: Boolean

    Permalink

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

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

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

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

    Permalink
  25. 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

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

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

    Permalink
    Definition Classes
    Any
  29. def isLiteral: Boolean

    Permalink

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

  30. def isNegatedConjunction: Boolean

    Permalink

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

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

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

  33. def isPurelyNegated: Boolean

    Permalink

    Return whether this conjunction only contains negated sub-conjunctions

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

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

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

    Permalink
  37. def isQuantifiedNegatedConjunction: Boolean

    Permalink

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

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

  39. def isSortedBy(otherOrder: TermOrder): Boolean

    Permalink
    Definition Classes
    SortedWithOrderSorted
  40. 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
  41. def iterator: Iterator[Conjunction]

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

    Permalink
    Definition Classes
    AnyRef
  43. def negate: Conjunction

    Permalink
  44. val negatedConjs: NegatedConjunctions

    Permalink
  45. final def notify(): Unit

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

    Permalink
    Definition Classes
    AnyRef
  47. def opCount: Int

    Permalink
  48. val order: TermOrder

    Permalink
    Definition Classes
    ConjunctionSortedWithOrder
  49. val predConj: PredConj

    Permalink
  50. lazy val predicates: Set[Predicate]

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

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

    Permalink
  53. def size: Int

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

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

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

    Permalink
  58. 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

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

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

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

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

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

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

  65. lazy val variables: Set[VariableTerm]

    Permalink
    Definition Classes
    ConjunctionTerFor
  66. final def wait(): Unit

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

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

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

    Permalink

Inherited from SortedWithOrder[Conjunction]

Inherited from Sorted[Conjunction]

Inherited from Formula

Inherited from TerFor

Inherited from AnyRef

Inherited from Any

Ungrouped