[SMT-LIB] executing scripts in SMTLIB

[cok@frontiernet.net]

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