[Z3] Z3 Tutorials

본 포스트는 아래 Youtube 링크에 해당하는 영상을 보고 정리하였습니다.

https://www.youtube.com/watch?v=56IIrBZy9Rc&list=PLlMMtlgw6qNiRlD_RaJMNbZj2kSUPrPtU&index=1 

강사의 github link는 아래와 같습니다.

https://github.com/philzook58/z3_tutorial/blob/master/Z3%20Tutorial.ipynb

philzook58/z3_tutorial

 

Z3 Variables

다른 종류(Sorts, z3의 type)의 z3 변수를 만듦

x = Bool("x")
x = Const("x" , BoolSort())
p, q, r = Bools("p q r") # convenience function for multiple definitions
x = Real("x")
x, y = Reals("x y")		# need space
y = Int("x") 
v = BitVec("n", 32) # 32 bit bitvector
f = FP("f", Float64()) #Floating point values
a = Array("a", IntSort(), BoolSort()) # arrays

 

Constraints / Operations

 

# Common numerical operations
print(x + x) # addition
print(x * x) # multiplication
print(x ** 4) # fourth power of x 

# Common boolean operations
print(And(p,q))
print(And(p,q,r)) # some can accept more than one argument for convenience.
print(Or(p,q))
print(Implies(p,q))
print(Xor(p,q))
print(Not(p))

# Constraints 
print(x == x) #equal
print(x != x) # not equal
print(x <= RealVal(3)) # inequality
print(Or( x < 3,  x == 3, x > 3  )) # Constraints are operations into booleans

# And many more! Look in the API docs for others https://z3prover.github.io/api/html/namespacez3py.html

 

Exercise

Get a root of the polynomial x**3 + 3*x**2 + 4*x + 2 == 0 using z3.

x = Real("x")
solve(x**3 + 3*x**2 + 4*x + 2)

증명 방법

x = Real("x")
solve(x**3 + 3*x**2+ 4*x + 2 ==0, x != -1)
# 또는
prove( Implies( x**3 + 3*x**2+ 4*x + 2 ==0, x == -1))

 

Exercise : Send More Money

    Send

+  More

----------

  Money

를 찾는 문제

 

from z3 import *

digits = Ints('s e n d m o r y')
s,e,n,d,m,o,r,y = digits
send = Sum([10**(3-i) * d for i,d in enumerate([s,e,n,d])]) # convert digits of number to number
more = Sum([10**(3-i) * d for i,d in enumerate([m,o,r,e])])
money = Sum([10**(4-i) * d for i,d in enumerate([m,o,n,e,y])])

print(type(digits))

solver = Solver()
solver.add([s > 0, m > 0]) # first digits are nonzero

# Constrain all digits constrained to be 0 through 9
# FILL IN
solver.add([ And(0 <= d, d <=9) for d in digits]) 

# Constrain all digits to be unique (Hint: Look at the 8-Queens constraints. Anything useful?)
# FILL IN
solver.add(Distinct(digits))

# Constrain send + more == money
# FILL IN
solver.add(send + more == money)

solver.check()
print(solver.check())
solver.model()

# see the value of send
print(solver.model().eval(send))

 

Proof = Exhaustively Not Finding Counterexamples

 

solver.check() may return

• sat - "I have found a solution. You may ask for it with solver.model()"
• unknown - This means "I give up". There may be a solution out there somewhere, there may not.
• unsat - "I KNOW there is no solution. I've tried EVERYTHING".

Z3 solver가 주어진 problem을 solve하기 위해 모든 것을 try해보기 때문에 실행 시간이 크다는 단점 존재