# Z3 Theorem Prover ss8651twtw https://hackmd.io/@ss8651twtw/z3 --- ## Z3 簡介 一個由微軟研究團隊開發的 SMT solver 工具 ---- ### SMT [Satisfiability Modulo Theories](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories) - general version of SAT ${ \begin{cases} x + 2y > 4 \\ 3x - y = 3 \\ \end{cases} }$ <!-- .element: class="fragment" data-fragment-index="1" --> Solve x, y = ? <!-- .element: class="fragment" data-fragment-index="1" --> ---- ### 安裝 Python binding ```shell pip install z3-solver ``` ---- ### 使用流程  ---- ### Z3 API in Python 1. define the variables 2. add constrains 3. solve the equations --- ## Z3 使用範例  ---- ## Z3 使用範例 ```python from z3 import * x, y = Int('x'), Int('y') s = Solver() s.add(x + 2 * y > 4) s.add(3 * x - y == 3) s.check() s.model() ``` --- ## Reference - https://en.wikipedia.org/wiki/Z3_Theorem_Prover - https://github.com/Z3Prover/z3 - https://ericpony.github.io/z3py-tutorial/guide-examples.htm - https://z3prover.github.io/api/html/namespacez3py.html --- ## Thanks for Listening