z3py

2熱度

1回答

我使用下面的z3py消除了量詞消除的以下示例。不過，我想用SMTLIB語法重寫它（代碼在python代碼下面）。不知何故，我沒有得到像我從python獲得的公式一樣的輸出。我想知道有沒有人能指出我的問題。 from z3 import * a, five = Ints('a five') cmp = Bool('cmp') j = Goal() j.add(Exists([five, cmp],

1熱度

1回答

如何在Z3py公式中正確使用ZeroExt（n，a）？

我想找出隱藏在二進制文件中的keygen算法的密碼。所以，我提取從組件式和翻譯（正確地，希望）在一個小Python腳本來解決它： #!/usr/bin/env python from z3 import * # Password initialization pwd = BitVecs('pwd0 pwd1 pwd2 pwd3 pwd4 pwd5', 8) # Internal sta

-2熱度

1回答

減少多modles

時它得到多個模型，但它需要time.So小時請給我建議，以減少時間讓所有models.how得到了滿足公式所有可能的解決方案在更短的時間？ z3python中是否有任何函數用於獲取所有可能的解決方案。 from z3 import * x0,x1,x2,x3,x4,x5=BitVecs('x0 x1 x2 x3 x4 x5',32) y0,y1,y2,y3,y4,y5=BitVecs('y0

1熱度

1回答

z3py：如何在z3py中設置使用的邏輯？

使用下面的代碼： import z3 solver = z3.Solver(ctx=z3.Context()) #solver = z3.Solver() Direction = z3.Datatype('Direction') Direction.declare('up') Direction.declare('down') Direction = Direction.creat

0熱度

1回答

如何在z3py中使用Z3-LIB中的（_ map op）

Z3-LIB支持擴展陣列理論的運算符，如（_ map op）。但是，我們如何在Z3py中使用這個運算符？

5熱度

1回答

Z3py支持「字符串」和「序列」

在Z3中，它支持字符串和序列。但Z3py是否也支持它們，或者我們必須使用Python中的字符串或列表？從最新版本看來，新版本確實支持String和Sequence的理論，但我不知道如何使用它。有人會給我一個關於序列的例子嗎？

0熱度

1回答

在Z3Py中發出實際的號碼

在Z3Py中給出像Real('x')這樣的實際號碼，我該如何獲得其樓層或天花板？等同地，我該如何整理它？我發現to_int是SMT規範中的一件事，但我不知道如何從Python中調用它。

0熱度

1回答

Z3求解差異邏輯的Python API

我一直在試圖做這樣的事情在python： (set-option :smt.arith.solver 1) (declare-const x Int) (declare-const y Int) (assert (>= 10 x)) (assert (>= x (+ y 7))) (maximize (+ x y)) (check-sat) 我已經能夠做到這一點的解算器（solve

6熱度

1回答

Z3Py中的K-out-of約束

我正在使用Z3 theorem prover（Z3Py）的Python綁定。我有N個布爾變量，x1，..，xN。我想表達這樣一個約束，即它們中的N個應該是正確的。我該怎麼做，在Z3Py？有沒有內置的支持？我查看了在線文檔，但Z3Py docs沒有提及任何API。我知道我可以分別表示至少有一個是真的（assert Or（x1，..，xN）），並且至多有一個是真的（assert Not（And）（x

0熱度

2回答

在Z3中聲明大小未知的矩陣

我知道我可以在Z3中聲明一個z3.Real的矩陣，通過單獨聲明它的元素（可能通過列表理解）。有沒有辦法來表示一個未知大小的矩陣？例如，考慮下面的例子：在圖像濾波，給定的size [X,Y]的圖像I和濾波器核的size [M,N]K，圖像I和濾波器內核K是I*K之間的卷積。我想Z3來證明（或反駁）存在任何大小的過濾器F1和F2，例如I*K == I*F1*F2。問題本身是完全組成的，可能沒有意