2016-05-22 7 views
1

これは私がやろうとしていることです。Z3の関数をJava実装で定義していますか?

のは、私はこれに似た表現で(結合し、そのJava)のZ3を使用してopの値を見つけたいとしましょう:

((exists (op Int)) (= (foo op) 2)

だから私はopに機能fooを呼びたいです変数を調べ、関数が返すopの値を調べる。2. Javaで関数fooを定義し、Z3がこれらの関数定義にアクセスする方法があると考えた。私はこのようにしたいと思います。なぜなら、関数は実際にJavaで実装しやすいHashMapのルックアップだからです。

私は一般的にSMTソルバーの初心者なので、できないことをやりたいと思う可能性があります。だから私はその話題に関するすべての提案には門を開いている。

お時間をいただきありがとうございます。

答えて

1

これは非常にいいですが、現時点では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 ...)) 
+0

感謝を持っている必要があります。この解決法も私の頭に浮かんだが、あまりにもオーバーヘッドになると思った...とにかく、私はこれのようにしなければならないだろう。 – localized

+0

ねえ、私はこれをJavaバインディングを使って実装し始めて、問題に遭遇しました。私はあなたが指定した例のようにマクロを使用したいと思いますが、mkFuncDeclはAPIを使用して戻り値に引数をマップする本体で関数(マクロ)を定義する方法を見つけることができません。関数を宣言してその本体を定義することはできません。 – localized

+0

良い点!私はそれを行う最も簡単な方法は、マクロファインダーの戦術を適用することだと思います。これを例に追加します。 –

関連する問題