DOMAINS :: SMT-LIB :: Some SMT-COMP/LIB issues

[QPQ]

Forums QPQ
DOMAINS :: SMT-LIB ::.. Some SMT-COMP/LIB issues

barrett wrote at Jan 14, 2005 - 10:48 AM
---------------------------------------------------------------------
On behalf of the SMT-COMP organizing committee, I am putting together an initial library of benchmarks in SMT-LIB format.  I hope this will lay the foundation for the first real incarnation of SMT-LIB.

As the first step in this process, I have reviewed the SMT-LIB standard and I would like to propose a couple of minor changes.

1) In his previous post, Cesare suggested some possible changes to the benchmark vs benchmark set definitions.  I think it would be simpler and more intuitive if we merged the two and got rid of benchmark sets altogether.  That way, each benchmark is a separate file and is completely self-contained.  I think this would be more appropriate for the competition as well.

2) Right now, there is no way to wrap up a theory with some language restrictions to form a benchmark division.  I would like to propose a new definition called "division" (let me know if you have a better name) which includes a theory and a set of syntactic restrictions on formulas in that theory (what is currently handled by the benchmark set "language" attribute).  That way, a benchmark simply needs to refer to the division it's in rather than both the theory and the language.

Those are my proposed changes.  Please reply if you have thoughts or objections.  As I will need to start implementing this soon, I encourage you to reply soon (before January 20) if you do have comments.

-Clark
---------------------------------------------------------------------

Reply to this message:
http://www.qpq.org/modules.php?op=modload&name=phpBB_14&file=index&action=reply&topic=54&forum=46

Browse thread:
http://www.qpq.org/modules.php?op=modload&name=phpBB_14&file=index&action=viewtopic&topic=54

You are receiving this Email because you are subscribed to be notified of events in forums at: http://www.qpq.org/