使用 Z3 求解器获取表达式答案

【问题标题】：Get expression using Z3 solver使用 Z3 求解器获取表达式
【发布时间】：2016-01-01 01:01:10
【问题描述】：

我是 Z3 求解器和 SMTLib2 的新手。我想获取约束中每个变量的表达式。假设，我有这个程序。

(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(assert (= x (+ y 1)))
(assert (= z (+ x 10)))
(check-sat)
(get-value (z))

使用get-value，我可以获得满足所有约束的z 的值。但是，我怎样才能得到z 的表达式。像z=y+11 这样的东西。

我发现使用simplify，我可以简化约束，但无论如何都可以获得约束中每个变量的表达式。

【问题讨论】：

【解决方案1】：

Z3 首先是一个 SMT 求解器；它解决了存在问题，即它只会显示存在一个解决方案，它不会计算所有解决方案的封闭形式。

也就是说，有一些方法可以至少获得该形式的某些结果，例如通过上述的简化，或者如果逻辑允许，也可以通过量词消除（例如参见 Equivalent Quantifier Free Formulas 或 @ 987654322@).

如果需要多个模型但可能不是所有模型，请查看Z3: finding all satisfying models 并搜索多个其他类似标题的问题。

【讨论】：