# Conjunction

### Related Docs: object Conjunction | package conjunctions

#### class Conjunction extends Formula with SortedWithOrder[Conjunction]

Class for representing (possibly quantified) conjunctions of arithmetic literal (equations, inequalities), predicate literals and negated `Conjunction`s. `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

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

Definition Classes
AnyRef → Any

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

Definition Classes
AnyRef → Any

9. #### final def asInstanceOf[T0]: T0

Definition Classes
Any

11. #### def clone(): AnyRef

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

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

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

Definition Classes
Conjunction → AnyRef → Any
15. #### def finalize(): Unit

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

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

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

Definition Classes
Conjunction → AnyRef → Any

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

21. #### def isArithLiteral: Boolean

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

22. #### def isDivisibility: Boolean

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

"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

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

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

Definition Classes
Any
29. #### def isLiteral: Boolean

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

30. #### def isNegatedConjunction: Boolean

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

31. #### def isNonDivisibility: Boolean

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

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

Return whether this conjunction only contains negated sub-conjunctions

34. #### def isQuantifiedDivisibility: Boolean

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

37. #### def isQuantifiedNegatedConjunction: Boolean

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

38. #### def isQuantifiedNonDivisibility: Boolean

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

Definition Classes
SortedWithOrderSorted
40. #### def isTrue: Boolean

Return `true` if this formula is obviously always true

Return `true` if this formula is obviously always true

Definition Classes
ConjunctionFormula

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

Definition Classes
AnyRef

45. #### final def notify(): Unit

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

Definition Classes
AnyRef

48. #### val order: TermOrder

Definition Classes
ConjunctionSortedWithOrder

50. #### lazy val predicates: Set[Predicate]

Definition Classes
ConjunctionSortedWithOrderTerFor

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

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

Definition Classes
Conjunction → AnyRef → Any

58. #### def unquantify(num: Int): Conjunction

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

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

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

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

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

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

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]

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

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

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

Definition Classes
AnyRef
Annotations
@throws( ... )