feat(cadical): version 2.1.3 with native propagate

cadical/Cargo.toml

@@ -51,6 +51,8 @@ v1-9-5 = []
 v2-0-0 = []
 v2-1-0 = []
 v2-1-1 = []
+v2-1-2 = []
+v2-1-3 = []
 
 [dependencies]
 anyhow.workspace = true

cadical/README.md

@@ -21,7 +21,7 @@ Armin Biere's SAT solver [CaDiCaL](https://github.com/arminbiere/cadical) to be
 ## CaDiCaL Versions
 
 CaDiCaL versions can be selected via cargo crate features.
-All CaDiCaL versions up to [Version 2.1.1](https://github.com/arminbiere/cadical/releases/tag/rel-2.1.1) are available.
+All CaDiCaL versions up to [Version 2.1.3](https://github.com/arminbiere/cadical/releases/tag/rel-2.1.3) are available.
 For the full list of versions and the changelog see [the CaDiCaL releases](https://github.com/arminbiere/cadical/releases).
 
 Without any features selected, the newest version will be used.

cadical/build-all.sh

@@ -125,6 +125,16 @@ if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo build --features=v2-1-1 &> v211-build.log
 echo "v2.1.1 build returned: $?"
 
+echo "Building v2.1.2"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
+cargo build --features=v2-1-2 &> v212-build.log
+echo "v2.1.2 build returned: $?"
+
+echo "Building v2.1.3"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
+cargo build --features=v2-1-3 &> v213-build.log
+echo "v2.1.3 build returned: $?"
+
 echo "Building quiet"
 if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo build --features=quiet &> quiet-build.log

cadical/build.rs

@@ -37,13 +37,20 @@ enum Version {
     V195,
     V200,
     V210,
-    #[default]
     V211,
+    V212,
+    #[default]
+    V213,
+    // Don't forget to update the crate documentation when adding a newer version
 }
 
 impl Version {
     fn determine() -> Self {
-        if cfg!(feature = "v2-1-1") {
+        if cfg!(feature = "v2-1-3") {
+            Version::V213
+        } else if cfg!(feature = "v2-1-2") {
+            Version::V212
+        } else if cfg!(feature = "v2-1-1") {
             Version::V211
         } else if cfg!(feature = "v2-1-0") {
             Version::V210
@@ -123,6 +130,8 @@ impl Version {
             Version::V200 => "refs/tags/rel-2.0.0",
             Version::V210 => "refs/tags/rel-2.1.0",
             Version::V211 => "refs/tags/rel-2.1.1",
+            Version::V212 => "refs/tags/rel-2.1.2",
+            Version::V213 => "refs/tags/rel-2.1.3",
         }
     }
 
@@ -141,7 +150,8 @@ impl Version {
             V192 | V193 | V194 | V195 => "v192.patch",
             V200 => "v200.patch",
             V210 => "v210.patch",
-            V211 => "v211.patch",
+            V211 | V212 => "v211.patch",
+            V213 => "v213.patch",
         }
     }
 
@@ -160,6 +170,10 @@ impl Version {
     fn has_ipasir_up(self) -> bool {
         self >= Version::V160
     }
+
+    fn has_propagate(self) -> bool {
+        self >= Version::V213
+    }
 }
 
 fn main() {
@@ -205,6 +219,17 @@ fn main() {
     let cadical_dir = get_cadical_dir(None);
 
     generate_bindings(&format!("{cadical_dir}/src/ccadical.h"), version, &out_dir);
+
+    // Set custom configs for features only present in some version
+    println!("cargo:rustc-check-cfg=cfg(cadical_feature, values(\"flip\", \"propagate\", \"pysat-propcheck\"))");
+    if version.has_flip() {
+        println!("cargo:rustc-cfg=cadical_feature=\"flip\"");
+    }
+    if version.has_propagate() {
+        println!("cargo:rustc-cfg=cadical_feature=\"propagate\"");
+    } else {
+        println!("cargo:rustc-cfg=cadical_feature=\"pysat-propcheck\"");
+    }
 }
 
 /// Generates Rust FFI bindings
@@ -231,6 +256,11 @@ fn generate_bindings(header_path: &str, version: Version, out_dir: &str) {
     } else {
         bindings
     };
+    let bindings = if version.has_propagate() {
+        bindings.clang_arg("-DPROPAGATE")
+    } else {
+        bindings.clang_arg("-DPYSAT_PROPCHECK")
+    };
     let bindings = bindings
         .generate()
         .expect("Unable to generate ffi bindings");
@@ -311,6 +341,11 @@ fn build(repo: &str, branch: &str, version: Version) {
     if version.has_ipasir_up() {
         cadical_build.define("IPASIRUP", None);
     }
+    if version.has_propagate() {
+        cadical_build.define("PROPAGATE", None);
+    } else {
+        cadical_build.define("PYSAT_PROPCHECK", None);
+    }
 
     let out_dir = std::env::var("OUT_DIR").unwrap();
     let out_dir = Path::new(&out_dir);

cadical/cppsrc/cadical_extension.hpp

@@ -5,5 +5,7 @@ int64_t propagations() const;
 int64_t decisions() const;
 int64_t conflicts() const;
 
+#ifdef PYSAT_PROPCHECK
 bool prop_check(const int *assumps, size_t assumps_len, bool psaving,
                 void (*prop_cb)(void *, int), void *cb_data);
+#endif

cadical/cppsrc/ccadical_extension.cpp

@@ -99,6 +99,7 @@ int ccadical_flippable(CCaDiCaL *wrapper, int lit) {
 }
 #endif
 
+#ifdef PYSAT_PROPCHECK
 int ccadical_propcheck(CCaDiCaL *wrapper, const int *assumps,
                        size_t assumps_len, int psaving,
                        void (*prop_cb)(void *, int), void *cb_data) {
@@ -113,4 +114,25 @@ int ccadical_propcheck(CCaDiCaL *wrapper, const int *assumps,
     return OUT_OF_MEM;
   }
 }
+#endif
+
+#ifdef PROPAGATE
+int ccadical_propagate(CCaDiCaL *wrapper) {
+  try {
+    return ((Wrapper *)wrapper)->solver->propagate();
+  } catch (std::bad_alloc &) {
+    return OUT_OF_MEM;
+  }
+}
+
+void ccadical_get_entrailed_literals(CCaDiCaL *wrapper,
+                                     void (*entrailed_cb)(void *, int),
+                                     void *cb_data) {
+  std::vector<int> entrailed{};
+  ((Wrapper *)wrapper)->solver->get_entrailed_literals(entrailed);
+  for (int lit : entrailed) {
+    entrailed_cb(cb_data, lit);
+  }
+}
+#endif
 }

cadical/cppsrc/ccadical_extension.h

@@ -25,6 +25,14 @@ int64_t ccadical_conflicts(CCaDiCaL *wrapper);
 int ccadical_flip(CCaDiCaL *wrapper, int lit);
 int ccadical_flippable(CCaDiCaL *wrapper, int lit);
 #endif
+#ifdef PYSAT_PROPCHECK
 int ccadical_propcheck(CCaDiCaL *wrapper, const int *assumps,
                        size_t assumps_len, int psaving,
                        void (*prop_cb)(void *, int), void *cb_data);
+#endif
+#ifdef PROPAGATE
+int ccadical_propagate(CCaDiCaL *wrapper);
+void ccadical_get_entrailed_literals(CCaDiCaL *wrapper,
+                                     void (*entrailed_cb)(void *, int),
+                                     void *cb_data);
+#endif

cadical/cppsrc/solver_extension.cpp

@@ -24,6 +24,7 @@ int64_t Solver::conflicts() const {
   return res;
 }
 
+#ifdef PYSAT_PROPCHECK
 // Propagate and check
 // This is based on the implementation in PySat
 // https://github.com/pysathq/pysat/blob/master/solvers/patches/cadical195.patch
@@ -147,5 +148,6 @@ bool Solver::prop_check(const int *assumps, size_t assumps_len, bool psaving,
 
   return !unsat && noconfl;
 }
+#endif
 
 } // namespace CaDiCaL

cadical/patches/v213.patch

@@ -0,0 +1,61 @@
+From d32cc1166635a6fd289c3fd9765823b2b68cdfe3 Mon Sep 17 00:00:00 2001
+From: Christoph Jabs <[email protected]>
+Date: Tue, 11 Feb 2025 11:15:59 +0200
+Subject: [PATCH] extend C api
+
+---
+ src/cadical.hpp  | 2 ++
+ src/ccadical.cpp | 2 ++
+ src/ccadical.h   | 2 ++
+ src/solver.cpp   | 2 ++
+ 4 files changed, 8 insertions(+)
+
+diff --git a/src/cadical.hpp b/src/cadical.hpp
+index 49adee9e..5cad21aa 100644
+--- a/src/cadical.hpp
++++ b/src/cadical.hpp
+@@ -940,6 +940,8 @@ public:
+   //
+   static void build (FILE *file, const char *prefix = "c ");
+
++#include "cadical_extension.hpp"
++
+ private:
+   //==== start of state ====================================================
+
+diff --git a/src/ccadical.cpp b/src/ccadical.cpp
+index 88ab164a..8186054a 100644
+--- a/src/ccadical.cpp
++++ b/src/ccadical.cpp
+@@ -186,3 +186,5 @@ void ccadical_conclude (CCaDiCaL *ptr) {
+   ((Wrapper *) ptr)->solver->conclude ();
+ }
+ }
++
++#include "ccadical_extension.cpp"
+diff --git a/src/ccadical.h b/src/ccadical.h
+index 6d1b3ff0..a8f1b48a 100644
+--- a/src/ccadical.h
++++ b/src/ccadical.h
+@@ -60,6 +60,8 @@ int ccadical_simplify (CCaDiCaL *);
+ #define ccadical_sat ccadical_solve
+ #define ccadical_deref ccadical_val
+
++#include "ccadical_extension.h"
++
+ /*------------------------------------------------------------------------*/
+ #ifdef __cplusplus
+ }
+diff --git a/src/solver.cpp b/src/solver.cpp
+index 9c002f3a..52d3e0eb 100644
+--- a/src/solver.cpp
++++ b/src/solver.cpp
+@@ -1740,3 +1740,5 @@ void Solver::error (const char *fmt, ...) {
+ }
+
+ } // namespace CaDiCaL
++
++#include "solver_extension.cpp"
+-- 
+2.47.1
+

cadical/src/lib.rs

@@ -14,7 +14,7 @@
 //! ## CaDiCaL Versions
 //!
 //! CaDiCaL versions can be selected via cargo crate features.
-//! All CaDiCaL versions up to [Version 2.1.1](https://github.com/arminbiere/cadical/releases/tag/rel-2.1.1) are available.
+//! All CaDiCaL versions up to [Version 2.1.3](https://github.com/arminbiere/cadical/releases/tag/rel-2.1.3) are available.
 //! For the full list of versions and the changelog see [the CaDiCaL releases](https://github.com/arminbiere/cadical/releases).
 //!
 //! Without any features selected, the newest version will be used.
@@ -774,13 +774,7 @@ impl FreezeVar for CaDiCaL<'_, '_> {
     }
 }
 
-// >= v1.5.4
-#[cfg(all(
-    not(feature = "v1-5-3"),
-    not(feature = "v1-5-2"),
-    not(feature = "v1-5-1"),
-    not(feature = "v1-5-0")
-))]
+#[cfg(cadical_feature = "flip")]
 impl rustsat::solvers::FlipLit for CaDiCaL<'_, '_> {
     fn flip_lit(&mut self, lit: Lit) -> anyhow::Result<bool> {
         if self.state != InternalSolverState::Sat {
@@ -845,6 +839,66 @@ impl GetInternalStats for CaDiCaL<'_, '_> {
     }
 }
 
+#[cfg(cadical_feature = "propagate")]
+impl Propagate for CaDiCaL<'_, '_> {
+    fn propagate(
+        &mut self,
+        assumps: &[Lit],
+        _phase_saving: bool,
+    ) -> anyhow::Result<PropagateResult> {
+        let start = ProcessTime::now();
+        self.state = InternalSolverState::Input;
+        // Propagate with cadical backend
+        for a in assumps {
+            handle_oom!(unsafe { ffi::ccadical_assume_mem(self.handle, a.to_ipasir()) });
+        }
+        let res = handle_oom!(unsafe { ffi::ccadical_propagate(self.handle) });
+        let mut props = Vec::new();
+        dbg!(res);
+        match res {
+            0 => {
+                let prop_ptr: *mut Vec<Lit> = &mut props;
+                unsafe {
+                    ffi::ccadical_get_entrailed_literals(
+                        self.handle,
+                        Some(ffi::rustsat_cadical_collect_lits),
+                        prop_ptr.cast::<std::os::raw::c_void>(),
+                    );
+                }
+            }
+            10 => {
+                self.state = InternalSolverState::Sat;
+                if let Some(max_var) = self.max_var() {
+                    for var in 0..=max_var.idx32() {
+                        let var = Var::new(var);
+                        props.push(match self.var_val(var)? {
+                            TernaryVal::True => var.pos_lit(),
+                            TernaryVal::False => var.neg_lit(),
+                            TernaryVal::DontCare => {
+                                unreachable!("returned SAT should have value for all variables")
+                            }
+                        });
+                    }
+                }
+            }
+            20 => {}
+            value => {
+                return Err(InvalidApiReturn {
+                    api_call: "ccadical_propagate",
+                    value,
+                }
+                .into())
+            }
+        }
+        self.stats.cpu_solve_time += start.elapsed();
+        Ok(PropagateResult {
+            propagated: props,
+            conflict: res == 20,
+        })
+    }
+}
+
+#[cfg(cadical_feature = "pysat-propcheck")]
 impl Propagate for CaDiCaL<'_, '_> {
     fn propagate(
         &mut self,

cadical/test-all.sh

@@ -125,6 +125,16 @@ if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=v2-1-1 &> v211-test.log
 echo "v2.1.1 test returned: $?"
 
+echo "Testing v2.1.2"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
+cargo test --features=v2-1-2 &> v212-test.log
+echo "v2.1.2 test returned: $?"
+
+echo "Testing v2.1.3"
+if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
+cargo test --features=v2-1-3 &> v213-test.log
+echo "v2.1.3 test returned: $?"
+
 echo "Testing quiet"
 if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi
 cargo test --features=quiet &> quiet-test.log

solvertests/src/unit.rs

@@ -231,6 +231,11 @@ pub fn propagate(slv: Type) -> TokenStream {
             solver.add_binary(!lit![1], lit![2]).unwrap();
             solver.add_binary(!lit![2], lit![3]).unwrap();
 
+            let res = solver.propagate(&[], false).unwrap();
+
+            assert!(!res.conflict);
+            assert!(res.propagated.is_empty());
+
             let res = solver.propagate(&[lit![0]], false).unwrap();
 
             assert!(!res.conflict);