[SMT-LIB] SMT-LIB Digest, Vol 55, Issue 4

[Mohammad Abdul Aziz]

Thank you very much.
Yours,
Mohammad Abdul Aziz

On Sat, Aug 27, 2011 at 6:02 PM, <smt-lib-request at cs.nyu.edu> wrote:

> Send SMT-LIB mailing list submissions to
>        smt-lib at cs.nyu.edu
>
> To subscribe or unsubscribe via the World Wide Web, visit
>        http://www.cs.nyu.edu/mailman/listinfo/smt-lib
> or, via email, send a message with subject or body 'help' to
>        smt-lib-request at cs.nyu.edu
>
> You can reach the person managing the list at
>        smt-lib-owner at cs.nyu.edu
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of SMT-LIB digest..."
>
>
> Today's Topics:
>
>   1. Concerning SMTCOMP tarballs (Mohammad Abdul Aziz)
>   2. Re: Concerning SMTCOMP tarballs (Morgan Deters)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Sat, 27 Aug 2011 00:51:07 +0300
> From: Mohammad Abdul Aziz <mohammad.abdulaziz8 at gmail.com>
> To: smt-lib at cs.nyu.edu
> Subject: [SMT-LIB] Concerning SMTCOMP tarballs
> Message-ID:
>        <CACtf-bBqjE7+Bc4BaV4APnP==M9JkCnyLAtExqVpcdTjJszLPw at mail.gmail.com
> >
> Content-Type: text/plain; charset=ISO-8859-1
>
> Hey all,
> I would like to know whether there is a common way to execute the
> tarballs of the solvers at the smtcomp website??(For example is it
> using using the associated shell script??)
>
> Yours,
> Mohammad Abdul Aziz
>
>
> ------------------------------
>
> Message: 2
> Date: Fri, 26 Aug 2011 18:12:46 -0400
> From: Morgan Deters <mdeters at gmail.com>
> To: Mohammad Abdul Aziz <mohammad.abdulaziz8 at gmail.com>
> Cc: smt-lib at cs.nyu.edu
> Subject: Re: [SMT-LIB] Concerning SMTCOMP tarballs
> Message-ID:
>        <CANE73x77x5pC0xhLKX9DUyhS6txfT07CzjVzcx39V0BT-pi1Jg at mail.gmail.com
> >
> Content-Type: text/plain; charset=ISO-8859-1
>
> Hi Mohammad,
>
> If you're referring to using the SMT-Exec service, then yes, setting
> up an SMT-Exec job should run the solvers the same way they ran in
> competition (the interface does not yet support running the
> "application" track, but if you want that, I can add it to the job
> submission interface).  That involves running a "prerun" script (if
> any), and then a "run" script to run the solver.
>
> If you're referring to downloading the solvers yourself (from
> http://www.smtexec.org/exec/competitors2011.php ) and running those
> manually on your own machine, then you need to untar the archive and
> change into the top-level directory of the unpacked archive.  If a
> "prerun" script exists, run it.  Then run the "run" script, providing
> an SMT-LIBv2 benchmark file on standard input.  (For competitions
> before 2011, some or all solvers use SMT-LIBv1 rather than v2.)  This
> benchmark file is somewhat restricted, so that competition solvers
> need not implement the entire standard (details are in the competition
> rules).  Not all solvers will support extensions to this restricted
> form (in particular, they may not be fully SMT-LIBv2 compliant), and
> they may not support all of the defined SMT-LIBv2 logics.
>
> It's easy to miss the detail about the benchmark being given to the
> run script on standard input (rather than as an argument), and it can
> appear that solvers are not operating correctly if you don't provide
> standard input.  Many solvers also support giving a file name on the
> command line (but their run script might not support this---you can
> look at the run scripts to see how to execute each solver.)
>
> Best,
> Morgan
>
> On Fri, Aug 26, 2011 at 5:51 PM, Mohammad Abdul Aziz
> <mohammad.abdulaziz8 at gmail.com> wrote:
> > Hey all,
> > I would like to know whether there is a common way to execute the
> > tarballs of the solvers at the smtcomp website??(For example is it
> > using using the associated shell script??)
> >
> > Yours,
> > Mohammad Abdul Aziz
> > _______________________________________________
> > 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
>
>
> ------------------------------
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>
>
> End of SMT-LIB Digest, Vol 55, Issue 4
> **************************************
>