Theory Reference: Datatypes

Logic

To enable cvc5’s decision procedure for datatypes, include DT in the logic:

(set-logic QF_DT)

Alternatively, use the ALL logic:

(set-logic ALL)

Syntax

cvc5 supports the following syntax for declaring mutually recursive blocks of datatypes in *.smt2 input files in the smt lib 2.6 format:

(declare-datatypes ((D1 n1) ... (Dk nk))
 (((C1 (S11 T1) ... (S1i Ti)) ... (Cj ... ))
  ...
  ((...) ... (...)))

where D1 ... Dk are datatype types, C1 ... Cj are the constructors for datatype D1, S11 ... S1i are the selectors (or “destructors”) of constructor C1, and each T1 ... Ti is a previously declared type or one of D1 ... Dk. The numbers n1 ... nk denote the number of type parameters for the datatype, where 0 is used for non-parametric datatypes.

In addition to declaring symbols for constructors and selectors, the above command also allows for tester (or “discriminator”) indexed 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. It also allows for updater indexed symbols of the form (_ update Sij) for each selector Sij, whose semantics are described below.

Semantics

The decision procedure for inductive datatypes is described in [BST07].

Example Declarations

An enumeration:

(declare-datatypes ((Color 0))
 (((Red) (Black))))

A List of Int with cons and nil as constructors:

(declare-datatypes ((list 0))
 (((cons (head Int) (tail list)) (nil))))

A parametric List of T’s:

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

Mutual recursion:

(declare-datatypes ((list 0) (tree 0))
 (((cons (head tree) (tail list)) (nil))
  ((node (data Int) (children list)))))

A (non-recursive) record type:

(declare-datatypes ((record 0))
 (((rec (fname String) (lname String) (id Int)))))

Examples

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

(declare-datatypes ((record 0))
  (((rec (fname String) (lname String) (id Int)))))
(declare-const x record)
(assert (and (= (fname x) "John") (= (lname x) "Smith")))
(check-sat)

Datatype Updaters

Datatype updaters are a (non-standard) extension available in datatype logics. The term:

((_ update Sij) t u)

is equivalent to replacing the field of t denoted by the selector Sij with the value u, or t itself if that selector does not apply to the constructor symbol of t. For example, for the list datatype, we have that:

((_ update head) (cons 4 nil) 7) = (cons 7 nil)
((_ update tail) (cons 4 nil) (cons 5 nil)) = (cons 4 (cons 5 nil))
((_ update head) nil 5) = nil

Note that datatype updaters can be seen as syntax sugar for an if-then-else term that checks whether the constructor of t is the same as the one associated with the given selector.

Parametric Datatypes

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

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

To declare a list of Int, use the command:

(declare-const 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))

Tuples

Tuples are a particular instance of an inductive datatype. cvc5 supports special syntax for tuples as an extension of the SMT-LIB version 2 format. For example:

(declare-const t (Tuple Int Int))
(assert (= ((_ tuple.select 0) t) 3))
(assert (not (= t (tuple 3 4))))

Codatatypes

cvc5 also supports co-inductive datatypes, as described in [RB15].

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 0))
 (((cons (head Int) (tail stream)))))

Syntax/API

For the C++ API examples in the table below, we assume that we have created a cvc5::Solver solver object.