Differences
This shows you the differences between two versions of the page.
Next revision | Previous revision | ||
sav08:smt-lib_format [2008/03/06 17:56] vkuncak created |
sav08:smt-lib_format [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== SMT-LIB Format ====== | ====== SMT-LIB Format ====== | ||
- | Here [[http://combination.cs.uiowa.edu/smtlib/|official SMT-LIB page]]. | + | Here is the [[http://combination.cs.uiowa.edu/smtlib/|official SMT-LIB page]]. |
To check satisfiability of formula | To check satisfiability of formula | ||
- | \[ | + | \begin{equation*} |
(x = 2 \land x < y \land y < 0) \lor (x = y \land x < 3 \land 4 < y) | (x = 2 \land x < y \land y < 0) \lor (x = y \land x < 3 \land 4 < y) | ||
- | \] | + | \end{equation*} |
you can write the following file in SMT-LIB format: | you can write the following file in SMT-LIB format: | ||
<code> | <code> |