NOTE: a little bit Z3 solver
source link: https://dannypsnl.github.io/blog/2020/01/24/cs/note-a-little-bit-z3-solver/
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
Satisfiability Modulo Theories(SMT) problem is a decision problem for logical formulas with respect to combinations of background theories…NOTE: a little bit Z3 solver
Email: [email protected]
GitHub: @dannypsnl
Twitter: @dannypsnl
Programming Language Theory • System Programming
NOTE: a little bit Z3 solver
Satisfiability Modulo Theories(SMT) problem is a decision problem for logical formulas with respect to combinations of background theories such as arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is an efficient SMT solver with specialized algorithms for solving background theories.
Wow, many words. But for me, right now, Z3 is a theorem prover from Microsoft. Use SMT-LIB this lisp-like language.
(declare-const x Int)
(declare-const y Int)
(assert (= 5 (+ x y 3)))
(check-sat)The program produce: sat as result. If we didn't provide a possible constraint:
(declare-const x Int)
(assert (= 5 (+ x 3)))
(assert (= 5 (+ x 2)))
(check-sat)The result would be unsat, not surprising.
As title, a little bit z3, this is the end, I hadn't know where can I use z3, XD.
author: Lîm Tsú-thuàn/林子篆/Danny
category:cs
tag:notesmtz3
Similar Articles
All works in this site is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK