[SMT-LIB] SMT-LIB theory and logic definitions

Rob Arthan rda at lemma-one.com
Sat Apr 30 07:17:15 EDT 2016


Cesare,

> On 29 Apr 2016, at 07:36, Cesare Tinelli <cesare-tinelli at uiowa.edu> wrote:
> 
> Hi Rob and all,
> 
> On 28 Apr 2016, at 11:04, Rob Arthan wrote:
> 
>> David,
>> 
>> Thanks (and thanks also to Tim). I should have explained that I had found those links on the SMT-LIB web site: it was the text files I was looking for.
>> 
>> I wasn't able to reconstruct the version 2.0 definitions from the git repo.
> 
> 
>> Are these still available anywhere?
>> 
> If you are referring to the Version 2.5 definitions, there were there on the SMT-LIB website although the direct links to them had been removed from the site's pages in one of the latest updates. This was an oversight that has now been corrected.
> 
> The pages
> 
> http://smtlib.org/theories.shtml
> http://smtlib.cs.uiowa.edu/logics-all.shtml
> 
> now have links to the text files. Look for "(raw file)" on the page.

Thanks. That’s useful.

I was looking for the version 2.0 definitions as well as version 2.5
(because it’s 2.0 that CVC4 and Z3 support).

Regards,

Rob.




More information about the SMT-LIB mailing list