Intelligent Expression rewriting in TotalRewriter

[GoogleCodeExporter]

Currently, TotalRewriter relies on the expressions depth first replacement 
logic to determine which sub-expressions should be checked next for rewriting. 
However, there are cases where it make sense to rewrite nested sub-expressions 
before there parents. An e.g. of this is in R_set_diff when handling 
expressions of this form:

S1 is { Alpha | C }_I and S2 is { Alpha' | C' }_I

it does:

C''<- R_formula_simplification(
       C and for all I' : C' => Alpha != Alpha')
       with cont. variables extended by I 

in this case it ends up being more efficient to simplify the 'for all' 
expression first because if the 'for all' expression is left in the conjunction 
it will be simplified multiple times under different contexts via the 
ConjunctsHoldTrueForEachOther rewriter. By simplifying it beforehand once under 
the intended conjunction you only perform the calculation once and get the 
correct simplification of the 'for all' expression in the overall conjunction 
that can be used to simplify other conjuncts later on in the 
ConjunctsHoldTrueForEachOther logic. 

Likely it would help if the rewriters indicated at a minimum if they did or did 
not look at sub-expressions as part of their simplification logic.

Original issue reported on code.google.com by ctjoreilly@gmail.com on 17 May 2013 at 11:33

[GoogleCodeExporter]

However, sometimes you want to go top down, for e.g. in the case when a 
conjunction contains a 'false' argument it makes more sense to simplify the 
whole expressions first based on this instead of looking at the sub-expressions 
first. Possibly one approach is to run rewriters that don't look at 
sub-expressions first and then run the more expensive sub-expression dependent 
rewriters in a bottom up manner.

Original comment by ctjoreilly@gmail.com on 17 May 2013 at 11:35

[GoogleCodeExporter]

Original comment by ctjoreilly@gmail.com on 17 May 2013 at 11:36

• Added labels: Milestone-Unscheduled