Support Gurobi expression trees

[hbierlee]

Initial draft for supporting expression trees. I've had to make many changes to flatten to prevent it from flattening expressions which are supported by the Gurobi expression trees. Now that the Gurobi side is working, I'm making a 2nd pass to make things more principled and stable again, as of course now the other solvers would break. However, it will remain difficult, as we no longer have Flat Normal Form for the later Gurobi transformations.

[tias]

euh, I can not recommend changing flatten...

the way I think about it is that if it accepts expression trees (like z3), then it does not need flatten... flatten outputs FNF and expression trees are very much not FNF.

So... ideally you follow the same flow as Z3; and if there are things that gurobi does not accept then you create a new transformation for that... (which can call flatten if it wants to)