[SMTCOMP] a question on the benchmark scrambler

[Roberto Sebastiani]

On Fri, 21 Jul 2006, Leonardo de Moura wrote:

> Hi Alberto,
>
>> Am I right or not?
>
> Yes you are correct.
>
>> And if I'm right, is there any particular reason why this is not done? Not 
>> that
>> I'm saying that this must (or should) be done, it is more a
>> curiosity...
>
> I didn't do that because in QF_RDL and QF_IDL the linear arithmetic
> atoms should have a specific format:
>
> - (op (- x y) c),
> - (op (- x y) (~ c)),
>
> where op is "=, <, <=, >=, >"
>
> I didn't want to change this format in the output produced by the scrambler
> because some tools may assume it.
>
> Anyway, if nobody depends on this restriction I can modify the scrambler
> to permute equalities.

I suspect barcelogic does depends on this restrictio. Am I wrong?

>
> Leonardo

-- 
------------------------------------------------------------------
Prof. ROBERTO SEBASTIANI
Dip. Informatica e Telecomunicazioni
Fac. Scienze M.F.N., Universita` di Trento    Tel: +39 0461 881514
Via Sommarive 14, I-38050, Trento, Italy      Fax: +39 0461 882093
roberto.sebastiani at dit.unitn.it     http://www.dit.unitn.it/~rseba
------------------------------------------------------------------