feat: Propagate trait

resolves #58

cadical/Cargo.toml

@@ -14,6 +14,7 @@ build = "build.rs"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [features]
+default = ["quiet"]
 debug = []
 quiet = []
 logging = []

cadical/build.rs

@@ -138,6 +138,18 @@ impl Version {
     fn has_flip(self) -> bool {
         self >= Version::V154
     }
+
+    fn has_ilb(self) -> bool {
+        self >= Version::V190
+    }
+
+    fn has_reimply(self) -> bool {
+        self >= Version::V190 && self < Version::V194
+    }
+
+    fn has_ipasir_up(self) -> bool {
+        self >= Version::V160
+    }
 }
 
 fn main() {
@@ -216,76 +228,81 @@ fn build(repo: &str, branch: &str, version: Version) {
         tmp
     };
     let cadical_dir = { Path::new(&cadical_dir_str) };
-    if update_repo(
+    update_repo(
         cadical_dir,
         repo,
         branch,
         version.reference(),
         Path::new("patches").join(version.patch()),
-    ) || !Path::new(&out_dir).join("libcadical.a").exists()
-    {
-        // Repo changed, rebuild
-        // We specify the build manually here instead of calling make for better portability
-        let src_files = glob(&format!("{cadical_dir_str}/src/*.cpp"))
-            .unwrap()
-            .filter_map(|res| {
-                if let Ok(p) = res {
-                    if let Some(name) = p.file_name() {
-                        if name == "cadical.cpp" || name == "mobical.cpp" || name == "ipasir.cpp" {
-                            return None; // Filter out application files and IPASIR interface
-                        }
-                    };
-                    Some(p)
-                } else {
-                    None
-                }
-            });
-        // Setup build configuration
-        let mut cadical_build = cc::Build::new();
-        cadical_build.cpp(true).std("c++11");
-        if cfg!(feature = "debug") && env::var("PROFILE").unwrap() == "debug" {
-            cadical_build
-                .opt_level(0)
-                .define("DEBUG", None)
-                .warnings(true)
-                .debug(true)
-                .define("NCONTRACTS", None) // --no-contracts
-                .define("NTRACING", None); // --no-tracing
-        } else {
-            cadical_build
-                .opt_level(3)
-                .define("NDEBUG", None)
-                .warnings(false);
-        }
-        #[cfg(feature = "quiet")]
-        cadical_build.define("QUIET", None); // --quiet
-        #[cfg(feature = "logging")]
-        cadical_build.define("LOGGING", None); // --log
-        if version.has_flip() {
-            cadical_build.define("FLIP", None);
-        }
+    );
+    // We specify the build manually here instead of calling make for better portability
+    let src_files = glob(&format!("{cadical_dir_str}/src/*.cpp"))
+        .unwrap()
+        .filter_map(|res| {
+            if let Ok(p) = res {
+                if let Some(name) = p.file_name() {
+                    if name == "cadical.cpp" || name == "mobical.cpp" || name == "ipasir.cpp" {
+                        return None; // Filter out application files and IPASIR interface
+                    }
+                };
+                Some(p)
+            } else {
+                None
+            }
+        });
+    // Setup build configuration
+    let mut cadical_build = cc::Build::new();
+    cadical_build.cpp(true).std("c++11");
+    if cfg!(feature = "debug") && env::var("PROFILE").unwrap() == "debug" {
+        cadical_build
+            .opt_level(0)
+            .define("DEBUG", None)
+            .warnings(true)
+            .debug(true)
+            .define("NCONTRACTS", None) // --no-contracts
+            .define("NTRACING", None); // --no-tracing
+    } else {
+        cadical_build
+            .opt_level(3)
+            .define("NDEBUG", None)
+            .warnings(false);
+    }
+    #[cfg(feature = "quiet")]
+    cadical_build.define("QUIET", None); // --quiet
+    #[cfg(feature = "logging")]
+    cadical_build.define("LOGGING", None); // --log
+    if version.has_flip() {
+        cadical_build.define("FLIP", None);
+    }
+    if version.has_ilb() {
+        cadical_build.define("ILB", None);
+    }
+    if version.has_reimply() {
+        cadical_build.define("REIMPLY", None);
+    }
+    if version.has_ipasir_up() {
+        cadical_build.define("IPASIRUP", None);
+    }
 
-        // Generate build header
-        let mut build_header = File::create(cadical_dir.join("src").join("build.hpp"))
-            .expect("Could not create kissat CaDiCaL header");
-        let mut cadical_version =
-            fs::read_to_string(cadical_dir.join("VERSION")).expect("Cannot read CaDiCaL version");
-        cadical_version.retain(|c| c != '\n');
-        let (compiler_desc, compiler_flags) =
-            get_compiler_description(&cadical_build.get_compiler());
-        write!(
+    // Generate build header
+    let mut build_header = File::create(cadical_dir.join("src").join("build.hpp"))
+        .expect("Could not create kissat CaDiCaL header");
+    let mut cadical_version =
+        fs::read_to_string(cadical_dir.join("VERSION")).expect("Cannot read CaDiCaL version");
+    cadical_version.retain(|c| c != '\n');
+    let (compiler_desc, compiler_flags) = get_compiler_description(&cadical_build.get_compiler());
+    write!(
                 build_header,
                 "#define VERSION \"{}\"\n#define IDENTIFIER \"{}\"\n#define COMPILER \"{}\"\n#define FLAGS \"{}\"\n#define DATE \"{}\"",
                 cadical_version, version.reference(), compiler_desc, compiler_flags, chrono::Utc::now()
             ).expect("Failed to write CaDiCaL build.hpp");
-        // Build CaDiCaL
-        cadical_build
-            .include(cadical_dir.join("src"))
-            .include("cppsrc")
-            .warnings(false)
-            .files(src_files)
-            .compile("cadical");
-    };
+    // Build CaDiCaL
+    cadical_build
+        .include(cadical_dir.join("src"))
+        .include("cppsrc")
+        .warnings(false)
+        .files(src_files)
+        .compile("cadical");
 }
 
 /// Returns true if there were changes, false if not

cadical/cppsrc/cadical_extension.hpp

@@ -4,3 +4,6 @@
 int64_t propagations() const;
 int64_t decisions() const;
 int64_t conflicts() const;
+
+bool prop_check(const int *assumps, size_t assumps_len, bool psaving,
+                void (*prop_cb)(void *, int), void *cb_data);

cadical/cppsrc/ccadical_extension.cpp

@@ -38,7 +38,7 @@ int ccadical_solve_mem(CCaDiCaL *wrapper) {
   }
 }
 
-bool ccadical_configure(CCaDiCaL *ptr, const char *name) {
+int ccadical_configure(CCaDiCaL *ptr, const char *name) {
   return ((Wrapper *)ptr)->solver->configure(name);
 }
 
@@ -52,11 +52,11 @@ void ccadical_unphase(CCaDiCaL *ptr, int lit) {
 
 int ccadical_vars(CCaDiCaL *ptr) { return ((Wrapper *)ptr)->solver->vars(); }
 
-bool ccadical_set_option_ret(CCaDiCaL *wrapper, const char *name, int val) {
+int ccadical_set_option_ret(CCaDiCaL *wrapper, const char *name, int val) {
   return ((Wrapper *)wrapper)->solver->set(name, val);
 }
 
-bool ccadical_limit_ret(CCaDiCaL *wrapper, const char *name, int val) {
+int ccadical_limit_ret(CCaDiCaL *wrapper, const char *name, int val) {
   return ((Wrapper *)wrapper)->solver->limit(name, val);
 }
 
@@ -90,12 +90,27 @@ int64_t ccadical_conflicts(CCaDiCaL *wrapper) {
 }
 
 #ifdef FLIP
-bool ccadical_flip(CCaDiCaL *wrapper, int lit) {
+int ccadical_flip(CCaDiCaL *wrapper, int lit) {
   return ((Wrapper *)wrapper)->solver->flip(lit);
 }
 
-bool ccadical_flippable(CCaDiCaL *wrapper, int lit) {
+int ccadical_flippable(CCaDiCaL *wrapper, int lit) {
   return ((Wrapper *)wrapper)->solver->flippable(lit);
 }
 #endif
+
+int ccadical_propcheck(CCaDiCaL *wrapper, const int *assumps,
+                       size_t assumps_len, int psaving,
+                       void (*prop_cb)(void *, int), void *cb_data) {
+  try {
+    if (((Wrapper *)wrapper)
+            ->solver->prop_check(assumps, assumps_len, psaving, prop_cb,
+                                 cb_data)) {
+      return 10;
+    }
+    return 20;
+  } catch (std::bad_alloc &) {
+    return OUT_OF_MEM;
+  }
+}
 }

cadical/cppsrc/ccadical_extension.h

@@ -1,27 +1,30 @@
 // CaDiCaL C API Extension (Christoph Jabs)
 // To be included at the bottom of `ccadical.h`
 
-#include <stdbool.h>
+#include <stddef.h>
 
 const int OUT_OF_MEM = 50;
 
 int ccadical_add_mem(CCaDiCaL *wrapper, int lit);
 int ccadical_assume_mem(CCaDiCaL *wrapper, int lit);
 int ccadical_constrain_mem(CCaDiCaL *wrapper, int lit);
 int ccadical_solve_mem(CCaDiCaL *wrapper);
-bool ccadical_configure(CCaDiCaL *ptr, const char *name);
+int ccadical_configure(CCaDiCaL *ptr, const char *name);
 void ccadical_phase(CCaDiCaL *ptr, int lit);
 void ccadical_unphase(CCaDiCaL *ptr, int lit);
 int ccadical_vars(CCaDiCaL *ptr);
-bool ccadical_set_option_ret(CCaDiCaL *wrapper, const char *name, int val);
-bool ccadical_limit_ret(CCaDiCaL *wrapper, const char *name, int val);
+int ccadical_set_option_ret(CCaDiCaL *wrapper, const char *name, int val);
+int ccadical_limit_ret(CCaDiCaL *wrapper, const char *name, int val);
 int64_t ccadical_redundant(CCaDiCaL *wrapper);
 int ccadical_simplify_rounds(CCaDiCaL *wrapper, int rounds);
 int ccadical_reserve(CCaDiCaL *wrapper, int min_max_var);
 int64_t ccadical_propagations(CCaDiCaL *wrapper);
 int64_t ccadical_decisions(CCaDiCaL *wrapper);
 int64_t ccadical_conflicts(CCaDiCaL *wrapper);
 #ifdef FLIP
-bool ccadical_flip(CCaDiCaL *wrapper, int lit);
-bool ccadical_flippable(CCaDiCaL *wrapper, int lit);
+int ccadical_flip(CCaDiCaL *wrapper, int lit);
+int ccadical_flippable(CCaDiCaL *wrapper, int lit);
 #endif
+int ccadical_propcheck(CCaDiCaL *wrapper, const int *assumps,
+                       size_t assumps_len, int psaving,
+                       void (*prop_cb)(void *, int), void *cb_data);

cadical/cppsrc/solver_extension.cpp

@@ -24,4 +24,128 @@ int64_t Solver::conflicts() const {
   return res;
 }
 
+// Propagate and check
+// This is based on the implementation in PySat
+// https://github.com/pysathq/pysat/blob/master/solvers/patches/cadical195.patch
+bool Solver::prop_check(const int *assumps, size_t assumps_len, bool psaving,
+                        void (*prop_cb)(void *, int), void *cb_data) {
+  if (internal->unsat || internal->unsat_constraint) {
+    return false;
+  }
+
+  // saving default options
+#ifdef ILB
+  int old_ilb = internal->opts.ilb;
+#endif
+#ifdef REIMPLY
+  int old_reimply = internal->opts.reimply;
+#endif
+  int old_psave = internal->opts.rephase;
+  int old_lucky = internal->opts.lucky;
+  int old_resall = internal->opts.restoreall;
+
+  // resetting the above options
+#ifdef ILB
+  internal->opts.ilb = 0;
+#endif
+#ifdef REIMPLY
+  internal->opts.reimply = 0;
+#endif
+  internal->opts.lucky = psaving;
+  internal->opts.rephase = psaving;
+  internal->opts.restoreall = 2;
+
+  int tmp = internal->already_solved();
+  if (!tmp)
+    tmp = internal->restore_clauses();
+  if (tmp) {
+    // restoring default option values
+#ifdef ILB
+    internal->opts.ilb = old_ilb;
+#endif
+#ifdef REIMPLY
+    internal->opts.reimply = old_reimply;
+#endif
+    internal->opts.lucky = old_lucky;
+    internal->opts.rephase = old_psave;
+    internal->opts.restoreall = old_resall;
+    internal->reset_solving();
+    internal->report_solving(tmp);
+    return false;
+  }
+  internal->opts.restoreall = old_resall;
+
+  bool unsat = false;
+  int level = internal->level;
+  bool noconfl = true;
+  Clause *old_conflict = internal->conflict;
+
+  // propagate each assumption at a new decision level
+  for (size_t i = 0; !unsat && noconfl && i < assumps_len; ++i) {
+    int p = assumps[i];
+
+    // deciding
+    const signed char tmp = internal->val(p);
+    if (tmp < 0) // if assumption is already set to false
+      unsat = true;
+    else {
+#ifdef IPASIRUP
+      if (tmp > 0) {
+        // add pseudo decision level
+#ifdef ILB
+        internal->new_trail_level(0);
+#else
+        internal->level++;
+        internal->control.push_back(Level(0, internal->trail.size()));
+#endif
+        internal->notify_decision();
+      } else
+        internal->search_assume_decision(p);
+
+      noconfl = internal->propagate();
+      if (noconfl)
+        noconfl = internal->external_propagate();
+#else
+      if (tmp == 0) {
+        internal->search_assume_decision(p);
+        noconfl = internal->propagate();
+      }
+#endif
+    }
+  }
+
+  // copy results
+  if (internal->level > level) {
+    for (size_t i = internal->control[level + 1].trail;
+         i < internal->trail.size(); ++i) {
+      prop_cb(cb_data, internal->trail[i]);
+    }
+    // if there is a conflict, push the conflicting literal as well
+    if (!noconfl) {
+      literal_iterator conflict_ptr = internal->conflict->begin();
+      int conflict_val = *conflict_ptr;
+      prop_cb(cb_data, conflict_val);
+    }
+    // backtrack
+    internal->backtrack(level);
+  }
+
+#ifdef ILB
+  internal->opts.ilb = old_ilb;
+#endif
+#ifdef REIMPLY
+  internal->opts.reimply = old_reimply;
+#endif
+
+  // restore phase saving
+  internal->opts.rephase = old_psave;
+  internal->opts.lucky = old_lucky;
+  // reset conflict
+  internal->conflict = old_conflict;
+  internal->reset_solving();
+  internal->report_solving(tmp);
+
+  return !unsat && noconfl;
+}
+
 } // namespace CaDiCaL