Knowledge of Z3, I guess ? It calls the simplification function (which is exposed as Z3.Expr.simplify in the ml-ng bindings) before solving. It's a bit more complicated when in the so-called "interactive" mode but still doing it. Note that the function is still useful when printing the formula for debugging purposes.Can you also explain in more depth your justification of Z3 doing expression simplification on my behalf for anything submitted? That was also my guess, but I didn't have that substantiated before my colleagues, so I wanted to be thorough.
I mean that, for a solver like Z3, two encodings of the same problem can result in different results (between UNSAT and UNKNOWN, in particular) and can result, and that's more sneaky, in completely different performance profiles. Solvers (and Z3 in particular) uses heuristics to know which branches to solve first so it's rather guess-y.
Shape?? I don't know what you mean.
If you are looking to encode an SSA control flow graph in Z3's SMT, I have the code to do that. I could extract it and get it into shape. It's based on llvm's IR, but It should be fairly reusable. Tell me if you are interested.
In any case, my plan was to use OCamlgraph and some hash-consing to construct correspondingly equivalent semantics, then reason about it in a distributed fashion.