3

z3 の python API を使用して、一連の制約が満足できるかどうかを確認しています。私は条件を文字列として持っており、トランスコードの処理時間を節約するために、可能な限りそれらを z3 に直接渡したいと考えています。制約が a = b のような割り当てである場合、それを入力する最良の方法は何ですか? 私は何かが欲しい

    str1 = "a = b"
    a = BitVec('a', 3)
    b = BitVec('b', 3)
    s = Solver()
    s.push()
    s.add(str1)

このプログラムは、「True、False、または Z3 ブール式が必要です」というエラーを出します
。最善の方法を教えてください。

4

1 に答える 1

4

文字列ではなく、大部分の API 関数 ( など) に Z3 式を渡す必要がありSolver.add(expr)ます。あなたの例 (z3py リンク: http://rise4fun.com/Z3Py/iu0 ):

str1 = "a = b"
a = BitVec('a', 3)
b = BitVec('b', 3)
constraint1 = a == b # sets constraint1 to be the z3 expression a == b
s = Solver()
s.push()
# s.add(str1) # error: 'True, False or Z3 Boolean expression expected'
s.add(constraint1)
print constraint1

中置記法 (「a = b」など) でエンコードされた文字列を渡したい場合は、Python の を使用できるはずですが、これは完全な汎用性で機能しない可能性があるため、パーサーを作成する必要がある場合があり、 on をeval使用することはできません。eval消毒剤によるrise4fun：

constraint2 = eval(str1)

使用に関する詳細は次のevalとおりです。 z3python: 文字列を式に変換する

SMT-LIB 標準 (「(= ab)」などのプレフィックス表記を使用する) でエンコードされた文字列がある場合は、parse_smt2_stringAPI 関数を使用できます。上記の続きの例を次に示します。

cstr1 = "(assert (= a b))"
ds = { 'a' : a, 'b' : b }
constraint3 = parse_smt2_string(cstr1, decls=ds)
print constraint3
prove(constraint1 == constraint3)

の API ドキュメントは次のparse_smt2_stringとおりです。 http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html#-parse_smt2_string

Z3式の出力にインフィックスを使用することに関するこの関連する質問と回答も参照してください: z3式をインフィックス式に変換する方法?

于 2013-05-10T04:13:06.387 に答える