Class/Object

ap.terfor.arithconj

ArithConj

Related Docs: object ArithConj | package arithconj

Permalink

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

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

    Permalink
    Definition Classes
    AnyRef → Any
  3. def --(that: ArithConj): ArithConj

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

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

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

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

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

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

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

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

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

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

    Permalink
    Definition Classes
    ArithConj → AnyRef → Any
  14. def implies(that: ArithConj): Boolean

    Permalink
  15. val inEqs: InEqConj

    Permalink
  16. def isEmpty: Boolean

    Permalink
  17. def isFalse: Boolean

    Permalink

    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

    Permalink
    Definition Classes
    Any
  19. def isLiteral: Boolean

    Permalink

    Return whether this conjunction actually only is a single literal

  20. def isSortedBy(otherOrder: TermOrder): Boolean

    Permalink
    Definition Classes
    SortedWithOrderSorted
  21. def isTrue: Boolean

    Permalink

    Return true if this formula is obviously always true

    Return true if this formula is obviously always true

    Definition Classes
    ArithConjFormula
  22. def iterator: Iterator[ArithConj]

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

    Permalink
    Definition Classes
    AnyRef
  24. def negate: ArithConj

    Permalink

    Create the negation of at most one equation

  25. val negativeEqs: NegEquationConj

    Permalink
  26. final def notify(): Unit

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

    Permalink
    Definition Classes
    AnyRef
  28. val order: TermOrder

    Permalink
    Definition Classes
    ArithConjSortedWithOrder
  29. val positiveEqs: EquationConj

    Permalink
  30. def predicates: Set[Predicate]

    Permalink
    Definition Classes
    ArithConjSortedWithOrderTerFor
  31. def remove(that: ArithConj, logger: ComputationLogger): ArithConj

    Permalink
  32. def size: Int

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

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

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

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

    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)

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

    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)

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

    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)

  39. lazy val variables: Set[VariableTerm]

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

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

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

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

Inherited from SortedWithOrder[ArithConj]

Inherited from Sorted[ArithConj]

Inherited from Formula

Inherited from TerFor

Inherited from AnyRef

Inherited from Any

Ungrouped