Print new top level expressions to human-readable rule trace

[niklasdewally]

• fix(rewrite_naive): remove duplicate log print for rule application
• rewriter: log new top level vars to human rule trace

[ozgurakgun]

The outputs look good! We also want the domains of the new aux variables though, is this easy to do? I think these should be in the symbols field.

(a != SafeDiv(b, c)), 
   ~~> flatten_binop ([("Minion", 4400)]) 
(a != __0) 
with new declarations:
  find __0 : some domain
with new constraints:
  __0 =aux SafeDiv(b, c)

[niklasdewally]

Added symbol table logs @Soph1514 @ozgurakgun

[niklasdewally]

Closes #526

[ozgurakgun]

I am fiddling with the output slightly, will push to this branch in a minute.

I noticed you talk about removed variables. I don't think we will remove variables in these local rules per se, instead that might be a global pass once all expressions are rewritten. Variables that are not referenced from any expression can be dropped, for example.

Removing in a local rule is tricky since you need to know if the same var is used in other places or not before you can remove it...

[ozgurakgun]

Updating the domain, on the other hand, should be possible.

[ozgurakgun]

I now notice something I had missed. The symbols field in Reduction copies all the symbols in the original model. I thought it would only contain the new symbols, like new_top.

Just noting for now that an alternative would be to only store the new symbols in the Reduction and extend the model once a rule is applied. I won't change the current behaviour.

[niklasdewally]

I noticed you talk about removed variables. I don't think we will remove variables in these local rules per se, instead that might be a global pass once all expressions are rewritten. Variables that are not referenced from any expression can be dropped, for example.

Removing in a local rule is tricky since you need to know if the same var is used in other places or not before you can remove it...

My assumption was that we can use the same APIs for both local and global rules (as discussed on Teams)

[ozgurakgun]

I guess we will have to think about these global rules at some point :)