add the ability to inline a symbol in a set

[redianthus]

This will be used in Owi (or maybe the simplification makes sense directly in Smt.ml, we'll see).

The idea is that, when we add something like symbol_0 = 42 in the PC. Then, we can propagate the equality and replace symbol_0 by 42 in order to simplify the PC and save time/solver calls in the remaining execution.

This is a quick draft, I'll finish it soon.

[redianthus]

@filipeom, should be good to review now. It finally decided that the function should take an expression and a map from symbol to expression as input, which is how we'll be using it in Owi. Let me know if you can think of a better API (or naming :-)).

While reading the code around, I also noticed some pattern matching that could be simplified a little bit and decided to commit all of this together, sorry about this 😅

[filipeom]

@filipeom, should be good to review now. It finally decided that the function should take an expression and a map from symbol to expression as input, which is how we'll be using it in Owi. Let me know if you can think of a better API (or naming :-)).

While reading the code around, I also noticed some pattern matching that could be simplified a little bit and decided to commit all of this together, sorry about this 😅

Thanks for taking the time to do this! I had a small question below. Regarding naming, I'm probably the worst person to suggest any change 😅 I actually like the API you're proposing

[redianthus]

@filipeom PTAL :)

[filipeom]

LGTM! I can merge if you want 😄

[redianthus]

Thanks! I merged directly ~~

[filipeom]

Thanks! 🙏