Questions Columns Rows
GitHub icon

SMT

SMT - Programming language

< >

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

#902on PLDB 20Years Old 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

View source

- Build the next great programming language · Search · Add Language · Features · Creators · Resources · About · Blog · Acknowledgements · Stats · Sponsor · Traffic · Traffic Today · Day 280 · feedback@pldb.com · Logout