[SMT-LIB] Validators and compliance testing

[cok at frontiernet.net]

SMTLIB people,

Opportunity:

Two of the tasks we would like to perform as part of SMT-EVAL 2013 are these:
1) Check that the current benchmarks conform to SMT-LIBv2 (and enable checking new benchmarks in the future).
2) Create and run a SMTLIBv2 compliance test that checks the degree to which existing solvers implement the SMTLIBv2 standard. [We realize that full compliance is not necessary for participation in competitions, but we think it is a relevant data point in selecting a solver to use.]

Item (1) requires a tool that parses benchmarks and checks that they conform to the logic they claim to be in (and perhaps will classify benchmarks into an appropriate logic).

Item (2) requires a set of functional tests and expected output.


Proposal:

As part of creating the SMTLIB tutorial and the jSMTLIB software a couple years ago, I have most of what is needed for (1) and (2) above. GrammaTech is willing to contribute the software as Open source (license TBD but in process). The jSMTLIB software (a Java tool) already does the conformance checking, with a few tasks needed: some completion and cleanup, a review of the standard and the code, and some reimplementation so that it is more memory-efficient on large benchmarks when in a checking mode. 

jSMTLIB also contains a significant number of SMTLIB validation tests, which I have personally used to check solvers (and report bugs to their authors). They would need to be reformatted and organized, but they do cover most of the standard already. Note that they do not test actual solving correctness or capability, just that the SMTLIBv2 commands and options are read and have the desired effect, symbols are resolved correctly, logics are interpreted correctly, etc.

Both of these tasks involve some work, so if another group already has either of these capabilities in a publicly contributable form, I would be happy to consider starting with that base - I certainly do not want duplicate work happening and would like to minimize the overall work required. 


I'd also welcome someone identifying an undergraduate willing to help with test organization and generation as an undergraduate project.


Comments on the above are welcome (and desired). In particular, I'd like near term resolution of the question of whether the SMTLIB community (a) would like these capabilities built on jSMTLIB, or (b) would prefer that these capabilities be built on another base, or (c) would like to modify what I have stated as a need, or (d) thinks the proposed project is completely unneeded.


- David Cok