Make SimpSolver::reset_constrain_clause public

[tautschnig]

Both Solver::reset_constrain_clause and
SimpSolver::reset_constrain_clause were added in b4fbc0a. The former
is public, while the latter was marked protected for some reason. Make
sure both of them are public as its use is required when doing
incremental solving with intermediate UNSAT results. This is the case as
solve_ invokes deactivate_constrain_clause(status) as last step,
which in turn implies that any subsequent call to failed_constraint()
will return true, and Solver::solve_ thereby always returning
l_False.

[conp-solutions]

Thanks for this PR. This seemingly fixes the issue you ran into. I wonder whether the solver itself should instead make sure a non-global UNSAT result should not block future incremental calls.

Do you have a local test case? Otherwise, I'll create one and fix the underlying usage logic for the constraint interface as well.

[tautschnig]

Thanks for this PR. This seemingly fixes the issue you ran into. I wonder whether the solver itself should instead make sure a non-global UNSAT result should not block future incremental calls.

Maybe :-) Well, perhaps at least when constrain clauses weren't used in the first place?

Do you have a local test case? Otherwise, I'll create one and fix the underlying usage logic for the constraint interface as well.

The only testing I've done is running CBMC's regression test suite - see the call to to reset_constrain_clause that I added in diffblue/cbmc#6439.