在Z3的Python不可满足的核心(Unsatisfiable Cores in Z3 Python

我试图与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标准（我相信），我是否失去了一些东西明显。

你观察到的崩溃已得到修复，并修复将在未来版本中提供。如果您尝试了“不稳定”（工作正在进行中）分支，你应该得到预期的行为。您可以使用检索不稳定分支

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。它“模拟” :named在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
    """
    ...