solvers: also link MiniSat2 options #3243
Conversation
To be able to parse options again when setting up a solver, the parseOption method has to be present. Hence, link against the Options.cc file of MiniSat2 as well. Signed-off-by: Norbert Manthey <[email protected]>
nmanthey
requested review from
chrisr-diffblue,
kroening,
peterschrammel,
smowton and
tautschnig
as code owners
CBMC compiles with more strict compiler warnings. To make the compiler happy, extend the MiniSat patch to fix the Option.cc file as well.
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: add5598).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/89574875
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.
|
Is the change to minisat/utils/Options.cc useful? |
|
The change to Options.cc is only there to make the CBMC CI build happy.
|
|
Ah, that's the extra { } ? |
|
Lets assume you want to tune MiniSat when its used as CBMC backend. My
MiniSat fork supports being configured via environment variable. Since that
part of new code requires Options.cc, this file has to be linked.
That being said: the PR makes sense in case you want to link against my
MiniSat fork. That would give you some other performance benefits, e.g.
faster simplification. If there is not interest in using another MiniSat,
this PR could be ignored.
That being said, I would love to have a discussion about jumping to my
MiniSat fork, as that might come with other CBMC relevant improvements in
the future.
Best,
Norbert
|
|
Very happy to link in options.cc -- I am mostly wondering whether you can simply drop the "diff to the diff" for options.cc? (Also very happy to benchmark your Minisat fork, independently). |
|
Unfortunately, your CI needs that diff, I tried without before. If you link
against my MiniSat, most of that diff could be dropped, as I carry those
fixes already.
You might want to talk to Michael about benchmarking, he wanted to look
into this as well.
|
|
Ok, I would consider that a bug in the CI, and would prefer to merge without. |
|
Well, that MiniSat code is not used to the aggressive warnings your CI
uses, but it is actually good that you have them. Hence, I do not agree
that this is a CI bug, but more a MiniSat code style issue.
|
|
@nmanthey BTW, does it make sense to point to your fork, eventually? |
|
Sure, the fork lives here: https://github.com/conp-solutions/minisat |
|
On Wed, 2018-10-31 at 04:54 -0700, norbert manthey wrote:
<snip>
That being said: the PR makes sense in case you want to link against
my MiniSat fork. That would give you some other performance benefits,
e.g. faster simplification. If there is not interest in using another
MiniSat, this PR could be ignored.
Maybe it would help to post instructions somewhere so people could try.
Generally if it has no / minimal impact I don't see why we can't
accept this patch.
<snip>
That being said, I would love to have a discussion about jumping to
my MiniSat fork, as that might come with other CBMC relevant
improvements in the future.
There has been a long standing goal to do more in the way of
performance benchmarking. This (IMHO) would be needed before we made
any decisions about changing back-ends.
Cheers,
- Martin
|
|
If desired, I can kick off a run with that version on http://svcomp.cprover.org/ to see what the performance impact is. |
How to build with the my MiniSat fork as backendI put a few commits on top of this one so that CBMC can be compiled with the other MiniSat. That actually required a few more changes, and would require MiniSat changes as well, so that you aggressive warnings are happy with my code extensions. https://github.com/nmanthey/cbmc/tree/conps-minisat The steps to build would be (re-)downloading the solver, which I turned into a git clone, and rebuilding cbmc, e.g. Benchmarking@peterschrammel I'm happy to give that solver a try wrt benchmarking. Is there a way I can evaluate further MiniSat changes with that system? Moving ForwardI can merge the two branches into a single PR, if you want me to do that. I'll make it a separate WIP PR for now. The changes I did on the new branch should not go into CBMC right away. I'd more modify my MiniSat so that I do not have to disable Werror. That currently looks like 2 changes: disable warning for the 2 deprecated pieces of code, and adding a missing pair of brackets. Furthermore, you might not clone the master branch each time, but rather download or checkout a specific release. I need to find time to get the IPASIR interface into that fork, and could imagine turning that code into a release afterwards which could be consumed by you. |
|
Ideally, we should fork minisat into the org and maintain our patches there. This should make it easier to maintain the changes, test and run CI on development versions of it. We could even add a submodule for it if we want. |
|
On Tue, 2018-11-06 at 05:21 -0800, Peter Schrammel wrote:
Ideally, we should fork minisat the org and maintain our patches
there. This should make it easier to maintain the changes, test and
run CI on development versions of it. We could even add a submodule
for it if we want.
I'm not apriori opposed to this. Submodule would seem to be the way to
go.
|
|
I also agree that for you it would be best if you have full control over the code you use. The only problem might be code duplication, as people who contribute to another MiniSat-fork might not automatically feed your MiniSat code - which also does not happen right now. That being said, I am happy to reformat my MiniSat code base to an accepted code style, and motivate other groups working on related SAT solvers to do the same, so that rebasing and cherry-picking is more straight forward as it currently is. |
@nmanthey, running on 9494ebe from your fork now. |
|
Thanks. I guess I have to compare the very last column (my commit) against the one before, because that's the one I rebased on top? |
|
From what I see so far last year's SV-COMP version is by far the fastest on larger benchmarks. We used Glucose there. I'll set up a run with Glucose so that we have a direct comparison between Minisat / tweaked Minisat / Glucose. Side note: On average we spend only ~30% of the time in the SAT solver in SV-COMP. Disclaimer: this is for benchmarks that don't time out only. |
|
I did not know Glucose is the better solver. I wonder why it's not enabled by default then. Note sure whether this should be discussed in this PR, or should be moved into a separate issue, but as we started here, I'll keep it here: Do you know where the time outs come from? I remember some profiling output from Michael which indicated that SAT preprocessing can consume quite a bit of run time, but disabling preprocessing makes the overall performance worse. Does that statement still hold? |
|
Closing this in favour of #6783 (same commits, rebased on top of Any other discussion on this, please feel free to add to the newer PR. |
To be able to parse options again when setting up a solver, the
parseOption method has to be present. Hence, link against the
Options.cc file of MiniSat2 as well.
Signed-off-by: Norbert Manthey [email protected]
Note: For the current CBMC, nothing will change from a feature or performance perspective (except binary size). This change allows to exchange the existing MiniSat with other versions of that solver, especially https://github.com/conp-solutions/minisat. This fork comes with solver performance improvements, and which allows to specify SAT solver parameters via environment variable - to allow SAT solver tuning for CBMC more easily.