Z3 Python中不可满足的核心
Z3 Python中不可满足的核心
提问于 2013-01-28 11:11:21
我正在使用Z3的Python，试图在我正在编写的一个研究工具中包含对它的支持。关于使用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函数的空列表：[]。我是不是不正确地使用这个函数？函数的docstring建议我应该执行类似于
solver.add(z3.Implies(p1, z3.Not(0 == 0)))但是，我想知道是否仍然可以按原样使用该查询，因为它符合SMT-Libv2.0标准(我相信)，以及是否遗漏了一些显而易见的内容。
回答 1
Stack Overflow用户
回答已采纳
发布于 2013-01-28 15:38:59
您观察到的崩溃已经修复，修复将在下一个版本中可用。如果您尝试“不稳定”(工作正在进行中)分支，您应该得到预期的行为。可以使用以下方法检索不稳定的分支
git clone https://git01.codeplex.com/z3 -b unstableAPI parse_smt2_string只为SMT2.0格式的解析公式提供基本支持。它不保留注释:named。我们将在今后的版本中解决这一问题和其他限制。同时，我们应该使用“应答文本”，比如p1和表单的断言：
solver.add(z3.Implies(p1, z3.Not(0 == 0)))在“不稳定”分支中，我们还支持以下新API。它“模拟”在SMT2.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
"""
...页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/14560745
复制相关文章
相似问题
腾讯云开发者
