अपने हैकिंग ट्रिक्स साझा करें, HackTricks के लिए PRs सबमिट करके HackTricks और HackTricks Cloud github repos में।
बहुत ही बुनियादी रूप से, यह टूल हमें उन मानों को खोजने में मदद करेगा जो कुछ स्थितियों को पूरा करने की आवश्यकता है और उन्हें हाथ से गणना बहुत परेशानीजनक होगा। इसलिए, आप Z3 को इंडिकेट कर सकते हैं कि मानों को कौन सी स्थितियों को पूरा करने की आवश्यकता है और यह कुछ मान (यदि संभव है) खोजेगा।
#pip3 install z3-solverfrom z3 import*s =Solver()#The solver will be given the conditionsx =Bool("x")#Declare the symbos x, y and zy =Bool("y")z =Bool("z")# (x or y or !z) and ys.add(And(Or(x,y,Not(z)),y))s.check()#If response is "sat" then the model is satifable, if "unsat" something is wrongprint(s.model())#Print valid values to satisfy the model
पूर्णांक/सरल/वास्तविक
from z3 import*x =Int('x')y =Int('y')#Simplify a "complex" ecuationprint(simplify(And(x +1>=3, x**2+ x**2+ y**2+2>=5)))#And(x >= 2, 2*x**2 + y**2 >= 3)#Note that Z3 is capable to treat irrational numbers (An irrational algebraic number is a root of a polynomial with integer coefficients. Internally, Z3 represents all these numbers precisely.)
#so you can get the decimals you need from the solutionr1 =Real('r1')r2 =Real('r2')#Solve the ecuationprint(solve(r1**2+ r2**2==3, r1**3==2))#Solve the ecuation with 30 decimalsset_option(precision=30)print(solve(r1**2+ r2**2==3, r1**3==2))
मॉडल प्रिंट करना
from z3 import*x, y, z =Reals('x y z')s =Solver()s.add(x >1, y >1, x + y >3, z - x <10)s.check()m = s.model()print ("x = %s"% m[x])for d in m.decls():print("%s = %s"% (d.name(), m[d]))
मशीन अंकगणित
आधुनिक सीपीयू और मुख्य प्रवाहित प्रोग्रामिंग भाषाएं निर्धारित-आकार बिट-वेक्टर पर अंकगणित का उपयोग करती हैं। मशीन अंकगणित Z3Py में बिट-वेक्टर के रूप में उपलब्ध है।
from z3 import*x =BitVec('x', 16)#Bit vector variable "x" of length 16 bity =BitVec('y', 16)e =BitVecVal(10, 16)#Bit vector with value 10 of length 16bitsa =BitVecVal(-1, 16)b =BitVecVal(65535, 16)print(simplify(a == b))#This is True!a =BitVecVal(-1, 32)b =BitVecVal(65535, 32)print(simplify(a == b))#This is False
साइन किए गए/असाइन किए गए संख्याएं
Z3 विशेष साइन रूपों के अंकगणितीय कार्यों प्रदान करता है जहाँ यह मायने रखता है कि बिट-वेक्टर को साइन या असाइन के रूप में कैसे देखा जाए। Z3Py में, ऑपरेटर <, <=, >, >=, /, % और >> साइन रूपों के संस्करणों को दर्शाते हैं। संबंधित असाइन ऑपरेटर हैं ULT, ULE, UGT, UGE, UDiv, URem और LShR।
from z3 import*# Create to bit-vectors of size 32x, y =BitVecs('x y', 32)solve(x + y ==2, x >0, y >0)# Bit-wise operators# & bit-wise and# | bit-wise or# ~ bit-wise notsolve(x & y ==~y)solve(x <0)# using unsigned version of <solve(ULT(x, 0))
कार्य
व्याख्यात कार्य जैसे अंकगणित जहाँ कार्य + का निश्चित मानक व्याख्या होता है (यह दो नंबर जोड़ता है)। अव्याख्यात कार्य और स्थिर संदर्भ हैं; वे किसी भी व्याख्या को अनुमति देते हैं जो कार्य या स्थिर संदर्भ के अधीन संबंधित है।
उदाहरण: x पर दो बार f लागू करने पर पुनः x परिणाम होता है, लेकिन x पर एक बार f लागू करने पर x से भिन्न है।
from z3 import*x =Int('x')y =Int('y')f =Function('f', IntSort(), IntSort())s =Solver()s.add(f(f(x)) == x, f(x) == y, x != y)s.check()m = s.model()print("f(f(x)) =", m.evaluate(f(f(x))))print("f(x) =", m.evaluate(f(x)))print(m.evaluate(f(2)))s.add(f(x) ==4)#Find the value that generates 4 as responses.check()print(m.model())
उदाहरण
सुडोकू सॉल्वर
# 9x9 matrix of integer variablesX = [ [ Int("x_%s_%s"% (i+1, j+1))for j inrange(9) ]for i inrange(9) ]# each cell contains a value in {1, ..., 9}cells_c = [ And(1<= X[i][j], X[i][j] <=9)for i inrange(9)for j inrange(9) ]# each row contains a digit at most oncerows_c = [ Distinct(X[i])for i inrange(9) ]# each column contains a digit at most oncecols_c = [ Distinct([ X[i][j] for i inrange(9) ])for j inrange(9) ]# each 3x3 square contains a digit at most oncesq_c = [ Distinct([ X[3*i0 + i][3*j0 + j]for i inrange(3) for j inrange(3) ])for i0 inrange(3)for j0 inrange(3) ]sudoku_c = cells_c + rows_c + cols_c + sq_c# sudoku instance, we use '0' for empty cellsinstance = ((0,0,0,0,9,4,0,3,0),(0,0,0,5,1,0,0,0,7),(0,8,9,0,0,0,0,4,0),(0,0,0,0,0,0,2,0,8),(0,6,0,2,0,1,0,5,0),(1,0,2,0,0,0,0,0,0),(0,7,0,0,0,0,5,2,0),(9,0,0,0,6,5,0,0,0),(0,4,0,9,7,0,0,0,0))instance_c = [ If(instance[i][j] ==0,True,X[i][j] == instance[i][j])for i inrange(9)for j inrange(9) ]s =Solver()s.add(sudoku_c + instance_c)if s.check()== sat:m = s.model()r = [ [ m.evaluate(X[i][j])for j inrange(9) ]for i inrange(9) ]print_matrix(r)else:print"failed to solve"