Incremental postsolve in TD3

[sim642]

Closes #368.

This PR is built on top of #370. It makes TD3 implement its own top-down postsolving, which additionally knows about all the TD3-specific incremental data structures to know what definitely doesn't need to be re-evaluated.

For verify, it uses a superstable set, consisting of loaded stable and every removal from stable permanently removes the node from superstable. Nothing ever gets added back there. After solving superstable contains all the variables that were continuously stable, hence definitely unchanged. These are considered the initially reachable set, which stops the top-down verify naturally.

Incremental warnings are a pain though: the correct constraint system Var module for hashtable usage is just available inside the solver itself. So TD3 hooks into the right-hand sides and the message system to know which warnings come from where.
Incrementally, the warnings at superstable nodes still apply, the rest gets filled in by postsolving again and recorded in var_messages for incremental re-save.

This is quite hacky, but the best we can do without putting warnings into the domain (which would have numerous bigger issues on its own).
Also this breaks race detection warnings because Access module uses its own global hashtables that are correctly filled in only when the entire program is re-verified. Incremental verification therefore gives incomplete race warnings and without major redesign of race warnings, it's not possible to get them incrementally.

[sim642]

Merging into the branch interactive for better experimentation.