[YICES] Documentation on Yices SMT-LIB
bruno at csl.sri.com
Mon Jun 25 14:53:15 PDT 2007
Hormoz Zarnani wrote:
> Hello. My name is Hormoz Zarnani, and I am a second-year computer
> science PhD student at CMU. I am working on a C interpreter with my
> adviser, Randy Bryant, which among other things generates specifications
> in SMT-LIB format. I have been using Yices 1.0 (which I downloaded off
> of the SMT-COMP web site) as the target for my tool.
> I am wondering if there is a documentation on Yices SMT-LIB. I wasn't
> able to find one on <http://yices.csl.sri.com/documentation.shtml> nor
> on the SMT-LIB web site.
Try to use an up-to-date version of Yices by downloading it at
http://yices.csl.sri.com/. The current released version is 1.0.9 and it
includes many bug fixes. Do not use Yices 1.0.
As for the SMT-LIB documentation, it can be found on the SMT-LIB website
at http://www.smt-lib.org. You'll need to check:
- the SMT-LIB Standard Version 1.2 (click on the "Documents" link)
- the theories and logic specifications (follow the links "Theories" and "Logics")
For the most recent news and upgrades to SMT-LIB, you'll have to read
the SMT-LIB mailing list. Archived at http://www.cs.nyu.edu/pipermail/smt-lib
To use Yices on SMT-LIB problems, just use the flag -smt. Type 'yices --help'
to see what other options you can use. Also double check the documentation:
http://yices.csl.sri.com/documentation.shtml. The options are the same whether
you use SMT-LIB or the Yices language.
More information about the YICES