我正在使用 Z3 的 Python API,试图在我正在编写的研究工具中包含对它的支持。我有一个关于使用 Python 接口(interface)提取不可满足的核心的问题。
我有以下简单的查询:
(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 标准(我相信),以及我是否遗漏了一些明显的东西。
最佳答案
您观察到的崩溃已修复,该修复将在下一个版本中提供。如果您尝试“不稳定”(正在进行的工作)分支,您应该会得到预期的行为。 您可以使用
检索不稳定的分支git clone https://git01.codeplex.com/z3 -b unstable
API parse_smt2_string
仅提供对 SMT 2.0 格式的解析公式的基本支持。它不保留注释 :named
。我们将在未来版本中解决此限制和其他限制。同时,我们应该使用诸如 p1
之类的“答案文字”和以下形式的断言:
solver.add(z3.Implies(p1, z3.Not(0 == 0)))
在“不稳定”分支中,我们还支持以下新 API。它“模拟”了 SMT 2.0 标准中使用的 :named
断言。
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
"""
...
关于z3 - Z3 Python 中无法满足的核心,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/14560745/