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

[Andrew Reynolds]

Hello Cesare and all,

Here are some comments for the version 2.6 draft.


* bottom of page 28 : "Suppose first that n>1 and p_1 is not a variable" ->
"Suppose first that n>1 and p_n is not a variable".
Below that paragraph, the last two returns of the ite corresponding to
match are incorrect.  In the second to last return value, "t1" should be
"tm".   The last return value should be "(let ((x_{n1} (s_{n1}
t))...(x_{nkn} (s_{nkn} t)) tn)".  Also, the x's are not introduced in this
paragraph, it may be more clear to remove the p's and say:
"(match t (((c1 x_{11} ... x_{1k1}) t1)...((cn x_{n1} ... x_{nkn}) tn)))"
has the same meaning as: ...


* Type annotations on constructors in patterns may be unnecessary.  Page 28
has:

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

I find the conventions in above formula to be inconsistent, since locally
parsing "(cons h t)" is also ambiguous since "h" and "t" are not given
types, so I'd expect something like:

(forall ((l1 (List  Int)) (l2 (List  Int)))
(= (append  l1 l2)
(match l1
  ((as nil (List Int)) l2)
  ((as (cons h t) (List Int)) (cons h (append t l2))))))

Regardless, we may infer the types of the constructors in patterns since we
know the type of l1, so I think it is reasonable to write:

(forall ((l1 (List  Int)) (l2 (List  Int)))
(= (append  l1 l2)
(match l1
  (nil l2)
  ((cons h t) (cons h (append t l2))))))


* For brevity, it would be nice if it were optional to state that a
datatype has zero type parameters within declare-datatypes.  In other
words, I'd like to write:

(declare-datatypes (List Tree)
((cons (head Tree) (tail List)) (nil))
((node (left Tree) (right Tree)) (leaf (data List))))

instead of:

(declare-datatypes ((List 0) (Tree 0))
((cons (head Tree) (tail List)) (nil))
((node (left Tree) (right Tree)) (leaf (data List))))

This barely complicates parsing, and in my opinion fits with the spirit of
the new commands.


* Like Jochen, I think the explanation of well-defined datatype needs
clarification.


Cheers,
Andy


On Wed, Jun 17, 2015 at 8:34 AM, Tinelli, Cesare <cesare-tinelli at uiowa.edu>
wrote:

> 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.
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>