Update CaDiCaL from 2.0.0 to 2.2.0

.github/workflows/pull-request-checks.yaml

@@ -545,7 +545,7 @@ jobs:
           echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
           echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
       - name: Configure using CMake
-        run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical" -DCMAKE_CXX_FLAGS=-m32
+        run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical" -DCMAKE_C_FLAGS=-m32 -DCMAKE_CXX_FLAGS=-m32
       - name: Zero ccache stats and limit in size
         run: ccache -z --max-size=500M
       - name: Build with Ninja

scripts/cadical_CMakeLists.txt

@@ -1,4 +1,4 @@
-file(GLOB sources "src/*.cpp" "src/*.hpp" "src/*.h")
+file(GLOB sources "src/*.cpp" "src/*.c" "src/*.hpp" "src/*.h")
 # Remove "app" sources from list
 list(REMOVE_ITEM sources
     "${CMAKE_CURRENT_SOURCE_DIR}/src/cadical.cpp"
@@ -9,7 +9,33 @@ add_library(cadical ${sources})
 
 # Pass -DNBUILD to disable including the version information, which is not
 # needed since cbmc doesn't run the cadical binary
-target_compile_options(cadical PRIVATE -DNBUILD -DNFLEXIBLE -DNDEBUG)
+if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU")
+    target_compile_options(
+        cadical
+        PRIVATE
+        -DNBUILD -DNFLEXIBLE -DNDEBUG
+        -Wno-error=switch-enum
+    )
+elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
+       "${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang")
+    if (CMAKE_HOST_SYSTEM_NAME STREQUAL Darwin)
+        target_compile_options(
+            cadical
+            PRIVATE
+            -DNBUILD -DNFLEXIBLE -DNDEBUG -DNCLOSEFROM
+            -Wno-error=switch-enum
+        )
+    else()
+        target_compile_options(
+            cadical
+            PRIVATE
+            -DNBUILD -DNFLEXIBLE -DNDEBUG
+            -Wno-error=switch-enum
+        )
+    endif()
+else()
+    target_compile_options(cadical PRIVATE -DNBUILD -DNFLEXIBLE -DNDEBUG)
+endif()
 
 set_target_properties(
     cadical

src/Makefile

@@ -186,14 +186,14 @@ glucose-download:
 	@(cd ../glucose-syrup; patch -p1 < ../scripts/glucose-syrup-patch)
 	@$(RM) $(glucose_rev).tar.gz
 
-cadical_release = rel-2.0.0
+cadical_release = rel-2.2.0
 cadical-download:
 	@echo "Downloading CaDiCaL $(cadical_release)"
 	@$(DOWNLOADER) https://github.com/arminbiere/cadical/archive/$(cadical_release).tar.gz
 	@$(TAR) xfz $(cadical_release).tar.gz
 	@rm -Rf ../cadical
 	@mv cadical-$(cadical_release) ../cadical
-	@(cd ../cadical; patch -p1 < ../scripts/cadical-2.0.0-patch)
+	@(cd ../cadical; patch -p1 < ../scripts/cadical-2.2.0-patch)
 	@(cd ../cadical && ./configure CXX="$(CXX)")
 	# Need to rename VERSION so that it isn't picked up by `#include<version>` on
 	# macOS which is case insensitive

src/solvers/CMakeLists.txt

@@ -121,11 +121,11 @@ foreach(SOLVER ${sat_impl})
         message(STATUS "Building solvers with cadical")
 
         download_project(PROJ cadical
-            URL https://github.com/arminbiere/cadical/archive/rel-2.0.0.tar.gz
-            PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-2.0.0-patch
+            URL https://github.com/arminbiere/cadical/archive/rel-2.2.0.tar.gz
+            PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-2.2.0-patch
             COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/cadical_CMakeLists.txt CMakeLists.txt
             COMMAND ./configure
-            URL_MD5 9fc2a66196b86adceb822a583318cc35
+            URL_MD5 856484d1a022ca22826fc6d67432e1d1
         )
 
         add_subdirectory(${cadical_SOURCE_DIR} ${cadical_BINARY_DIR})
@@ -144,10 +144,10 @@ foreach(SOLVER ${sat_impl})
         message(STATUS "Building with IPASIR solver linking against: CaDiCaL")
 
         download_project(PROJ cadical
-            URL https://github.com/arminbiere/cadical/archive/rel-2.0.0.tar.gz
-            PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-2.0.0-patch
+            URL https://github.com/arminbiere/cadical/archive/rel-2.2.0.tar.gz
+            PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-2.2.0-patch
             COMMAND ./configure
-            URL_MD5 9fc2a66196b86adceb822a583318cc35
+            URL_MD5 856484d1a022ca22826fc6d67432e1d1
         )
 
         message(STATUS "Building CaDiCaL")

src/solvers/Makefile

@@ -282,7 +282,8 @@ solvers$(LIBEXT): $(OBJ) $(SOLVER_LIB)
 	$(LINKLIB)
 
 ../../cadical/build/libcadical$(LIBEXT):
-	$(MAKE) $(MAKEARGS) -C $(CADICAL)/build libcadical.a CXX="$(CXX)" CXXFLAGS="$(CP_CXXFLAGS) -DNFLEXIBLE -DNDEBUG"
+	$(MAKE) $(MAKEARGS) -C $(CADICAL)/build libcadical.a CXX="$(CXX)" \
+		CXXFLAGS="$(filter-out -Wswitch-enum, $(CP_CXXFLAGS)) -DNFLEXIBLE -DNDEBUG -DNCLOSEFROM"
 
 -include smt2/smt2_solver$(DEPEXT)
 

src/solvers/sat/satcheck_cadical.cpp

@@ -27,11 +27,11 @@ tvt satcheck_cadical_baset::l_get(literalt a) const
   if(a.var_no() > narrow<unsigned>(solver->vars()))
     return tvt(tvt::tv_enumt::TV_UNKNOWN);
 
-  const int val = solver->val(a.dimacs());
+  const int val = solver->val(a.var_no(), true);
   if(val>0)
-    result = tvt(true);
+    result = tvt(!a.sign());
   else if(val<0)
-    result = tvt(false);
+    result = tvt(a.sign());
   else
     return tvt(tvt::tv_enumt::TV_UNKNOWN);
 
@@ -140,6 +140,35 @@ void satcheck_cadical_baset::set_assignment(literalt a, bool value)
   INVARIANT(false, "method not supported");
 }
 
+#  if 0
+/// Generate a new variable and return it as a literal
+/// \return New variable as literal
+literalt satcheck_cadical_baset::new_variable()
+{
+  int new_var_index = solver->declare_more_variables(1);
+  CHECK_RETURN(new_var_index >= 0);
+  set_no_variables(new_var_index + 1);
+  return literalt{static_cast<literalt::var_not>(new_var_index), false};
+}
+
+/// Generate a vector of new variables.
+/// \return Vector of new variables.
+bvt satcheck_cadical_baset::new_variables(std::size_t width)
+{
+  bvt result;
+  result.reserve(width);
+
+  for(std::size_t i = _no_variables; i < _no_variables + width; ++i)
+    result.emplace_back(i, false);
+
+  int new_max_var_index = solver->declare_more_variables(width);
+  CHECK_RETURN(new_max_var_index >= 0);
+  set_no_variables(new_max_var_index + 1);
+
+  return result;
+}
+#  endif
+
 satcheck_cadical_baset::satcheck_cadical_baset(
   int _preprocessing_limit,
   int _localsearch_limit,
@@ -150,6 +179,12 @@ satcheck_cadical_baset::satcheck_cadical_baset(
     localsearch_limit(_localsearch_limit)
 {
   solver->set("quiet", 1);
+  // Explicitly disable bounded variable addition; this is disabled by default
+  // in version 2.2.0, but will be enabled in the next major release. Early
+  // experiments, however, suggest that this results in degraded performance. If
+  // we ever choose to enable it then the above overrides of `new_variable` and
+  // `new_variables` need to be enabled.
+  solver->set("factor", 0);
 }
 
 satcheck_cadical_baset::~satcheck_cadical_baset()

src/solvers/sat/satcheck_cadical.h

@@ -44,6 +44,11 @@ class satcheck_cadical_baset : public cnf_solvert, public hardness_collectort
   }
   bool is_in_conflict(literalt a) const override;
 
+#if 0
+  literalt new_variable() override;
+  bvt new_variables(std::size_t width) override;
+#endif
+
 protected:
   resultt do_prop_solve(const bvt &assumptions) override;