14

テキスト形式でZ3を使用すると、define-fun後で再利用するための関数を定義するために使用できます。例えば：

(define-fun mydiv ((x Real) (y Real)) Real
  (if (not (= y 0.0))
      (/ x y)
      0.0))

define-fun関数の本体をどこでも繰り返すのではなく、Z3 API（私はF＃を使用）で作成する方法を考えています。重複を避け、数式を簡単にデバッグするために使用したいと思います。で試してみましContext.MkFuncDeclたが、解釈できない関数しか生成されないようです。

4

1 に答える 1

15

define-funコマンドはマクロを作成するだけです。SMT 2.0 標準では、再帰的な定義が許可されていないことに注意してください。my-divZ3 は、解析時にが出現するたびに展開します。このコマンドdefine-funは、入力ファイルを単純にして読みやすくするために使用できますが、内部的には Z3 にはあまり役立ちません。

現在の API では、マクロの作成はサポートされていません。マクロのインスタンスを作成する C または F# 関数を定義できるため、これは実際の制限ではありません。ただし、Z3 API を使用して作成された数式を表示 (および手動で検査) したいようです。この場合、マクロは役に立ちません。

代替手段の 1 つは、量指定子を使用することです。解釈されない関数my-divを宣言して、全称量化された式をアサートできます。

(declare-fun mydiv (Real Real) Real)
(assert (forall ((x Real) (y Real))
                (= (mydiv x y)
                   (if (not (= y 0.0))
                       (/ x y)
                       0.0))))

これで、解釈されない関数を使用して数式を作成できますmydiv。

このような定量化された数式は、Z3 で処理できます。実際、この種の量指定子を処理するには 2 つのオプションがあります。

  1. マクロ ファインダを使用します。この前処理ステップでは、本質的にマクロを定義している量指定子を識別して展開します。ただし、展開は前処理時にのみ発生し、解析時 (つまり、式の構築時) には発生しません。モデルファインダーを有効にするには、使用する必要がありますMACRO_FINDER=true
  2. もう 1 つのオプションは、使用することですMBQI(モデルベースの量指定子のインスタンス化)。このモジュールは、この種の量指定子も処理できます。ただし、量指定子は必要に応じて拡張されます。

もちろん、解決にかかる時間は、使用するアプローチによって大きく異なります。たとえば、式が の「意味」とは無関係に満足できない場合は、mydivおそらくアプローチ 2 の方が適しています。

于 2011-10-12T18:53:47.323 に答える