Add CaDiCaL support to CMake #4758

tautschnig · 2019-06-06T14:28:30Z

Add CMake configuration to build using CaDiCaL, which was already
supported with Makefiles. Also bump the version of CaDiCaL to sr19 and
fix the use of the cnf_solvert interface.

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.

tautschnig · 2019-06-06T14:32:33Z

FWIW: running the regression suite with CaDiCaL appears to be quite a bit slower, but an evaluation on more realistic benchmarks is yet to be done.

smowton

Build script stuff looks fine to me, no opinion on the solvers stuff that I'm not that familiar with

smowton · 2019-06-06T14:49:55Z

src/solvers/CMakeLists.txt

+    download_project(PROJ cadical
+        URL https://github.com/arminbiere/cadical/archive/sr19.tar.gz
+        PATCH_COMMAND true
+        COMMAND CXX=${CXX_COMPILER} CXXFLAGS=-O3 ./configure --debug


Double-check: is the --debug asking configure for verbose output, or setting -g for the build, or could it even be overriding the -O3 given in CXXFLAGS to get -g -O0?

I did double-check when building locally: it just adds -g, the -O3 from CXXFLAGS is passed on as desired.

codecov-io · 2019-06-06T15:19:05Z

Codecov Report

Merging #4758 (528164d) into develop (60feede) will increase coverage by 0.00%.
The diff coverage is 100.00%.

@@           Coverage Diff            @@
##           develop    #4758   +/-   ##
========================================
  Coverage    69.66%   69.67%           
========================================
  Files         1248     1248           
  Lines       100873   100874    +1     
========================================
+ Hits         70278    70279    +1     
  Misses       30595    30595

Flag	Coverage Δ
cproversmt2	`43.38% <0.00%> (-0.01%)`	⬇️
regression	`66.64% <100.00%> (+<0.01%)`	⬆️
unit	`32.19% <50.00%> (+<0.01%)`	⬆️

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files	Coverage Δ
src/solvers/refinement/refine_arithmetic.cpp	`60.37% <ø> (-0.19%)`	⬇️
src/solvers/refinement/bv_refinement_loop.cpp	`94.23% <100.00%> (+0.23%)`	⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 60feede...528164d. Read the comment docs.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 7931e35).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/114606145

thk123

I don't have any strong opinions on this, but it should probably build cadical on CI and run the tests?

thk123 · 2019-06-11T09:47:07Z

src/solvers/sat/satcheck_cadical.cpp

@@ -79,6 +79,21 @@ propt::resultt satcheck_cadicalt::do_prop_solve()
  }
  else
  {
+    // if assumptions contains false, we need this to be UNSAT


⛏️ I don't understand this change or why the assume falses need special casing, but it should probably go in its own commit explaining in more detail why this is required

Preferably with a test that only passes with this

Just for the record: this is done in keeping with other solvers, and thus about the way in which we use the solver interface. I agree that a test would be useful.

BTW, the reason why 'assume false' needs special casing is that SAT solvers don't have a 'false' literal.

src/solvers/sat/satcheck_cadical.cpp

martin-cs

Seems good to me.

peterschrammel

I'd suggest to merge also #5305 so that we can use the other solvers too without having to implement hardness_collectort everywhere.

hannes-steffenhagen-diffblue

@tautschnig I'm noticing that the second commit has quite a few related changes at once. Is there any chance these could be split up into indivial commits that still make sense on their own? No real issue with the changes themselves.

hannes-steffenhagen-diffblue · 2021-01-22T16:23:55Z

src/solvers/CMakeLists.txt

+
+    set_target_properties(
+        cadical
+        PROPERTIES IMPORTED_LOCATION ${cadical_SOURCE_DIR}/build/libcadical.a


This will only work on Linux, is that OK? If cadical also works on Windows/OSX it'd be nice if just used something like find_library here to get a more portable library path.

Cadical's makefile hard-codes this, so I don't think it'll work out of the box on other platforms.

src/solvers/sat/satcheck_cadical.cpp

hannes-steffenhagen-diffblue · 2021-01-22T16:30:18Z

src/solvers/sat/satcheck_cadical.cpp

    }
  }

+  for(const auto &a : assumptions)
+    solver->assume(a.dimacs());


Why do we need to do this now? This wasn't here previously?

Support for assumptions simply was missing before.

tautschnig · 2021-01-22T22:48:45Z

@tautschnig I'm noticing that the second commit has quite a few related changes at once. Is there any chance these could be split up into indivial commits that still make sense on their own? No real issue with the changes themselves.

I'm not entirely convinced this adds value: the previous implementation was pretty broken, and not really usable. All these changes are necessary to make things work.

A SAT instance that is satisfiable need not remain so when adding clauses. Solvers strictly asserting this (such as Cadical) would refuse getting the model of a satisfiable instance after having added further clauses since the last solve() call. Thus, request the values of all approximations first, and only then add further constraints. Doing so makes cbmc-library/Float-div1-refine pass again, even when using Cadical.

Add CMake configuration to build using CaDiCaL, which was already supported with Makefiles. Also bump the version of CaDiCaL to rel-1.3.0 and fix the use of the cnf_solvert interface. Run the ubuntu-18_04-package GitHub PR action with -Dsat_impl=cadical to avoid future regressions. Fixes: diffblue#5348

tautschnig added the Solvers label Jun 6, 2019

tautschnig requested review from chrisr-diffblue, forejtv, kroening, martin-cs, peterschrammel, smowton and thk123 as code owners June 6, 2019 14:28

smowton approved these changes Jun 6, 2019

View reviewed changes

allredj reviewed Jun 6, 2019

View reviewed changes

kroening approved these changes Jun 7, 2019

View reviewed changes

tautschnig assigned thk123, forejtv and peterschrammel Jun 7, 2019

thk123 reviewed Jun 11, 2019

View reviewed changes

peterschrammel reviewed Jun 14, 2019

View reviewed changes

src/solvers/sat/satcheck_cadical.cpp Outdated Show resolved Hide resolved

tautschnig force-pushed the cadical branch from 7931e35 to 0832c09 Compare June 19, 2019 13:33

tautschnig assigned tautschnig and unassigned thk123, peterschrammel and forejtv Jun 19, 2019

tautschnig force-pushed the cadical branch from 0832c09 to 7434d5e Compare October 27, 2020 18:04

tautschnig requested a review from hannes-steffenhagen-diffblue as a code owner October 27, 2020 18:04

tautschnig force-pushed the cadical branch 5 times, most recently from 31b75e2 to ab8b90b Compare November 6, 2020 14:47

martin-cs approved these changes Nov 6, 2020

View reviewed changes

tautschnig assigned peterschrammel and hannes-steffenhagen-diffblue and unassigned tautschnig Nov 6, 2020

peterschrammel approved these changes Nov 6, 2020

View reviewed changes

tautschnig force-pushed the cadical branch from ab8b90b to e71012b Compare November 6, 2020 21:42

tautschnig unassigned peterschrammel Nov 6, 2020

tautschnig force-pushed the cadical branch 2 times, most recently from c442def to d0db452 Compare November 16, 2020 22:15

tautschnig force-pushed the cadical branch from d0db452 to bf17dab Compare November 24, 2020 00:55

tautschnig requested a review from romainbrenguier as a code owner November 24, 2020 00:55

tautschnig force-pushed the cadical branch 2 times, most recently from 575d549 to e8b2338 Compare January 1, 2021 19:50

tautschnig requested a review from a team as a code owner January 1, 2021 19:50

tautschnig force-pushed the cadical branch from e8b2338 to 4d06165 Compare January 2, 2021 10:44

tautschnig mentioned this pull request Jan 15, 2021

Make IPASIR configuration build after solver hardness changes #5710

Merged

3 tasks

tautschnig force-pushed the cadical branch from 4d06165 to af315b5 Compare January 17, 2021 00:39

hannes-steffenhagen-diffblue approved these changes Jan 22, 2021

View reviewed changes

tautschnig assigned tautschnig and unassigned hannes-steffenhagen-diffblue Jan 22, 2021

tautschnig added 2 commits January 22, 2021 22:56

tautschnig force-pushed the cadical branch from af315b5 to 528164d Compare January 22, 2021 23:02

tautschnig merged commit c0b29cb into diffblue:develop Jan 23, 2021

tautschnig deleted the cadical branch January 23, 2021 01:05

Add CaDiCaL support to CMake #4758

Add CaDiCaL support to CMake #4758

Uh oh!

Conversation

tautschnig commented Jun 6, 2019

Uh oh!

tautschnig commented Jun 6, 2019

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

codecov-io commented Jun 6, 2019 • edited by codecov bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

peterschrammel left a comment

Choose a reason for hiding this comment

Uh oh!

hannes-steffenhagen-diffblue left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Jan 22, 2021

Uh oh!

Uh oh!

codecov-io commented Jun 6, 2019 •

edited by codecov bot

Loading

hannes-steffenhagen-diffblue left a comment •

edited

Loading