-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathexamples.shtml
300 lines (279 loc) · 7.64 KB
/
examples.shtml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<!--
Design by http://www.bluewebtemplates.com
Released for free under a Creative Commons Attribution 3.0 License
-->
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>SMT-LIB The Satisfiability Modulo Theories Library</title>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
<link href="style.css" rel="stylesheet" type="text/css" />
<!-- CuFon: Enables smooth pretty custom font rendering. 100% SEO friendly. To disable, remove this section -->
<script type="text/javascript" src="js/cufon-yui.js"></script>
<script type="text/javascript" src="js/arial.js"></script>
<script type="text/javascript" src="js/cuf_run.js"></script>
<!-- CuFon ends -->
<link href="code-prettify/prettify.css" type="text/css" rel="stylesheet" />
<script src="code-prettify/run_prettify.js?lang=smtlib&skin=desert"></script>
</head>
<body>
<div class="main">
<div class="header">
<div class="header_resize">
<div class="menu_nav">
<ul>
<li><a href="index.shtml">Home</a></li>
<li><a href="about.shtml">About</a></li>
<li><a href="news.shtml">News</a></li>
<li class="active"><a href="standard.shtml">Standard</a></li>
<li><a href="benchmarks.shtml">Benchmarks</a></li>
<li><a href="software.shtml">Software</a></li>
<li><a href="credits.shtml">Credits</a></li>
</ul>
</div>
<div class="clr"></div>
<div class="logo">
<h1><a href="index.shtml">SMT-LIB <br/>
<small>The Satisfiability Modulo Theories Library</small></a>
</h1>
</div>
</div>
</div>
<div class="content">
<div class="content_resize">
<div class="mainbar">
<h2>Examples</h2>
<pre class="prettyprint lang-smtlib">; 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)</pre>
<br>
<pre class="prettyprint lang-smtlib">; Integer arithmetic
(set-logic QF_LIA)(declare-const x Int)(declare-const y Int)(assert (= (- x y) (+ x (- y) 1)))
(check-sat); unsat
(exit)</pre>
<br>
<pre class="prettyprint lang-smtlib">; 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)</pre>
<br>
<pre class="prettyprint lang-smtlib">; Modeling sequential code in SSA form
;; Buggy swap
; int x, y;
; int t = x;
; x = y;
; y = x;
(set-logic QF_UFLIA)
(set-option :produce-models true)
(declare-fun x (Int) Int) (declare-fun y (Int) Int)
(declare-fun t (Int) Int)
(assert (= (t 0) (x 0)))
(assert (= (y 1) (t 0)))
(assert (= (x 1) (y 1)))
(assert (not
(and (= (x 1) (y 0))
(= (y 1) (x 0)))))
(check-sat)
(get-value ((x 0) (y 0) (x 1) (y 1)))
; possible returned valuation:
; (((x 0) (- 1)) ((y 0) 2) ((x 1) (- 1)) ((y 1) (- 1)))
(get-model)
; possible returned model:
; (
; (define-fun x ((_ufmt_1 Int)) Int (- 1))
; (define-fun y ((_ufmt_1 Int)) Int (ite (= _ufmt_1 1) (- 1) 2))
; (define-fun t ((_ufmt_1 Int)) Int (- 1))
; )
(exit)</pre>
<br>
<pre class="prettyprint lang-smtlib">; Modeling sequential code with bitvectors
;; Correct swap with no temp var
; int x, y;
; x = x + y;
; y = x - y;
; x = x - y;
(set-logic QF_BV)
(set-option :produce-models true)
(declare-const x_0 (_ BitVec 32))
(declare-const x_1 (_ BitVec 32))
(declare-const x_2 (_ BitVec 32))
(declare-const y_0 (_ BitVec 32))
(declare-const y_1 (_ BitVec 32))
(assert (= x_1 (bvadd x_0 y_0)))
(assert (= y_1 (bvsub x_1 y_0)))
(assert (= x_2 (bvsub x_1 y_1)))
(assert (not
(and (= x_2 y_0)
(= y_1 x_0))))
(check-sat)
; unsat
(exit)</pre>
<br>
<pre class="prettyprint lang-smtlib">; Using scopes to explore multiple problems
(set-option :print-success false)(set-logic QF_LIA)(declare-const x Int) (declare-const y Int)(assert (= (+ x (* 2 y)) 20))(push 1) (assert (= (- x y) 2)) (check-sat) ; sat(pop 1)(push 1) (assert (= (- x y) 3)) (check-sat) ; unsat(pop 1)(exit)</pre>
<br>
<pre class="prettyprint lang-smtlib">; Defining and using new sorts
(set-option :print-success false)(set-logic QF_UF)(declare-sort A 0)(declare-const a A) (declare-const b A) (declare-const c A)(declare-const d A) (declare-const e A)(assert (or (= c a)(= c b)))(assert (or (= d a)(= d b)))(assert (or (= e a)(= e b)))(push 1) (assert (distinct c d)) (check-sat) ; sat(pop 1)(push 1) (assert (distinct c d e)) (check-sat) ; unsat(pop 1)(exit)</pre>
<br>
<pre class="prettyprint lang-smtlib">; Getting info
(get-info :name); (:name "CVC4")
(get-info :version ); (:version "4.0" )(get-info :authors ); (:authors "The CVC4 Team" )(exit)</pre>
<br>
<pre class="prettyprint lang-smtlib">; Getting assignments
(set-option :produce-assignments true)(set-logic QF_UF)(declare-const p Bool) (declare-const q Bool) (declare-const r Bool)(assert (not (=(! (and (! p :named P) q) :named PQ) (! r :named R))))(check-sat); sat(get-assignment); ((P true) (R false) (PQ true))
(exit)</pre>
<br>
<pre class="prettyprint lang-smtlib">; Getting unsatisfiable cores
(set-option :produce-unsat-cores true)(set-logic QF_UF)(declare-const p Bool) (declare-const q Bool) (declare-const r Bool)(declare-const s Bool) (declare-const t Bool)(assert (! (=> p q) :named PQ))(assert (! (=> q r) :named QR))(assert (! (=> r s) :named RS))(assert (! (=> s t) :named ST))(assert (! (not (=> q s)) :named NQS))(check-sat); unsat(get-unsat-core); (QR RS NQS)
(exit)</pre>
<br>
<pre class="prettyprint lang-smtlib">; 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)</pre>
<br>
</div>
<div class="sidebar">
<div class="gadget">
<ul class="sb_menu">
<li><a href="index.shtml">Home</a></li>
<li><a href="about.shtml">About</a></li>
<li><a href="news.shtml">News</a></li>
<li>Standard
<ul class="ex_menu">
<li><a href="language.shtml">Language</a>
<li><a href="theories.shtml">Theories</a>
<li><a href="logics.shtml">Logics</a>
<li><a href="examples.shtml">Examples</a>
</ul>
</li>
<li><a href="benchmarks.shtml">Benchmarks</a></li>
<li>Software
<ul class="ex_menu">
<li><a href="solvers.shtml">Solvers</a></li>
<li><a href="utilities.shtml">Utilities</a></li>
</ul>
</li>
<li><a href="contact.shtml">Contact</a></li>
<li><a href="related.shtml">Related</a></li>
<li><a href="credits.shtml">Credits</a></li>
</ul>
</div>
</div>
</div>
</div>
<div class="clr"></div>
<div class="footer">
<div class="footer_resize">
<p class="lf">
© Copyright The SMT-LIB Initiative <br>
Based on a design by
Blue <a href="http://www.bluewebtemplates.com">Web Templates</a>
</p>
<ul class="fmenu">
<li><a href="index.shtml">Home</a></li>
<li><a href="about.shtml">About</a></li>
<li><a href="news.shtml">News</a></li>
<li class="active"><a href="standard.shtml">Standard</a></li>
<li><a href="benchmarks.shtml">Benchmarks</a></li>
<li><a href="software.shtml">Software</a></li>
<li><a href="credits.shtml">Credits</a></li>
</ul>
<div class="clr"></div>
</div>
</div>
</div>
</body>
</html>