假设一组公理简化 Z3 中的非布尔表达式

Question

有没有办法在 Z3 中假设一组公理来简化非布尔表达式？

例如，我想断言“a==b”，然后简化表达式 "If(a == b, 1, 2)" 得到 "1"。

特别是，我对使用数组理论很感兴趣：

I = BitVecSort(32)
A = Array('A', I, I)
a = BitVec('a',32)
b = BitVec('b',32)
c = BitVec('c',32)
...
A2 = Store(A, a, 1) 
A3 = Store(A2, b, 2) 
A4 = Store(A3, c, 3)

simplify_assuming(A4[a], Distinct(a, b, c))

这应该返回“1”，因为根据数组理论规则，假设所有索引都是不同的，Select 表达式可以简化为“1”。

我尝试使用“ctx-solver-simplify”策略，但它似乎只适用于布尔表达式。有没有其他方法可以简化非布尔表达式，或者以某种方式告诉数组重写器索引是不同的？

谢谢。

Answer 1

正如 Nikolaj 在上面的评论中所描述的，ctx-solver-simplify 不会在非布尔表达式下运行。另一种选择是使用策略solve-eqs，它将使用断言的等式来重写公式的其余部分。例如，给定等式a == b，Z3 将用a 替换每次出现的b（反之亦然）。之后，if(a == b, 1, 2) 将被重写为1。

但是，solve-eqs 不会使用不等式，例如 Distinct(a, b, c)。另一种选择是使用策略propagate-values。它将每次出现的断言P 替换为true。同样，如果我们有一个断言not P，它将用false 替换所有其他出现的P。 这种策略本质上是执行单元布尔传播。此外，它旨在快速，并且不会应用任何形式的理论推理。例如，如果我们有Distinct(a, b, c)，它不会用false 替换a == b。因此，对于您的目的，这种方法可能太脆弱了。 这是一个使用它的脚本。也可在线获取here。在此脚本中，我使用新谓词 P 包装表达式 A4[a]，因为 Z3 目标是一组布尔公式。 我使用blast_distinct 将Distinct 转换为不等式序列，并使用expand_select_store 将store(A, i, v)[j] 形式的术语扩展为if-then-else 形式的if(i == j, v, A[j])。请注意，结果包含P(1)，表示P(A4[a]) 已简化为1。

I = BitVecSort(32)
A = Array('A', I, I)
a = BitVec('a',32)
b = BitVec('b',32)
c = BitVec('c',32)
A2 = Store(A, a, 1) 
A3 = Store(A2, b, 2) 
A4 = Store(A3, c, 3)

P = Function('P', I, BoolSort())
G = Goal()
G.add(P(A4[a]))
G.add(Distinct(c, b, a))

T = Then(With("simplify", blast_distinct=True, expand_select_store=True), "propagate-values")
print(T(G))