solver3: Introduce new Assume() and Enqueue() helpers and use them

These are taken roughly from the MiniSAT paper. We still have a bit
to go in actually encoding all clauses so the reasons are still
variables, and Assume() isn't fully working yet.

Adjust the existing Install()/Reject() code to use these functions,
we already see additional lines in the log that we failed to log
before, and this ensures more consistency.

This is sort of still the wrong direction: Install()/Reject() do the
propagation too; but that is tbd.

0 files changed, 0 insertions, 0 deletions