Add further assumptions to this reducer.
Add further assumptions to this reducer.
Add further assumptions to this reducer.
Add further assumptions to this reducer.
Factory to generate further instances of this plugin.
Factory to generate further instances of this plugin.
Do a final check whether a complete conjunction can be reduced.
Do a final check whether a complete conjunction can be reduced. All sub-formulas are already fully reduced at this point.
Construct a new reducer to work underneath num
quantifiers.
Construct a new reducer to work underneath num
quantifiers.
Reduce the given predicate formulas.
Reduce the given predicate formulas. The result indicates whether nothing changed, or whether the formulas were updated, possibly generating additional arithmetic constraints or negated constraints. Reduction is not required to be idempotent.
(Since version ) see corresponding Javadoc for more information.
Reducer plugin that always just returns unchanged formulas.