2

次の2つのステートメントの違いは何ですか?

ステートメント 1

(define-fun max_integ ((x Int) (y Int)) Int 
  (ite (< x y) y x))

ステートメント 2

(declare-fun max_integ ((Int)(Int)) Int)
(assert (forall ((x Int) (y Int)) (= (max_integ x y) (if (< x y) y x))))

Statement1 を使用すると、z3 制約によって 0.03 秒で結果が得られることがわかりました。Statement2 を使用した場合、2 分で終了せず、ソルバーを終了します。C-APIを使用してそれを達成する方法も知りたいです。

ありがとう ！

4

1 に答える 1

3

ステートメント 1 はマクロです。Z3 は、出現するすべてmax_integの式をその式に置き換えiteます。解析時にそれを行います。2 番目のステートメントでは、デフォルトでは、Z3 は を削除せずmax_integ、すべてのおよびの量指定子を満たすsat未解釈のシンボルの解釈を構築する必要があります。Z3 には というオプションがあり、本質的にマクロをエンコードしている量指定子を検出し、それらを削除します。以下に例を示します (こちらからオンラインでも入手できます)。max_integxy:macro-finder

(set-option :macro-finder true)
(declare-fun max_integ ((Int)(Int)) Int)
(assert (forall ((x Int) (y Int)) (= (max_integ x y) (if (< x y) y x))))
(check-sat)
(get-model)

そうは言っても、指定された Z3 式が新しい Z3 式を返す関数を作成することで、プログラム API でマクロを簡単にシミュレートできます。Python API を使用した例 (こちらからオンラインでも入手可能):

def max(a, b):
   # The function If builds a Z3 if-then-else expression
   return If(a >= b, a, b)

x, y = Ints('x y')
solve(x == max(x, y), y == max(x, y), x > 0)

さらに別のオプションは、C API を使用することですZ3_substitute_vars。アイデアは、自由変数を含む式です。自由変数は API を使用して作成されますZ3_mk_bound。各変数は引数を表します。次に、Z3_substitute_vars変数を他の式に置き換えるために使用します。

于 2013-04-02T16:00:23.863 に答える