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