问题描述
我在文档中找不到关于此主题的任何内容。我试过像s.add("Or(a==1,a==2,a==3),Or(b==1,b==2,b==3),Or(c==1,c==2,c==3)")那样，但这不起作用。有可能吗？
在sympy中，我们可以使用sympify或parse_expr
编辑：
我看到我只能使用python eval。它还有parse_smt2_string()，但没有参考SMT2的工作原理。
解决方法
eval是必经之路。 z3py中没有以任何方式来解析本质上是Python程序的支持。请注意，要使其正常工作，您应该以某种方式在环境中使用变量a / b和c，无论是通过显式声明还是通过eval对其进行声明像"a,b,c = Ints('a b c')"
关于您的评论“没有参考SMT2的工作原理：” SMTLib是所有SMT求解器（包括z3）接受的标准格式。看到这里：http://smtlib.cs.uiowa.edu/