[SMT-LIB] [SMT-API] SMTLIB resources - tutorial, Java tool, API, and Eclipse plug-in

[Tinelli, Cesare]

Hi all,

I'd like to give a belated but big public thank you to David for writing this tutorial and creating its accompanying tools. They are a great service to the community and will be invaluable in popularizing the SMT-LIB 2 standard.

The tutorial and the tools are now also accessible from the SMT-LIB web site.

Please help improve the (already high) quality of the tutorial further by sending your feedback to David.

Thanks,


Cesare


On 3 Jan 2011, at 08:38, <cok at frontiernet.net>
 <cok at frontiernet.net> wrote:

> SMT-LIB community:
> 
> I'd like to (pre-)announce a number of SMT-LIB resources.
> These are available from http://www.grammatech.com/resources/smt 
> [see the DISCLAIMER below].
> In particular, feedback and comments are highly welcome.  These
> are all early versions and will be corrected and modified based
> on input received.
> 
> 1) A tutorial - at the request of the SMT-LIB authors, I've written a
>   tutorial on SMT-LIB v.2, with examples and a more informal, explanatory
>   style than the formal reference manual.
> STATUS: The first complete draft is out for comment; a revision will be
>   issued once comments are received.  You are welcome to add your comments
>   to those I have directly solicited. If you would find this useful to your
>   students (particularly, perhaps, with the Eclipse plug-in below), I would
>   be very interested in some collaboration.
> 
> 2) jSMTLIB.jar - This Java (Java 1.6) software package includes the
> following capabilities [If you absolutely need Java 1.5 support, let me know]:
>  a) an application that parses and type-checks SMT-LIB scripts (from files,
>     direct user input, or through a network port)
>  b) a Java API for programmatically creating and working with SMT-LIB scripts
>     (and designed to be extensible - able to add commands, new concrete syntax,
>     new back-end adapters, additional logics and theories, eventually new
>     expression syntax)
>  c) adapters that connect SMT-LIB to the input languages of some
>     SMT solvers that do not (yet) (completely) conform to SMT-LIBv2
>     (in particular, so far, Simplify 1.5.4, Yices 1.0.28, CVC3 2.2, Z3 2.11
>      on Cygwin/Windows)
> STATUS: the package is available: (2.a) is documented and tested; the documentation
>    for (2.b) is in progress; the implementations for (2.c) exist as early alpha
>    versions but are not yet complete. 
> 
>    I'd welcome interaction with individuals interested in using the API; the API
>    is at present directed toward providing OpenJML a connection to SMT solvers
>    through SMT-LIBv2, but its design would benefit from having other applications
>    as well. (OpenJML is an implementation of JML tools, in particular ESC/Java2,
>    built on OpenJDK - contact me if you are interested in that separate activity.)
> 
> 3) A user guide for jSMTLIB.jar
> STATUS: Available and documents the jSMTLIB application (2a); the documentation of
>   the Java API (2b), the adapter implementations (2c), and the Eclipse plug-in (4) 
>   are underway.
> 
> 4) An Eclipse plug-in that encapsulates the jSMTLIB tool. This plug-in provides a
>   custom SMT-LIB-aware GUI editor, with syntax coloring and with standard Eclipse 
>   problem markers for parse and type errors.  It allows sending a script to a 
>   back-end SMT solver for execution, receiving and displaying the results in the GUI. 
>   Features such as grammar and type-aware navigation, refactoring tools, and
>   a host of would-be-nice GUI embellishments are in progress.
> STATUS: Exists, works, and is available from the standard plug-in update site
>    http://www.grammatech.com/resources/smt/jSMTLIB-UpdateSite (online help 
>   documentation is in draft form) (Eclipse 3.6, using Java 1.6)
> 
> "5") I also have a validation suite for SMT-LIBv2 tools, that checks conformity to
>   the SMT-LIBv2 standard. (It checks conformity of command syntax and semantics,
>   not of the SMT solving capability.) I will make a public release once it is more 
>   automated and has had more experience with tools under development; 
>   in the meantime, I would be happy to share the suite's assessment of
>   any tool under development, if the developers contact me.
> 
> [DISCLAIMER: Though these items are hosted at grammatech.com, they are not products
> of GrammaTech, my employer, nor supported or warranted by the company.
> The usual disclaimer is included in the material - "AS IS" with no warranties, etc.
> The standard license is for academic or not-for-profit use; if you want to include
> them in other material or use them in a commercial product, please contact me.]
> 
> David Cok
> 
> _______________________________________________
> SMT-API mailing list
> SMT-API at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-api