Z3 数组：为什么 Select() 不返回 Store() 保存的值？答案

【问题标题】：Z3 array: why Select() does not return value saved by Store()?Z3 数组：为什么 Select() 不返回 Store() 保存的值？
【发布时间】：2012-11-21 09:30:49
【问题描述】：

我有简单的 Z3 python 代码，如下所示。我希望“打印”行将返回存储在其上方行中的“y”。结果，我得到了“A[x]”。

I = IntSort()
A = Array('A', I, I)
x = Int('x')
y = Int('y')
Store(A, x, y)
print Select(A,x)

为什么Select()不返回Store()存储的值？

谢谢。

【问题讨论】：

标签： z3 smt

【解决方案1】：

有两点需要注意：

首先：当你写

Store(A, x, y)

您创建一个带有三个参数 A、x 和 y 的术语。 A 没有副作用。您可以通过编写来为该术语创建一个名称

B = Store(A,x,y)

第二：除非您愿意，否则 Z3 不会简化术语。 python API 公开了一个名为simplified 的简化函数。您可以通过调用简化器来获得缩减项。例子是：

I = IntSort()
A = Array('A', I, I)
x = Int('x')
y = Int('y')
B = Store(A, x, y)
print Select(B,x)
print simplify (Select(B,x))

【讨论】：

Nikolaj，这太棒了，谢谢！不过，我对 Z3 的 simple() 真的很好奇。它似乎可以做一些“优化”，但效果如何？与编译器所做的优化有什么比较？关于简化如何在内部工作的任何文档/论文？谢谢！
simplify 只是一个自下而上的重写器。我们没有论文描述它，因为它基于众所周知的技术。我还假设它比 gcc 等编译器应用的中间代码优化要简单得多。您可以在 Z3 代码库 (z3.codeplex.com) 的目录 src/ast/rewriter 中找到它的实现。数组简化规则在文件z3.codeplex.com/SourceControl/changeset/view/2a286541e002#src/…中实现