0
私は理論上Z3で非常に簡単なことをしようとしていますが、その方法はわかりません。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のための解決策を得ません。
私はそれをどのようにすればよいですか?
ありがとうございました!