hacktricks/reversing/reversing-tools-basic-methods/satisfiability-modulo-theories-smt-z3.md

<details>

<summary><strong>Leer AWS-hacking van nul tot held met</strong> <a href="https://training.hacktricks.xyz/courses/arte"><strong>htARTE (HackTricks AWS Red Team Expert)</strong></a><strong>!</strong></summary>

Ander maniere om HackTricks te ondersteun:

* As jy jou **maatskappy geadverteer wil sien in HackTricks** of **HackTricks in PDF wil aflaai**, kyk na die [**SUBSCRIPTION PLANS**](https://github.com/sponsors/carlospolop)!
* Kry die [**amptelike PEASS & HackTricks swag**](https://peass.creator-spring.com)
* Ontdek [**The PEASS Family**](https://opensea.io/collection/the-peass-family), ons versameling eksklusiewe [**NFTs**](https://opensea.io/collection/the-peass-family)
* **Sluit aan by die** 💬 [**Discord-groep**](https://discord.gg/hRep4RUj7f) of die [**telegram-groep**](https://t.me/peass) of **volg** ons op **Twitter** 🐦 [**@carlospolopm**](https://twitter.com/hacktricks_live)**.**
* **Deel jou hacktruuks deur PR's in te dien by die** [**HackTricks**](https://github.com/carlospolop/hacktricks) en [**HackTricks Cloud**](https://github.com/carlospolop/hacktricks-cloud) github-opslag.

</details>


Baie basies sal hierdie instrument ons help om waardes vir veranderlikes te vind wat aan sekere voorwaardes moet voldoen, en dit sal baie vervelig wees om dit met die hand te bereken. Daarom kan jy aan Z3 aandui watter voorwaardes die veranderlikes moet bevredig en dit sal enkele waardes vind (indien moontlik).

**Sommige teks en voorbeelde is onttrek uit [https://ericpony.github.io/z3py-tutorial/guide-examples.htm](https://ericpony.github.io/z3py-tutorial/guide-examples.htm)**

# Basiese Operasies

## Booleans/En/Of/Nie
```python
#pip3 install z3-solver
from z3 import *
s = Solver() #The solver will be given the conditions

x = Bool("x") #Declare the symbos x, y and z
y = Bool("y")
z = Bool("z")

# (x or y or !z) and y
s.add(And(Or(x,y,Not(z)),y))
s.check() #If response is "sat" then the model is satifable, if "unsat" something is wrong
print(s.model()) #Print valid values to satisfy the model
```
## Inte/Simplifiseer/Reëls

Die Z3 SMT-solver bied 'n verskeidenheid funksies vir die hantering van ints, vereenvoudiging en werk met reële getalle. Hier is 'n oorsig van die basiese metodes wat beskikbaar is:

### Inte

- `Int` is die tipe vir ints in Z3.
- Jy kan ints skep deur die `IntVal`-funksie te gebruik, byvoorbeeld `IntVal(42)` sal 'n int met die waarde 42 skep.
- Inte kan ook geskep word deur die `Int`-funksie te gebruik, byvoorbeeld `Int('x')` sal 'n int met die naam 'x' skep.
- Inte kan gebruik word in wiskundige uitdrukkings, byvoorbeeld `x + 2` of `y * 3`.

### Vereenvoudiging

- Die `simplify`-funksie kan gebruik word om wiskundige uitdrukkings te vereenvoudig.
- Byvoorbeeld, `simplify(x + 0)` sal vereenvoudig na `x`, en `simplify(x * 1)` sal vereenvoudig na `x`.
- Vereenvoudiging kan help om die uitdrukking te vereenvoudig en die oplossing te vind.

### Reële getalle

- `Real` is die tipe vir reële getalle in Z3.
- Jy kan reële getalle skep deur die `RealVal`-funksie te gebruik, byvoorbeeld `RealVal(3.14)` sal 'n reële getal met die waarde 3.14 skep.
- Reële getalle kan ook geskep word deur die `Real`-funksie te gebruik, byvoorbeeld `Real('y')` sal 'n reële getal met die naam 'y' skep.
- Reële getalle kan gebruik word in wiskundige uitdrukkings, byvoorbeeld `y + 2.5` of `z * 1.5`.

Met hierdie basiese metodes kan jy ints en reële getalle hanteer, vereenvoudig en gebruik in jou SMT-probleme met die Z3-solver.
```python
from z3 import *

x = Int('x')
y = Int('y')
#Simplify a "complex" ecuation
print(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 solution
r1 = Real('r1')
r2 = Real('r2')
#Solve the ecuation
print(solve(r1**2 + r2**2 == 3, r1**3 == 2))
#Solve the ecuation with 30 decimals
set_option(precision=30)
print(solve(r1**2 + r2**2 == 3, r1**3 == 2))
```
## Druk Model

To print the model generated by Z3, you can use the `model` method. This method returns a string representation of the model.

Om die model wat deur Z3 gegenereer is af te druk, kan jy die `model` metode gebruik. Hierdie metode gee 'n teksvoorstelling van die model terug.
```python
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]))
```
# Masjienrekenkunde

Moderne CPU's en algemene programmeertale gebruik rekenkunde oor **vasgestelde grootte bit-vektore**. Masjienrekenkunde is beskikbaar in Z3Py as **Bit-Vektore**.
```python
from z3 import *

x = BitVec('x', 16) #Bit vector variable "x" of length 16 bit
y = BitVec('y', 16)

e = BitVecVal(10, 16) #Bit vector with value 10 of length 16bits
a = 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
```
## Ondertekende/Ondertekende Getalle

Z3 bied spesiale ondertekende weergawes van aritmetiese operasies waar dit 'n verskil maak of die **bit-vektor as ondertekend of onondertekend behandel word**. In Z3Py, stem die operatore **<, <=, >, >=, /, % en >>** ooreen met die **ondertekende** weergawes. Die ooreenstemmende **onondertekende** operatore is **ULT, ULE, UGT, UGE, UDiv, URem en LShR.**
```python
from z3 import *

# Create to bit-vectors of size 32
x, y = BitVecs('x y', 32)
solve(x + y == 2, x > 0, y > 0)

# Bit-wise operators
# & bit-wise and
# | bit-wise or
# ~ bit-wise not
solve(x & y == ~y)
solve(x < 0)

# using unsigned version of <
solve(ULT(x, 0))
```
## Funksies

**Geïnterpreteerde funksies** soos aritmetika waar die **funksie +** 'n **vasgestelde standaardinterpretasie** het (dit tel twee getalle bymekaar). **Ongeïnterpreteerde funksies** en konstantes is **maximaal buigsaam**; hulle laat **enige interpretasie** toe wat **konsekwent** is met die **beperkings** oor die funksie of konstante.

Voorbeeld: f toegepas twee keer op x lei tot x weer, maar f toegepas een keer op x is verskillend van x.
```python
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 response
s.check()
print(m.model())
```
# Voorbeelde

## Sudoku-oplosser
```python
# 9x9 matrix of integer variables
X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ]
for i in range(9) ]

# each cell contains a value in {1, ..., 9}
cells_c  = [ And(1 <= X[i][j], X[i][j] <= 9)
for i in range(9) for j in range(9) ]

# each row contains a digit at most once
rows_c   = [ Distinct(X[i]) for i in range(9) ]

# each column contains a digit at most once
cols_c   = [ Distinct([ X[i][j] for i in range(9) ])
for j in range(9) ]

# each 3x3 square contains a digit at most once
sq_c     = [ Distinct([ X[3*i0 + i][3*j0 + j]
for i in range(3) for j in range(3) ])
for i0 in range(3) for j0 in range(3) ]

sudoku_c = cells_c + rows_c + cols_c + sq_c

# sudoku instance, we use '0' for empty cells
instance = ((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 in range(9) for j in range(9) ]

s = Solver()
s.add(sudoku_c + instance_c)
if s.check() == sat:
m = s.model()
r = [ [ m.evaluate(X[i][j]) for j in range(9) ]
for i in range(9) ]
print_matrix(r)
else:
print "failed to solve"
```
## Verwysings

* [https://ericpony.github.io/z3py-tutorial/guide-examples.htm](https://ericpony.github.io/z3py-tutorial/guide-examples.htm)


<details>

<summary><strong>Leer AWS-hacking van nul tot held met</strong> <a href="https://training.hacktricks.xyz/courses/arte"><strong>htARTE (HackTricks AWS Red Team Expert)</strong></a><strong>!</strong></summary>

Ander maniere om HackTricks te ondersteun:

* As jy jou **maatskappy geadverteer wil sien in HackTricks** of **HackTricks in PDF wil aflaai**, kyk na die [**SUBSCRIPTION PLANS**](https://github.com/sponsors/carlospolop)!
* Kry die [**amptelike PEASS & HackTricks swag**](https://peass.creator-spring.com)
* Ontdek [**The PEASS Family**](https://opensea.io/collection/the-peass-family), ons versameling eksklusiewe [**NFTs**](https://opensea.io/collection/the-peass-family)
* **Sluit aan by die** 💬 [**Discord-groep**](https://discord.gg/hRep4RUj7f) of die [**telegram-groep**](https://t.me/peass) of **volg** ons op **Twitter** 🐦 [**@carlospolopm**](https://twitter.com/hacktricks_live)**.**
* **Deel jou hacktruuks deur PR's in te dien by die** [**HackTricks**](https://github.com/carlospolop/hacktricks) en [**HackTricks Cloud**](https://github.com/carlospolop/hacktricks-cloud) github-opslagplekke.

</details>