If we want to implement the memory optimization without the help of the solver, we have to be able to answer the question "are expressions e1 and e2 equivalent?" and "do expressions e1 and e2 differ by a constant?".
Note that this is only needed for expressions inside bus interactions, but since transitivity of equivalence should go across algebraic constraints, the first question is also useful for those.
Equivalence:
The solver generates a set of equivalent expressions for an expression e1 by going through all constraints that share a variable with e1 and "solves" the constraint for e1, i.e. if the constraint is f * e1 - e2 = 0, then e1 is equivalent to e2 / f. This is difficult to model in the constraint system since it would require us to create new expressions. Note that the solver only does this for affine expressions but it also performs linearization. It also does not repeat the process. We have to see how much of equivalence is actually needed.
Constant difference:
This is even trickier. For a pair of expression e1 and e2, the solver iterates over all pairs of equivalent expressions (e1', e2') and then even performs an exhaustive search to find if e1' - e2' is a constant. Again, we need to see what candidates we have and how much of an exhausive search we need to perform.
If we want to implement the memory optimization without the help of the solver, we have to be able to answer the question "are expressions e1 and e2 equivalent?" and "do expressions e1 and e2 differ by a constant?".
Note that this is only needed for expressions inside bus interactions, but since transitivity of equivalence should go across algebraic constraints, the first question is also useful for those.
Equivalence:
The solver generates a set of equivalent expressions for an expression
e1by going through all constraints that share a variable withe1and "solves" the constraint fore1, i.e. if the constraint isf * e1 - e2 = 0, thene1is equivalent toe2 / f. This is difficult to model in the constraint system since it would require us to create new expressions. Note that the solver only does this for affine expressions but it also performs linearization. It also does not repeat the process. We have to see how much of equivalence is actually needed.Constant difference:
This is even trickier. For a pair of expression
e1ande2, the solver iterates over all pairs of equivalent expressions(e1', e2')and then even performs an exhaustive search to find ife1' - e2'is a constant. Again, we need to see what candidates we have and how much of an exhausive search we need to perform.