[SMT-LIB] Adding algebraic datatypes to the SMT-LIB 2 language: an initial proposal
Tim King
tim.king at imag.fr
Wed Jul 8 09:17:48 EDT 2015
Hello all,
I am forwarding three minor problems in the v2.6 draft proposal that
Cristina Serban noticed.
1. On pages 26 and 92, the rules for <qual_constructor> and <pattern> has
two different resolutions into <symbol>. This can lead to problems in
generated parsers (specifically reduce-reduce conflicts). For example, in
the following:
> (match t
> ((cons h t) 0)
> (nil 1))
it is ambiguous for whether nil is a variable or a nullary constructor.
Additional context is needed to resolve this. This seems to be unavoidable
at the moment, but we thought we should point this out.
2. The rule describing a declare-datatype [without the 's'] command (pages
44 and 95) is missing a <symbol> for the name of the datatype. For example,
this example would be invalid:
> ( declare-datatype Color ( ( red ) ( green ) ( blue ) ))
as there is no <symbol> to match "Color".
3. The "enumeration datatype" example on page 61 is missing a closing
parenthesis.
Best,
Tim
On Thu, Jun 25, 2015 at 11:12 AM, Andrew Reynolds <
andrew.j.reynolds at gmail.com> wrote:
> 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
> >
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>
>
More information about the SMT-LIB
mailing list