[SMT-LIB] URL for draft Command Language

[Grundy, Jim D]

Hi Aaron

Thanks for producing this document.  Here are some comments.

* While I appreciate that this document has been developed in parallel with the SMT-LIB 2 draft and hence it makes sense to have defined things in terms of the earlier 1.2 draft, now that the SMT-LIB 2 draft is out... well, you know.

* I don't think I'd bother with supporting both "(pop)" and "(pop <numeral>)", the latter is sufficient.  Humans aren't going to be interacting with this interface much, it will get most of its use from tools, so keep it simple.  It's really and textual API you're defining.

* As one of the earlier commentators noted, it is overkill to allow symbols to be undeclared and redeclared.  A tool that connects via this interface, and which allows the undeclaration and redeclaration of its symbols can handle the situation via internal name mangling.  I could, however, see an application half-way where symbols may be undeclared, after which no new uses of them will be allowed.  Knowing that, the terms that defined them may be able to be garbage collected (when all references to them are gone).

* The command dump-assertions "causes the solver to print the set of current assertions in a parenthesis-delimited list".  I figure this is for human tinkering/debugging since any tool using the interface could remember what it had asserted (and would rather to do so than parse it back in).  In that case, you would probably rather it was printed as a "parenthesis-delimited list of lists" so that the human can also observe the stack structure and understand what their "pop" and "push" commands are doing.

* The command "keep-sat-assertions" is described as "requests the solver to assert all of those formulas".  Would it be clearer to say "requests the solver to add all of those formulas to the current assertion set".

* the "time" query is defined to return "the running time taken during the search".  I guess you need to specify the unit of time, is it seconds?

* similarly, the "memory" query is defined to return "the memory allocated during the search".  What is the unit of memory, bytes?

* I see that the "authors" query is required.  I don't see why it needs to be; it isn't useful in operating the tool. Requiring it just looks like a good way to generate irritations by the time we have open source tools and people are picking them up and modifying them to make their own versions.  What should those modified versions return, the list of all contributors ever?  What if you do a major rewrite, can you leave out earlier authors, how will they feel about that? If you're going to have required data of this type recommend something that has a more precise meaning where if it provokes an argument it is an argument that needed provoking and resolving; lets have queries for "copyright-holder", "copyright-year" and, maybe, "license".  (I'm not sure I'm advocating that, but I believe all of those would be more useful that than the "authors" query.)

* There is a required "version" query.  Again, I don't know how useful this is.  Maybe it need not be required. If it is useful, maybe "major-version" and "minor-version" would be better.

* What I think would be useful would be an "smt-version" (or "smt-major-version" and "smt-minor-version") query.  This would be included in this and all future version of this standard and would indicate which version of the standard a tool understood. It would be the first thing a tool communicating with an SMT tool would ask for, it would then know how to communicate with the tool.

So, finally, I think it might be a slightly clearer presentation to partition things into <command>s and <query>s, where a script is a sequence of either.  A command changes the state the returns "success" or "error" (I'm not sure why you'd turn off the "success" printing; how else do you know when the command is done?).  A query doesn't change the state and prints the answer to your query.  (See, http://en.wikipedia.org/wiki/Command-query_separation).  In this case the only real change is that it would be clearer to me which things where meant to print "success" and which something else. Also, "check-sat" would then print "success" or "error" and you would introduce a new query, say, "outcome", to get "sat" or "unsat" of the last check, just as things like "dump-proof" or "dump-sat-assertions" get you that information about the last sat check.

OK, so that wasn't finally, but this is. I'd also want a "dump-model" facility.  This might not be supported by all solvers, but would be stronger than the "dump-sat-assertions" facility because it would give you an actual assignment to the variables.  This sort of facility is essential to many applications.  The syntax for the output is fairly straight forward and can be described for the solvers that support it, a list of symbol/value pairs would do nicely.

All the best

Jim

-----Original Message-----
From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On Behalf Of Aaron Stump
Sent: Sunday, 02 August, 2009 05:16
To: smt-lib at cs.nyu.edu
Cc: smt-api at cs.nyu.edu
Subject: [SMT-LIB] URL for draft Command Language

Hello, again.  The draft of the Command Language (maybe scrubbed from my
email of yesterday) is available at

http://www.cs.uiowa.edu/~astump/papers/smt-cmd-lang.pdf

Aaron
_______________________________________________
SMT-LIB mailing list
SMT-LIB at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/smt-lib