# 1. SMT-solver as a calculator

Một ví dụ về SMT-solver như một máy tính dưới z3py API:

```python
#!/usr/bin/env python3
from z3 import *
s=Solver()
x,y,z=Ints('x y z')
s.add(x==2)
s.add(y==3)
s.add(z==x+y)
print (s.check())
print (s.model())
```

Kết quả:

```
sat
[z = 5, y = 3, x = 2]
```

Hoặc in SMT-LIB 2.0 form:

```markup
(declare-fun x () (_ BitVec 16)
(declare-fun y () (_ BitVec 16)
(declare-fun z () (_ BitVec 16)

(assert (= x (_ bv2 16)))
(assert (= y (_ bv3 16)))

(assert (= z (bvadd x y)))

(check-sat)
(get-model)
```

Kết quả sẽ là thế cả trên mạng với code (hiện nay thì tôi chưa nghiên cứu để chạy trên CMD, chỉ chạy trên online ([link](https://compsys-tools.ens-lyon.fr/z3/)).

```
sat
(model 
  (define-fun z () (_ BitVec 16)
    #x0005)
  (define-fun y () (_ BitVec 16)
    #x0003)
  (define-fun x () (_ BitVec 16)
    #x0002)
)
```

Hãy nghĩ về nó như về mạch điện tử - bạn có thể xây dựng một bộ công cụ từ các bộ cộng và cổng logic. Sau đó bật mạc của mình và nhận kết quả ở đầu ra của bộ công cụ. (sẽ có ở phần sau)

Bây giờ sẽ là máy tính nghịch đảo. Chúng ta có thể giải được phương trình như `x + 3 = 17`?

```
(declare-fun x () (_ BitVec 16))

(assert (= (bvadd x (_ bv3 16)) (_ bv17 16)))

(check-sat)
(get-model)
```

Và nhận được kết quả là:

```
sat
(model 
  (define-fun x () (_ BitVec 16)
    #x000e)
)
```


---

# 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-smt-by-example/equations/1.-smt-solver-as-a-calculator.md?ask=<question>
```

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.