class ReduceWithAC extends AnyRef
- Alphabetic
- By Inheritance
- ReduceWithAC
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- def apply(conj: PredConj, logger: ComputationLogger): PredConj
- def apply(conj: EquationConj): EquationConj
- def apply(conj: ArithConj): ArithConj
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- def lowerBound(t: Term): Option[IdealInt]
Check whether known inequalities imply a lower bound of the given term.
- def lowerBoundWithAssumptions(t: Term): Option[(IdealInt, Seq[LinearCombination])]
Check whether the known inequalities imply a lower bound of the given term.
Check whether the known inequalities imply a lower bound of the given term. Also return assumed inequalities needed to derive the bound.
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def passQuantifiers(num: Int): ReduceWithAC
- def plainReduce(conj: ArithConj): (ArithConj, ReduceWithAC)
Just reduce the components of the conjunction individually, do not do any internal propagation.
- def reduceAndAdd(conj: ArithConj, logger: ComputationLogger): (ArithConj, ReduceWithAC)
Reduce an arithmetic conjunction using the information stored in this object.
Reduce an arithmetic conjunction using the information stored in this object. The result is the simplified conjunction, as well as a new reducer to which the information from the simplified arithmetic conjunction has been added.
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- AnyRef → Any
- def upperBound(t: Term): Option[IdealInt]
Check whether known inequalities imply an upper bound of the given term.
- def upperBoundWithAssumptions(t: Term): Option[(IdealInt, Seq[LinearCombination])]
Check whether the known inequalities imply an upper bound of the given term.
Check whether the known inequalities imply an upper bound of the given term. Also return assumed inequalities needed to derive the bound.
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
(Since version 9)