使用 Z3 获取符号值答案

【问题标题】：Obtaining symbolic values using Z3使用 Z3 获取符号值
【发布时间】：2014-04-16 09:36:59
【问题描述】：

请考虑以下陈述。

y := 10

z := x + y

在这两个语句执行后，“z”的值为“x + 10”，其中“x”代表一个符号值；这样的符号值在程序验证中很重要——例如，使用 Dijkstra'a 最弱的前置条件方法计算路径特征。

现在，考虑 Z3 的以下代码。

(declare-const x Int)
(declare-const y Int)
(declare-const z Int)

(assert (= y 10))
(assert (= z (+ x y)))

(check-sat)
(get-value (z))

它产生以下输出，因为它考虑了“y”具有 10 而“x”具有值 0 的解释。

sat

((z 10))

有什么方法可以让 Z3 产生输出“x + 10”吗？即，我有兴趣根据尚未使用任何特定值实例化的变量来获取符号值。

【问题讨论】：

“就尚未使用任何特定值实例化的变量而言”：您是指不受约束的变量还是恒定的变量？如果您只想处理常量，可以通过简单的替换来完成。
由于计算最弱的前置条件基本上涉及替换——我认为替换应该完成这项工作。但是就像 Juan Ospina 说的，Z3-SMT-LIB 中是否有对应于他在 Z3Py 中的代码的替代方案？
我不确定。但是，我确实认为 C++ API 比 Z3-SMT-LIB 具有更灵活的选项。

标签： z3

【解决方案1】：

我不是专家，但我认为使用 Z3-SMT-LIB 是不可能的。但是使用 Z3Py 是可能的。

x = Int('x')
y = 10
z = x + y
print z

输出是

x + 10

【讨论】：

这只是在做替换。没有调用实际求解器。如果我给 z3py，下面的代码： {x = Int('x') y = Int('y') z = Int('z') proof(And(z == x + y, y == 10 ))}，我得到输出 {counterexample [y = 10, z = 1, x = -10]}，这不是 LKB 正在寻找的。证明调用实际上调用了 SMT 求解器。
嗨 Tushar，你是对的。关键是当求解器被调用时，输出是一个数值，而不是一个符号表达式。你同意吗？
是的，我同意。我知道 C++ API 中有一个 eval 函数，其中一个 z3 表达式可以通过查看 z3 模型来评估为另一个 z3 表达式。如果 z3 模型不完整（即它没有对不受约束的变量进行估值），那么它应该能够给我一个 Z3 表达式，它是一个符号表达式，而不是一个数值。但是，上次我检查时，它报告了一个错误，它希望客户端将模型完成设置为 true，在这种情况下 z3 eval 将给出一个数值。
换句话说，可能有一些聪明的（也许是hackish）可以用Z3求解器获得符号表达式的部分模型来做。最后我检查了 Z3 C++ API 不支持。