Improve solver factory #3588
Improve solver factory #3588
Conversation
peterschrammel
commented
Dec 17, 2018
peterschrammel
commented
- Each commit message has a non-empty body, explaining why the change was made.
- Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- 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).
- My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- White-space or formatting changes outside the feature-related changed lines are in commits of their own.
peterschrammel
requested review from
chrisr-diffblue,
kroening,
smowton and
tautschnig
as code owners
src/goto-checker/solver_factory.cpp
Outdated
| { | ||
| } | ||
|
|
||
| solver_factoryt::solvert::solvert() |
src/goto-checker/solver_factory.cpp
Outdated
| return get_default(); | ||
| } | ||
|
|
||
| solver_factoryt::~solver_factoryt() |
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: ae24500).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/95015757
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.
|
Why? A lot of these seem like the kind of one-liner ideally suited to inline definition |
To be honest, most of our inline definitions seem to be driven by laziness rather than conscious decisions about what to inline for performance or other data-driven reasons. And now that some cleanup is happening, we might as well take a look at those aspects as well. I'm ok with a rule like "you may define any function with up to N statements inline without providing performance data," but right now it seems entirely arbitrary. |
peterschrammel
force-pushed
the
improve-solver-factory
branch
from
ae24500 to
33daefe
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 33daefe).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/95102698
peterschrammel
force-pushed
the
improve-solver-factory
branch
from
33daefe to
0471a5a
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 0471a5a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/95188405
peterschrammel
force-pushed
the
improve-solver-factory
branch
from
0471a5a to
b76cd5f
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: b76cd5f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/95419536
