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

【问题标题】：How to get solutions for an expression in Z3如何在 Z3 中获得表达式的解决方案
【发布时间】：2016-08-03 00:59:10
【问题描述】：

我正在尝试用 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 的解决方案。

我该怎么做？

非常感谢！

【问题讨论】：

标签： z3 smt

【解决方案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 的所有解，你可以反复否定模型并将它们添加为约束。请在此处查看 Taylor 的回复：Z3: finding all satisfying models

编辑：添加，程序的稍微更直接的翻译将使用：

(>= 65 c)

而不是

(> 64 c)

【讨论】：