# z3
{% file src="/files/v8wFcdCtxejqlfDMjDx7" %}
## z3py
{% hint style="success" %}
**Setup**:
* pip install z3-solver
* apt install python3-z3
{% endhint %}
{% code overflow="wrap" %}
```python
# Set up the environment and import z3 python-bindings
from z3 import *
# ... and create a solver
s = z3.Solver()
# Then, declare the variables we have
# machine code is allowed - registers and flags here!
eax_in = z3.BitVec('eax_in',32)
ecx_in = z3.BitVec('ecx_in',32)
eax1, eax2, eax3 = z3.BitVecs("eax1 eax2 eax3", 32)
edx1, edx2 = z3.BitVecs("edx1 edx2", 32)
# model the problem
model = [
eax1 == eax_in + ecx_in,
eax2 == eax1 << z3.BitVecVal(12, 32),
eax3 == eax2 * ecx_in,
edx1 == eax3,
edx2 == edx1 ^ ecx_in
]
# Add the model to the solver
s.add(model)
# ... and as before, check for satisfiability
# Which means, check if there is an answer to our question
if s.check() == z3.unsat:
print('Can not find a solution!')
sys.exit(-1)
print(s.check())
# Keep adding more constraints (chỗ này để thêm ràng buộc như gán giá trị cho các thanh ghi)
requirement = edx2 == z3.BitVecVal(0x100, 32)
s.add(requirement)
# And checking for solutions, including the new constraints.
if s.check() == z3.sat:
print(f'Found a solution for {requirement}')
# Retrieve the found solution
m = s.model()
eax_val = m[eax_in].as_long()
ecx_val = m[ecx_in].as_long()
print(f'EAX : 0x{eax_val:02x}, ECX : 0x{ecx_val:02x}')
else:
print("Can not solve it!")
# Found a solution for 256 == edx2
# EAX : 0xfff00, ECX : 0x100
# Find all solutions and update the constraints dynamically
solutions = [('eax_in', 'ecx_in')]
while s.check() == z3.sat:
m = s.model()
eax_val = int(f'{m[eax_in]}')
ecx_val = int(f'{m[ecx_in]}')
requirement_eax = eax_in != m[eax_in]
requirement_ecx = ecx_in != m[ecx_in]
s.add(requirement_eax)
s.add(requirement_ecx)
solutions.append((m[eax_in], m[ecx_in]))
print(f'EAX : 0x{eax_val:02x}, ECX : 0x{ecx_val:02x}')
if len(solutions) >10:
break
```
{% endcode %}
> **Resources:**
>
> * [z3py documentation](http://z3prover.github.io/api/html/namespacez3py.html)
> * [z3py functions documentation](http://z3prover.github.io/api/html/namespacez3py.html#func-members)
> * [z3py - the Solver class](http://z3prover.github.io/api/html/classcom_1_1microsoft_1_1z3_1_1_solver.html)
> * [z3py - the BitVecNum](http://z3prover.github.io/api/html/classz3py_1_1_bit_vec_num_ref.html)
> * [z3py - check() and sat](http://z3prover.github.io/api/html/classz3py_1_1_check_sat_result.html)
> * [z3 online](https://compsys-tools.ens-lyon.fr/z3/index.php)
> * [z3 Distinct()](https://z3prover.github.io/api/html/namespacez3py.html#aac3e33e977e8037611916937caffa78e)
---
# Agent Instructions: Querying This Documentation
If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.
Perform an HTTP GET request on the current page URL with the `ask` query parameter:
```
GET https://viettaliii.gitbook.io/home/education/reverse-engineering/symbolic-analysis/sat-and-constraints/z3.md?ask=
```
The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.
Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.