Search code examples
z3smtcvc4

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

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.

Solution

  • 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