Difference between revisions of "Datatypes"
From CVC4
| Line 11: | Line 11: | ||
Here are some examples: | Here are some examples: | ||
An enumeration: | An enumeration: | ||
| − | (declare-datatypes () ((Color (Red) (Black)))) | + | (declare-datatypes () ((Color (Red) (Black)))) |
A List of Int with "cons" and "nil" as constructors: | A List of Int with "cons" and "nil" as constructors: | ||
| − | (declare-datatypes () ((list (cons (head Int) (tail list)) (nil)))) | + | (declare-datatypes () ((list (cons (head Int) (tail list)) (nil)))) |
A parametric List of T's: | A parametric List of T's: | ||
| − | (declare-datatypes (T) ((list (cons (head T) (tail (list T))) (nil)))) | + | (declare-datatypes (T) ((list (cons (head T) (tail (list T))) (nil)))) |
Mutual recursion: | Mutual recursion: | ||
| − | (declare-codatatypes () ((list (cons (head tree) (tail list)) (nil)) | + | (declare-codatatypes () ((list (cons (head tree) (tail list)) (nil))(tree (node (data Int) (children list))))) |
| − | + | ||
| − | )) | + | |
Revision as of 10:48, 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)))))
