[SMT-LIB] executing scripts in SMTLIB

[Aaron Stump]

Hi, David.  Can you say a bit more about how you envision such
functionality being used?  I'm just wondering, because since we expect
mostly the scripts will be generated, probably dynamically, by other
tools, they can just as well take care of reading some file of
background definitions or something, and then sending that in.  It may
become just another issue of where should we put the burden, on the
solver side or application side.  And it should be noted that, as far
as I understood talking to several (on the order of 2 or 3) solver
implementors, they did not submit to SMT-COMP 2010 at least partly
because they did not manage yet to add support for the new language.
So pushing more stuff onto the solver side is a real issue right now.

Aaron

On Wed, Jul 14, 2010 at 6:42 PM,  <cok at frontiernet.net> wrote:
> On looking over the SMTLIB v2 after Cesare's talk today, it occurred to me that we are missing the ability to execute subscripts.  That is, a command such as
>
> (exec <string> )
>
> is needed, where string is a filename.  Unfortunately that introduces some system dependence for translating the string to a file within the directory/folder hierarchy.
>
> There is a complicated alternative - namely writing a conventional (e.g. bash) command that feeds content into a (single) running instance of an SMT solver.  Then one can use all the capabilities of one's favorite shell to formulate SMT-LIB commands.
>
> - David
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>