The Satisfiability Modulo Theories Library, aka Satisfiability Modulo Theories, is an actively used programming language created in 2003.

16Years Old 1,005Users 0Jobs
  • The Satisfiability Modulo Theories Library ranks in the bottom 50% of languages
  • the The Satisfiability Modulo Theories Library website
  • The Satisfiability Modulo Theories Library first appeared in 2003
  • I have 26 facts about The Satisfiability Modulo Theories Library. just email me if you need more.

Example code 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 code 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)
Edit

Last updated February 11th, 2019