Update CaDiCaL from 2.0.0 to 2.2.0

Update to the latest release.

Author: tautschnig

scripts/cadical-2.0.0-patch renamed to scripts/cadical-2.2.0-patch

@@ -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,14 @@ 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")
+    target_compile_options(cadical PRIVATE -DNBUILD -DNFLEXIBLE -DNDEBUG -Wno-error=switch-enum)
+else()
+    target_compile_options(cadical PRIVATE -DNBUILD -DNFLEXIBLE -DNDEBUG)
+endif()
 
 set_target_properties(
     cadical

scripts/cadical_CMakeLists.txt

@@ -186,7 +186,7 @@ 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

src/Makefile

@@ -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/CMakeLists.txt

@@ -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.cpp

@@ -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;