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

[QPQ]

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

tinelli wrote at Jan 19, 2005 - 11:22 AM
---------------------------------------------------------------------
Thanks to Clark for his suggestions. Here is our reply. 
Unless anybody objects by the end of this week, we plan to change the SMT-LIB standard as proposed below.

Silvio & Cesare


> 
> 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.
>
There have been calls by others as well to do without benchsets in the language. If they do not seem to be useful let's eliminate them. 
We agree with the proposal then.

 
> 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.
>
Basically, Silvio had thought of the same kind of proposal (mentioned in a previous post by Cesare), with the difference though that he wanted to redefine the notion of theory itself as proposed above. That is, define a theory in essence as a pair consisting as set of axioms/models and a syntactic restriction on the formulas to consider.
So, for instance, the "linear real arithmetic theory" would be defined as a pair (T, F) where T is the axiom set for the real closed fields and F is the class of boolean combinations of linear equations and inequations (
---------------------------------------------------------------------

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/