Jannis Harder

This, including the comment, is copied from Ghidra's PPC definitions. Without the vectorPermute pcodeop defined, the PPCEmulateInstructionStateModifier class produces an exception, breaking all Ghidra functionality that depends on pcode emulation.

#21 introduced sampling modes, which need to be documented in the manual. This is probably best done after #22 landed.

Solver configuration should be documented in the manual.

Varisat's own proof format is intentionally unspecified and without stability guarantees (so it can always be kept in sync with all implemented techniques). I do want to support checking proofs...

Slowly the CLI is becoming non-trivial, so it really should be tested to make sure it doesn't break.

I want to have something like the [visualzation done with Cryptominisat 3](https://www.msoos.org/sat_visualization/) built in. This requires efficient data logging that has almost no overhead when disabled.

Making it easy to run a SAT solver in the browser.

I'd love to have python bindings for varisat to do quick experiments from jupyter notebooks.

Right now every time new units are found, the formula is simplified. If this happens often, it'd be better to do the simplification in batches.

Implement addition of non-transitive hyper binary resolvents using in-tree based probing. Described in ["Revisiting Hyper Binary Resolution"](https://link.springer.com/chapter/10.1007%2F978-3-642-38171-3_6). This finds implied binary clauses, so I want to implement this before I...