propt: change interface for solving under assumptions

[kroening]

This changes the interface offered by propt for 'solving under assumptions' from a state-ful variant to the state-less API that MiniSat uses.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[martin-cs]

Seems reasonable and stateless does make things simpler. I wonder if there is a way to tweak the API so that you can also get back the set of necessary assumptions if it is UNSAT.

[kroening]

Seems reasonable and stateless does make things simpler. I wonder if there is a way to tweak the API so that you can also get back the set of necessary assumptions if it is UNSAT.

That would be nice -- I can't think of a nice way to do that without state however. Note we already have is_in_conflict(...).

[codecov]

Codecov Report

Attention: 5 lines in your changes are missing coverage. Please review.

Comparison is base (a010865) 78.45% compared to head (9508799) 78.06%.
Report is 4 commits behind head on develop.

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #7976      +/-   ##
===========================================
- Coverage    78.45%   78.06%   -0.39%     
===========================================
  Files         1701     1701              
  Lines       196270   196325      +55     
===========================================
- Hits        153976   153258     -718     
- Misses       42294    43067     +773     

Files	Coverage Δ
src/solvers/prop/prop.cpp	65.21% <100.00%> (+7.32%)	⬆️
src/solvers/prop/prop_conv_solver.cpp	87.35% <100.00%> (-0.15%)	⬇️
src/solvers/refinement/bv_refinement_loop.cpp	98.43% <100.00%> (ø)
src/solvers/sat/cnf_clause_list.h	80.00% <100.00%> (ø)
src/solvers/sat/external_sat.cpp	80.45% <100.00%> (ø)
src/solvers/sat/satcheck_minisat2.cpp	63.39% <100.00%> (+0.24%)	⬆️
src/solvers/sat/satcheck_minisat2.h	75.00% <100.00%> (ø)
unit/solvers/sat/satcheck_minisat2.cpp	100.00% <100.00%> (ø)
src/solvers/sat/dimacs_cnf.h	27.27% <0.00%> (ø)
src/solvers/sat/external_sat.h	0.00% <0.00%> (ø)
... and 2 more

... and 75 files with indirect coverage changes

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[tautschnig]

How about just using {} as an argument here instead of the static local?

[kroening]

The idea is that the static prevents the creation of a new object, and hence, would be a tiny bit more efficient. But that may well not be measurable.