如何解决我们可以从字符串中评估z3py表达式吗?
我在文档中找不到关于此主题的任何内容。我试过像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/
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。