missing modification methods on C++ APIs

Question

I wanted to make some transformation on a z3::expr object. How can I use Z3_substitute_vars, Z3_translate and Z3_substitute_ with the C++ API? They are implemented in C#, but I can't find them in C++. It's very strange that they are not implemented.

I tried to use the C api but without any result, here an example:

void substitute(){
z3::context c;
z3::expr a = c.int_const("a");
Z3_ast astA = a;
z3::expr plus = 2*a;
errs() << Z3_ast_to_string(c,plus);
z3::expr b = c.int_const("b");
Z3_ast astB = a;
z3::expr subs(c,Z3_substitute(c,plus,1,&astA,&astB));
errs() << Z3_ast_to_string(c,subs);
}

But a doesn't get substituted. Am I doing something wrong?

score 2 · Accepted Answer · edited May 23 '17 at 12:18

Thanks for pointing out that these functions are absent. The C++ wrapper adds conveniences beyond the C API and it will be reasonable to add convenciences for these API functions as well since you indicate you are using them.

The C++ wrappers can still be used together with the basic C API. You can therefore call functions, such as Z3_translate and Z3_substitute when using the C++ API. A number of other API functions are also not present in the C++ wrapper, but the way that existing functions are wrapped should give a very good idea how to call remaining functions.

Here are some related posts:

Thanks! I tried to use the C api, without any result, I edited my question with an example, but it doesn't work, am I using the method wrongly? — Giacomo Tagliabue, Apr 18 '13 at 13:58

score 1 · Answer 2 · answered Apr 18 '13 at 17:10

1

I believe your example has a typo:

  Z3_ast astB = a;

Try

  Z3_ast astB = b;

answered Apr 18 '13 at 17:10

Nikolaj Bjorner

8,229
14
15

missing modification methods on C++ APIs

2 Answers2