# Python [Learning] - Z3

> [name=D]

## Introduction
- Z3 is the SMT( [Satisfiability Modulo Theories](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories) ) solver, the library of Python.
- It is developed at Microsoft Research.

## Installation
- Github : https://github.com/Z3Prover/z3
- Microsoft Windows
- `pip install z3-solver`

## Usage
### Boolean Theory
- Boolean values
- `BoolVal(False)`
- `BoolVal(True)`
- Boolean sort
- `BoolSort()`
- `p = Const('p', BoolSort())` == `p = Bool('p')`
- `f = Function('f', IntSort(), BoolSort(), BoolSort())`
- `bool_variables = [Const(f'p{i}', BoolSort()) for i in range(10)]`
- Constant declaration
- `Bool(name)`
- `bool_variables = [Bool(f'p{i}') for i in range(10)]`
- `Bool(name1, name2)` = `Bools(names)`
- Unary operator
- `Not(negation)`
- Binary operators
- `Or(disjunction)`
- `And(conjunction)`
- `Xor(exclusive or)`
- `Implies(implication)` : `A => B` ( if-than statement )
- If A is true, than B must also be true.
- If A is false, than B can be either true or false.

#### Easy Code

from z3 import *

s = Solver()
x = Bool('X')

s.add(Not(x))

if s.check() == sat:
    print(s.model())
    
# OUTPUT : [X = False]

### Arithmetic Theory
- Integer sort
- `IntSort()`
- `RealSort()`
- Integer values
- `IntVal(value)`
- `RealVal(value)`
- Constant declaration
- `Int(name)`
- `Real(name)`
- Binary operators
- `+`, `-`, `*`, `/`, `%`
- Binary relations
- `<`, `<=`, `>`, `>=`

#### Easy Code

from z3 import *

s = Solver()

i = Int('I')
x = Real('X')

s.add(i < x)
s.add(x < i + 1)

if s.check() == sat:
    print(s.model())

### Bitvectory Theory
- Sort declaration
- `BitVecSort(width)`
- Constant declaration
- `BitVec(name, width)`
- Binary operators
- `&`, `|`, `~`, `^`, `+`, `-`, `*`, `/`, `%`, `>>`, `<<`
- Binary relations
- `<`, `<=`, `>`, `>=`
- Additional functions
- `Concat(bitvecs)`
- `Extract(high, low, bitvec)`
- `RotateLeft(bitvec, r)`
- `RotateRight(bitvec, r)`
#### Easy Code

from z3 import *

s = Solver()

x = BitVec('x', 16) 
# the range of x is 0 ~ 65535(2^16 - 1)

s.add(x > 0)
s.add(x & (x - 1) == 0)

while s.check() == sat:
    print(s.model()[x])
    s.add(x != s.model()[x])
    
# OUTPUT : 2 次方的數 (1, 2, 4, 8, ...)

## Getting Started
### Steps
- Import Z3 library
- Create the Constant
- Create the Formula
- Create a Solver
- Add a Formula
- Check Satisfiability
- Obtain a model

### Example
- Simultaneous Linear Equations

> $\begin{cases}
> Y = -4X
> \\3X+2Y = 5
> \end{cases}$

- Output
> `X = -1, Y = 4`

### Import Z3 library
> `import z3 from *`

### Create the Constant
> `x = Int('X')`
> `y = Int('Y')`
- Z3 constant -> Python variable
- Z3 constant `X` -> Python Integer variable `x`
- Z3 constant `Y` -> Python Integer variable `y`

#### Python Variable Type
- `Int(name)`
- `Real(name)`
- `Bool(name)`
- `BitVec(name, width)`

### Create the Formula
> `formula = And(y == (-4 * x), (3 * x + 2 * y) == 5)`
#### Conjunction
- Z3 conjunction -> Python formula
- Z3 conjunction `Y = -4X` -> Python formula `y == (-4 * x)`
- Z3 conjunction `3X + 2Y = 5` -> Python formula `(3 * x + 2 * y) == 5`
#### Function for Z3
- `And(condiction1, condiction2, ...)`
- `Or(condiction1, condiction2, ...)`

### Create a Solver
> `s = Solver()`

### Add the Formula
> `s.add(formula)`

OR

> `s.add(y == -4 * x)`
> `s.add(3 * x + 2 * y == 5)`

### Check Satisfiability
> `s.check()`

- satisfiability, return `sat`
- unsatisfiability, return `unsat`

### Obtain a model
> `s.model()`

- return the satisfiable answers of formula

### Code

# import Z3 library
from z3 import *

# Create the Constant
x = Int('X')
y = Int('Y')

# Create the Formula
formula = And(y == -4*x, 3*x + 2*y == 5)

# Create a SMT solver s
s = Solver()

# Add the Formula
s.add(formula)

# Check Satisfiability, then obtain the Model
if s.check() == sat:
    ans = s.model()
    # ans : [X = -1, Y = 4]
    print(f'X = {ans[x]}, Y = {ans[y]}')

## McCarthy91

int mccarthy91 (int n) {
      int c;
      int ret;
      ret = n;
      c = 1;
      while (c > 0) {
        if (ret > 100) {
          ret = ret - 10;
          c--;
        } else {
          ret = ret + 11;
          c++;
        }
      }
      return ret;
    }

### [Before]

from z3 import *

n = Int ('n')
ret = Int ('ret')
c = Int ('c')

solver = Solver ()

def pre (eta):
    b_true  = Implies (ret > 100, 
                       substitute (substitute (eta, (c, c - 1)),
                                   (ret, ret - 10)))
    b_false = Implies (Not (ret > 100),
                       substitute (substitute (eta, (c, c + 1)),
                                   (ret, ret + 11)))
    return And (b_true, b_false)

def check_implies (phi, psi):
    solver.push ()
    f = And (phi, Not (psi))
    solver.add (f)
    result = solver.check ()
    if result == sat:
        print ('(n, ret, c) = (', solver.model()[n], solver.model()[ret], solver.model()[c], ')')
    solver.pop ()
    return result != sat

def check_pre (pre, eta, name):
    result = check_implies (pre, eta)
    result_str = 'pass' if result else 'fail'
    print ('check precondition ({0}): {1}'.format (name, result_str))
    return result

def check_post (eta, post, name):
    result = check_implies (And (Not (c > 0), eta), post)
    result_str = 'pass' if result else 'fail'
    print ('check postcondition ({0}): {1}'.format (name, result_str))
    return result

def check_invariant (eta, name):
    result = check_implies (And (c > 0, eta), pre (eta))
    result_str = 'pass' if result else 'fail'
    print ('check invariant ({0}): {1}'.format (name, result_str))
    return result

""" find eta_easy for input n > 100 """

eta_easy = BoolVal (False)

check_pre (And (n > 100, ret == n, c == 1), eta_easy, 'easy')
check_invariant (eta_easy, 'easy')
check_post (eta_easy, ret == n - 10, 'easy')

""" find eta_hard for input n <= 100 """

eta_hard = BoolVal (False)

check_pre (And (n <= 100, ret == n, c == 1), eta_hard, 'hard')
check_invariant (eta_hard, 'hard')
check_post (eta_hard, ret == 91, 'hard')

""" combine eta_easy and eta_hard """

eta = And (Implies (n > 100, eta_easy), Implies (n <= 100, eta_hard))

check_pre (And (n <= 100, ret == n, c == 1), eta, 'all')
check_invariant (eta, 'all')
check_post (eta, And (Implies (n >  100, ret == n - 10),
                      Implies (n <= 100, ret == 91)), 'all')

### [After]

from z3 import *

n = Int ('n')
ret = Int ('ret')
c = Int ('c')

solver = Solver ()

def pre (eta):
    b_true  = Implies (ret > 100, 
                       substitute (substitute (eta, (c, c - 1)),
                                   (ret, ret - 10)))
    b_false = Implies (Not (ret > 100),
                       substitute (substitute (eta, (c, c + 1)),
                                   (ret, ret + 11)))
    return And (b_true, b_false)

def check_implies (phi, psi):
    solver.push ()
    f = And (phi, Not (psi))
    solver.add (f)
    result = solver.check ()
    if result == sat:
        print ('(n, ret, c) = (', solver.model()[n], solver.model()[ret], solver.model()[c], ')')
    solver.pop ()
    return result != sat

def check_pre (pre, eta, name):
    result = check_implies (pre, eta)
    result_str = 'pass' if result else 'fail'
    print ('check precondition ({0}): {1}'.format (name, result_str))
    return result

def check_post (eta, post, name):
    result = check_implies (And (Not (c > 0), eta), post)
    result_str = 'pass' if result else 'fail'
    print ('check postcondition ({0}): {1}'.format (name, result_str))
    return result

def check_invariant (eta, name):
    result = check_implies (And (c > 0, eta), pre (eta))
    result_str = 'pass' if result else 'fail'
    print ('check invariant ({0}): {1}'.format (name, result_str))
    return result

""" find eta_easy for input n > 100 """
""" {n > 100} ret = mccarthy91(n) {ret == n - 10} """

eta_easy = And(c >= 0, n > 100, ret == n - 10 + 10 * c)

check_pre (And (n > 100, ret == n, c == 1), eta_easy, 'easy')
check_invariant (eta_easy, 'easy')
check_post (eta_easy, ret == n - 10, 'easy')

""" find eta_hard for input n <= 100 """
""" { n <= 100 } ret = mccarthy91(n) { ret == 91 }"""

eta_hard = And (Implies (ret >= 90, And(91 - c <= ret, ret <= 91 + 10 * c)), 
                Implies (ret < 90, c > 0))

check_pre (And (n <= 100, ret == n, c == 1), eta_hard, 'hard')
check_invariant (eta_hard, 'hard')
check_post (eta_hard, ret == 91, 'hard')

""" combine eta_easy and eta_hard """
""" { true } ret = mccarthy91(n) {(n > 100 ==> ret == n - 10) && (n <= 100 ==> ret == 91) } """

eta = And (Implies (n > 100, eta_easy), Implies (n <= 100, eta_hard))

check_pre (And (n <= 100, ret == n, c == 1), eta, 'all')
check_invariant (eta, 'all')
check_post (eta, And (Implies (n >  100, ret == n - 10),
                      Implies (n <= 100, ret == 91)), 'all')


## Reference
- [Z3 API in Python - Chinese](https://nen9ma0.github.io/2018/03/14/z3py/)
- [Z3 API in Python - English](https://ericpony.github.io/z3py-tutorial/guide-examples.htm)
- [Programming Z3](https://theory.stanford.edu/~nikolaj/programmingz3.html)
- [從 CTF 入門 z3 solver](https://blog.shi1011.cn/learn/1789)
- [Z3 API in Python - English](https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/#machine-arithmetic)
- [Z3 - Satisfiability Modulo Theories (SMT)](https://book.hacktricks.xyz/reversing/reversing-tools-basic-methods/satisfiability-modulo-theories-smt-z3)
- [Z3py.py](https://z3prover.github.io/api/html/z3py_8py_source.html#l01691)