Type Members

1.  class InEqConj extends Formula with SortedWithOrder[InEqConj] with IndexedSeq[LinearCombination]

   Class for storing a conjunction of inequalities that are normalised to the form t >= 0.

   Class for storing a conjunction of inequalities that are normalised to the form t >= 0. Together with the actual inequalities, also all inequalities that can be inferred using Fourier-Motzkin elimination steps, as well as all equations that can be inferred using Fourier-Motzkin are stored. This implies that it can always be decided in constant time whether the inequalities have rational solutions.

2.  class IntervalProp extends AnyRef

   Interval constraint propagation (ICP) for linear inequalities.

3.  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)

4.  abstract class ReduceWithInEqs extends AnyRef

   Reduce certain terms or formulas drawing information from inequalities that are assumed as facts.

5.  class ReduceWithInEqsImpl extends ReduceWithInEqs

   The standard implementation