SMT

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

#893on PLDB	20Years Old	201Users
0Books	7Papers	582Repos

Common input and output languages for SMT solvers.

SMT website
There are at least 582 SMT repos on GitHub
file extensions for SMT include smt2 and smt
The Google BigQuery Public Dataset GitHub snapshot shows 130 users using SMT in 149 repos on GitHub
GitHub supports syntax highlighting for SMT
HTML of this page generated by LanguagePage.ts

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)

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

title	authors	year	citations	influentialCitations
Scala to the Power of Z3: Integrating SMT and Programming	A. Köksal and Viktor Kuncak and Philippe Suter	2011	40	0
SMT Solving for Functional Programming over Infinite Structures	Bartek Klin and Michal Szynwelski	2016	19	2
SMT in Verification, Modeling, and Testing at Microsoft	N. Bjørner	2012	3	0
Effective Encodings of Constraint Programming Models to SMT	E. Davidson and Ozgur Akgun and Joan Espasa and P. Nightingale	2020	3	0
Inter-theory dependency analysis for SMT string solvers	Minh-Thai Trinh and D. Chu and J. Jaffar	2020	2	1
Using SMT Solver and Logic Puzzles for Teaching Computational Logics in Discrete Mathematics Class	Shin Hong	2020	1	0
Programming Behavioral Test Models for SMT Solving in Scala	B. Aichernig and Benedikt Maderbacher and Stefan Tiran	2019	1	0

SMT - Programming language

Language features

Publications about SMT from Semantic Scholar