1

私は動的観測のいくつかの簡単な分析にMicrosoftのZ3を使用しています。この一環として、ある数式をある変数のセットを使用してから別のターゲットの変数のセットに変換できれば便利です。

私はZ3を初めて使用しますが、内部の簡略化ルールや数式を変換する他の手段があることを知っています...基本的に、次のような変換を実行できるかどうか疑問に思っています。

(declare-const local Real)
(declare-const x Real)
(declare-const y Real)
(declare-const midstep Real)
(declare-const local_1 Real)
(declare-const foo_ret Real)

(assert (= local (/ x y)))
(assert (= midstep local))
(assert (= local_1 (+ midstep 1.0)))

(assert (= foo_ret local_1) :name toTransform)

; this is what I'd love to do - give Z3 a formula and a target set of variables
(special-simplify (= foo_ret local_1) (foo_ret x y))
; and have Z3 do the appropriate substitutions, etc to spit back 
; a "simplified" version in terms of foo_ret, x, and y, e.g.: 
;    (= foo_ret (+ (/ x y) 1.0))

これがZ3の主な目標ではないことは認識していますが、すでに簡略化/解決できる機能があることはわかっていました...ヘルプテキストから判断すると、目標の状態と戦術を設計する方法があるという印象を受けました。それらに到達しましたが、Z3のコマンドに基づいてそれを行う方法についての情報を実際に見つけることができませんでした(help)（何かが足りない場合を除いて...）。

私は実際には複雑なことをするつもりはありません-ターゲットセットにないシンボルの単純な置換/削除...これを行うためにツールを誘導する方法があるのだろうか？

4

1 に答える 1

1

Z3 4.0 は戦術をサポートしています。これらを使用して、式を前処理し、いくつかの変換を適用できます。チュートリアルhttp://rise4fun.com/z3/tutorial/guideには、この新機能に関する詳細情報が含まれています。このコマンド(help-tactic)は、Z3 で利用可能なすべての戦術を表示します。

そうは言っても、既存の戦術はどれもあなたが望んでいることを正確に行うものではありません. 最も近いのは量指定子の除去戦術/コマンドだと思います。あなたの例では、量指定子の削除手順を使用してlocal、 、local_1およびを削除できますmidsep。もちろん、この手順は非常にコストがかかる可能性があり、変数を置き換えるだけではありません。ここに例があります。elim-quantifierstactic の代わりにcommand を使用していqeます。さらに、ご覧のとおり、結果は必ずしも「簡略化された」形式であるとは限りません。量指定子の削除手順によって提供される唯一の保証は、それが成功した場合、結果の式が入力式と同等であることです。Z3 を使用して、 によって生成された結果elim-quantifiersが実際に式 と等しいことを証明できます(= foo_ret (+ (/ x y) 1.0)))。

http://rise4fun.com/Z3/jzZF

(declare-const x Real)
(declare-const y Real)
(declare-const foo_ret Real)

(set-option :pp-max-depth 100)

(elim-quantifiers 
  (exists ((local Real) (midstep Real) (local_1 Real))
    (and (= local (/ x y))
         (= midstep local)
         (= local_1 (+ midstep 1.0))
         (= foo_ret local_1))))
于 2012-06-19T18:59:29.943 に答える