Difference between revisions of "Datatypes"
| Line 1: | Line 1: | ||
=Syntax= | =Syntax= | ||
CVC4 supports the following syntax for declaring mutually recursive blocks of datatypes in *.smt2 input files: | CVC4 supports the following syntax for declaring mutually recursive blocks of datatypes in *.smt2 input files: | ||
| − | (declare-datatypes ( | + | (declare-datatypes (U1...Un) ((D1 (C1 (S1 T1)....(Si Ti)) .... (Cj .... ))...(Dk (....) ... (....))) |
| − | where D1...Dk are datatype types, | + | where D1...Dk are datatype types, C1...Cj are the constructors for datatype D1, S1....Si are the selectors (or "destructors") of constructor C1, and each T1...Ti is a previously declared type or one of D1...k. The symbols U1...Un are "type parameters", if the datatypes in this block are parametric. |
| − | In addition to | + | In addition to declaring symbols for constructors and selectors, the above command also adds tester symbols of the form is-C1,...,is-Cn for constructors C1,...Cn. |
=Examples= | =Examples= | ||
| Line 19: | Line 19: | ||
Mutual recursion: | Mutual recursion: | ||
(declare-codatatypes () ((list (cons (head tree) (tail list)) (nil))(tree (node (data Int) (children list))))) | (declare-codatatypes () ((list (cons (head tree) (tail list)) (nil))(tree (node (data Int) (children list))))) | ||
| + | |||
| + | =Parametric Datatypes= | ||
| + | |||
| + | Instances of parametric datatypes must have their arguments instantiated with concrete types. For instance, in the example: | ||
| + | (declare-datatypes (T) ((list (cons (head T) (tail (list T))) (nil)))) | ||
| + | |||
| + | To declare a list of Int, use the command: | ||
| + | (declare-fun f () (List Int)) | ||
| + | |||
| + | Since | ||
Revision as of 10:56, 27 July 2016
Syntax
CVC4 supports the following syntax for declaring mutually recursive blocks of datatypes in *.smt2 input files:
(declare-datatypes (U1...Un) ((D1 (C1 (S1 T1)....(Si Ti)) .... (Cj .... ))...(Dk (....) ... (....)))
where D1...Dk are datatype types, C1...Cj are the constructors for datatype D1, S1....Si are the selectors (or "destructors") of constructor C1, and each T1...Ti is a previously declared type or one of D1...k. The symbols U1...Un are "type parameters", if the datatypes in this block are parametric.
In addition to declaring symbols for constructors and selectors, the above command also adds tester symbols of the form is-C1,...,is-Cn for constructors C1,...Cn.
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)))))
Parametric Datatypes
Instances of parametric datatypes must have their arguments instantiated with concrete types. For instance, in the example:
(declare-datatypes (T) ((list (cons (head T) (tail (list T))) (nil))))
To declare a list of Int, use the command:
(declare-fun f () (List Int))
Since
