これは非常にいいですが、現時点ではZ3は他の言語/ APIの関数定義を使用できません。
;; define foo
(define-fun foo ((x Int)) Int
(ite (= x 1) 42
(ite (= x 2) 43
;; ...
78)))
;; use foo
(assert (exists ((op Int)) (= (foo op) 43)))
(apply skip)
は
(goal
(exists ((op Int)) (= (ite (= op 1) 42 (ite (= op 2) 43 78)) 43))
:precision precise :depth 0)
)
(と、それを生成します。彼らは簡単にカスケードTHEN-ELSE IF-としてエンコードすることができますので、以下のように、ルックアップ・テーブルの場合には、それは、例えば、しかし簡単にする必要がありますあまりにも、迅速に解決される)
APIを経由してこれを行う最も簡単な方法は、関数宣言の問題を設定し、その後macro-finder
戦術によって認識される普遍数量詞を経由してマクロ定義を提供することである:。
を関数定義をピックアップするマクロファインダー用
;; declare foo
(declare-fun foo ((Int)) Int)
;; define foo
(assert (forall ((x Int)) (= (foo x)
(ite (= x 1) 42
(ite (= x 2) 43
;; ...
78)))))
;; use foo
(assert (exists ((op Int)) (= (foo op) 43)))
(apply macro-finder) ;; replaces foo with it's definition
、数量詞は、フォームに質問に答えるために時間を割いて
(forall ((x ...)) (= (foo x) (... definition ...))
感謝を持っている必要があります。この解決法も私の頭に浮かんだが、あまりにもオーバーヘッドになると思った...とにかく、私はこれのようにしなければならないだろう。 – localized
ねえ、私はこれをJavaバインディングを使って実装し始めて、問題に遭遇しました。私はあなたが指定した例のようにマクロを使用したいと思いますが、mkFuncDeclはAPIを使用して戻り値に引数をマップする本体で関数(マクロ)を定義する方法を見つけることができません。関数を宣言してその本体を定義することはできません。 – localized
良い点!私はそれを行う最も簡単な方法は、マクロファインダーの戦術を適用することだと思います。これを例に追加します。 –