Πολύ βασικά, αυτό το εργαλείο θα μας βοηθήσει να βρούμε τιμές για μεταβλητές που πρέπει να ικανοποιούν κάποιες συνθήκες και η υπολογιστική τους χειροκίνητα θα είναι πολύ ενοχλητική. Επομένως, μπορείτε να υποδείξετε στο 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]))
Μηχανική Άλγεβρα
Οι σύγχρονοι επεξεργαστές και οι κυριότερες γλώσσες προγραμματισμού χρησιμοποιούν άλγεβρα πάνω σε σταθερού μεγέθους bit-vectors. Η μηχανική άλγεβρα είναι διαθέσιμη στο Z3Py ως Bit-Vectors.
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 παρέχει ειδικές υπογεγραμμένες εκδόσεις αριθμητικών λειτουργιών όπου έχει σημασία αν το bit-vector αντιμετωπίζεται ως υπογεγραμμένο ή μη υπογεγραμμένο. Στο 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
Ερμηνευμένες συναρτήσεις όπως η αριθμητική όπου η συνάρτηση + έχει μια σταθερή τυπική ερμηνεία (προσθέτει δύο αριθμούς). Μη ερμηνευμένες συναρτήσεις και σταθερές είναι μέγιστης ευελιξίας; επιτρέπουν οποιαδήποτε ερμηνεία που είναι συνεπής με τους περιορισμούς πάνω στη συνάρτηση ή τη σταθερά.
Παράδειγμα: η f εφαρμοσμένη δύο φορές στο x έχει ως αποτέλεσμα το x ξανά, αλλά η f εφαρμοσμένη μία φορά στο x είναι διαφορετική από το 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())
Παραδείγματα
Λύτης Sudoku
# 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"
