SMT - Programming language

home edit

SMT, aka Satisfiability Modulo Theories, is a programming language created in 2003.

#935on PLDB

21Years Old

582Repos

Homepage

Common input and output languages for SMT solvers.

Tags: programming language
There are at least 582 SMT repos on GitHub
Early development of SMT happened in University of Iowa
The Google BigQuery Public Dataset GitHub snapshot shows 130 users using SMT in 149 repos on GitHub
GitHub supports syntax highlighting for SMT

Example from the web:

; Getting assertions
(set-option :produce-assertions true)
(set-logic QF_UF)
(declare-const p Bool) (declare-const q Bool)
(push 1)
 (assert (or p q))
 (push 1)
  (assert (not q))
  (get-assertions)
  ; ((or p q)
  ;  (not q)
  ; )
 (pop 1)
  (get-assertions)
 ; ((or p q))
 (pop 1)
 (get-assertions)
 ; ()
(exit)

Example from Linguist:

(set-logic QF_LIA)
(set-info :source | SMT-COMP'06 organizers |)
(set-info :smt-lib-version 2.0)
(set-info :category "check")
(set-info :status unsat)
(set-info :notes |This benchmark is designed to check if the DP supports bignumbers.|)
(declare-fun x1 () Int)
(declare-fun x2 () Int)
(declare-fun x3 () Int)
(declare-fun x4 () Int)
(declare-fun x5 () Int)
(declare-fun x6 () Int)
(assert (and (or (>= x1 1000) (>= x1 1002))
             (or (>= x2 (* 1230 x1)) (>= x2 (* 1003 x1)))
			 (or (>= x3 (* 1310 x2)) (>= x3 (* 1999 x2)))
			 (or (>= x4 (* 4000 x3)) (>= x4 (* 8000 x3)))
			 (or (<= x5 (* (- 4000) x4)) (<= x5 (* (- 8000) x4)))
			 (or (>= x6 (* (- 3) x5)) (>= x6 (* (- 2) x5))) (< x6 0)))
(check-sat)
(exit)

Language features

Feature	Supported	Example	Token
Comments	✓	; A comment
Line Comments	✓	; A comment	;
Semantic Indentation	X