[SMT-LIB] executing scripts in SMTLIB

[cok@frontiernet.net]

Aaron,

I did envision this as classic subroutine capability.  For example, one might have a standard prelude one runs that is contained in its own file and does not need repeating each time - whether running in batch or interactive mode.

You are correct that if all scripts are completely generated prior to being run, this would not be necessary, but I don't see that being the case for interactive use.  I am also sensitive to the implementation burden; though there is nothing particularly difficult about reading from a file and having a stack of open file handles, it is more work.

It would be appropriate to keep this feature on a to-be-considered list and wait for more experience with SMTLIB in actual use before making any more requirements in a standard document.

- David


----- "Aaron Stump" <aaron-stump at uiowa.edu> wrote:

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