在 Z3 中以表达式形式获取战术应用的结果

Question

在 C++ 中有没有类似的东西，比如 Z3py 接口的 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？

Answer 1

一般来说，战术应用的结果是一组目标。大多数战术只会产生一个目标，但有些战术会产生不止一个目标。对于这些子目标中的每一个，您可以使用as_expr()，然后将它们逻辑或一起使用。如果有帮助，我们可以将as_expr(...) 添加到class apply_result。 （我现在正忙于其他事情；如果您自己添加，请提交拉取请求，非常欢迎贡献！）