z3變量類型切換

在玩Z3時，我發現變量在變化類型時會出現問題。我已經能夠得到Int與Real發揮很好。我也得到Int轉換爲BitVec，然後回來。但是，似乎一旦我達到了在Int和BitVec之間轉換的閾值，z3解算器就會退出軌道並且不會返回。z3變量類型切換

我的求解器狀態的一個例子是這樣的：

[271733878 == a, 
562383102 == b, 
4023233417 == c, 
1732584193 == d, 
e == 
BV2Int(int2bv(d)^
    int2bv(BV2Int(int2bv(b) & 
        int2bv(BV2Int(int2bv(c)^
           int2bv(a)))))), 
f == e, 
305419896 == g]

，實際工作正常。但是，如果我再做一個int2bv轉換Z3永遠不會返回，我必須殺死python。同樣，這些變量的問題實際上是非常不穩定的，只要它們可能採取什麼類型。我曾經考慮過只使用BitVec，但如果我想一起添加BitVec和Real，會導致問題。

我是不是想用Z3來做一些不適合的東西？有沒有什麼方法可以使用Z3來解決這類問題？

來源

2016-03-15 Owl Owl

對於int2bv和bv2int轉換沒有特別的調整，所以你經常留下的回退機制會發生位衝突，然後進行位向量和算術推理的精細組合。我建議您嘗試延遲從位向量到整數的轉換，直到您在前端的最後一招。在這個例子中，沒有特別的理由繼續將中間位向量轉換爲整數。 Z3不檢測這種冗餘。它還必須考慮到整數到位矢量轉換可能是有損的，因爲它是以位寬爲模的。

來源

2016-03-15 13:09:27

感謝您的反饋意見。如你所述，我肯定會延遲轉換。不過，我也希望在某些時候能夠更多地投入到這些轉換中，因爲我認爲將來可能需要更有效的轉換方法（或者甚至是兩者之間的隱式轉換）。 –

出於興趣，您是否有一個實際需要兩種理論之間轉換的應用程序，或者您是否爲了方便而在它們之間進行轉換，並且所有這些都可以完全在其中一種理論中完成？ –

z3變量類型切換

回答

相關問題