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

[ThanhVu (Vu) Nguyen]

ah I see, I didn't try the nightly release of CVC3,  I was trying the
nightly release of CVC4.   Will try it again tonight.

I'll try to send you the failed log of cvc4 later.

Thanks,


Vu,


On Wed, Aug 10, 2011 at 12:22 PM, Morgan Deters <mdeters at gmail.com> wrote:

> 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
>