Languages Features Creators CSV Resources Challenges Add Language
GitHub icon

SMT

SMT - Programming language

< >

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.


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 Token Example
Comments
; A comment
Line Comments ;
; A comment
Semantic Indentation X

Publications about SMT from Semantic Scholar

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
wasp-lang.html · smt.html · ezhil.html

View source

- Build the next great programming language · Search · Day 214 · About · Blog · Acknowledgements · Traffic · Traffic Today · GitHub · feedback@pldb.com