z3py

1熱度

2回答

我想使用z3py來簡化表達式，但是我無法找到任何有關不同策略的文檔。我找到的最好的資源是一個stack overflow question，它按名稱列出了所有的策略。是否有人能夠將我鏈接到有關可用策略的詳細文檔？在線python教程是不夠的。或者可以有人推薦一個更好的方法來實現這一點。的問題的一個例子是這樣的表達式： x < 5, x < 4, x < 3, x = 1謹以此向下簡化到x

6熱度

2回答

使用Z3檢查溢出問題

我是Z3的新手，我正在檢查在線python教程。然後我想我可以檢查BitVecs中的溢出行爲。我寫這個代碼： x = BitVec('x', 3) y = Int('y') solve(BV2Int(x) == y, Not(BV2Int(x + 1) == (y + 1))) 和我期待[Y = 7，X = 7]（即，當值相等但繼任者不是因爲X + 1將是0和y + 1將是8）但是

5熱度

2回答

如何使用BitVector建模帶符號整數？

假設a是值爲254的8位整數。如果a是一個有符號的整數，那麼它實際上被認爲是-2。相反，如果a未簽名，它仍然是254。我想用BitVector理論與Z3來模擬這個有符號/無符號整數問題，但似乎BitVector不允許這樣做。這是真的？那麼有關如何在Z3py中建模的想法？非常感謝。

1熱度

2回答

在決策變量時，Z3可以調用python函數嗎？

我想解決一個問題，例如我有一個4點，每兩點之間有一個成本。現在我想要找到總成本小於邊界的節點序列。我寫了一個代碼，但它似乎不工作。主要的問題是我定義了一個python函數並試圖在約束中調用它。這裏是我的代碼：我有一個功能def getVal(n1,n2):其中n1, n2是Int Sort。 Nodes = [ Int("n_%s" % (i)) for i in range(totalNode

2熱度

1回答

可以從Z3獲得最終的CNF公式嗎？

這是我的簡單編碼。我希望得到最終的布爾CNF，它提供了所有這些約束條件。 Z3求解器中有沒有選項可以獲得最終的布爾CNF？ x = Int('x') y = Int('y') c1 = And(x >= 1, x <= 10) c2 = And(y >= 1, y <= 10) c3 = Distinct(x,y) s = Solver() s.add(c1 , c2 , c3)

0熱度

2回答

使用Z3py可以計算Kauffman括號嗎？

我正在嘗試使用Z3py來計算三葉草結的Kauffman支架。到現在爲止，我有以下代碼： a, b, c, d, e, f, A, B = Ints('a b c d e f A B') delta = Function('delta', IntSort(), IntSort(), IntSort()) def X(a,b,c,d): return A*delta(a,d)*delt

1熱度

3回答

如何使用Z3的Python API執行量詞消除

如何使用Z3的Python API執行量詞消除？雖然我檢查了教程和API，但無法做到這一點。我有一個有一個存在量詞的公式，我想Z3給我一個新的公式，這個量詞被消除。我基本上是想要做同樣的事情，因爲這： How to hide variable with Z3 但與Python接口。另外我的公式是線性算術。謝謝！此外：做了量詞消除之後，我會將「無量詞」的公式與另一個「添加」。所以如果我使用策

1熱度

2回答

如何使用Z3Py和想法來自泰勒在電網絡的情況下進行量詞消去

請考慮以下電網該電網的SAT問題是此問題使用Z3Py在線使用以下代碼解決： r01, r02, r12, r13, r23 = Reals('r01 r02 r12 r13 r23') i0, i01, i02, i12, i13, i23, i3 = Reals('i0 i01 i02 i12 i13 i23 i3') u0, u1, u2, u3 = Reals('u0 u1 u2 u

0熱度

1回答

如何使用Z3Py在線計算的RO人口與性胡亞蓉異質性和適度的miximg

爲了解決我們用下面的代碼的問題： R_H, R_L, g_H, g_L, x, R_0 = Reals('R_H R_L g_H g_L x R_0') R_HH = R_H*g_H R_HL = R_L*g_H R_LH = R_H*g_L R_LL = R_L*g_L eq1 = R_HH*x+R_HL*(1-x) eq2 = R_LH*x+R_LL*(1-x) equation

2熱度

1回答

使用推送命令在Z3中增量求解

我正在使用Z3的python api來做某種增量求解。我使用solver.push()命令，在迭代中將約束條件推給解算器，同時檢查每個步驟的不可滿足性。我想知道Z3是否會使用從先前的約束中學習的引理或者使用新添加的約束求解時以前獲得的令人滿意的解決方案。我從來沒有使用solver.pop()命令。我在哪裏可以獲得更多關於以前迭代中所做工作的詳細信息？