我在使用 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);
我在这个问题上卡住了好几天。
谢谢
最佳答案
无法在示例中使用该特定字符串,但您可以使用 parse_string
,它理解 SMT2 格式的字符串。
关于c++ - 在 z3::expr 中使用 C++ 字符串?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/51063153/