[SMT-LIB] SMT solver for Mac OS that accepts smtlib v2 format

[Alberto Griggio]

Hello,

> Regarding models, you mention a (model) command, but there is no such
> thing in the SMT-LIBv2 standard (yet)---the standard provides only
> (get-value...) and (get-assignment).  As an extension to the standard,
> Z3 provides (get-model).  Perhaps smtlib2parser doesn't include
> support for it simply because it's nonstandard.  

Morgan is right. (model) is not a standard SMT-LIBv2 command, and so it
is not implemented in smtlib2parser. However, (get-value) is. It doesn't
work for *arbitrary* terms, but for constants it does work. For example, 

  (get-value (x y z))

where x, y, and z are free constants (i.e. "variables") should work, but

  (get-value ((+ x (* 3 y) (* (- 1) z))))

doesn't. As an example:

    [alb at allblack smtlib2parser]$ ./smtlib2yices 
    (set-option :produce-models true)
    > success
    (declare-fun x () Int)
    > success
    (declare-fun y () Int)
    > success
    (assert (> (+ x (* 3 y)) 5))
    > success
    (check-sat)
    > sat
    (get-value (x y))
    > ( (x 6)
    >   (y 0) )
    (get-value ((+ (* 4 x) (* (- 1 y)))))
    > (error "error computing model")

If this is enough for your needs, then smtlib2parser should run fine on
OS X (and if not, I'd be interested in knowing it).


HTH,
Alberto

P.S: I've just released a new version of smtlib2parser, which fixes an
error in parsing terms like (- x y)