-
Notifications
You must be signed in to change notification settings - Fork 1
Format SMT LIB
Satisfiability Modulo Theories (SMT) is an area of automated deduction that studies methods for checking the satisfiability of first-order formulas with respect to some logical theory of interest. The SMT-LIB format is in its current version essentially a format for first-order logic, with interpreted theories and combination thereof. The syntax is based on lisp-like s-expressions.
The format is well-adopted among the SMT community, most SMT solvers accept the SMT-LIB syntax. It is used for the annual SMT-COMP competition of SMT solvers.
The syntax is described in the external document provided on the SMT-LIB site here.
The semantics is described in the external document provided on the SMT-LIB site here.
The current stable version is SMT-LIB 2.6. A new version, SMT-LIB 3.0, is currently being designed. It will notably introduce higher-order features and a better module system for theory representation and combination thereof. A preliminary proposal is available here
A simplistic formula in SMT-LIB format is provided below. The first line specifies the logic, i.e., the sorts (and their domain of interpretation) and symbols that are interpreted, particularly here allowing uninterpreted functions and linear arithmetic on integer to be used in the formula. Then a certain amount of symbols are declared. Formulas are asserted and the check-sat command notifies the solver that it should check the satisfiability of the above assertions.
(set-info :status unsat)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun f (Int Int) Int)
(declare-fun g (Int) Int)
(declare-fun h (Int Int) Int)
(assert (forall ((x Int) (y Int)) (> (f (g x) y) (h x y))))
(assert (= (f a b) 0))
(assert (= (h c b) 1))
(assert (forall ((x Int)) (= (g x) (+ x 2))))
(assert (= a 2))
(assert (= c 0))
(check-sat)
(exit)