Revision as of 10:52, 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])....(Si [TYPE_i])) .... (Cj .... ))...(Dk (....) ... (....)))

where D1...Dk are datatype types, C_1...C_j 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 the datatypes in this block are parametric.

In addition to adding symbols for constructors C1,...,Cn, and selectors S1,

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