Z3 all the things

[frabert]

Converts Rellic to operate on Z3 expressions for as long as possible, only materializing to Clang AST before expression simplification.

Also keeps conditions in CNF without exponential blowup with a neat trick*

*it's still quadratic tho

[frabert]

Also removes a bunch of options from the external API. I figured nobody was actually using them, and if someone actually needs the amount of control it provided, they may as well use the passes manually

[frabert]

Unfortunately this still seems way too slow to be actually usable, especially on some Anvill-produced modules

[surovic]

Overall great work! May the Z3ConvVisitor rest in piece.

PS: I haven't gotten to GenerateAST.(h|cpp) or IRToASTVisitor.(h|cpp) yet, but could you add some short comments to the affected parts? Think "if there's a blank line, I might as well use it for a short comment describing what follows".

[frabert]

There wasn't much change in GenerateAST or IRToASTVisitor, I mainly just moved the Z3->C conversion from one to the other because it now needs to happen later in the process.

[frabert]

I think this is ready for merge now