다음의 가이드를 참고하는 글이다.

https://ericpony.github.io/z3py-tutorial/guide-examples.htm

---

Basic

Quadratic Equation

이차 방정식의 해를 구한다.

x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)

결과

root@ubuntu:/work/exploits/z3# python b1.py
[y = 0, x = 7]

Simplify

수식을 간단히 표현하는 기능이다.

x = Int('x')
y = Int('y')
print simplify(x + y + 2*x + 3)
print simplify(x < y + x + 2)
print simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5))

결과

root@ubuntu:/work/exploits/z3# python b2.py
3 + 3*x + y
Not(y <= -2)
And(x >= 2, 2*x**2 + y**2 >= 3)

set_option

set_option()은 모든 표현식과 수식의 표현방식을 설정할 수 있다.
html_mode 옵션은 html 엔티티 형식으로 출력할건지를 결정한다.

x = Int('x')
y = Int('y')
print x**2 + y**2 >= 1
set_option(html_mode=True)
print x**2 + y**2 >= 1

결과

root@ubuntu:/work/exploits/z3# python b3.py
x**2 + y**2 >= 1
x<sup>2</sup> + y<sup>2</sup> &ge; 1

다음은 소수점 30개까지 출력하는 예제다.

>>> x = Real('x')
>>> y = Real('y')
>>> solve(x**2+y**2==3, x**3==2)
[x = 1.2599210498?, y = -1.1885280594?]
>>> set_option(precision=30)
>>> solve(x**2+y**2==3, x**3==2)
[x = 1.259921049894873164767210607278?, y = -1.188528059421316533710369365015?]

Traversing Expression

z3로 수식을 만들면, 각 요소를 접근할 수 있는 함수를 제공해준다.

x = Int('x')
y = Int('y')
n = x + y >= 3
print "num args: ", n.num_args()
print "children: ", n.children()
print "1st child:", n.arg(0)
print "2nd child:", n.arg(1)
print "operator: ", n.decl()
print "op name:  ", n.decl().name()

결과

root@ubuntu:/work/exploits/z3# python b4.py
num args:  2
children:  [x + y, 3]
1st child: x + y
2nd child: 3
operator:  >=
op name:   >=

Power Operator

근을 구할 수 있다.

x = Real('x')
y = Real('y')
solve(x**2 + y**2 > 3, x**3 + y < 5)
solve(x**2 == 4)

결과

root@ubuntu:/work/exploits/z3# python b5.py 
[x = 1/8, y = 2]
[x = 2]

Fractional

분수는 Q(분자, 분모)로 나타낼 수 있다.
또한 RealVal()로 상수를 표현해 분수를 만들 수 있다.

print 1/3
print RealVal(1)/3
print Q(1,3)
print '---------------'
x = Real('x')
print x + 1/3
print x + Q(1,3)
print x + "1/3"
print x + 0.25

결과

root@ubuntu:/work/exploits/z3# python b7.py 
0
1/3
1/3
---------------
x + 0
x + 1/3
x + 1/3
x + 1/4

Rational to Decimal

유리수를 10진수 표현으로 출력

x = Real('x')
solve(3*x == 1)

set_option(rational_to_decimal=True)
solve(3*x == 1)

결과

root@ubuntu:/work/exploits/z3# python b8.py 
[x = 1/3]
[x = 0.3333333333?]

Boolean

Boolean도 마찬가지로 답을 구할 수 있다.

p = Bool('p')
q = Bool('q')
r = Bool('r')
solve(p == Not(r), Or(Not(q), r))

결과

root@ubuntu:/work/exploits/z3# python bool.py
[r = False, q = False, p = True]

또한 그냥 상수값 True, False를 사용할 수도 있다.

p = Bool('p')
q = Bool('q')
print And(p, q, True)
print simplify(And(p, q, True))
print simplify(And(p, False))

결과

root@ubuntu:/work/exploits/z3# python bool2.py
And(p, q, True)
And(p, q)
False

논리 연산자를 Solve에 사용할 수도 있다.

p = Bool('p')
x = Real('x')
solve(Or(x < 5, x > 10), Or(p, x**2 == 2), Not(p))

결과

root@ubuntu:/work/exploits/z3# python bool4.py 
[x = -1.4142135623?, p = False]

Solver

solve() 대신 사용할 수 있다.
Solver()로 객체를 생성한 후에 add로 수식을 추가하는 방식이다.

t('x')
y = Int('y')

s = Solver()
print s

s.add(x > 10, y == x + 2)
print s
print "Solving constraints in the solver s ..."
print s.check()

print "Create a new scope..."
s.push()
s.add(y < 11)
print s
print "Solving updated set of constraints..."
print s.check()

print "Restoring state..."
s.pop()
print s
print "Solving restored set of constraints..."
print s.check()

push()는 현재 상태를 저장하는 것이고, pop()은 저장했던 상태를 복구한다.

check()는 Solver()의 해가 존재하는지 확인하는 것이다. 존재할 경우 sat, 아닐 경우 unsat 이다.

해결할 수 없을 때는 unknown이다. 예를 들어 다음처럼 다항식이 아닌 조건을 전달했을 때

x = Real('x')
s = Solver()
s.add(2**x == 3)
print s.check()

위 코드의 실행으로 unknown이 출력될 것이다.

Traversal - assert

Solver.assertions()으로 수식 단위로 접근할 수 있다.

x = Real('x')
y = Real('y')
s = Solver()
s.add(x > 1, y > 1, Or(x + y > 3, x - y < 2))
print "asserted constraints..."
for c in s.assertions():
    print c

print s.check()
print "statistics for the last check method..."
print s.statistics()
# Traversing statistics
for k, v in s.statistics():
    print "%s : %s" % (k, v)

결과

root@ubuntu:/work/exploits/z3# python tra.py 
asserted constraints...
x > 1
y > 1
Or(x + y > 3, x - y < 2)
sat
statistics for the last check method...
(:arith-iterations    1
 :arith-lower         1
 :arith-make-feasible 3
 :arith-max-columns   4
 :arith-max-rows      2
 :arith-pivots        1
 :arith-rows          4
 :arith-upper         3
 :decisions           2
 :final-checks        1
 :max-memory          2.38
 :memory              2.19
 :mk-bool-var         10
 :num-allocs          456090
 :rlimit-count        213)
mk bool var : 1
decisions : 2
final checks : 1
mk bool var : 5
arith-lower : 1
arith-upper : 3
arith-rows : 4
arith-iterations : 1
arith-pivots : 1
arith-make-feasible : 3
arith-max-columns : 4
arith-max-rows : 2
mk bool var : 1
mk bool var : 1
mk bool var : 1
mk bool var : 1
num allocs : 456090
rlimit count : 213
max memory : 2.38
memory : 2.19
root@ubuntu:/work/exploit

Model

Model은 해의 집합(?)을 말하는 것 같다.

We say the solution is a model for the set of asserted constraints.

어쨌든 model()을 이용해 각 solution에 접근할 수 있다.

x, y, z = Reals('x y z')
s = Solver()
s.add(x > 1, y > 1, x + y > 3, z - x < 10)
print s.check()

m = s.model()
print "x = %s" % m[x]

print "traversing model..."
for d in m.decls():
    print "%s = %s" % (d.name(), m[d])

결과

root@ubuntu:/work/exploits/z3# python pp.py
sat
x = 3/2
traversing model...
z = 0
y = 2
x = 3/2