3

私が書いている調査ツールにPythonAPIのサポートを含めるために、Z3のPythonAPIを使用しています。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-LIB v2.0標準に準拠しているため（私は信じています）、クエリをそのまま使用できるかどうか、そして明らかな何かが欠けているかどうか疑問に思いました。

4

1 に答える 1

8

あなたが確認したクラッシュは修正されており、修正は次のリリースで利用可能になります。「不安定な」(進行中の) ブランチを試すと、期待どおりの動作が得られるはずです。を使用して不安定なブランチを取得できます

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

APIparse_smt2_stringは、SMT 2.0 形式の数式を解析するための基本的なサポートのみを提供します。注釈は保持されません:named。将来のバージョンでは、この制限およびその他の制限に対処する予定です。それまでの間、次のような「回答リテラル」p1と次の形式のアサーションを使用する必要があります。

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

「unstable」ブランチでは、次の新しい API もサポートしています。:namedSMT 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
    """
    ...
于 2013-01-28T15:38:59.513 に答える