2016-03-15 91 views
1

在玩Z3時,我發現變量在變化類型時會出現問題。我已經能夠得到IntReal發揮很好。我也得到Int轉換爲BitVec,然後回來。但是,似乎一旦我達到了在IntBitVec之間轉換的閾值,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來解決這類問題?

回答

1

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

+0

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

+0

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