class ReduceWithEmptyInEqs extends ReduceWithInEqs
The implementation for the trivial case that there are no inequalities (this is realised as an own class for performance reasons)
- Alphabetic
- By Inheritance
- ReduceWithEmptyInEqs
- ReduceWithInEqs
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Instance Constructors
- new ReduceWithEmptyInEqs(order: TermOrder)
- Attributes
- protected[inequalities]
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 addInEqs(furtherInEqs: InEqConj): ReduceWithInEqs
- Definition Classes
- ReduceWithEmptyInEqs → ReduceWithInEqs
- def apply(conj: InEqConj): InEqConj
Reduce a conjunction of inequalities.
Reduce a conjunction of inequalities. This means that subsumed inequalities are removed, contradictions are detected, and possibly further equations are inferred.
- Definition Classes
- ReduceWithEmptyInEqs → ReduceWithInEqs
- def apply(conj: NegEquationConj, logger: ComputationLogger): (NegEquationConj, InEqConj)
Reduce a conjunction of negated equations by removing all equations from which we know that they hold anyway.
Reduce a conjunction of negated equations by removing all equations from which we know that they hold anyway. This will also turn disequalities into inequalities if possible.
- Definition Classes
- ReduceWithEmptyInEqs → ReduceWithInEqs
- def apply(conj: EquationConj): EquationConj
- Definition Classes
- ReduceWithEmptyInEqs → ReduceWithInEqs
- def apply(conj: NegEquationConj): (NegEquationConj, InEqConj)
Reduce a conjunction of negated equations by removing all equations from which we know that they hold anyway.
Reduce a conjunction of negated equations by removing all equations from which we know that they hold anyway. This will also turn disequalities into inequalities if possible.
- Definition Classes
- ReduceWithInEqs
- 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 the known inequalities imply a lower bound of the given term.
Check whether the known inequalities imply a lower bound of the given term.
- Definition Classes
- ReduceWithEmptyInEqs → ReduceWithInEqs
- 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.
- Definition Classes
- ReduceWithEmptyInEqs → ReduceWithInEqs
- 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): ReduceWithInEqs
Create a
ReduceWithEqsthat can be used underneathnumbinders.Create a
ReduceWithEqsthat can be used underneathnumbinders. The conversion of de Brujin-variables is done on the fly, which should give a good performance when the resultingReduceWithEqsis not applied too often (TODO: caching)- Definition Classes
- ReduceWithEmptyInEqs → ReduceWithInEqs
- def reduceNoEqualityInfs(conj: InEqConj): InEqConj
Reduce a conjunction of inequalities without implied equations.
Reduce a conjunction of inequalities without implied equations. (i.e.,
conj.equalityInfs.isEmpty)- Definition Classes
- ReduceWithEmptyInEqs → ReduceWithInEqs
- 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 the known inequalities imply an upper bound of the given term.
Check whether the known inequalities imply an upper bound of the given term.
- Definition Classes
- ReduceWithEmptyInEqs → ReduceWithInEqs
- 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.
- Definition Classes
- ReduceWithEmptyInEqs → ReduceWithInEqs
- 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)