[SMT-LIB] Concerning SMTCOMP tarballs

[Morgan Deters]

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