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

假设一组公理Z3中有非简化非布尔表达式的方法吗？例如，我想断言“a == b”，然后简化表达式 “If（a == b，1，2）”以获得“1”。假设一组公理Z3中的非布尔表达式简化

特别是，我在数组理论工作很感兴趣：

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”，因为选择表达式可以简化为“1”，假设所有指标根据阵列理论规则，它是独特的。

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

谢谢。

来源

2013-03-23 user2203454

“我试图用‘CTX-解算器，简化’的战术，但它似乎只针对布尔表达式的工作。” 这是正确的。 ctx-solver-simplify例程不会在非布尔方式下行走。这个简化器使用的算法可以推广到非布尔型条件，，但我没有期待这个应用程序。它利用了这样一个假设：它在一些地方简化了布尔表达式。 – 2013-03-24 00:23:39

正如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。它用true代替断言P的每一次出现。同样，如果我们有一个断言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(i == j, v, A[j])的if-then-else。请注意，结果包含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-24 16:59:38

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

回答

相关问题