2

I'm using Z3 C++ API (Version 4.3.1) and I want to extract variables of a formula (An object of type expr). I've found a similar question but it is in Z3py. I am wonder if there is a method in Z3 C/C++ API to extract variables from expr object. Thanks!

For example (some details omitted):

    expr fs = implies(x + y == 0, z * x < 15);
    std::vector<expr> varlist = get_vars(fs);

Then varlist should contain x,y,z.

Community
  • 1
  • 1
cxcfan
  • 185
  • 9

1 Answers1

3

The C++ example in the distribution (examples/c++/example.cpp) shows a sample visitor pattern. It is very simplistic, but will give the idea.

I repeat it here below:

void visit(expr const & e) {
if (e.is_app()) {
    unsigned num = e.num_args();
    for (unsigned i = 0; i < num; i++) {
        visit(e.arg(i));
    }
    // do something
    // Example: print the visited expression
    func_decl f = e.decl();
    std::cout << "application of " << f.name() << ": " << e << "\n";
}
else if (e.is_quantifier()) {
    visit(e.body());
    // do something
}
else { 
    assert(e.is_var());
    // do something
}
}

The visitor function can be improved by using a cache of previously visited expressions because in general Z3 uses shared sub-expressions. This is similar to the Python example.

Hope this helps

Nikolaj Bjorner
  • 8,229
  • 14
  • 15
  • Thank you very much, and I have another question. I noticed that `e.is_app()` and `e.is_var()` are two different branches. However, a variable is also an application. So what kind of expression `e` could enter `e.is_var()` branch instead of `e.is_app()` branch? – cxcfan Sep 28 '14 at 06:42
  • An expression can be either an application, a quantifier, or a bound variable. The e.is_var() check succeeds only for bound variables. Z3 uses indices for bound variables. So the cases for e.is_app and e.is_var never overlap. – Nikolaj Bjorner Nov 28 '16 at 17:36