cooper2.png

What is Cooper?

Cooper is the component of Mistral for performing quantifier elimination. It implements Cooper's method for eliminating quantifiers in Presburger arithmetic (i.e., linear arithmetic over integers).

How to Use Cooper

To perform existential quantifier elimination, one can use the eliminate_evar methods provided in Constraint.h. Here is a simple example illustrating existential quantifier elimination:

VariableTerm* x = VariableTerm::make("x");
VariableTerm* y = VariableTerm::make("y");

map<Term*, long int> elems;
elems[x] = 1;
elems[y] = 1;
Term* t = ArithmeticTerm::make(elems, 0);

Constraint c1(x, ConstantTerm::make(0), ATOM_LT);
Constraint c2(t, ConstantTerm::make(0), ATOM_GEQ);
Constraint c3 = c1 & c2;

cout << "Before elimination: " << c3 << endl;
c3.eliminate_evar(x);
cout << "After elimination: " << c3 << endl;

Here, we first construct a constraint c3 which represents the formula x<0 & x+y >=0. We then call the eliminate_evar method to eliminate variable x as an existentially quantified variable. The constraint that is printed at the last line is y>0, which is the result of performing quantifier elimination.

There is also an interface that allows eliminating multiple variables at the same time. For instance, in the previous example, here is how we would eliminate both x and y from constraint c3:

set<VariableTerm*> vars;
vars.insert(x);
vars.insert(y);
c3. eliminate(vars);
cout << "Result of quantifier elimination: " << c3 << endl;

In addition, Cooper provides an interface for eliminating universally quantified variables. For this purpose, one can use the eliminate_uvar method as follows:

VariableTerm* x = VariableTerm::make("x");
VariableTerm* y = VariableTerm::make("y");

map<Term*, long int> elems;
elems[x] = 1;
elems[y] = 1;
Term* t = ArithmeticTerm::make(elems, 0);

Constraint c1(x, ConstantTerm::make(0), ATOM_GEQ);
Constraint c2(t, ConstantTerm::make(0), ATOM_LT);
Constraint c3 = c1 & c2;

cout << "Before elimination: " << c3 << endl;
c3.eliminate_uvar(x);
cout << "After elimination: " << c3 << endl;

Here, the original constraint c3 is (x>=0 | x+y<0). After eliminating x as a universally quantified variable, we obtain y <= 0.