在 z3::expr 中使用 C++ 字符串？

Question

我在使用 Z3::expr 时遇到了困难。在 z3 中，expr conj 可以这样定义：

expr x = c.bool_const("x");
expr y = c.bool_const("y");
expr conj = (!x || !y);

有没有办法使用字符串变量来定义conj？比如：

expr x = c.bool_const("x");
expr y = c.bool_const("y");
string str = "(!x || !y)";
expr conj = some_API(str);

我被这个问题困扰了好几天。

谢谢

Answer 1

在示例中无法使用该特定字符串，但您可以使用parse_string，它可以理解 SMT2 格式的字符串。