[SMT-LIB] simplify test suite and boogie benchmarks in AUFLIA logic

[Michal Moskal]

Hi all,

I've updated, as requested by Clark. The changes are:
- the symbols / and % are not used, uninterpreted divide and modulo
operators are used
- * is only used on constants, otherwise uninterpreted function multiply is used

This probably made some benchmarks that were previously unsatisfiable,
satisfiable (for example is there is an axiom forall x. ... x*y ....,
if it was instantiated with x being constant it would work in the old
translation, but in the new translation, multiply is used in the axiom
instead).

It seems there is only one Boogie benchmark affected by this, namely
Search_Search.Reverse_Div_System.Int32.array_notnull-noinfer.smt,
otherwise fx7 is still able to prove the benchmarks expected to unsat.
It also proves the ones, that were previously in the non-linear
directory, it seems the non-linearity was not crucial.

As for simplify test suite benchmarks, there is several ones, that are
failing for me. I've put them in *_possibly_sat directories.

cvc3 -lang smtlib +translate now reports the benchmarks to be in
AUFLIA logic. BTW, it seems to translate (distinct ...) into quadratic
number of inequalities.

The updated files are:
http://nemerle.org/~malekith/smt/benchmarks/boogie-AUFLIA-2007.05.02.tar.bz2
http://nemerle.org/~malekith/smt/benchmarks/simplify_benchmarks-AUFLIA-2007.05.02.tar.bz2

I would like to bring up the problem of triggers in the benchmarks. I
was hoping for the triggers to be also present in benchmarks in the
competition:
- they are there in the original benchmarks,
- the SMT standard mentions triggers as a possible use for
annotations, it just doesn't define the syntax,
- changing any SMT solver, that currently infers triggers, so that it
can also read the explicit ones seems like a simple hack for me.

I agree it might be controversial to have them introduced that late though...

What do you think about adding them to the SMT standard anyway?

On 4/27/07, Michal Moskal <michal.moskal at gmail.com> wrote:
> Hi,
>
> A while ago I have posted a proposal for a logic for ESC-like software
> verifiers. There was little answer, so I figured that as an
> intermediate step, I could translate the Simplify test suite and
> Boogie benchmarks to the existing AUFLIA logic, by treating everything
> as Int.
>
> This is exactly what the current translation (available in SMT LIB) of
> the Simplify test suite benchmarks does. The translation doesn't make
> use of the builtin arrays, but instead defines its own. We have to
> either do this, or define some kind of casting functions (which I
> proposed in the emails sent in January).
>
> The main differences between my translation and the currently available are:
> - all 2300-something front end test suite benchmarks are translated
> (smt lib currently has around 900), I'll be trying to filter out the
> ones that require non-linear reasoning and flag them
> - small Simplify suite benchmarks are translated - they seem to be much harder
> - Boogie benchmarks (from Spec# website) are translated
> - I use the native (distinct x y z) predicate instead of (= x (+
> dist_1 0)), (= y (+ dist_1 1)), (= z (+ dist_1 2))
> - the triggers are preserved:
>  (PATS t1 (MPAT t2 t3) t4) => :pat { t1 } :pat { t2 t3 } :pat { t4 }
>  (NOPATS t1 t2) => :nopat { t1 } :nopat { t2 }
> It would be great if the scrambler would know about it.
>
> The benchmarks can be found here:
>  http://nemerle.org/~malekith/smt/benchmarks/
> in particular:
>  http://nemerle.org/~malekith/smt/benchmarks/boogie-AUFLIA-2007.04.27.tar.bz2
>  http://nemerle.org/~malekith/smt/benchmarks/simplify_benchmarks-AUFLIA-2007.04.27.tar.bz2
>
> For boogie, there are three directories: valid, invalid and
> non-linear. Valid contains benchmarks that are supposed (by the
> authors) to be unsat (and are actually proven unsat by my prover).
> Invalid contains test cases that are supposed to be sat. Non-linear
> contains testcases that make use of non-linear terms.
>
> Simplify front end test suite benchmarks are all supposed to be valid,
> but the following ones:
>
> javafe.ast.Identifier.003.smt
> javafe.ast.Identifier.010.smt
> javafe.parser.TokenQueue.006.smt
> javafe.util.LocationManagerCorrelatedReader.001.smt
> javafe.ast.Identifier.008.smt
> javafe.parser.TokenQueue.008.smt
>
> contain non-linear terms. The last two don't require the non-linear
> terms to be proven valid.
>
> Simplify small suite benchmarks are also supposed to be all valid, I'm
> currently testing for linearity.
>
> I hope these benchmarks cases will make into 2007 smt comp.
>
> Cheers!
>    Michał
>


-- 
   Michał