Z3 Python 中无法满足的核心 [英] Unsatisfiable Cores in Z3 Python

问题描述

我正在使用 Z3 的 Python API，试图在我正在编写的研究工具中包含对它的支持.我有一个关于使用 Python 接口提取不可满足的核心的问题.

I am working with the Python API of Z3 in an attempt to include support for it in a research tool that I am writing. I have a question regarding extracting the unsatisfiable core using the 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)运行此查询，我收到了预期的结果:

Running this query through the z3 executable (for Z3 4.1), I receive the expected result:

unsat
(__constraint0)

对于 Z3 4.3，我得到一个分段错误:

For Z3 4.3, I obtain a segmentation fault:

unsat
Segmentation fault

这不是主要问题，尽管这是一个有趣的观察.然后我将查询(在文件内)修改为

That isn't the main question, although that was an intriguing observation. I then modified the query (inside a file) as

(assert (! (not (= (_ bv0 32) (_ bv0 32))) :named __constraint0))
(exit)

使用文件处理程序，我将此文件的内容(在变量 `queryStr' 中)传递给以下 Python 代码:

Using a file handler, I passed the contents of this file (in a variable `queryStr') to the following Python code:

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' 函数的空列表:[].我是否错误地使用了此功能?该函数的文档字符串表明我应该做类似的事情

I receive the empty list from the `unsat_core' function: []. Am I using this function incorrectly? The docstring for the function suggests that I should instead be doing something similar to

solver.add(z3.Implies(p1, z3.Not(0 == 0)))

但是，我想知道是否仍然可以按原样使用查询，因为它符合 SMT-LIB v2.0 标准(我相信)，以及我是否遗漏了一些明显的东西.

However, I was wondering if it were still possible to use the query as is, since it conforms to SMT-LIB v2.0 standards (I believe), and whether I was missing something obvious.

推荐答案

您观察到的崩溃已得到修复，该修复将在下一个版本中提供.如果您尝试不稳定"(正在进行中)分支，您应该得到预期的行为.您可以使用

The crash you observed has been fixed, and the fix will be available in the next release. If you try the "unstable" (work-in-progress) branch, you should get the expected behavior. You can retrieve the unstable branch using

git clone https://git01.codeplex.com/z3 -b unstable

API parse_smt2_string 仅提供对解析 SMT 2.0 格式公式的基本支持.它不保留注释 :named.我们将在未来版本中解决这个和其他限制.同时，我们应该使用答案文字"，例如 p1 和以下形式的断言:

The API parse_smt2_string provides only basic support for parsing formulas in SMT 2.0 format. It does not keep the annotations :named. We will address this and other limitations in future versions. In the meantime, we should use "answer literals" such as p1 and assertions of the form:

solver.add(z3.Implies(p1, z3.Not(0 == 0)))

在unstable"分支中，我们还支持以下新 API.它模拟"了 SMT 2.0 标准中使用的 :named 断言.

In the "unstable" branch, we also support the following new API. It "simulates" the :named assertions used in the SMT 2.0 standard.

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 Python 中无法满足的核心的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！