[SMT-LIB] Fwd: logic for ESC/Java and Boogie benchmarks

[Michal Moskal]

Sorry, of course I wanted to mail the list...

---------- Forwarded message ----------
From: Michal Moskal <michal.moskal at gmail.com>
Date: Jan 18, 2007 9:25 PM
Subject: Re: [SMT-LIB] logic for ESC/Java and Boogie benchmarks
To: Clark Barrett <barrett at cs.nyu.edu>


On 1/13/07, Clark Barrett <barrett at cs.nyu.edu> wrote:
> > While I still haven't got the original Simplify files that were used
> > to generate those (maybe somebody has them around?), I have some other
> > ESC/Java benchmarks generated by running it on parts of its own source
> > code. I also used Boogie benchmarks available on the Spec# web page.
>
> The benchmarks can be found bundled with the Simplify theorem prover.  I put up
> a tarball of the benchmarks here:
> http://www.cs.nyu.edu/~barrett/tmp/simplify_benchmarks.tar.gz
>
> We've been looking at doing the same translation ourselves, but I'm always
> happy to let someone else do the work :)
>
> We'll take a closer look at your translation and get back to you about it.

I've put an improved translation of the benchmarks online [1].

The changes are:
  1. fixed handling of DEFPRED (it's no longer treated as a macro)
  2. removal of empty and one-term (distinct ...) (there are things
like that in simplify_benchmarks)
  3. support for DEFPREDMAP as well as some other glitches for
ESC/Modula-3 examples
  4. change in the output encoding from utf8 (with BOM) to ASCII

I've also set the :status of the examples according to my best
knowledge. :status sat means that both fx7 and Simplify say sat on an
example, which basically proves nothing, but is some indication. In
Boogie examples it is also the intended (by the human being creating a
given testcase) status.

As for the 4. -- the smtlib parser currently ignores unknown
characters, I don't think this is the best idea, I'll submit a patch
for it later.

[1] http://nemerle.org/~malekith/smt/benchmarks/


--
   Michał


-- 
   Michał