Binary clause implementation 2017-11

[shnarazk]

related: #51

[shnarazk]

[shnarazk]

Reimplementation plan

The true order of literals in a conflicting binary clause can be determined with two calls of valueLit. Therefore we don't need to allocate a new clause after each conflict.

• Use bWatches, which type, however, is identical to watches.

That's all.

(2018 Jan after 1.5.1): 2 for 1 encoding

data Clause = ... | BiClause Lit Lit | ...   -  as is

data Solver = Solver {
     biWatches :: Vec        -- extensible chain of (blocker, index) for BiClause
   ...

• getNth bWatches $ div n 2 returns n-th BiClause's blocker
• getNth bWatches $ div n 2 + 1 returns n-th BiClause's index for biWatches
• In propagate, biWatches should be handled before watches, as glucose does.
• propagate doesn't need to allocate a new BiClause for a return value.
• All the primitive functions don't need to check literals' order any more.