Difference between revisions of "Datatypes"
From CVC4
| Line 1: | Line 1: | ||
| + | =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 (T1...Tj) ((D1 (C1 (S1 [TYPE_1])....(Sn [TYPE_n])) .... (Cn .... ))...(Dm (....) ... (....))) | (declare-datatypes (T1...Tj) ((D1 (C1 (S1 [TYPE_1])....(Sn [TYPE_n])) .... (Cn .... ))...(Dm (....) ... (....))) | ||
| Line 4: | Line 5: | ||
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). | 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). | ||
| − | + | =Examples= | |
An enumeration: | An enumeration: | ||
(declare-datatypes () ((Color (Red) (Black)))) | (declare-datatypes () ((Color (Red) (Black)))) | ||
Revision as of 10:49, 27 July 2016
Syntax
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).
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)))))
