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

[Nikolaj Bjorner]

Yes, Z3 aims to accept a super-set of SMT-LIB2. It also aims to be forgiving with lack of quotes around strings etc, as they are most often redundant.

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