When a new clauses is added and it is a conflict (i.e all atoms
are false), one must take care of which literals to watch.
In order to work, the watched literals must be those with the higher
decision levels, or else the watched literals might not react when
needed. This is fixed by sorting the literals in decreasing order of
decision level when adding a new clause which happens to be false in the
current trail.
Apart from new assumptions, clause level can always
be computed from the histoy of the clause, so it is
better to do it in Solver_types when creating clauses.
Aditionally, it seems there was an error in the manual
computing of clause level somewhere, this fixes the bug.
Apart from new assumptions, clause level can always
be computed from the histoy of the clause, so it is
better to do it in Solver_types when creating clauses.
Aditionally, it seems there was an error in the manual
computing of clause level somewhere, this fixes the bug.
This ensures that the same solver_types module is not reused
for two different solvers, which would be problematic.
Marked minor because of the low use of multiple instances of a solver.
When the solver finds a SAT result, it sends the whole
model to the theory, because maybe it can do something
interesting/costly to expand the proof search. After
that there must be a check to see if the theory has effectively done
something, in which case we should resume proof search, or if nothing
has been done, in which case the solver should return that the problem
is satisfiable. That check was incorrect before (checking number of
assumptions, and if the queue is all caught up), because new learnt
clauses (i.e tautologies, which are *not* assumptions) can be added that
do not immediately causes propagation, so that the number of assumptions
and the element queue is constant, but we should still resume the
search.
Thgis is meant to be used for debugging and/or benchmarking purposes.
For instance, when using msat in an application, all unsat cores can
be output this way to different files so that the results can be checked
and easily reproduced in case of errors.
