Update CaDiCaL to version 1.0.3. (#3137)

* Removes incremental API check (#3011)
* Fixes toSatValueLit to use the new semantics of CaDiCaL's val()

Fixes #3011

diff --git a/cmake/ConfigureCVC4.cmake b/cmake/ConfigureCVC4.cmake
index cdf8e4d9a7efde1f1683ccaa419671b7c7025d6b..67c1f414d0a1478f651de247d1970fdb277c8ac0 100644 (file)
--- a/cmake/ConfigureCVC4.cmake
+++ b/cmake/ConfigureCVC4.cmake
@@ -67,20 +67,6 @@ check_symbol_exists(sigaltstack "signal.h" HAVE_SIGALTSTACK)
 check_symbol_exists(strerror_r "string.h" HAVE_STRERROR_R)
 check_symbol_exists(strtok_r "string.h" HAVE_STRTOK_R)
 
-# Check whether the verison of CaDiCaL used supports incremental solving
-if(USE_CADICAL)
-  check_cxx_source_compiles(
-    "
-    #include <${CaDiCaL_HOME}/src/cadical.hpp>
-    int main() { return sizeof(&CaDiCaL::Solver::assume); }
-    "
-    CVC4_INCREMENTAL_CADICAL
-  )
-  if(CVC4_INCREMENTAL_CADICAL)
-    add_definitions(-DCVC4_INCREMENTAL_CADICAL)
-  endif()
-endif()
-
 # Determine if we have the POSIX (int) or GNU (char *) variant of strerror_r.
 check_c_source_compiles(
   "

diff --git a/contrib/get-cadical b/contrib/get-cadical
index 359afaaa79a3a2f8268351e92ef86a59c75d454c..6cc1208c6fd4dc49870070c036d2fd3b0c7d80f4 100755 (executable)
--- a/contrib/get-cadical
+++ b/contrib/get-cadical
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 #
 source "$(dirname "$0")/get-script-header.sh"
 
@@ -7,11 +7,13 @@ if [ -e cadical ]; then
   exit 1
 fi
 
-commit="b44ce4f0e64aa400358ae3a8adb45b24ae6e742c"
+version="rel-1.0.3"
 
-git clone https://github.com/arminbiere/cadical cadical
+webget "https://github.com/arminbiere/cadical/archive/$version.tar.gz" "cadical-$version.tar.gz"
+tar xfvz "cadical-$version.tar.gz"
+rm "cadical-$version.tar.gz"
+mv "cadical-$version" cadical
 cd cadical
-git checkout $commit
 
 CXXFLAGS="-fPIC" ./configure && make -j$(nproc)
 

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 15436646f0b2fd20e5ed8cc10e0903c8fe1b8dab..b0a1cd1ad54c983ac101cd59cccf74dc4fe405f7 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -1174,17 +1174,6 @@ theory::bv::SatSolverMode OptionsHandler::stringToSatSolver(std::string option,
   }
   else if (optarg == "cadical")
   {
-#ifndef CVC4_INCREMENTAL_CADICAL
-    if (options::incrementalSolving()
-        && options::incrementalSolving.wasSetByUser())
-    {
-      throw OptionException(std::string(
-          "CaDiCaL version used does not support incremental mode. \n\
-                       Update CaDiCal or Try --bv-sat-solver=cryptominisat or "
-          "--bv-sat-solver=minisat"));
-    }
-#endif
-
     if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY
         && options::bitblastMode.wasSetByUser())
     {

diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index b4851f945e6a33bd4833fdce298b22fada9c6050..479ec2414cc8e9a815e27fe5991aae64c0e9f1e8 100644 (file)
--- a/src/prop/cadical.cpp
+++ b/src/prop/cadical.cpp
@@ -37,10 +37,12 @@ SatValue toSatValue(int result)
   return SAT_VALUE_UNKNOWN;
 }
 
+/* Note: CaDiCaL returns lit/-lit for true/false. Older versions returned 1/-1.
+ */
 SatValue toSatValueLit(int value)
 {
-  if (value == 1) return SAT_VALUE_TRUE;
-  Assert(value == -1);
+  if (value > 0) return SAT_VALUE_TRUE;
+  Assert(value < 0);
   return SAT_VALUE_FALSE;
 }
 
@@ -119,7 +121,6 @@ SatValue CadicalSolver::solve(long unsigned int&)
 
 SatValue CadicalSolver::solve(const std::vector<SatLiteral>& assumptions)
 {
-#ifdef CVC4_INCREMENTAL_CADICAL
   TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
   for (const SatLiteral& lit : assumptions)
   {
@@ -129,9 +130,6 @@ SatValue CadicalSolver::solve(const std::vector<SatLiteral>& assumptions)
   d_okay = (res == SAT_VALUE_TRUE);
   ++d_statistics.d_numSatCalls;
   return res;
-#else
-  Unimplemented("CaDiCaL version used does not support incremental solving");
-#endif
 }
 
 void CadicalSolver::interrupt() { d_solver->terminate(); }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 9a1e5d6dc376bd09c5675af52862f7e8b2d8a3a9..df553b8bdd373bf863acf4f82d2e321d45ebdcab 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -250,6 +250,7 @@ set(regress_0_tests
   regress0/bv/core/slice-20.smt
   regress0/bv/divtest_2_5.smt2
   regress0/bv/divtest_2_6.smt2
+  regress0/bv/eager-inc-cadical.smt2
   regress0/bv/eager-inc-cryptominisat.smt2
   regress0/bv/eager-force-logic.smt2
   regress0/bv/fuzz01.smt

diff --git a/test/regress/regress0/bv/eager-inc-cadical.smt2 b/test/regress/regress0/bv/eager-inc-cadical.smt2
new file mode 100644 (file)
index 0000000..01840df
--- /dev/null
+++ b/test/regress/regress0/bv/eager-inc-cadical.smt2
@@ -0,0 +1,27 @@
+; REQUIRES: cadical
+; COMMAND-LINE: --incremental --bv-sat-solver=cadical --bitblast=eager
+(set-logic QF_BV)
+(set-option :incremental true)
+(declare-fun a () (_ BitVec 16))
+(declare-fun b () (_ BitVec 16))
+(declare-fun c () (_ BitVec 16))
+
+(assert (bvult a (bvadd b c)))
+(set-info :status sat)
+(check-sat)
+
+(push 1)
+(assert (bvult c b))
+(set-info :status sat)
+(check-sat)
+
+
+(push 1)
+(assert (bvugt c b))
+(set-info :status unsat)
+(check-sat)
+(pop 2)
+
+(set-info :status sat)
+(check-sat)
+(exit)