Packages

object InEqConj

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. InEqConj
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##: Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. val AC: AC_INEQUALITIES.type
  5. val FALSE: InEqConj
  6. val INF_STOP_THRESHOLD: Int
  7. val INF_THROTTLE_THRESHOLD: Int

    When computing the inferences for a given set of inequalities, throttle the number of inferences that are stored for each leading term as soon as INEQ_INFS_THRESHOLD has been reached, which is then restricted to THROTTLED_INF_NUM.

    When computing the inferences for a given set of inequalities, throttle the number of inferences that are stored for each leading term as soon as INEQ_INFS_THRESHOLD has been reached, which is then restricted to THROTTLED_INF_NUM. Once the hard limit INF_STOP_THRESHOLD is reached for a particular leading term, generation of inferences for that term is stopped altogether.

  8. val THROTTLED_INF_NUM: Int
  9. val TRUE: InEqConj
  10. def apply(lhs: LinearCombination, order: TermOrder): InEqConj
  11. def apply(lhss: Iterable[LinearCombination], order: TermOrder): InEqConj

    Create an inequality conjunction from an arbitrary set of geq-zero-inequalities (left-hand sides).

  12. def apply(lhss: Iterator[LinearCombination], order: TermOrder): InEqConj
  13. def apply(lhss: Iterator[LinearCombination], logger: ComputationLogger, order: TermOrder): InEqConj

    Create an inequality conjunction from an arbitrary set of geq-zero-inequalities (left-hand sides).

  14. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  15. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
  16. def conj(conjs: Iterable[InEqConj], order: TermOrder): InEqConj

    Compute the conjunction of a number of inequality conjunctions.

  17. def conj(conjs: Iterator[InEqConj], order: TermOrder): InEqConj
  18. def conj(conjs: Iterator[InEqConj], logger: ComputationLogger, order: TermOrder): InEqConj

    Compute the conjunction of a number of inequality conjunctions.

  19. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  20. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  21. def exactShadow(t: Term, inEqs: Seq[LinearCombination], logger: ComputationLogger, order: TermOrder): (Seq[LinearCombination], Seq[LinearCombination])

    Perform Fourier-Motzkin elimination on one particular symbol t.

    Perform Fourier-Motzkin elimination on one particular symbol t. The result is the collection of eliminated inequalities, and the collection of remaining inequalities (including inferences from the removed inequalities). If an unsatisfiable inequality is derived, the exception UNSATISFIABLE_INEQ_EXCEPTION is thrown.

  22. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  23. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  24. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  25. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  26. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  27. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  28. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  29. def toString(): String
    Definition Classes
    AnyRef → Any
  30. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  31. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  32. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  33. object UNSATISFIABLE_INEQ_EXCEPTION extends Exception

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable]) @Deprecated
    Deprecated

    (Since version 9)

Inherited from AnyRef

Inherited from Any

Ungrouped