refactor: remove AIG optimizations

[hargoniX]

In investigating #82 I first tried to see how much the constant folding optimizations actually get us. Funnily enough it turns out that they make us slower. For example Eval.Popcount is a problem that has lots of constant folding present:

def optimized (x : BitVec 32) : BitVec 32 :=
    let x := x - ((x >>> 1) &&& 0x55555555);
    let x := (x &&& 0x33333333) + ((x >>> 2) &&& 0x33333333);
    let x := (x + (x >>> 4)) &&& 0x0F0F0F0F;
    let x := x + (x >>> 8);
    let x := x + (x >>> 16);
    x &&& 0x0000003F

The baseline with optimizations enabled is a total runtime of 2.9s with:

• 8577 AIG nodes
• 24503 CNF clauses
• a CaDiCal runtime of 1.33s
• a checker runtime of 1.37s

On the other hand with this PR the new total run time is 1.4s with:

• 10114 AIG nodes
• 30080 CNF clauses
• a CaDiCal runtime of 0.68s
• a checker runtime of 0.5s

It would thus appear that optimizing the AIG in this way is confusing the SAT solver more than it's helping it and we should consider just removing them entirely.

Note that this does not generally disable constant folding as the pre processor is still capable of partial symbolic evaluation of the terms that are given, though not at a bit precise level like the AIG.

Interestingly Bitwuzla implements all AIG optimizations from the paper: https://github.com/bitwuzla/bitwuzla/blob/main/src/lib/bitblast/aig/aig_manager.cpp#L183-L391

[hargoniX]

Decided not to do this as in big problems constant propagation might actually be highly relevant, simply to reduce the size of problems.