[SMT-LIB] Version 2.0 of SMT-LIB is finally here!

[Cesare Tinelli]

Hi Geoff,

On 10 Feb 2010, at 10:55, geoff at cs.miami.edu wrote:

> Hi Cesare, all,
> 
>> we are pleased to announce that, after a very long gestation, we are very close to finalizing Version 2.0 of the SMT-LIB standard. An almost final draft of the reference document is available at
>> 
>> http://www.smt-lib.org/papers/v2-ref-manual-draft.pdf
>> 
>> The document has been prepared with the input and feedback of three working groups, consisting of SMT researchers, developers and power users. 
>> 
>> We encourage interested people in this wider list to take a look at the document and give us their feedback **by the end of this month.**
> 
> I don't know if I mentioned this before, but I encourage you to consider 
> using the SZS ontology for system result values ...
>    http://www.tptp.org/cgi-bin/SeeTPTP?Category=Documents&File=SZSOntology
> ... instead of the unsupported | success | error, timeout | memout | 
> incomplete, and sat | unsat | unknown values currently listed. The ontology 
> supports more fine grained reporting, and has a sound semantic basis. There 
> is a paper about it at ...
>    http://www.cs.miami.edu/~geoff/Papers/Conference/2008_Sut08_KEAPPA-38-49.pdf
> 
Thanks for your suggestion. Unfortunately, it does not look like the SZS ontology is well suited for SMT-LIB purposes. It is not clear right now how the semantics of the ontology would apply to the check-sat command. Maybe it is possible to find the right fit, but this will certainly need further discussion with you to figure this out. So I'm afraid it will not make it to Version 2.0.
But we look forward to your suggestions on which specific output values from the ontology would be appropriate for us and why, so that we can consider using those values in a later version.


> Generally, it looks like SMT is ready to conquer the world!
> 

Oh no, just the automated reasoning world ;)

Cheers,


Cesare (also for Aaron and Clark)



> Cheers,
> 
> Geoff
> 
> Geoff Sutcliffe                           http://www.cs.miami.edu/~geoff
> Department of Computer Science            Email : geoff at cs.miami.edu
> University of Miami                       Phone : +1 305 2842158/2842268
> (Director of Undergraduate Studies)       FAX   : +1 305 2842264
> ----- "My cat" is not a float. Every string should learn to swim. ------