Consider integrating 3rd-party expression simplifiers/solvers

[pfalcon]

Currently, ScratchABlock uses adhoc expression simplification implementation, which is partly imperative code, partly semi-declarative poor man's inference engine, and is far from complete in coverage, developed in on-demand manner.

At the same time, 3rd-party project solving this matter definitely exist.

My approach to this is similar to why the project was started in the first place. Expression simplification is only part of decompilation, and as there're many parts, a small part. And no 3rd-party would work as needed, so instead of working on decompilation, it would be restling with a 3rd-party library.

Well, that's of course a rather conservative approach, reusing existing libraries could save a bunch of work too. So, this ticket is opened to called ideas/references and solicit feedback/contributions from developers with more experience in this area.

[pfalcon]

Miasm:

https://github.com/cea-sec/miasm/blob/master/test/expression/simplifications.py

[pfalcon]

Z3:

Typical case with Z3: https://stackoverflow.com/questions/30736834/simplifying-z3-expressions . In other words, it can simplify expressions... The way it finds it useful, not the way you need.

[pfalcon]

angr:

angr's claripy: https://github.com/angr/claripy/blob/master/claripy/operations.py#L131

[pfalcon]

SymPy:

SymPy doesn't have explicit bitvector type (can't and/or/xor numbers!), but supports modular arithmetics: sympy/sympy#13821

[pfalcon]

Sage:

Searching Sage docs doesn't give hints for explicit type like bitvector, but the word is mentioned in the doc, and interwebs have it mentioned to in Sage contexts. So, something is there...