[SMT-LIB] Validators and compliance testing

[David Cok]

Cesare, and other interested people,

This is in progress (but taking a while since I need some time from 
GrammaTech's lawyer). The intention is indeed to use an OSI license 
(something like an MIT or BSD license), with a contributor agreement.

However, I would welcome input on what hosting site and VCS to use.
I'm most familiar with sourceforge and SVN (with modest experience with 
Mercurial and Git), but would welcome specific input regarding 
experience with other sites and tools, specifically experience on the 
organization of the VCS when combining contributions from a variety of 
sources, the need to generate specific public releases, and support for 
branching non-public projects. (These would seem to point to using a DVCS).

- David


On 7/29/13 6:34 PM, Tinelli, Cesare wrote:
> David,
>
> Many thanks for your proposal below. We, the SMT-LIB coordinators, welcome Grammatech's offer to make jSMTLIB an open source tool and your willingness to work on making it a standard conformance checker for SMT-LIB 2 benchmarks.
>
> Since no-one as objected to your proposal or offered alternatives until now, we would like to go ahead with yours, assuming that you can release the jSMTLIB with an OSI-approved open source license (ideally a copy-free one). If so, we would like to adopt jSMTLIB as the official validator/preprocessor for benchmarks uploaded to StarExec.
>
> The first step will probably be to put jSMTLIB on some public site such as GitHub or SourceForge once the licensing issues have been resolved. Let's get in touch directly on how to proceed next.
>
> Best,
>
>
> Cesare, Clark, and Pascal
>
>
> On 12 Jul 2013, at 23:50, cok at frontiernet.net wrote:
>
>> 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
>> _______________________________________________
>> SMT-LIB mailing list
>> SMT-LIB at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>