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

[cok@frontiernet.net]

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