SMT-LIB

https://smt-lib.org
Admin
SMT-LIB is an international initiative providing standard descriptions of background theories,...
Tokens:33,323
Snippets:223
Trust Score:8.9
Update:1 week ago
Show doc for...
Tokens:
Raw
### Getting Values or Models

Source: https://smt-lib.org/examples.shtml

Enables model production and uses get-value and get-model to retrieve satisfying assignments. The example shows a sat result with x=8 and y=6.

```smt2
; Getting values or models
(set-option :print-success false)
(set-option :produce-models true)
(set-logic QF_LIA)
(declare-const x Int)
(declare-const y Int)
(assert (= (+ x (* 2 y)) 20))
(assert (= (- x y) 2))
(check-sat)
; sat
(get-value (x y))
; ((x 8) (y 6))
(get-model)
; ((define-fun x () Int 8)
;  (define-fun y () Int 6)
; )
(exit)
```

--------------------------------

### Basic Boolean Example

Source: https://smt-lib.org/examples.shtml

Checks satisfiability of a contradictory Boolean formula. Expects 'unsat' from check-sat.

```smt2
; Basic Boolean example
(set-option :print-success false)
(set-logic QF_UF)
(declare-const p Bool)
(assert (and p (not p))) 
(check-sat) ; returns 'unsat'
(exit)
```

--------------------------------

### Getting Info

Source: https://smt-lib.org/examples.shtml

Queries solver metadata such as name, version, and authors. The output shows CVC4 version 4.0.

```smt2
; Getting info
(get-info :name)
; (:name "CVC4")
(get-info :version )
; (:version "4.0" )
(get-info :authors )
; (:authors "The CVC4 Team" )
(exit)
```

--------------------------------

### Integer Arithmetic Example

Source: https://smt-lib.org/examples.shtml

Solves a linear integer arithmetic constraint. The formula is unsatisfiable, so check-sat returns 'unsat'.

```smt2
; Integer arithmetic
(set-logic QF_LIA)
(declare-const x Int)
(declare-const y Int)
(assert (= (- x y) (+ x (- y) 1)))
(check-sat)
; unsat
(exit)
```

--------------------------------

### Getting Assertions

Source: https://smt-lib.org/examples.shtml

Enables assertion retrieval and uses push/pop to show how get-assertions returns the current assertion stack. The output shows the assertions at each scope level.

```smt2
; 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)
```
Tokens:
Raw