projects / cvc5.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
api: Rename get(Selector|Constructor)Term() to getTerm(). (#8537)
[cvc5.git] / docs / theories / datatypes.rst
1 Theory Reference: Datatypes
2 ===========================
3
4 cvc5 implements some extensions to the support for datatypes in SMT-LIB 2.
5
6 Logic
7 -----
8
9 To enable cvc5's decision procedure for datatypes, include ``DT`` in the logic:
10
11 .. code:: smtlib
12
13 (set-logic QF_DT)
14
15 Alternatively, use the ``ALL`` logic:
16
17 .. code:: smtlib
18
19 (set-logic ALL)
20
21 Syntax
22 ------
23
24 cvc5 supports the following syntax for declaring mutually recursive blocks of
25 datatypes in ``*.smt2`` input files in the smt lib 2.6 format:
26
27 .. code:: smtlib
28
29 (declare-datatypes ((D1 n1) ... (Dk nk))
30 (((C1 (S11 T1) ... (S1i Ti)) ... (Cj ... ))
31 ...
32 ((...) ... (...)))
33
34 where ``D1 ... Dk`` are datatype types, ``C1 ... Cj`` are the constructors for
35 datatype ``D1``,
36 ``S11 ... S1i`` are the selectors (or "destructors") of constructor ``C1``, and
37 each ``T1 ... Ti`` is a previously declared type or one of ``D1 ... Dk``.
38 The numbers ``n1 ... nk`` denote the number of type
39 parameters for the datatype, where ``0`` is used for non-parametric datatypes.
40
41 In addition to declaring symbols for constructors and selectors, the above
42 command also allows for tester (or "discriminator") indexed symbols of the form
43 ``(_ is C)`` for each constructor ``C``, which are unary predicates which
44 evaluate to true iff their argument has top-symbol ``C``. It also allows for
45 updater indexed symbols of the form ``(_ update Sij)`` for each selector ``Sij``,
46 whose semantics are described below.
47
48 Semantics
49 ---------
50
51 The decision procedure for inductive datatypes is described in
52 :cite:`BarrettST07`.
53
54 Example Declarations
55 --------------------
56
57 An enumeration:
58
59 .. code:: smtlib
60
61 (declare-datatypes ((Color 0))
62 (((Red) (Black))))
63
64 A List of ``Int`` with ``cons`` and ``nil`` as constructors:
65
66 .. code:: smtlib
67
68 (declare-datatypes ((list 0))
69 (((cons (head Int) (tail list)) (nil))))
70
71 A parametric List of T's:
72
73 .. code:: smtlib
74
75 (declare-datatypes ((list 1))
76 ((par (T) ((cons (head T) (tail (list T))) (nil)))))
77
78 Mutual recursion:
79
80 .. code:: smtlib
81
82 (declare-datatypes ((list 0) (tree 0))
83 (((cons (head tree) (tail list)) (nil))
84 ((node (data Int) (children list)))))
85
86 A (non-recursive) record type:
87
88 .. code:: smtlib
89
90 (declare-datatypes ((record 0))
91 (((rec (fname String) (lname String) (id Int)))))
92
93
94 Examples
95 --------
96
97 .. code:: smtlib
98
99 (declare-datatypes ((list 0))
100 (((cons (head Int) (tail list)) (nil))))
101 (declare-const a list)
102 (declare-const b list)
103 (assert (and (= (tail a) b) (not ((_ is nil) b)) (> (head b) 0)))
104 (check-sat)
105
106 .. code:: smtlib
107
108 (declare-datatypes ((record 0))
109 (((rec (fname String) (lname String) (id Int)))))
110 (declare-const x record)
111 (assert (and (= (fname x) "John") (= (lname x) "Smith")))
112 (check-sat)
113
114 Datatype Updaters
115 --------------------
116
117 Datatype updaters are a (non-standard) extension available in datatype logics.
118 The term:
119
120 .. code:: smtlib
121 ((_ update Sij) t u)
122
123 is equivalent to replacing the field of ``t`` denoted by the selector ``Sij``
124 with the value ``u``, or ``t`` itself if that selector does not apply to the
125 constructor symbol of ``t``. For example, for the list datatype, we have that:
126
127 .. code:: smtlib
128 ((_ update head) (cons 4 nil) 7) = (cons 7 nil)
129 ((_ update tail) (cons 4 nil) (cons 5 nil)) = (cons 4 (cons 5 nil))
130 ((_ update head) nil 5) = nil
131
132 Note that datatype updaters can be seen as syntax sugar for an if-then-else
133 term that checks whether the constructor of ``t`` is the same as the one
134 associated with the given selector.
135
136 Parametric Datatypes
137 --------------------
138
139 Instances of parametric datatypes must have their arguments instantiated with
140 concrete types. For instance, in the example:
141
142 .. code:: smtlib
143
144 (declare-datatypes ((list 1)) ((par (T) (cons (head T) (tail (list T))) (nil))))
145
146 To declare a list of ``Int``, use the command:
147
148 .. code:: smtlib
149
150 (declare-const f (list Int))
151
152 Use of constructors that are ambiguously typed must be cast to a concrete type,
153 for instance all occurrences of ``nil`` for the above datatype must be cast with
154 the syntax:
155
156 .. code:: smtlib
157
158 (as nil (list Int))
159
160 Tuples
161 ------
162
163 Tuples are a particular instance of an inductive datatype. cvc5 supports
164 special syntax for tuples as an extension of the SMT-LIB version 2 format.
165 For example:
166
167 .. code:: smtlib
168
169 (declare-const t (Tuple Int Int))
170 (assert (= ((_ tuple.select 0) t) 3))
171 (assert (not (= t (tuple 3 4))))
172
173
174 Codatatypes
175 -----------
176
177 cvc5 also supports co-inductive datatypes, as described in
178 :cite:`ReynoldsB15`.
179
180 The syntax for declaring mutually recursive coinductive datatype blocks is
181 identical to inductive datatypes, except that ``declare-datatypes`` is replaced
182 by ``declare-codatatypes``. For example, the following declares the type denote
183 streams of ``Int``:
184
185 .. code:: smtlib
186
187 (declare-codatatypes ((stream 0))
188 (((cons (head Int) (tail stream)))))
189
190
191 Syntax/API
192 ----------
193
194 For the C++ API examples in the table below, we assume that we have created
195 a `cvc5::Solver solver` object.
196
197 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
198 | | SMTLIB language | C++ API |
199 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
200 | Logic String | ``(set-logic QF_DT)`` | ``solver.setLogic("QF_DT");`` |
201 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
202 | Datatype Sort | ``(declare-datatype ...)`` | ``Sort s = solver.mkDatatypeSort(...);`` |
203 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
204 | Datatype Sorts | ``(declare-datatypes ...)`` | ``std::vector<Sort> s = solver.mkDatatypeSorts(...);`` |
205 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
206 | Constructor | ``(Ci <Term_1>, ..., <Term_n>)`` | ``Sort s = solver.mkDatatypeSort(...);`` |
207 | | | |
208 | | | ``Datatype dt = s.getDatatype();`` |
209 | | | |
210 | | | ``Term ci = dt[i].getTerm();`` |
211 | | | |
212 | | | ``Term r = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {ci, <Term_1>, ..., <Term_n>});`` |
213 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
214 | Selector | ``(Sij t)`` | ``Sort s = solver.mkDatatypeSort(...);`` |
215 | | | |
216 | | | ``Datatype dt = s.getDatatype();`` |
217 | | | |
218 | | | ``Term sij = dt[i].getSelector(j).getTerm();`` |
219 | | | |
220 | | | ``Term r = solver.mkTerm(Kind::APPLY_SELECTOR, {sij, t});`` |
221 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
222 | Updater | ``((_ update Sij) t u)`` | ``Sort s = solver.mkDatatypeSort(...);`` |
223 | | | |
224 | | | ``Datatype dt = s.getDatatype();`` |
225 | | | |
226 | | | ``Term upd = dt[i].getSelector(j).getUpdaterTerm();`` |
227 | | | |
228 | | | ``Term r = solver.mkTerm(Kind::APPLY_UPDATER, {upd, t, u});`` |
229 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
230 | Tester | ``((_ is Ci) t)`` | ``Sort s = solver.mkDatatypeSort(...);`` |
231 | | | |
232 | | | ``Datatype dt = s.getDatatype();`` |
233 | | | |
234 | | | ``Term upd = dt[i].getTesterTerm();`` |
235 | | | |
236 | | | ``Term r = solver.mkTerm(Kind::APPLY_TESTER, {upd, t, u});`` |
237 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
238 | Tuple Sort | ``(Tuple <Sort_1>, ..., <Sort_n>)`` | ``std::vector<cvc5::Sort> sorts = { ... };`` |
239 | | | |
240 | | | ``Sort s = solver.mkTupleSort(sorts);`` |
241 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
242 | | ``(declare-const t (Tuple Int Int))`` | ``Sort s_int = solver.getIntegerSort();`` |
243 | | | |
244 | | | ``Sort s = solver.mkTupleSort({s_int, s_int});`` |
245 | | | |
246 | | | ``Term t = solver.mkConst(s, "t");`` |
247 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
248 | Tuple Constructor | ``(tuple <Term_1>, ..., <Term_n>)`` | ``Sort s = solver.mkTupleSort(sorts);`` |
249 | | | |
250 | | | ``Datatype dt = s.getDatatype();`` |
251 | | | |
252 | | | ``Term c = dt[0].getTerm();`` |
253 | | | |
254 | | | ``Term r = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {c, <Term_1>, ..., <Term_n>});`` |
255 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
256 | Tuple Selector | ``((_ tuple.select i) t)`` | ``Sort s = solver.mkTupleSort(sorts);`` |
257 | | | |
258 | | | ``Datatype dt = s.getDatatype();`` |
259 | | | |
260 | | | ``Term sel = dt[0].getSelector(i).getTerm();`` |
261 | | | |
262 | | | ``Term r = solver.mkTerm(Kind::APPLY_SELECTOR, {sel, t});`` |
263 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
264 | Tuple Updater | ``((_ tuple.update i) t u)`` | ``Sort s = solver.mkTupleSort(sorts);`` |
265 | | | |
266 | | | ``Datatype dt = s.getDatatype();`` |
267 | | | |
268 | | | ``Term upd = dt[0].getSelector(i).getUpdaterTerm();`` |
269 | | | |
270 | | | ``Term r = solver.mkTerm(Kind::APPLY_UPDATER, {upd, t, u});`` |
271 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
272 | Tuple Projection | ``((_ tuple.project i1 ... in) t)`` | ``Sort s = solver.mkTupleSort(sorts);`` |
273 | | | |
274 | | | ``Datatype dt = s.getDatatype();`` |
275 | | | |
276 | | | ``Term proj = solver.mkOp(Kind::TUPLE_PROJECT, {i1, ..., in});`` |
277 | | | |
278 | | | ``Term r = solver.mkTerm(Kind::TUPLE_PROJECT, {proj, t});`` |
279 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
280 | Record Sort | n/a | ``Sort s = mkRecordSort(const std::vector<std::pair<std::string, Sort>>& fields);`` |
281 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
282 | | n/a | ``std::vector<std::pair<std::string, Sort>> fields;`` |
283 | | | |
284 | | | ``fields.push_back(std::pair<std::string, Sort>("fst", solver.getIntegerSort()));`` |
285 | | | |
286 | | | ``fields.push_back(std::pair<std::string, Sort>("snd", solver.getIntegerSort()));`` |
287 | | | |
288 | | | ``Sort s = mkRecordSort(fields);`` |
289 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
290 | Record Constructor | n/a | ``Sort s = mkRecordSort(fields);`` |
291 | | | |
292 | | | ``Datatype dt = s.getDatatype();`` |
293 | | | |
294 | | | ``Term c = dt[0].getTerm();`` |
295 | | | |
296 | | | ``Term r = solver.mkTerm(Kind::APPLY_CONSTRUCTOR, {c, <Term_1>, ..., <Term_n>});`` |
297 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
298 | Record Selector | n/a | ``Sort s = mkRecordSort(fields);`` |
299 | | | |
300 | | | ``Datatype dt = s.getDatatype();`` |
301 | | | |
302 | | | ``Term sel = dt[0].getSelector(name).getSelectorTerm();`` |
303 | | | |
304 | | | ``Term r = solver.mkTerm(Kind::APPLY_SELECTOR, {sel, t});`` |
305 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+
306 | Record Updater | n/a | ``Sort s = solver.mkRecordSort(sorts);`` |
307 | | | |
308 | | | ``Datatype dt = s.getDatatype();`` |
309 | | | |
310 | | | ``Term upd = dt[0].getSelector(name).getUpdaterTerm();`` |
311 | | | |
312 | | | ``Term r = solver.mkTerm(Kind::APPLY_UPDATER, {upd, t, u});`` |
313 +--------------------+----------------------------------------+---------------------------------------------------------------------------------------------------------------------------------+