Cse wv

[Wout4]

first version, not extensively tested. TODO: decompose globals

[JoD]

As I understand it now: when creating new reification variables, the code checks whether there already is a variable for the reified expression based on its string representation, and returns that one instead. Makes sense.

• is the representation unique for non-equivalent expressions? E.g., if we have a variable called "1", is x >= 1 represented differently when 1 is the name of the variable or a numeric value.
• is the representation canonical? E.g., do x + y >= 1 and y + x >= 1 have the same representation? This case can be covered by lexicographically ordering the subexpressions of the sum at creation time, which is basically the only thing we need to do (for all commutative expressions).
• the dictionary is passed around a lot, and is initialized in different spots. It's hard to have any guarantee about what's going to be in the dictionary at any timepoint. Would it make sense to have a global dictionary instead?