[SMT-LIB] submitting SMTLIB2 benchmarks?

[Philipp Ruemmer]

Hi Cesare & all,

On Sat, 2013-07-20 at 21:16 +0000, Tinelli, Cesare wrote:
> 
> 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).

That is largely correct I'm afraid. We were expecting to obtain larger
amounts of verification conditions involving sets (and other datatypes),
but in the end did not really get to this point. Since quite some work
went into working out syntax and semantics of the theories, it would be
great if this effort could be continued of course!

I am attaching what I believe was the last version of the theory
declaration files, which contain some changes compared to the pdf
document linked above; compared to current SMT-LIB 2 the syntax might be
a bit outdated.

Regards, Philipp

> 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. 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: SMT-LIB.tar.gz
Type: application/x-compressed-tar
Size: 3257 bytes
Desc: not available
URL: </pipermail/smt-lib/attachments/20130721/a39e1763/attachment.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: </pipermail/smt-lib/attachments/20130721/a39e1763/attachment.asc>