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 [email protected] on 17 May 2013 at 11:33