Z3で式の解を得る方法

Question

私は理論上Z3で非常に簡単なことをしようとしていますが、その方法はわかりません。

だから私はCでこのコードを持っていると想像：

int c; 
if (c>=65 && C<91) 
    int d = c + 32; 

私は例97のために、私はこのようにZ3で問題を表現しようとすると、Dのための可能な解決策を知っていると思います：

(declare-const c Int) 
(assert (> c 64)) 
(assert (< c 91)) 
(define-fun d() Int 
(+ 32 c) 
) 
(assert (> d 0)) 
(check-sat) 
(get-model) 

しかし、このようにして、私は変数dのための解決策を得ません。

私はそれをどのようにすればよいですか？

ありがとうございました！

Answer 1

あなたがDのための1つの解決策を取得したい場合は、使用することができます。

(declare-const c Int) 
(declare-const d Int) 

(assert (> c 64)) 
(assert (< c 91)) 

(assert (= d (+ c 32))) 
(check-sat) 
(get-model) 

あなたがDのためのすべてのソリューションを検索したい場合は、あなたが何度モデルを否定し、制約として追加することができます。ここではテイラーの応答を参照してください：Z3: finding all satisfying models

編集：使用するプログラムの少しより直接的な翻訳、上の追加：

(>= 65 c) 

ではなく

(> 64 c)