बहुत बुनियादी रूप से, यह उपकरण हमें उन चर के लिए मान खोजने में मदद करेगा जिन्हें कुछ शर्तों को संतुष्ट करना आवश्यक है और उन्हें हाथ से गणना करना बहुत परेशान करने वाला होगा। इसलिए, आप 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
Ints/Simplify/Reals
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]))
मशीन अंकगणित
आधुनिक CPU और मुख्यधारा की प्रोग्रामिंग भाषाएँ फिक्स्ड-साइज़ बिट-वेक्टर पर अंकगणित का उपयोग करती हैं। मशीन अंकगणित 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
Signed/Unsigned Numbers
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))
Functions
व्याख्यायित कार्य जैसे अंकगणित जहां कार्य + का स्थिर मानक व्याख्या है (यह दो संख्याओं को जोड़ता है)। अव्याख्यायित कार्य और स्थिरांक अधिकतम लचीले होते हैं; वे किसी भी व्याख्या की अनुमति देते हैं जो कार्य या स्थिरांक पर प्रतिबंधों के साथ संगत हो।
उदाहरण: 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"
