Check whether the function objective
has both a lower and an
upper bound subject to constraint
, and return such bounds.
Check whether the function objective
has both a lower and an
upper bound subject to constraint
, and return such bounds.
Find an interpretation of the constants in the given terms that will make all terms evaluate to pairwise distinct integers.
Quantifier elimination procedure that can also handle uninterpreted predicates, provided that predicates never occur in the scope of quantifiers.
Quantifier elimination procedure that can also handle uninterpreted predicates, provided that predicates never occur in the scope of quantifiers. Quantifiers above predicate occurrences are left in the formula. The method can also handle formulas with bit-vector arithmetic or non-linear multiplication, and is optimised for post-processing of interpolants.
Compute the most general quantifier-free formula without uninterpreted predicates that implies the given formula, modulo the given axioms.
Compute the most general quantifier-free formula without uninterpreted predicates that implies the given formula, modulo the given axioms. If the input formula or the axioms contain quantifiers, this might not terminate.
Enumerate the disjuncts of a formula that already is in DNF.
Enumerate the models of a given formula.
Enumerate the models of a given formula. Currently, we assume that the formula does not contain predicates and only existential quantifiers (this could be relaxed)
Check whether the function objective
has a lower bound
subject to constraint
, and return such a bound.
Check whether the function objective
has a lower bound
subject to constraint
, and return such a bound.
Minimise the given formula by eliminating unnecessary disjuncts.
Minimise the given formula by eliminating unnecessary disjuncts.
This is a stronger version of the simplification performed by
ReduceWithConjunction
, and also simplifies formulae
a & (b | c) & (b | c')
where c & c'
is
unsatisfiable.
Enumerate the disjuncts of a formula (which might not be in DNF).
Turn a formula into DNF.
Turn a formula into DNF. The DNF might not be complete in the sense that
a formula a & b | a & c
might only be normalised to
a & (b | c)
Convert a given formula to prenex form.
Convert a given formula to prenex form. TODO: do something special for divisibilities?
A collection of tools for analysing and transforming formulae in Presburger arithmetic