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

16Years Old 5Users 0Jobs
  • The Satisfiability Modulo Theories Library ranks in the top 50% of languages
  • the The Satisfiability Modulo Theories Library website
  • The Satisfiability Modulo Theories Library first appeared in 2003
  • file extensions for The Satisfiability Modulo Theories Library include smt2 and smt
  • I have 28 facts about The Satisfiability Modulo Theories Library. what would you like to know? email me and let me know how I can help.

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)

Trending Repos

repo stars description

Last updated November 16th, 2019