Baie basies sal hierdie instrument ons help om waardes vir veranderlikes te vind wat aan sekere voorwaardes moet voldoen, en dit sal baie vervelig wees om dit met die hand te bereken. Daarom kan jy aan Z3 aandui watter voorwaardes die veranderlikes moet bevredig en dit sal enkele waardes vind (indien moontlik).
#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
Inte/Simplifiseer/Reëls
Die Z3 SMT-solver bied 'n verskeidenheid funksies vir die hantering van ints, vereenvoudiging en werk met reële getalle. Hier is 'n oorsig van die basiese metodes wat beskikbaar is:
Inte
Int is die tipe vir ints in Z3.
Jy kan ints skep deur die IntVal-funksie te gebruik, byvoorbeeld IntVal(42) sal 'n int met die waarde 42 skep.
Inte kan ook geskep word deur die Int-funksie te gebruik, byvoorbeeld Int('x') sal 'n int met die naam 'x' skep.
Inte kan gebruik word in wiskundige uitdrukkings, byvoorbeeld x + 2 of y * 3.
Vereenvoudiging
Die simplify-funksie kan gebruik word om wiskundige uitdrukkings te vereenvoudig.
Byvoorbeeld, simplify(x + 0) sal vereenvoudig na x, en simplify(x * 1) sal vereenvoudig na x.
Vereenvoudiging kan help om die uitdrukking te vereenvoudig en die oplossing te vind.
Reële getalle
Real is die tipe vir reële getalle in Z3.
Jy kan reële getalle skep deur die RealVal-funksie te gebruik, byvoorbeeld RealVal(3.14) sal 'n reële getal met die waarde 3.14 skep.
Reële getalle kan ook geskep word deur die Real-funksie te gebruik, byvoorbeeld Real('y') sal 'n reële getal met die naam 'y' skep.
Reële getalle kan gebruik word in wiskundige uitdrukkings, byvoorbeeld y + 2.5 of z * 1.5.
Met hierdie basiese metodes kan jy ints en reële getalle hanteer, vereenvoudig en gebruik in jou SMT-probleme met die Z3-solver.
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))
Druk Model
To print the model generated by Z3, you can use the model method. This method returns a string representation of the model.
Om die model wat deur Z3 gegenereer is af te druk, kan jy die model metode gebruik. Hierdie metode gee 'n teksvoorstelling van die model terug.
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]))
Masjienrekenkunde
Moderne CPU's en algemene programmeertale gebruik rekenkunde oor vasgestelde grootte bit-vektore. Masjienrekenkunde is beskikbaar in Z3Py as Bit-Vektore.
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
Ondertekende/Ondertekende Getalle
Z3 bied spesiale ondertekende weergawes van aritmetiese operasies waar dit 'n verskil maak of die bit-vektor as ondertekend of onondertekend behandel word. In Z3Py, stem die operatore <, <=, >, >=, /, % en >> ooreen met die ondertekende weergawes. Die ooreenstemmende onondertekende operatore is ULT, ULE, UGT, UGE, UDiv, URem en 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))
Funksies
Geïnterpreteerde funksies soos aritmetika waar die funksie + 'n vasgestelde standaardinterpretasie het (dit tel twee getalle bymekaar). Ongeïnterpreteerde funksies en konstantes is maximaal buigsaam; hulle laat enige interpretasie toe wat konsekwent is met die beperkings oor die funksie of konstante.
Voorbeeld: f toegepas twee keer op x lei tot x weer, maar f toegepas een keer op x is verskillend van 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())
Voorbeelde
Sudoku-oplosser
# 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"