Z3 Python中不满意的核心
发布时间:2020-12-20 11:25:11 所属栏目:Python 来源:网络整理
导读:我正在使用Z3的 Python API,试图在我正在编写的研究工具中包含对它的支持.我有一个关于使用Python接口提取不可满足核心的问题. 我有以下简单查询: (set-option :produce-unsat-cores true)(assert (! (not (= (_ bv0 32) (_ bv0 32))) :named __constraint0
我正在使用Z3的
Python API,试图在我正在编写的研究工具中包含对它的支持.我有一个关于使用Python接口提取不可满足核心的问题.
我有以下简单查询: (set-option :produce-unsat-cores true) (assert (! (not (= (_ bv0 32) (_ bv0 32))) :named __constraint0)) (check-sat) (get-unsat-core) (exit) 通过z3可执行文件(对于Z3 4.1)运行此查询,我收到了预期的结果: unsat (__constraint0) 对于Z3 4.3,我获得了一个分段错误: unsat Segmentation fault 这不是主要问题,尽管这是一个有趣的观察.然后我将查询(在文件中)修改为 (assert (! (not (= (_ bv0 32) (_ bv0 32))) :named __constraint0)) (exit) 使用文件处理程序,我将此文件的内容(在变量`queryStr’中)传递给以下Python代码: import z3 ... solver = z3.Solver() solver.reset() solver.add(z3.parse_smt2_string(queryStr)) querySatResult = solver.check() if querySatResult == z3.sat: ... elif querySatResult == z3.unsat: print solver.unsat_core() 我从`unsat_core’函数接收空列表:[].我是否正确使用此功能?该函数的文档字符串表明我应该做类似的事情 solver.add(z3.Implies(p1,z3.Not(0 == 0))) 但是,我想知道是否仍然可以按原样使用查询,因为它符合SMT-LIB v2.0标准(我相信),以及我是否遗漏了一些明显的东西. 解决方法
您观察到的崩溃已得到修复,修复程序将在下一版本中提供.如果您尝试“不稳定”(work-in-progress)分支,则应该获得预期的行为.
您可以使用检索不稳定分支 git clone https://git01.codeplex.com/z3 -b unstable API parse_smt2_string仅为解析SMT 2.0格式的公式提供基本支持.它不保留注释:命名.我们将在未来版本中解决此问题和其他限制.在此期间,我们应该使用“回答文字”,如p1和形式的断言: solver.add(z3.Implies(p1,z3.Not(0 == 0))) 在“不稳定”分支中,我们还支持以下新API.它“模拟”SMT 2.0标准中使用的命名断言. def assert_and_track(self,a,p): """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`. If `p` is a string,it will be automatically converted into a Boolean constant. >>> x = Int('x') >>> p3 = Bool('p3') >>> s = Solver() >>> s.set(unsat_core=True) >>> s.assert_and_track(x > 0,'p1') >>> s.assert_and_track(x != 1,'p2') >>> s.assert_and_track(x < 0,p3) >>> print(s.check()) unsat >>> c = s.unsat_core() >>> len(c) 2 >>> Bool('p1') in c True >>> Bool('p2') in c False >>> p3 in c True """ ... (编辑:李大同) 【声明】本站内容均来自网络,其相关言论仅代表作者个人观点,不代表本站立场。若无意侵犯到您的权利,请及时与联系站长删除相关内容! |