在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。 （我现在忙于其他的东西;如果你自己添加，提交拉取请求，非常欢迎贡献！）