Investigate a more guided approach to `Z3CondSimplify`

[surovic]

In Z3CondSimplify, we currently use simplifier tactics made out of combined built-in tactics of Z3. We could try to make our own simplification tactic based on satisfiability queries, similar to ctx-solver-simplify, but tailored for readability and interoperability with other refinements, such as CondBasedRefine or ReachBasedRefine. This could be done via removing sub-expressions and asking the solver if the conditions are still equivalent.

[frabert]

Z3CondSimplify and NestedCondProp have been reworked to employ Z3 as less of a black box in order to improve expression simplification. We may need to re-open this if we want to use a more radical technique (e-graphs?)