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

[Cesare Tinelli]

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
>