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
    @HotSpotIntrinsicCandidate() @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. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate()
  11. def groundAtoms: Set[Atom]

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

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

    Permalink
  14. val inEqs: InEqConj

    Permalink
  15. def isEmpty: Boolean

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

    Permalink
    Definition Classes
    Any
  18. def isLiteral: Boolean

    Permalink

    Return whether this conjunction actually only is a single literal

  19. def isSortedBy(otherOrder: TermOrder): Boolean

    Permalink
    Definition Classes
    SortedWithOrderSorted
  20. 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
  21. def iterator: Iterator[ArithConj]

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

    Permalink
    Definition Classes
    AnyRef
  23. def negate: ArithConj

    Permalink

    Create the negation of at most one equation

  24. val negativeEqs: NegEquationConj

    Permalink
  25. final def notify(): Unit

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

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate()
  27. val order: TermOrder

    Permalink
    Definition Classes
    ArithConjSortedWithOrder
  28. val positiveEqs: EquationConj

    Permalink
  29. def predicates: Set[Predicate]

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

    Permalink
  31. def size: Int

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

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

    Permalink
    Definition Classes
    ArithConj → AnyRef → Any
  35. 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)

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

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

  38. lazy val variables: Set[VariableTerm]

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

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

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

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

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[ArithConj]

Inherited from Sorted[ArithConj]

Inherited from Formula

Inherited from TerFor

Inherited from AnyRef

Inherited from Any

Ungrouped