SMT Solver support for SMT-LIB 2.6 declare-datatypes statements

Question

The draft for SMT-LIB Version 2.6 specifies a (declare-datatypes) statement. In the original announcement for this feature it is mentioned that the proposed syntax is different from the syntax supported by Z3 and CVC4 at the time.

Is there any SMT solver with SMT-LIB support that currently supports the proposed syntax from the SMT-LIB 2.6 draft, or a patch that adds support for the proposed syntax to a solver?

The logic I'm interested in is QF_ABV plus datatypes for simple n-tuples. I do not require advanced datatype features such as recursive datatypes or parametric datatypes.

Z3 does not yet implement the syntax from the draft spec. The more substantial change is the introduction of pattern matching, which can be compiled away using pattern matching compiler (or as LISP programmers would do by hand). — Nikolaj Bjorner

user7723234 user7723234 · Accepted Answer · 2017-03-16T18:32:37

I've added support for SMT LIB version 2.6 datatypes in the latest development version of CVC4 (commit 594301e6f2893ebe9baba5083ff084933b1e9da9). The 2.6 syntax is not enabled by default, but you can use:

cvc4 --lang=smt2.6 [input]

Hope this helps, Andrew

SMT Solver support for SMT-LIB 2.6 declare-datatypes statements

1 Answers