Difference between revisions of "Datatypes"
(Created page with "CVC4 supports the following syntax for *.smt2 files: (declare-datatypes (T1...Tj) ((D1 (C1 (S1 [TYPE_1])....(Sn [TYPE_n])) .... (Cn .... )) …") |
|||
| Line 1: | Line 1: | ||
| − | CVC4 supports the following syntax for *.smt2 files: | + | CVC4 supports the following syntax for declaring mutually recursive blocks of datatypes in *.smt2 input files: |
(declare-datatypes (T1...Tj) ((D1 (C1 (S1 [TYPE_1])....(Sn [TYPE_n])) .... (Cn .... )) | (declare-datatypes (T1...Tj) ((D1 (C1 (S1 [TYPE_1])....(Sn [TYPE_n])) .... (Cn .... )) | ||
| Line 7: | Line 7: | ||
where D1...Dm are datatype types, C1...Cn are the constructors for datatype D1, S1....Sn are the selectors (or "destructors") of C1, and each TYPE_1...TYPE_n is a previously declared type or one of D1...Dm. | where D1...Dm are datatype types, C1...Cn are the constructors for datatype D1, S1....Sn are the selectors (or "destructors") of C1, and each TYPE_1...TYPE_n is a previously declared type or one of D1...Dm. | ||
| − | The symbols T1...Tj are "type parameters", if your datatypes are parametric (see below) | + | The symbols T1...Tj are "type parameters", if your datatypes are parametric (see below). |
Here are some examples: | Here are some examples: | ||
Revision as of 11:47, 27 July 2016
CVC4 supports the following syntax for declaring mutually recursive blocks of datatypes in *.smt2 input files:
(declare-datatypes (T1...Tj) ((D1 (C1 (S1 [TYPE_1])....(Sn [TYPE_n])) .... (Cn .... ))
...
(Dm (....) ... (....)))
where D1...Dm are datatype types, C1...Cn are the constructors for datatype D1, S1....Sn are the selectors (or "destructors") of C1, and each TYPE_1...TYPE_n is a previously declared type or one of D1...Dm.
The symbols T1...Tj are "type parameters", if your datatypes are parametric (see below).
Here are some examples: An enumeration: (declare-datatypes () ((Color (Red) (Black))))
A List of Int with "cons" and "nil" as constructors: (declare-datatypes () ((list (cons (head Int) (tail list)) (nil))))
A parametric List of T's: (declare-datatypes (T) ((list (cons (head T) (tail (list T))) (nil))))
Mutual recursion: (declare-codatatypes () ((list (cons (head tree) (tail list)) (nil))
(tree (node (data Int) (children list)))
))
