Upgrade CaDiCaL to 1.4.1 #6128
Upgrade CaDiCaL to 1.4.1 #6128
Conversation
tautschnig
requested review from
chrisr-diffblue,
kroening,
peterschrammel,
smowton and
a team
as code owners
src/solvers/CMakeLists.txt
Outdated
| @@ -139,7 +139,7 @@ elseif("${sat_impl}" STREQUAL "ipasir-cadical") | |||
| download_project(PROJ cadical | |||
| URL https://github.com/arminbiere/cadical/archive/rel-1.4.0.tar.gz | |||
| PATCH_COMMAND true | |||
| COMMAND ./configure CXX=g++ | |||
| COMMAND CXX=${CMAKE_CXX_COMPILER} ./configure -O3 -s | |||
There was a problem hiding this comment.
Sorry, I'm not sure if this is correct.
I had tried this back when I was working with this, but this has a problem: On MacOS systems, we specify the compiler to be /usr/bin/clang for the C one, and /usr/bin/clang++ for the C++ one, otherwise we get an error while building CBMC.
The problem is though, that CaDiCaL fails to build with clang++ on any (mac) machine that I tried it - I cannot remember the reason exactly (I think it was dependent on some gcc intrinsics, though don't quote me on that).
This is the reason I had hardcoded it to be g++.
There was a problem hiding this comment.
Ah, great call out! Perhaps we should actually upgrade to tag sc2021 then, where this has been fixed: https://github.com/arminbiere/cadical/blob/master/configure#L246. That said, https://github.com/arminbiere/cadical/blob/master/configure#L255 could probably still do with a fix.
There was a problem hiding this comment.
I've updated the branch to use sc2021.
There was a problem hiding this comment.
Wait, I looked into it a bit further, and my previous call is wrong - it just seems that when we build natively with /usr/bin/clang++ the standard isn't set to C++11 by default.
I managed to get it to build by changing that line to:
COMMAND CXX=${CMAKE_CXX_COMPILER} ./configure CXXFLAGS=-std=c++11
but just touching CXXFLAGS is causing the build to break (e.g., if you change it to CXXFLAGS="${CMAKE_CXX_FLAGS} -std=c++11").
I am not sure why it behaves this way though; I thought we setup the standard globally, so I'm surprised it doesn't propagate.
There was a problem hiding this comment.
COMMAND CXX=${CMAKE_CXX_COMPILER} ./configure CXXFLAGS="${CMAKE_CXX_FLAGS} -std=c++11" won't work, because CMake has an interesting approach to quoting. I don't think there's a way to pass anything that uses spaces in this place. So CXXFLAGS=-std=c++11 might actually work.
There was a problem hiding this comment.
Flags updated in this PR.
There was a problem hiding this comment.
@tautschnig Okay, I spent the last hour researching this and I think I now understand what's happening:
- When you pass a
CXX=flag to CaDiCaL'sconfigurescript, for a strange kind of fashion it messes up itsCXXFLAGSas well, losing the configuration for the standard (among other things). - By losing the configuration for the standard,
clang++becomes allergic to some things, for example template syntax (it complains that>>needs to have a space - this is a build error). - As soon as you fix the standard before the configure script is run, then everything is working again.
So just as an example, CXX=/usr/bin/clang++ ./configure is giving us these:
configure: compiling with '/usr/bin/clang++ -W -O -DNDEBUG',/usr/bin/clang++ -W -O -DNDEBUG -I../build -c ../src/analyze.cpp(sample compilation)
But by default it looks like this:
configure: compiling with 'g++ -Wall -Wextra -O3 -DNDEBUG -std=c++0x'g++ -Wall -Wextra -O3 -DNDEBUG -std=c++0x -I../build -c ../src/analyze.cpp.
So the conclusion is that if you manage to patch CXXFLAGS as well before the call to configure, it should work, even with CaDiCaL 1.4.0. Something like CXX=/usr/bin/clang++ CXXFLAGS="-Wall -Wextra -O3 -DNDEBUG -std=c++11" ./configure should work, translated to CMake syntax.
There was a problem hiding this comment.
It seems we might have to wait for the next release as the build issues have been fixed: arminbiere/cadical@c87965f.
Codecov Report
@@ Coverage Diff @@
## develop #6128 +/- ##
========================================
Coverage 75.96% 75.96%
========================================
Files 1508 1508
Lines 163292 163292
========================================
Hits 124052 124052
Misses 39240 39240 Continue to review full report at Codecov.
|
tautschnig
force-pushed
the
cadical_1.4.0
branch
2 times, most recently
from
a266834 to
728f74a
Compare
tautschnig
force-pushed
the
cadical_1.4.0
branch
from
728f74a to
f621084
Compare
Armin Biere has released the version of CaDiCaL competing in the 2021 SAT competition plus additional bug fixes.
CaDiCaL should be built with optimisations turned on, and the compiler must not be hard-coded. This is now consistent with sat_impl=cadical build flags.
tautschnig
force-pushed
the
cadical_1.4.0
branch
from
f621084 to
cd3a177
Compare
Armin Biere has released the version of CaDiCaL competing in the 2021
SAT competition.
More precisely, there's also a tag sc2021 in the CaDiCaL repository, but the changes do not seem to substantially impact performance when evaluated over SV-COMP.Comparing releases 1.3.0 and sc2021 doesn't show any major performance differences, so really this is just to make consistent what the cadical and ipasir-cadical CMake configurations will use.