假設一組公理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中的非布爾表達式簡化

回答

相關問題