[SMT-LIB] SMT-LIB: Syntax Error in smtlib/logics/QF_UFIDL.smt

[Paulo J. Matos]

On 12/10/2007, Grundy, Jim D <jim.d.grundy at intel.com> wrote:
> How is a tool to know it's Foo theory resembles the requested Foo theory
> unless it takes a look at the theory file and concludes that it supports
> the same signature as the theory file describes?  (Not that we are doing
> that yet, but I figured that was what was ultimately intended.)
>

Well, you could just implement in your solver a way to recognize the
theory by looking at the :logic value at the benchmark and send the
problem to the builtin decision procedures at your discretion without
ever looking at the theory files (since when you build your solver,
you build it based on the SMT theory files). I think most of the
[minimal] solvers (at least mine) have only a parser for benchmarks.

If you have implemented only LIA, LRA and Arrays decision procedure
then, if a benchmark for UF shows up, you report your solver doesn't
support that and that's it.

Cheers,

Paulo Matos

> All the best
>
> Jim
>
> -----Original Message-----
> From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On
> Behalf Of Cesare Tinelli
> Sent: Friday, October 12, 2007 1:31 PM
> To: smt-lib at cs.nyu.edu
> Subject: Re: [SMT-LIB] SMT-LIB: Syntax Error in
> smtlib/logics/QF_UFIDL.smt
>
> Hi Jim,
>
> On Oct 12, 2007, at 2:30 PM, Grundy, Jim D wrote:
>
> > Hi All
> >
> > There is a syntax error in the file smtlib/logics/QF_UFIDL.smt
> > hosted on
> > http://combination.cs.uiowa.edu/smtlib/logics/QF_UFIDL.smt.  The close
> > quote on the :language section is missing, which violates the
> > published
> > SMT-LIB grammar.
> >
> Thanks for pointing that out. The error has now been fixed.
>
> > We were using an old version (due to Clark), which was syntactically
> > correct, that we downloaded some time back until just recently, so we
> > only just noticed this error - which has presumably been there for
> > some
> > time.  I'm wondering why other people haven't been complaining about
> > this, do other solvers not actually parse the referenced logic files
> > when running a benchmark?
> >
> Most solvers have those theories/logics built-in, which is the whole
> point of SMT ;)
> So, no, they do not parse the theory or logic specifications.
> It is good to know though that there is at least one tool that parses
> them and checks them out.
>
> Cheers,
>
>
> Cesare
>
>
>
>
> > All the best
> >
> > Jim
> >
> > --
> > Jim Grundy, Research Scientist. Intel Corporation, Strategic CAD Labs
> > Mail Stop RA2-451, 2501 NW 229th Ave, Hillsboro, OR 97124-5503, USA
> > Phone: +1 971 214-1709  Fax: +1 971 214-1771
> > Key Fingerprint: 5F8B 8EEC 9355 839C D777  4D42 404A 492A AEF6 15E2
> >
> >
> >
> > _______________________________________________
> > 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
>
>
>


-- 
Paulo Jorge Matos - pocm at soton.ac.uk
http://www.personal.soton.ac.uk/pocm
PhD Student @ ECS
University of Southampton, UK