4

私の質問は次のようなものです: Z3: Z3py 式を SMT-LIB2 に変換しますか?

z3py 式を smtlib2 形式に変換しようとしています。次のスクリプトを使用しますが、結果を z3 またはその他の SMT にフィードしているときに変換すると、次のようになります。

「構文エラー、予期しない let」

長い式を再度記述する必要がないように、z3py を使用して smtlib2 形式にする方法はありますか。

以下は、変換に使用しているコードです。

def convertor(f, status="unknown", name="benchmark", logic=""):
v = (Ast * 0)()
if isinstance(f, Solver):
a = f.assertions()
if len(a) == 0:
  f = BoolVal(True)
else:
  f = And(*a)
return Z3_benchmark_to_smtlib_string(f.ctx_ref(), name, logic, status, "", 0, v, f.as_ast())

x = Int('x')
y = Int('y')
s = Solver()
s.add(x > 0)
s.add( x < 100000)
s.add(x==2*y)
print convertor(s, logic="QF_LIA")

これは出力です：

(set-info :status unknown)
(set-logic QF_LIA)
(declare-fun y () Int)
(declare-fun x () Int)
(let (($x34 (= x (* 2 y))))
(let (($x31 (< x 100000)))
(let (($x10 (> x 0)))
(let (($x35 (and $x10 $x31 $x34)))
(assert $x35)))))
(check-sat)
4

1 に答える 1

1

これは別の質問hereにも関連しています。

おそらく、この問題は古いバージョンの Z3 が原因です。まだ master ブランチに反映されていない多数のバグ修正があり、unstable ブランチ (またはここでプリコンパイルされたナイトリー バイナリ) を使用すると、Z3 でエラーなしで受け入れられる別の出力が得られます。

(set-info :status unknown)
(set-logic QF_LIA)
(declare-fun y () Int)
(declare-fun x () Int)
(assert
(let (($x34 (= x (* 2 y))))
(let (($x31 (< x 100000)))
(let (($x10 (> x 0)))
(and $x10 $x31 $x34)))))
(check-sat)
于 2014-03-24T22:03:07.937 に答える