z3py

3熱度

2回答

我正在使用Z3 Python接口爲我的實驗創建公式。然後我將這個公式發送給Z3解算器。如果我是正確的Z3使用它自己的求解器！如何在Z3py中使用不同的SAT/SMT解算器？我在CBMC（C有界模型檢查器）中使用它的方式：運行程序並吐出中間DIMAC表示（在文件中），然後將該文件用作其他SAT求解器的輸入。我可以在Z3做類似的事情嗎？謝謝。

0熱度

1回答

如何獲取z3中給定的可能整數集合中的整數列表？

最小示例如下：給定一組可能的整數[1, 2, 3]使用z3py創建大小爲5的任意列表。允許重複。預期的結果是一樣的東西[1, 1, 1, 1, 1]或[3, 1, 2, 2, 3]等如何解決這個問題，以及如何實現「選擇」？最後，我想找到所有解決方案，可以通過添加其他約束來解決，如link中所述。任何幫助將非常感激。

0熱度

1回答

如何在z3中實現指針的解引用

試圖用python中的z3分析一些C程序，並用指針引起麻煩。我與條款的工作，如： float * buffer = (float*)malloc(5*sizeof(float)) 我解釋緩衝區作爲BitVec(32)值所以*buffer應該Real()。就應該沒什麼問題，但我應該寫什麼斷言的術語如 *(buffer+3) or *(buffer+i) 應該如何斷言寫，如果我索引出像 *

2熱度

2回答

z3py將數據類型/枚舉與字符串進行比較

在此示例中（在此處找到：z3py），我可以將c與例如Color.green。 Color = Datatype('Color') Color.declare('red') Color.declare('green') Color.declare('blue') Color = Color.create() # Let c be a constant of sort Color c =

-1熱度

2回答

數學方程

我有這樣的等式：S = val.X^3 - val.X^2 + val.X -Val 知道，所有的變量是Int64類型，和S和val是已知的值，什麼是解決這個問題的最好辦法，我用numpy的和Z3，但不能得到正確的答案，任何鉛將是有益的

2熱度

1回答

Z3PY方程，大小限制

我的工作Z3PY我想知道如何限制一個公式的計算規模 v0 = Int('v0') const = 0x12345678 I wrote this : s.add((const*(v0 + const*(func(v0*const) - v0)) - v0) == somevalueof64bits) 我的問題是，「（常量*（V0計算+ const *（func（v0 *

3熱度

2回答

Z3 Prover返回錯誤的解決方案

我試圖用Python中的Z3 Thoerem Prover解決方程。但我得到的解決方案是錯誤的。 from z3 import * solv = Solver() x = Int("x") y = Int("y") z = Int("z") s = Solver() s.add(x/(y+z)+y/(x+z)+z/(x+y)==10, x>0, y>0, z>0) s.add()

0熱度

1回答

z3py：存在量詞

這個腳本 from z3 import * solver = z3.Solver() x = Int('x') def f(y): return y+y solver.add(x >= 0, x < 10, Exists(x, f(x) == 4)) print solver.check() print solver.model() 的用法給我 sat [x = 0]

2熱度

1回答

Z3和浮點係數

我是用一個小的多目標整數規劃問題，玩的解釋：在Z3（使用Python綁定），我們可以很優雅地說明這一點： from z3 import * x1,x2 = Ints('x1 x2') z1,z2 = Reals('z1 z2') opt = Optimize() opt.set(priority='pareto') opt.add(x1 >= 0, x2 >=0, x1 <= 2,

1熱度

1回答

無法爲z3py提取Z3 EnumSort的值

我正在嘗試將問題編碼到Z3中，並且我希望爲「三態」布爾值（即，帶有true,false和unknown的布爾值）建模。這裏是我怎麼也仿照它： #!/usr/bin/env python import z3 from collections import OrderedDict TristateValues = ["True", "False", "Unknown"] Tristate