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

[Morgan Deters]

Hi Vu,

Recent nightly releases of CVC3 do support SMT-LIBv2 (although the
last release version does not), and the nightly builds are pretty
stable, since we're preparing a release.
http://goedel.cims.nyu.edu/cvc3-builds/

Also, CVC4 should build cleanly on a Mac, as I regularly develop and
test on Snow Leopard + MacPorts myself.  Could you please (off-list)
share with me some more detail, like a failed build log?

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.  There has been some
discussion of adding additional model-inspection commands to the
standard, but I'll let others comment on that.

Thanks,
Morgan


On Wed, Aug 10, 2011 at 1:33 PM, ThanhVu (Vu) Nguyen <tnguyen at cs.unm.edu> wrote:
> Hi,
>
> I am wondering if there is some SMT solver for Mac OS (Snow Leopard +
> Macport) that supports Linear arithmetic  and also accept smtlib2 as input
> format.   So far I've tried cvc3 but I don't believe it supports smtlib2 and
> I can't get cvc4 (nightly release) to build properly on Mac.     I have also
> tried smtlib2parser which uses Yices 1 backend but it doesn't support the
> (model) command.
>
> Right now I am using Z3 which does all I want except doesn't run on Mac
> natively.   I was able to run it via Wine but it is extremely slow that way.
>
>
> Another question is if it is possible to get several models instead of just
> 1 if the formula is satisfied.   I could always get the model 1,  then put
> back the negated result as assertion to get a different model 2 (if it
> exists) and so on  -  just want to know if there's some better way.
>
>
> Thanks,
>
>
>
> Vu,
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>
>



-- 
Morgan Deters
mdeters at gmail.com