#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
해석된 함수는 산술과 같은 것으로, **함수 +**는 고정된 표준 해석을 가지고 있습니다(두 숫자를 더합니다). 해석되지 않은 함수와 상수는 최대 유연성을 가지고 있으며, 이는 함수 또는 상수에 대한 제약과 일관된 모든 해석을 허용합니다.
예: 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())
예제
스도쿠 해결기
# 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"
