[SMT-LIB] submitting SMTLIB2 benchmarks?

[Tinelli, Cesare]

Hi Ranjit and all,

On 20 Jul 2013, at 10:26, Pascal Fontaine <Pascal.Fontaine at inria.fr>
 wrote:

> Dear Ranjit,
> 
> we are always looking for benchmarks; and your benchmarks having an incremental flavor, I believe they can be valuable for people working on incremental solvers.  The sets operation you mention may classify your benchmarks outside QF_UFLIA, but they may be recast to UFLIA, or they may trigger some interest in new logics. Anyway they are valuable.
> 
> SMT-LIB is currently reorganizing itself, and for various reasons the process is a bit slow.  The benchmarks will thus not be available immediately on the web site.  In order not to forget them, just send them to Cesare, Clark or myself (if you want to have an account on a system for transferring large files, let me know).
> 
> Cesare and Clark may want to add information or correct this message.

My only addition to Pascal's accurate reply is that there was some interest in the past in adding a theory of finite sets with cardinalities to SMT-LIB. 

We worked out a declaration with Philipp Ruemmer a while ago based on a larger proposal by him, Daniel Kroening and Georg Weissenbacher (http://www.philipp.ruemmer.org/publications/smt-lsm.pdf).
But the theory was never added because, as I recall, the promise of benchmarks did not materialize in the end (apologies to Philipp if I am misremembering this now).

Ranjit, if you have a substantial number of benchmarks with set operations, we could revive those plans and also add a logic that includes sets, UF and LIA.

Since we are at it, let me make the same invitation to anybody else in this list who may be able to generate benchmarks involving finite sets.

Please let us, the coordinators, know.

Thanks,


Cesare


>  I am just stepping in the organization.
> 
> Thank you for helping us to provide a comprehensive library of problems!
> 
> Best,
> 
>  Pascal
> 
> On 07/20/2013 06:59 AM, Ranjit Jhala wrote:
>> Hi all,
>> 
>> I have a bunch of SMTLIB2 benchmarks of the form
>> 
>>   (push . assert* . checksat . pop)*
>> 
>> the queries are QF_UFLIA formulas (though there
>> are some which require SET operations like union,
>> intersection, subset etc.)
>> 
>> Is there any interest in adding these to the SMTLIB benchmark set? If so,
>> could you point me in the right direction?
>> 
>> Many thanks (and apologies if this was the wrong
>> place to ask!)
>> 
>> Ranjit Jhala.
>> _______________________________________________
>> 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