Re: [Toss-devel] Bounded/Guarded Sum

[Lukasz S. <luk...@gm...>]

On Sun, Jun 27, 2010 at 7:05 PM, Lukasz Kaiser <luk...@gm...> wrote:
>> Could you change the Sum construnct into a BoundedSum (or GuardedSum) construct,
>>
>>  BoundedSum of fo_var * formula * real_expr
>>
>> Both are expressible in the other
>>
>>  BoundedSum (v, guard, expr) = Sum (v, Times (Char guard, expr))
>>  Sum (v, expr) = BoundedSum (v, And [], expr)
>>
>> but I believe BoundedSum will result in considerably more efficient
>> calculations of heuristics, because [expr] will not be computed for
>> instances of [v] for which [Char guard = 0].
>> (I promised to commit in the afternoon, but I'll finish generating
>> heuristics and commit tonight I guess...)
>
> You are right in general, but at present the evaluation is so bad,
> that it will not help at all

But perhaps it is enough to just optimize multiplication computation
for the zero case? BoundedSum is better in principle because it allows
for whatever tricks logic has up its sleeve, but the multiplication
optimization would help the translation "Char (And [a; b]) ==>
Times(Char [a], Char [b])" not deteriorate performance.

> There is a TODO in Solver ml to correct
> that - so that evaluating RealExpr uses the contex. But this is some
> larger work, I suggest we stick to what we have for now and get back
> to that later (also important: negation is handled wrong at present,
> because there is some bug for 1-element structures; correcting this
> gives 2x speedup, but I never find enough time to get to it; I hope
> next week will be a bit better, but full real_expr rewrite is too much).
>

I consider it not my department but I could work on it if necessary.