[SMT-LIB] (distinct ...) in AUFLIA/simplify benchmarks

[Leonardo de Moura]

> I think using types is going to be hard, because I guess it would be
> hard to tell what the type Elem is - you can store arrays, integers
> and other objects in arrays. I guess you would need conversion
> operators to be inserted here and there. So in the end I think that
> mapping everything to Int was a rather clever hack :)

You are correct, the translation is going to be hard. I believe Cesare Tinelli is leading this effort.

The main argument against the "everything is an integer" approach is that the array theory is handled using quantifiers instead of the SMT-LIB array theory. Of course, one may argue that the original benchmark was stated using quantifiers to encode the array theory, and it is not clear whether we should change that or not.


> I noticed these benchmarks to use lots of arithmetic, i.e. my solver
> spending lots of time in arithmetic reasoning. Definitely more than
> Boogie benchmarks and I guess more than ESC benchmarks I was playing
> with previously. This might be because of the true_term being integer
> messing with things - which is my problem.

Yes, this is another nasty side-effect of the translation. The translation assumed that "everything is a function", and the true_term was mapped to 1.

> Also did the original benchmarks have PATS directives? If so, I guess
> they could be copied to SMT format using annotations.

I think this is a good idea.

Cheers,
Leonardo