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.
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.
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.
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.
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.
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)
Reduce a conjunction of inequalities without implied equations.
Reduce a conjunction of inequalities without implied equations.
(i.e., conj.equalityInfs.isEmpty
)
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.
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.
The implementation for the trivial case that there are no inequalities (this is realised as an own class for performance reasons)