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

[Leonardo de Moura]

Sorry about that, it was my mistake. I agree with you that the SMT-LIB
DISTINCT should be used. I was playing with the translator and forgot to disable this "hack".

This translation of the Simplify benchmarks will be probably substituted by a more faithful one. An interesting suggestion was to add types and use the SMT-LIB array theory in the translation instead of mapping everything to integers like I did.

Cheers,
Leonardo

-----Original Message-----
From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On Behalf Of Michal Moskal
Sent: Friday, November 03, 2006 12:00 PM
To: smt-lib at cs.nyu.edu
Subject: [SMT-LIB] (distinct ...) in AUFLIA/simplify benchmarks

Hi,

I (and I guess not only I :-) have noticed that you use the following
encoding for (DISTINCT ...) Simplify opertor:

(and (= t1 (+ c 1)) (= t2 (+ c 2)) ...)

which is quite strange for me, as smt-lib format also provides
(distinct ...) operator.

I guess this is not in line with ,,catch benchmarks as they are in the
wild'' principle. It causes performance problems in my prover [1], and
it (at least) used to cause problems in Zap.

I attach a perl script that can be run on all AUFLIA/simplify
benchmarks to fix the problem. It would be great if you could apply it
on official smt-lib.

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

--
   Michał

_______________________________________________
SMT-LIB mailing list
SMT-LIB at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/smt-lib