c++ - 在Z3中获取战术应用的结果作为表达式

C++中是否有类似Z3py接口(interface)的as_expr()的东西。我正在尝试将策略应用为z3表达式 exp 而不是 apply_result 类型的结果。

例如，在下面的代码中

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";

另外，有什么方法可以将apply_result转换为z3 expr？

最佳答案

通常，战术应用的结果是一组目标。大多数战术只产生一个目标，但有些则产生不止一个目标。对于每个子目标，您可以使用as_expr()，然后将它们逻辑或在一起。如果可以，我们可以在as_expr(...)中添加class apply_result。 (目前我正忙于其他事情；如果您自己添加，请提交请求请求，非常感谢您的贡献!)