1

假设一组公理，有没有办法简化 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”策略，但它似乎只适用于布尔表达式。是否有其他方法可以简化非布尔表达式，或者以某种方式告诉数组重写器索引是不同的？

谢谢。

4

1 回答 1

1

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

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