z3 - Z3: Z3py 式を SMT-LIB2 に変換しますか?

Question

Z3py で与えられた式を SMT-LIB2 言語に変換できますか? (したがって、SMT-LIB2 をサポートする他の SMT ソルバーにこの SMT-LIB2 式をフィードできます)

可能であれば、一例を挙げてください。

どうもありがとう。

Answer 1

CAPIを使用できますZ3_benchmark_to_smtlib_string。CAPIのすべての関数はZ3Pyで使用できます。この関数は当初、ベンチマークをSMT 1.0形式でダンプするために使用されていましたが、SMT2.0よりも前のものです。そのため、不要と思われるパラメータがいくつかあります。現在、デフォルトでは、ベンチマークがSMT2.0形式で表示されます。出力は、人間が読める形式ではありません。次のPython関数を記述して、より使いやすくすることができます。

def toSMT2Benchmark(f, status="unknown", name="benchmark", logic=""):
  v = (Ast * 0)()
  return Z3_benchmark_to_smtlib_string(f.ctx_ref(), name, logic, status, "", 0, v, f.as_ast())

これを使用した小さな例を次に示します（ここからオンラインでも入手できます）

a = Int('a')
b = Int('b')
f = And(Or(a > If(b > 0, -b, b) + 1, a <= 0), b > 0)
print toSMT2Benchmark(f, logic="QF_LIA")