Satcheck need not implement hardness_collectort #5305
Conversation
peterschrammel
requested review from
chrisr-diffblue,
kroening,
smowton and
tautschnig
as code owners
Codecov Report
@@ Coverage Diff @@
## develop #5305 +/- ##
===========================================
- Coverage 68.52% 68.52% -0.01%
===========================================
Files 1187 1187
Lines 98265 98269 +4
===========================================
+ Hits 67339 67341 +2
- Misses 30926 30928 +2
Flags with carried forward coverage won't be shown. Click here to find out more.
Continue to review full report at Codecov.
|
src/goto-checker/solver_factory.cpp
Outdated
| @@ -178,12 +178,16 @@ static std::unique_ptr<SatcheckT> | |||
| make_satcheck_prop(message_handlert &message_handler, const optionst &options) | |||
| { | |||
| auto satcheck = util_make_unique<SatcheckT>(message_handler); | |||
| if(options.is_set("write-solver-stats-to")) | |||
| if(auto hardness_collector = dynamic_cast<hardness_collectort *>(&*satcheck)) | |||
There was a problem hiding this comment.
Hm, the idea was that satchecks that don't want to do hardness collection could just implement these functions as no-ops?
There was a problem hiding this comment.
Then you should have implemented it in all existing satchecks, which are broken now.
Besides, noop functions defeat the purpose of extension interfaces. Thus, I would rather merge this PR.
src/goto-checker/solver_factory.cpp
Outdated
| satcheck->with_solver_hardness([&options](solver_hardnesst &hardness) { | ||
| hardness.set_outfile(options.get_option("write-solver-stats-to")); | ||
| }); | ||
| if(options.is_set("write-solver-stats-to")) |
There was a problem hiding this comment.
I think we should provide an error message to the user in case --write-solver-stats-to is used with a SAT solver that doesn't support hardness collection.
Otherwise compilation fails for SAT solvers that don't implement hardness_collectort yet, e.g. Glucose.
peterschrammel
force-pushed
the
satcheck-no-hardness
branch
from
e8a0d65 to
ab1c041
Compare
Otherwise compilation fails for SAT solvers that don't implement hardness_collectort yet, e.g. Glucose.