# ArithConj

### Related Docs: object ArithConj | package arithconj

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

The class for a conjunction of equations, negated equations and inequalities

Linear Supertypes
Ordering
1. Alphabetic
2. By inheritance
Inherited
1. ArithConj
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

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

Definition Classes
AnyRef → Any
5. #### final def asInstanceOf[T0]: T0

Definition Classes
Any
6. #### def clone(): AnyRef

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

Definition Classes
ArithConjSortedWithOrderTerFor
8. #### final def eq(arg0: AnyRef): Boolean

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

Definition Classes
ArithConj → AnyRef → Any
10. #### def finalize(): Unit

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

Definition Classes
AnyRef → Any
12. #### def groundAtoms: Set[Atom]

Definition Classes
ArithConjFormula
13. #### def hashCode(): Int

Definition Classes
ArithConj → AnyRef → Any

17. #### def isFalse: Boolean

Return `true` if this formula is obviously always false

Return `true` if this formula is obviously always false

Definition Classes
ArithConjFormula
18. #### final def isInstanceOf[T0]: Boolean

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

Return whether this conjunction actually only is a single literal

20. #### def isSortedBy(otherOrder: TermOrder): Boolean

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

Return `true` if this formula is obviously always true

Return `true` if this formula is obviously always true

Definition Classes
ArithConjFormula

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

Definition Classes
AnyRef
24. #### def negate: ArithConj

Create the negation of at most one equation

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

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

Definition Classes
AnyRef
28. #### val order: TermOrder

Definition Classes
ArithConjSortedWithOrder

30. #### def predicates: Set[Predicate]

Definition Classes
ArithConjSortedWithOrderTerFor

33. #### def sortBy(newOrder: TermOrder): ArithConj

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

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

Definition Classes
ArithConj → AnyRef → Any
36. #### def updateInEqs(newInEqs: InEqConj)(implicit newOrder: TermOrder): ArithConj

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

37. #### def updateNegativeEqs(newEqs: NegEquationConj)(implicit newOrder: TermOrder): ArithConj

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

38. #### def updatePositiveEqs(newEqs: EquationConj)(implicit newOrder: TermOrder): ArithConj

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

39. #### lazy val variables: Set[VariableTerm]

Definition Classes
ArithConjTerFor
40. #### final def wait(): Unit

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

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

Definition Classes
AnyRef
Annotations
@throws( ... )