0

現在、Pythonでz3を使用して、プログラムトレースの実現可能性を確認しています。z3式とアサーションを作成するトレースに基づいて、次のアプローチは現在、Z3_benchmark_to_smtlib_stringを介して中間言語としてSMT2を使用して、これらのアサーションをiZ3とsmtinterpolにフィードしています。

小さな例：x = Int（'x'）y = Int（'y'）

s = Solver()

# Assertions
s.assert_and_track(x > y, 'p1')
s.assert_and_track(x == 0, 'p2')
s.assert_and_track(y > 0, 'p3')

a = s.assertions()
v = a[0].as_ast()
f = And(a[1], a[2])
print Z3_benchmark_to_smtlib_string(a[0].ctx_ref(), "name", "QF_LIA", "unsat", "", 1, v, f.as_ast())

これにより、出力が生成されます

; name    
(set-info :status unsat)
(set-logic QF_LIA)
(declare-fun y () Int)
(declare-fun x () Int)
(assert
(> x y))
(assert
(let (($x12 (> y 0)))
(let (($x10 (= x 0)))
(and $x10 $x12))))
(check-sat)

これは、いくつかの自主的に変更した後、smtinterpolにフィードするのに適しています。

; name
(set-info :status unsat)
(set-option :produce-proofs true)
(set-logic QF_LIA)
(declare-fun y () Int)
(declare-fun x () Int)
(assert (!
(> x y) :named p1))
(assert (!
(let (($x12 (> y 0)))
(let (($x10 (= x 0)))
(and $x10 $x12))) :named p2))
(check-sat)
(get-interpolants p1 p2)

私たちが望んでいるのは、ハックなしですべてのアサーションをsmt2出力に入れて、ANDを介してすべての1：endアサーションを1つの方程式に結合する可能性です。c-codeドキュメント（capi.html＃gaf93844a5964ad8dee609fac3470d86e4"> http://research.microsoft.com/en-us/um/redmond/projects/z3/group_capi.html#gaf93844a5964ad8dee609fac3470d86e4）で推測しようとした場合6番目と7番目のパラメーターですが、アサーションのリストを提供することで機能させることができました。

私は例えば試しました：

print Z3_benchmark_to_smtlib_string(a[0].ctx_ref(), "name", "QF_LIA", "unsat", "", 2, f.as_ast(), v)

しかし、に遭遇します

exception: access violation reading 0x00000004

また、リストを与えるだけでは機能しません。

print Z3_benchmark_to_smtlib_string(a[0].ctx_ref(), "name", "QF_LIA", "unsat", "", 2, [a[0].as_ast(), a[1].as_ast()], a[2].as_ast())

基本的に、誰かが__in_ecount（num_assumptions）Z3_ast constに相当するPythonを知っていますか？または、ソルバーのアサーションのリストからsmt2出力を生成する別の可能性はありますか？

4

1 に答える 1

1

お気づきのとおり、Python APIは、ベンチマークを出力する関数にPythonラッパーを公開しません。C署名は次のとおりです。

/**
   \brief Convert the given benchmark into SMT-LIB formatted string.

   \conly \warning The result buffer is statically allocated by Z3. It will
   \conly be automatically deallocated when #Z3_del_context is invoked.
   \conly So, the buffer is invalidated in the next call to \c Z3_benchmark_to_smtlib_string.

   \param c - context.
   \param name - name of benchmark. The argument is optional.
   \param logic - the benchmark logic. 
   \param status - the status string (sat, unsat, or unknown)
   \param attributes - other attributes, such as source, difficulty or category.
   \param num_assumptions - number of assumptions.
   \param assumptions - auxiliary assumptions.
   \param formula - formula to be checked for consistency in conjunction with assumptions.

   def_API('Z3_benchmark_to_smtlib_string', STRING, (_in(CONTEXT), _in(STRING), _in(STRING), _in(STRING), _in(STRING), _in(UINT), _in_array(5, AST), _in(AST)))
*/
Z3_string Z3_API Z3_benchmark_to_smtlib_string(__in   Z3_context c, 
                                               __in Z3_string name,
                                               __in Z3_string logic,
                                               __in Z3_string status,
                                               __in Z3_string attributes,
                                               __in   unsigned num_assumptions,
                                               __in_ecount(num_assumptions) Z3_ast const assumptions[],
                                               __in   Z3_ast formula);

z3.pyには、配列を引数として取る同様の関数の例がいくつかあり、それらは同じパターンを使用して、C関数に2つの引数を与えます。（1）配列の長さ（2）実際の配列。配列の長さと選択されていない配列をC関数に渡す必要があります。この変更を加えた例の変形はここにあります：http：//rise4fun.com/Z3Py/rGEp

于 2013-03-25T01:23:57.460 に答える