Add flag for LCM, as well as a reverse method.

The current version compiles, but does not respect the PT changes yet.
The implemented parameters should be functional. By default, LCM is not
active.

When a clause is modified via LCM, tracking the PT level is difficult.
As an over approximation, use the level of the current node. This way, we
can at least use LCM, and still share clauses downwards correctly. For now,
this is good enough, compared to not being able to share clauses at all.

Track the share indexes during LCM. This way, we do not loose sharing
information when doing LCM.

Move vector initialization 2 loops out, to reduce the number of
re-alloactions.

When using an index to point into the learnts vector, make sure the items
in that vector are valid, or in release mode are dropped to not crash the
solver. This was found when using LCM which modified the learnts vector.

The tmp dir variable has been read from $3, while $2 was the actual aim.

In the old version, the wrong variable has been used as index value,
leading to out of bound errors.

If there are no candidate literals to compute a score for, stop the
computation, and skip.

The split variable next has to be initialized, such that in case of
failures during computing the candidates, e.g. due to too small formulas,
there lit_Undef value can still be returned.

Consequently, make sure nobody consumes lit_Undef as an index.

As getting stuck might be due to a race condition, allow the solver to
see this condition more often before actually aborting the search. On the
other hand, make sure we assert before exit, so that debugging would be
doable, and the problem can be identified during fuzzing.

When multiple slaves work on the same node, make sure they do not overwrite
the state of each other. Only set a state to unknown, if the node actually
has an unknown state.

Currently, the stopUnsatChilds option had to be set to write the unsat
state for a node. However, the state should always be written. Hence, the
check for the option is moved closer to actually running the related
algorithm.

In the reduceDB, new clauses are added to the clauses to be shared, but
no clauses are removed. This way, faulty pointers might be used, as the
clauses that are shared might become invalid, or wrong indexes are used.

When we know a level does not have clauses to share, do not lock the level,
but instead skip the level right away.

We should not have unit clauses as conflicts in the first place.

Learnt clauses can become units. Hence, they need to be treated
accordingly, especially added on level 0.

The current implementation would allow to drop first lits of clauses
that are used for splitting. Do not allow this, as this might result
in unsound behavior.

While learning units is good, the extra decision level jumps might be hard
to maintain. Hence, for now, do not use the units right away.

To make sure we do not stop at a higher level, set the lastLevel
accordingly.

When building the debug version of the solver, the added formula is most
of the time reported as unsatisfiable, although it is satisfiable.

This is the invocation to trigger the bug on a 4 core machine:

./pcasso -verb=2 -model -child-count=7 -threads=3 \
        -print-tree -verbosity=6
        cnfs/bug-180394467.cnf

In case a node is solved by receiving shared clauses, make sure
we store the ptlevel for failing before.

As the solver is unsound, we might want to suppress unsat answers, and
turn them into unknown, to result in a sound solver for satisfiable
formulas again, without fixing the bug in the first place.

Show a little more info about state evaluation in verbose mode.

We need to track causalities of dropped literals. This was not
implemented in original LCM.

Signed-off-by: Norbert Manthey <[email protected]>