[SMT-LIB] submitting SMTLIB2 benchmarks?

[Ranjit Jhala]

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
>
>