如何在 Z3 中获得表达式的解决方案

Question

我想用 Z3 做一些理论上很容易的事情，但我不知道该怎么做。

所以假设我在 C:

中有这段代码

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

我想知道d的可能解法，例如97。我试着这样表达Z3中的问题：

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

但是通过这种方式我得到了 c 而不是变量 d 的解。

我应该怎么做？

非常感谢！

Answer 1

如果你想得到 d 的一个解，你可以使用：

(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)

How to get solutions for an expression in Z3