feat: add Valaig package for Aiger solving in Blase

[georgerennie]

Fixes #1906. This adds Valaig as a dependency and replaces the debugDumpAiger config option with solveRIC3. There are many sorries still on this code path and certificates aren't checked yet, but this should at least allow getting some performance numbers. I'm not particularly convinced yet that there aren't bugs here, so please let me know if you see weird behaviour!

This assumes you have rIC3 installed an on your path, and defaults to solving with the single threaded ic3 engine currently.

[bollu]

I asked for two changes. Overall, this is fantastic! I want to use if-then-else instead of early returns to make control flow super duper obvious, and secondly, I want to not use sorry, and instead just use axioms.

[georgerennie]

I've pushed a new version that uses a load of changes to Valaig, the main differences being:

• There are now no sorries in the lowering to Aiger! This is just proofs of structural properties of the Aig however, the semantic preservation is still to come
• The conversion from Blase's representation to Valaig's is simpler, using a new fromStd method in Valaig that just requires Blase to provide information about which atoms are inputs/latches
• The config option has changed to externalSolver to enable an external solver, and externalSolverConfig to set the config. This currently defaults to rIC3's ic3 engine with a 5s timeout and requires rIC3 to be installed on the machine. externalSolver defaults to false so must be set to true to enable this

[bollu]

Awesome! @georgerennie, hit merge :)