What is SMT-LIBv2
SMT-LIBv2 is a standard for writing SMT constraints, its latest version v2.6 can be found here.
Being a standard means any SMT solver such as z3 should be able to parse and check the SMT constraints complying to this standard.
A simple SMT file has the suffix .smt and looks like the following:
1
2
3
4
5
6
7
8
9
10
(set-option :produce-models true)
(set-logic QF_LIA) ;; different logics use different theoreies to solve the constraints
(declare-fun x () Int) ;; declare interger constant
(declare-fun y () Int)
(assert (and (<= (+ x 3) (* 2 y)) (>= (* 2 x) 5))) ;; adding constraint
(check-sat)
(get-model) ;; if sat, produce an assignment of x and y that satisfies all assertions
Input the above file to a SMT solver, and the solver will output the assignments as following, which means x = 3 and y = 3 satisfies the assertion.
1
2
3
4
5
6
7
sat
(
(define-fun x () Int
3)
(define-fun y () Int
3)
)
If there is no way to satisfy all assertions, the solver will output unsat, and then one can query the set of assertions that cannot be satisfied by:
- adding
set-option :produce-unsat-cores truein the beginning; - assign a name to each assertion (i.e.
assert (! (=> P Q) :named PQ)); and - append
(get unsat-core)in the end.
Basic syntax
Using z3 solver in Emacs
There exists Emacs package to support z3-mode, the github repo can be found here.
After the successful installation, one should be able to see the syntax highlights for most key words when z3-mode is activated, and with C-c C-c one could execute the solver and get the result in another buffer.