Move command framer to microcode
Closed this issue · 1 comments
MattWindsor91 commented
If command framing happens at the Microcode
level instead of the BoolExpr
level, then we have more/easier access to information about:
- Exactly which variables are being written to—in fact, we could reuse the write map code from normalisation;
- Which variables have been
havoc
ed and thus have no assigned value; - The fact that only variables are being assigned, since
BoolExprs
are a lot more freeform. So, type safety.
I'm thinking of pushing this through as part of the run-up to #104, but whether or not we need #104 for symbolics is unclear at the moment.
MattWindsor91 commented
Closed by #119.