Simon Cruanes

possible investigation leads: - use a SMT instead of tableau architecture (sidekick?) - imperative CC - use external prover (vendored?)

the option is there, but there must be, in `Cnf`, a decision between rewrite rules and axioms

- [ ] use `Arg.Enum` for i and o - [ ] put `--prelude` in common set of options cc @rafoo

bindings to raygui?

8

are there plans to support [raygui](https://github.com/raysan5/raygui)? It'd be useful to get a quick GUI running in OCaml…

- use module alias to reduce binary bloat - use `(wrapped true)` in dune - move all heavy components (relational combinators, IO, mlist) into separate modules - keep only the...

on pigeon/hole9.cnf it's quite clear. possibly caused by the bitfield for polarity saving that might be erased when we clear the whole bitfield (even though the default polarity might be...

- use a bool flag in the variable to save last phase - use `false` by default (corresponds to this flag being cleared)