Datatypes

CVC4 supports the following syntax for *.smt2 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). In most use cases, this is empty.

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

))