Quantifier Elimination for LIA in Z3 via C/C++ API

Question

I would like to use Z3 for eliminating quantifiers in linear integer arithmetic formulas via C/C++ API. Consider a simple example: Exists (x) ( x <= y & y <= 2*x). A quantifier-free formula with the same models is y >= 0.

I tried to do it this way:

   context ctx;
   ctx.set("ELIM_QUANTIFIERS", "true");
   expr x = ctx.int_const("x"); 
   expr y = ctx.int_const("y"); 
   expr sub_expr = (x <= y)  && (y <= 2*x);

   Z3_ast qf = Z3_mk_exists_const(ctx, 0, 1, (Z3_app[]) {x}, 
                                  0, {}, // patterns don't seem to make sense here.
                                  sub_expr); //No C++ API for quantifiers :(
   qf = Z3_simplify(ctx, qf);
   cout << Z3_ast_to_string(ctx, qf);

what I get is

(exists ((x Int) (and (<= x y) (<= y (* 2 x))))

whereas I'd like to obtain something like

(<= 0 y)

Is there a possibility to get it with Z3? Many thanks in advance.

Answer 1

The simplifier does not invoke the quantifier elimination procedures any longer. Quantifier elimination and many other special purpose simplification rewrites are available over tactics.

The C++ wrapper z3++.h exposes methods for creating tactic objects. You would have to create a tactic object for the "qe" tactic. THe Z3 distribution comes with a couple of samples for using the tactics from the z3++.h API. For example:

void tactic_example1() {
/*
  Z3 implements a methodology for orchestrating reasoning engines where "big" symbolic
  reasoning steps are represented as functions known as tactics, and tactics are composed
  using combinators known as tacticals. Tactics process sets of formulas called Goals.

  When a tactic is applied to some goal G, four different outcomes are possible. The tactic succeeds
  in showing G to be satisfiable (i.e., feasible); succeeds in showing G to be unsatisfiable (i.e., infeasible); 
  produces a sequence of subgoals; or fails. When reducing a goal G to a sequence of subgoals G1, ..., Gn, 
  we face the problem of model conversion. A model converter construct a model for G using a model for some subgoal Gi.

  In this example, we create a goal g consisting of three formulas, and a tactic t composed of two built-in tactics: 
  simplify and solve-eqs. The tactic simplify apply transformations equivalent to the ones found in the command simplify. 
  The tactic solver-eqs eliminate variables using Gaussian elimination. Actually, solve-eqs is not restricted 
  only to linear arithmetic. It can also eliminate arbitrary variables. 
  Then, sequential composition combinator & applies simplify to the input goal and solve-eqs to each subgoal produced by simplify. 
  In this example, only one subgoal is produced.
*/
std::cout << "tactic example 1\n";
context c;
expr x = c.real_const("x");
expr y = c.real_const("y");
goal g(c);
g.add(x > 0);
g.add(y > 0);
g.add(x == y + 2);
std::cout << g << "\n";
tactic t1(c, "simplify");
tactic t2(c, "solve-eqs");
tactic t = t1 & t2;
apply_result r = t(g);
std::cout << r << "\n";

}

In your case you would want something along the lines of:

context ctx;
expr x = ctx.int_const("x"); 
expr y = ctx.int_const("y"); 
expr sub_expr = (x <= y)  && (y <= 2*x);

Z3_ast qf = Z3_mk_exists_const(ctx, 0, 1, (Z3_app[]) {x}, 
                              0, {}, // patterns don't seem to make sense here.
                              sub_expr); //No C++ API for quantifiers :(
tactic qe(ctx, "qe");
goal g(ctx);
g.add(qf);
cout << qe.apply(g);

Answer 2

Nikolaj already pointed out that tactics can be used to perform quantifier elimination. In this post, I'd like to emphasize how to safely mix the C++ and C APIs. The Z3 C++ API uses reference counting to manage the memory. expr is essentially a "smart-pointer" that manages the reference counters automatically for us. I discussed this issue in the following post: Array select and store using the C++ API.

So, when we invoke a C API that returns a Z3_ast, we should wrap the result using the functions to_expr, to_sort or to_func_decl. The signature of to_expr is:

inline expr to_expr(context & c, Z3_ast a);

By using this function, we avoid memory leaks, and crashes (when accessing objects that have been garbage collected by Z3). Here is the complete example using to_expr(). You can test it by copying this function in the example.cpp file in the c++ folder in the Z3 distribution.

void tst_quantifier() {
    context ctx;
    expr x = ctx.int_const("x"); 
    expr y = ctx.int_const("y"); 
    expr sub_expr = (x <= y) && (y <= 2*x);
    Z3_app vars[] = {(Z3_app) x};

    expr qf = to_expr(ctx, Z3_mk_exists_const(ctx, 0, 1, vars,
                                              0, 0, // patterns don't seem to make sense here.
                                              sub_expr)); //No C++ API for quantifiers :(
    tactic qe(ctx, "qe");
    goal g(ctx);
    g.add(qf);
    std::cout << qe.apply(g);
}