Signal restarts in notify_backtrack IPASIR-UP callbacks

crates/pindakaas-build-macros/src/ipasir_up.h

@@ -29,7 +29,7 @@ void ipasir_connect_external_propagator(
   // to an assignment.
   void (*prop_notify_assignment) (void* prop, int lit, bool is_fixed),
   void (*prop_notify_new_decision_level) (void* prop),
-  void (*prop_notify_backtrack) (void* prop, size_t new_level),
+  void (*prop_notify_backtrack) (void* prop, size_t new_level, bool restart),
   // Check by the external propagator the found complete solution (after
   // solution reconstruction). If it returns false, the propagator must
   // provide an external clause during the next callback.

crates/pindakaas-build-macros/src/lib.rs

@@ -80,7 +80,7 @@ macro_rules! ipasir_up_definitions {
 					propagator_data: *mut std::ffi::c_void,
 					prop_notify_assignment: unsafe extern "C" fn(*mut std::ffi::c_void, i32, bool),
 					prop_notify_new_decision_level: unsafe extern "C" fn(*mut std::ffi::c_void),
-					prop_notify_backtrack: unsafe extern "C" fn(*mut std::ffi::c_void, usize),
+					prop_notify_backtrack: unsafe extern "C" fn(*mut std::ffi::c_void, usize, bool),
 					prop_cb_check_found_model: unsafe extern "C" fn(*mut std::ffi::c_void, *const i32, usize) -> bool,
 					prop_cb_has_external_clause: unsafe extern "C" fn(*mut std::ffi::c_void) -> bool,
 					prop_cb_add_external_clause_lit: unsafe extern "C" fn(*mut std::ffi::c_void) -> i32,
@@ -101,7 +101,7 @@ macro_rules! ipasir_up_definitions {
 					propagator_data: *mut std::ffi::c_void,
 					prop_notify_assignment: unsafe extern "C" fn(*mut std::ffi::c_void, i32, bool),
 					prop_notify_new_decision_level: unsafe extern "C" fn(*mut std::ffi::c_void),
-					prop_notify_backtrack: unsafe extern "C" fn(*mut std::ffi::c_void, usize),
+					prop_notify_backtrack: unsafe extern "C" fn(*mut std::ffi::c_void, usize, bool),
 					prop_cb_check_found_model: unsafe extern "C" fn(*mut std::ffi::c_void, *const i32, usize) -> bool,
 					prop_cb_has_external_clause: unsafe extern "C" fn(*mut std::ffi::c_void) -> bool,
 					prop_cb_add_external_clause_lit: unsafe extern "C" fn(*mut std::ffi::c_void) -> i32,

crates/pindakaas-cadical/src/ccadical_override.cpp

@@ -10,12 +10,11 @@ void ccadical_connect_external_propagator(
     CCaDiCaL *slv, void *propagator_data,
     void (*prop_notify_assignment)(void *prop, int lit, bool is_fixed),
     void (*prop_notify_new_decision_level)(void *prop),
-    void (*prop_notify_backtrack)(void *prop, size_t new_level),
+    void (*prop_notify_backtrack)(void *prop, size_t new_level, bool restart),
     bool (*prop_cb_check_found_model)(void *prop, const int *model,
                                       size_t size),
     bool (*prop_cb_has_external_clause)(void *prop),
-    int (*prop_cb_add_external_clause_lit)(void *prop),
-    bool is_lazy,
+    int (*prop_cb_add_external_clause_lit)(void *prop), bool is_lazy,
     int (*prop_cb_decide)(void *prop), int (*prop_cb_propagate)(void *prop),
     int (*prop_cb_add_reason_clause_lit)(void *prop, int propagated_lit)) {
   ((Wrapper *)slv)

crates/pindakaas-cadical/src/ccadical_up.h

@@ -15,19 +15,18 @@ extern "C" {
 // C wrapper for CaDiCaL's C++ API following IPASIR-UP.
 
 void ccadical_connect_external_propagator(
-	CCaDiCaL *slv,
-	void *propagator_data,
-	void (*prop_notify_assignment) (void* prop, int lit, bool is_fixed),
-	void (*prop_notify_new_decision_level) (void* prop),
-	void (*prop_notify_backtrack) (void* prop, size_t new_level),
-	bool (*prop_cb_check_found_model) (void* prop, const int* model, size_t size),
-	bool (*prop_cb_has_external_clause) (void* prop),
-	int (*prop_cb_add_external_clause_lit) (void* prop),
-	bool is_lazy = false,
-	int (*prop_cb_decide) (void* prop) = prop_decide_default,
-	int (*prop_cb_propagate) (void* prop) = prop_propagate_default,
-	int (*prop_cb_add_reason_clause_lit) (void* prop, int propagated_lit) = prop_add_reason_clause_lit_default
-);
+    CCaDiCaL *slv, void *propagator_data,
+    void (*prop_notify_assignment)(void *prop, int lit, bool is_fixed),
+    void (*prop_notify_new_decision_level)(void *prop),
+    void (*prop_notify_backtrack)(void *prop, size_t new_level, bool restart),
+    bool (*prop_cb_check_found_model)(void *prop, const int *model,
+                                      size_t size),
+    bool (*prop_cb_has_external_clause)(void *prop),
+    int (*prop_cb_add_external_clause_lit)(void *prop), bool is_lazy = false,
+    int (*prop_cb_decide)(void *prop) = prop_decide_default,
+    int (*prop_cb_propagate)(void *prop) = prop_propagate_default,
+    int (*prop_cb_add_reason_clause_lit)(void *prop, int propagated_lit) =
+        prop_add_reason_clause_lit_default);
 void ccadical_disconnect_external_propagator(CCaDiCaL *);
 
 void ccadical_add_observed_var(CCaDiCaL *, int var);

crates/pindakaas/src/solver.rs

@@ -158,8 +158,9 @@ pub trait Propagator {
 		let _ = persistent;
 	}
 	fn notify_new_decision_level(&mut self) {}
-	fn notify_backtrack(&mut self, new_level: usize) {
+	fn notify_backtrack(&mut self, new_level: usize, restart: bool) {
 		let _ = new_level;
+		let _ = restart;
 	}
 
 	/// Method called to check the found complete solution (after solution

crates/pindakaas/src/solver/libloading.rs

@@ -504,13 +504,14 @@ pub(crate) unsafe extern "C" fn ipasir_notify_new_decision_level_cb<P: Propagato
 pub(crate) unsafe extern "C" fn ipasir_notify_backtrack_cb<P: Propagator, A>(
 	state: *mut c_void,
 	level: usize,
+	restart: bool,
 ) {
 	let prop = &mut *(state as *mut IpasirPropStore<P, A>);
 	prop.pqueue.clear();
 	prop.explaining = None;
 	prop.rqueue.clear();
 	prop.cqueue = None;
-	prop.prop.notify_backtrack(level);
+	prop.prop.notify_backtrack(level, restart);
 }
 #[cfg(feature = "ipasir-up")]
 pub(crate) unsafe extern "C" fn ipasir_check_model_cb<P: Propagator, A: SolvingActions>(