[SMT-LIB] submitting SMTLIB2 benchmarks?

[Ranjit Jhala]

Hi all,

I have bundled the benchmarks, you can download them at:

http://goto.ucsd.edu/~rjhala/liquidhaskell_smtlib2_benchmarks.zip

OR

http://goto.ucsd.edu/~rjhala/liquidhaskell_smtlib2_benchmarks.tgz

There is README inside with some explanations.

Let me know if you have any questions.

Best!

Ranjit.



On Sat, Jul 20, 2013 at 4:01 PM, Ranjit Jhala <jhala at cs.ucsd.edu> wrote:

> Hi all,
>
> thanks for the speedy response.
>
> I will make a tarball with the queries and send over shortly!
>
> Best!
>
> Ranjit.
>
>
> On Sat, Jul 20, 2013 at 2:16 PM, Tinelli, Cesare <cesare-tinelli at uiowa.edu
> > wrote:
>
>> 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
>>
>>
>