Datatypes

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)))

))