Revision as of 12:08, 27 July 2016

Syntax

CVC4 supports the following syntax for declaring mutually recursive blocks of datatypes in *.smt2 input files:

 (declare-datatypes (U1...Un) 
   ((D1 (C1 (S1 T1)....(Si Ti))...(Cj .... ))
    ...
    (Dk (....) ... (....)))

where D1...Dk are datatype types, C1...Cj are the constructors for datatype D1, S1....Si are the selectors (or "destructors") of constructor C1, and each T1...Ti is a previously declared type or one of D1...k. The symbols U1...Un are type parameters (fresh symbols).

In addition to declaring symbols for constructors and selectors, the above command also adds tester (or "discriminator") symbols of the form "is-C" for each constructor C, which are unary predicates which evaluate to true iff their argument has top-symbol C.

Semantics

The decision procedure for inductive datatypes can be found here.

Example Declarations

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

Examples

 (declare-datatypes () 
   ((list (cons (head Int) (tail list)) (nil))))
 (declare-fun a () list)
 (declare-fun b () list)
 (assert (and (= (tail a) b) (not (is-nil b)) (> (head b) 0)))
 (check-sat)

Parametric Datatypes

Instances of parametric datatypes must have their arguments instantiated with concrete types. For instance, in the example:

 (declare-datatypes (T) ((list (cons (head T) (tail (list T))) (nil))))

To declare a list of Int, use the command:

 (declare-fun f () (List Int))

Use of constructors that are ambiguously typed must be cast to a concrete type, for instance all occurrences of "nil" for the above datatype must be cast with the syntax:

 (as nil (List Int))

Codatatypes

CVC4 also supports co-inductive datatypes, as described here. The syntax for declaring mutually recursive coinductive datatype blocks is identical to inductive datatypes, except that "declare-datatypes" is replaced by "declare-codatatypes". For example, the following declares the type denote streams of Int:

 (declare-codatatypes () 
   ((stream (cons (head Int) (tail stream)))))