# ReduceWithInEqsImpl

### Related Doc: package inequalities

#### class ReduceWithInEqsImpl extends ReduceWithInEqs

The standard implementation

Linear Supertypes
ReduceWithInEqs, AnyRef, Any
Ordering
1. Alphabetic
2. By inheritance
Inherited
1. ReduceWithInEqsImpl
2. ReduceWithInEqs
3. AnyRef
4. Any
1. Hide All
2. Show all
Visibility
1. Public
2. All

### Instance Constructors

1. #### new ReduceWithInEqsImpl(ineqLowerBound: (LinearCombination) ⇒ Option[IdealInt], containsVariables: Boolean, order: TermOrder)

Attributes
protected[ap.terfor.inequalities]

### 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. #### def addInEqs(furtherInEqs: InEqConj): ReduceWithInEqs

Definition Classes
ReduceWithInEqsImplReduceWithInEqs
5. #### 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
ReduceWithInEqsImplReduceWithInEqs
6. #### def apply(conj: NegEquationConj, logger: ComputationLogger): (NegEquationConj, InEqConj)

Reduce a conjunction of disequalities; sometimes, this will turn disequalities into inequalities.

Reduce a conjunction of disequalities; sometimes, this will turn disequalities into inequalities.

Definition Classes
ReduceWithInEqsImplReduceWithInEqs
7. #### def apply(conj: EquationConj): EquationConj

Definition Classes
ReduceWithInEqsImplReduceWithInEqs
8. #### 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
9. #### final def asInstanceOf[T0]: T0

Definition Classes
Any
10. #### def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( ... )
11. #### final def eq(arg0: AnyRef): Boolean

Definition Classes
AnyRef
12. #### def equals(arg0: Any): Boolean

Definition Classes
AnyRef → Any
13. #### def finalize(): Unit

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

Definition Classes
AnyRef → Any
15. #### def hashCode(): Int

Definition Classes
AnyRef → Any
16. #### final def isInstanceOf[T0]: Boolean

Definition Classes
Any
17. #### 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
ReduceWithInEqsImplReduceWithInEqs
18. #### 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
ReduceWithInEqsImplReduceWithInEqs
19. #### final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
20. #### final def notify(): Unit

Definition Classes
AnyRef
21. #### final def notifyAll(): Unit

Definition Classes
AnyRef
22. #### def passQuantifiers(num: Int): ReduceWithInEqs

Create a `ReduceWithEqs` that can be used underneath `num` binders.

Create a `ReduceWithEqs` that can be used underneath `num` binders. The conversion of de Brujin-variables is done on the fly, which should give a good performance when the resulting `ReduceWithEqs` is not applied too often (TODO: caching)

Definition Classes
ReduceWithInEqsImplReduceWithInEqs
23. #### 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
ReduceWithInEqsImplReduceWithInEqs
24. #### final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef
25. #### def toString(): String

Definition Classes
AnyRef → Any
26. #### 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
ReduceWithInEqsImplReduceWithInEqs
27. #### 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
ReduceWithInEqsImplReduceWithInEqs
28. #### final def wait(): Unit

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

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

Definition Classes
AnyRef
Annotations
@throws( ... )