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

[Grundy, Jim D]

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

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