Differences
This shows you the differences between two versions of the page.
|
sav08:smt-lib_format [2008/03/06 17:56] vkuncak created |
sav08:smt-lib_format [2015/04/21 17:30] |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== SMT-LIB Format ====== | ||
| - | |||
| - | Here [[http://combination.cs.uiowa.edu/smtlib/|official SMT-LIB page]]. | ||
| - | |||
| - | To check satisfiability of formula | ||
| - | \[ | ||
| - | (x = 2 \land x < y \land y < 0) \lor (x = y \land x < 3 \land 4 < y) | ||
| - | \] | ||
| - | you can write the following file in SMT-LIB format: | ||
| - | <code> | ||
| - | (benchmark test | ||
| - | :extrafuns ((x Int) (y Int)) | ||
| - | |||
| - | :formula (or (and (= x 2) (< x y) (< y 0)) | ||
| - | (and (= x y) (< x 3) (< 4 y))) | ||
| - | ) | ||
| - | </code> | ||
| - | |||
| - | Here is the [[http://www.cs.nyu.edu/acsys/cvc3/|Web site for CVC3 prover]], with documentation and download. | ||
| - | |||
| - | To invoke CVC3 on file test.smt file in SMT-LIB format, use command line | ||
| - | cvc3 -lang smt test.smt | ||
| - | |||
| - | The prover should output "sat" or "unsat" on the standard output. | ||
| - | |||
| - | Formula $F$ is valid if the prover outpus "unsat" on a file encoding formula $\lnot F$. | ||