Get result of tactics application as an expression in Z3

Question

Is there anything similar in C++ like Z3py interface's as_expr(). I'm trying to get the result of applying the tactics as a z3 expression, exp, not as type apply_result.

For example, in the below code

context c;
expr x = c.bool_const("x");
expr y = c.bool_const("y");
expr f = ( (x || y) && (x && y) );
solver s(c);
goal g(c);
g.add( f );
tactic t1(c, "simplify");
apply_result r = t1(g);
std::cout << r << "\n";

Also, is there any way to convert the apply_result into z3 expr?

Answer 1

In general, the result of a tactic application is a set of goals. Most tactics produce only one goal, but some produce more than one. For each of those subgoals, you can use as_expr() and then logical-or them together. We can add an as_expr(...) to class apply_result if that helps. (I'm busy with other stuff at the moment; if you add it yourself, submit a pull request, contributions very welcome!)