[SMT-LIB] Benchmark Conformance: log in AUFLIRA/nasa/

[Cesare Tinelli]

Hi Nikolaj,

On 3 Nov 2010, at 16:44, Nikolaj Bjorner wrote:

> Hi Cesare,
> 
> This is likely a useful discussion to have for many, but I would also like to respect that the SMT-LIB mailing list should be about SMT-LIB and not about Z3.

That is true.

> The boundary here is a bit floating because it may be informative to get this kind of feedback for the community.
> I am currently answering you directly to not spam the mailing list. If you like to put the discussion back to the list, feel free.
> 
Let's continue this thread privately, as you suggest. I'm putting just this one message back in the list to record that you did reply to my latest message, and to reply to your non-Z3 specific comments below.



> There are two reasons:
> 1. The support started in January before the standard was finalized. I did not remove support for features added then. The examples are also from then, they were not changed. 
> 2. It is convenient. It happens to not be ambiguous, the standard could have defined a sequence of commands as S-expressions, where atoms are included in the definition of S-expression
> (eg: s-expr ::= atom | '(' s-expr* ')' , atom ::= <string> | <symbol> | <integer> | <floating-point> ).
> 
> Going forward, it can be nice to have online examples that illustrate SMT-LIB2.

Yes, it would. For now, the plan is simply to have a tutorial document, with examples, which is sorely needed. As David mentioned some time ago, he has been working on that. So we hope to have at least a tutorial online in the near future.

> We may also later support creating online material/samples as there is in Pex4fun.com, 
> this could be used as a service for illustrating SMT-LIB2. Having such online ways of using 
> SMT solvers from SMT-COMP could also be a nice thing for SMT. Geoff's service for running 
> TPTP provers comes to mind, but what seems to be missing so far is some educational twist that should be appealing with SMT solvers.
> 
This would be nice indeed. Would you guys at MSR be willing to do that? We, the SMT-LIB coordinators, would be happy to help by double-checking the examples and making sure that they conform to the SMT-LIB2 standard :)

Actually, I'm serious. It would be really great for the whole community if you were willing to create and maintain the online material you propose.

Cheers,


Cesare


> We still pretty print according to SMT-2 format whenever possible 
> (the main exception I am aware of now is that we admit symbol parameters to functions, not only integers, so we can parse and print '(_ foo alice 1 bob)').
> 
> Nikolaj
> 
> 
> 
> -----Original Message-----
> From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On Behalf Of Cesare Tinelli
> Sent: Wednesday, November 03, 2010 12:31 PM
> To: smt-lib at cs.nyu.edu
> Subject: Re: [SMT-LIB] Benchmark Conformance: log in AUFLIRA/nasa/
> 
> Nikolaj,
> 
> On 3 Nov 2010, at 13:14, Nikolaj Bjorner wrote:
> 
>> Yes, Z3 aims to accept a super-set of SMT-LIB2.
> 
> That is certainly reasonable, especially considering that the command language is currently quite limited.
> 
> 
>> It also aims to be forgiving with lack of quotes around strings etc, as they are most often redundant.
>> 
> This statement and the example below though seem at odd with the view of SMT-LIB2 as a low level, machine interchange format. For instance, I do not quite see the rationale for accepting both pop and (pop 1), quit and (exit), declare-funs and declare-fun, etc.
> 
> 
> Cesare
> 
> 
> 
>> Cheers,
>> 
>> Nikolaj
>> 
>> -----Original Message-----
>> From: cok at frontiernet.net [mailto:cok at frontiernet.net]
>> Sent: Wednesday, November 03, 2010 12:27 AM
>> To: Nikolaj Bjorner
>> Cc: Cesare Tinelli; smt-lib at cs.nyu.edu
>> Subject: Re: [SMT-LIB] Benchmark Conformance: log in AUFLIRA/nasa/
>> 
>> 
>> ----- "Nikolaj Bjorner" <nbjorner at microsoft.com> wrote:
>> 
>>> 
>>> While I support the SMT-LIB2 format (see my shameless plug:
>>> http://rise4fun.com/z3 ), I see its main priority as a low-level 
>>> mostly machine writeable/readable interchange format that as an added 
>>> benefit is also human read/write-able.
>>> 
>>> Thanks,
>>> 
>>> Nikolaj
>>> 
>> 
>> Nikolaj - A nifty web-site but what is written on that web site is not (pure) SMT-LIB.
>> In particular it has
>> 
>> (declare-funs ((x Int) (y Int) (z Int)))  (assert (>= (* 2 x) (+ y 
>> z)))  (declare-funs ((f Int Int) (g Int Int Int)))  (assert (< (f x) 
>> (g x x)))  (assert (> (f y) (g x x)))  check-sat  (get-info model)  
>> push  (assert (= x y))  check-sat  pop  quit
>> 
>> 
>> 
>> (declare-funs ((x Int) (y Int) (z Int))) - I've wanted the 
>> convenience of combining declarations also, but SMT-LIB does not 
>> currently have it.  Even better actually would be (declare-funs ((x  y 
>> z Int)))
>> 
>> 
>> (get-info model) - Keywords used in get-info are supposed to start with a :, and :model is not one of them.  This is perhaps the not well-documented command get-model?
>> 
>> push
>> check-sat
>> pop - As commands, these should all be in ()
>> 
>> quit - should be (exit)
>> 
>> David
>> 
> 
> 
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>