[SMT-LIB] Translating SMT-LIB 1.2 Benchmarks into 2.0?

[Philipp Ruemmer]

On Thu, 2011-01-20 at 17:30 +0800, Min Zhou wrote:
> >From SMT-LIB 2 to SMT-LIB 1.2 ?
> How do you handle those interactive commands such as *push*, *pop* ? Do you
> translate a single SMT-LIB 2 instance to multiple instances in 1.2 ?
> 
> Thanks :-)

In fact, currently most of the SMT-LIB command language (including push
and pop) is not handled; the main parts of the converter were written in
2009 before the command language was finalised. I recently updated the
converter to support some basic features of the command language, but
this does not yet include most of the interactive stuff.

The plan is to eventually produce multiple SMT-LIB 1 instances from a
single SMT-LIB 2 problem. The main purpose of the converter, btw, was to
handle some theories that are not (yet) part of the SMT-LIB standard,
including lists, finite sets, and floating point arithmetic. This is
done by reduction to existing theories (partly plus axioms), or by
directly interfacing the API of individual SMT solvers.

Cheers, Philipp

> On Thu, Jan 20, 2011 at 5:20 PM, Philipp Ruemmer <
> Philipp.Ruemmer at comlab.ox.ac.uk> wrote:
> 
> > Thanks for the advertising ... but this is actually a converter from
> > SMT-LIB 2 to SMT-LIB 1.2, not the other way round.