CODEWITHSUNDEEP
z3
cxcfan
cxcfan

Reputation: 185

Z3 - How to extract variables from a given formula?

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.

Upvotes: 2

Views: 1152

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

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

Upvotes: 3

Related Questions