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

[Min Zhou]

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

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.
>
> Bests, Philipp
>
> On Wed, 2011-01-19 at 17:45 +0000, Christoph M. Wintersteiger wrote:
> > There is a converter  that was implemented by Philipp Ruemmer as part of
> a
> > proposal for a List/Set/Map theory. It's available at
> > http://www.cprover.org/SMT-LIB-LSM/
> >
> > Christoph
> >
> >
> > -----Original Message-----
> > From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On
> > Behalf Of Tjark Weber
> > Sent: 19 January 2011 15:02
> > To: smt-lib
> > Subject: [SMT-LIB] Translating SMT-LIB 1.2 Benchmarks into 2.0?
> >
> > Is there a tool (or tool chain) that can translate SMT-LIB 1.2 benchmarks
> > into SMT-LIB 2 format?
> >
> > Kind regards,
> > Tjark
> >
> > _______________________________________________
> > 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
>
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>



-- 
Min Zhou
Department of Computer Science & Technology
Tsinghua University
Beijing, 100084, P.R.China,
zhoumin03 at mails.tsinghua.edu.cn