[SMT-LIB] Adding algebraic datatypes to the SMT-LIB 2 language: an initial proposal

[Tinelli, Cesare]

Hi all,

In response to several requests to add algebraic datatypes to the SMT-LIB 2 language, we would like to propose an extension to Version 2.5 that supports that.

>From the point of view of the language, this addition is substantial. Datatypes cannot be formulated as a theory in SMT-LIB because, typically, applications need to define their own datatypes on the fly. As a consequence, we have to extend both the SMT-LIB concrete language and its semantics to make datatypes user-definable.

A draft of a new version of SMT-LIB, Version 2.6, that incorporates datatypes and gives a few examples can be found at 

 http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-draft-1.pdf

The datatype-related text is in red. You can find quickly it by searching for "adts" in the PDF file.

In brief, the proposed extension adds a new command (declare-datatype) to declare a single, possibly recursive, datatype and one (declare-datatypes) to declare several, possibly mutually recursive, datatypes at once. The former is just an abbreviation of the latter. With either command, the declared datatypes can be parametric. 

-----------------------------------------------
Examples:

; an enumeration datatype
(declare-datatype Color ( (red) (green) (blue) ))

; integer lists with "empty" and "insert" constructors
(declare datatype IntList
  ( (empty) (insert (head Int) (tail IntList) )))

; parametric lists with "nil" and "cons" constructors
(declare -datatype List (par (T)
  ( (nil) (cons (car T) (cdr (List T)) ))))

; option datatype
(declare datatype Option (par (X) ( (none) (some (val X) ))))

; parametric pairs
(declare datatype Pair (par (X Y)
  ( (pair (first X) (second X)) ))))

; two mutually recursive datatypes
(declare-datatypes ( (Tree 1) (TreeList 1) ) (
  ; Tree
  (par (X) ( (node (value X) (children (TreeList X)) )))
  ; TreeList
  (par (Y) ( (empty) 
    (insert (head (Tree Y)) (tail (TreeList Y))) ))))

-----------------------------------------------

In declare-datatypes, the arity of each datatype symbol is provided explicitly and upfront, in the first argument, to facilitate type checking of mutually recursive datatypes. This is similar to what is currently done in define-funs-rec.

The proposal also adds a new binder to the term language (match) which can be used to do pattern-matching-based case analysis on datatype values.

-----------------------------------------------
Examples:

; Axiom for list append: version 1
; List is a parametric datatype with constructors "nil" and "cons"
;
(forall ((l1 (List Int)) (l2 (List Int)))
  (= (append l1 l2)
     (match l1
       ((as nil (List Int)) l2)
       ((cons h t) (cons h (append t l2)))))) ; h and t are bound variables

; Axiom for list append: version 2
(forall ((l1 (List Int)) (l2 (List Int)))
  (= (append l1 l2)
     (match l1
       ((cons h t) (cons h (append t l2)))
       (_ l2))))   ; _ is a bound variable
-----------------------------------------------


A solver will need to implement these new commands and the match binder only if it accepts logics (to be defined) that include datatypes. 

Note that the syntax of declare-datatypes differs from the (unofficial) SMT-LIB syntax currently used by some solvers such as Z3 and CVC4 that support datatypes. The proposed one is both more general and more systematic, and designed to keep parsing simple. Also, similarly to declarations of parametric function symbols in theory declarations, parametric datatype declarations use the par binder to introduce the sort parameters.

Also note that currently neither Z3 nor CVC4 supports the match binder. However, we expect that adding support for it will not too onerous because (i) match can be re-expressed in terms of ite and let, and (ii) match patterns are restricted to non-nested ones.

The current proposal is based on several conversations we have had on this extensions with a number of people in the community. As usual, we solicit your comments, corrections, additional requests, etc. Clarification requests are also welcome. 

Best,


Cesare, Clark & Pascal


PS: The current draft is missing a revision of Chapter 5, defining the logical semantics of datatypes. We plan to do that at a later time. However, it will be the expected one, along the lines of the semantics given in 

Clark Barrett, Igor Shikanian, and Cesare Tinelli. An Abstract Decision Procedure for Satisfiability in the Theory of Inductive Data Types. Journal on Satisfiability, Boolean Modeling and Computation, 3:1-17, 2007.