From 8e4b76db52811913583717e6a0ec70a244aea231 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Tue, 3 Sep 2024 12:01:22 +1000 Subject: [PATCH] Signal restarts in notify_backtrack IPASIR-UP callbacks --- crates/pindakaas-build-macros/src/ipasir_up.h | 2 +- crates/pindakaas-build-macros/src/lib.rs | 4 +-- .../src/ccadical_override.cpp | 5 ++-- crates/pindakaas-cadical/src/ccadical_up.h | 25 +++++++++---------- crates/pindakaas-cadical/vendor/cadical | 2 +- crates/pindakaas/src/solver.rs | 3 ++- crates/pindakaas/src/solver/libloading.rs | 3 ++- 7 files changed, 22 insertions(+), 22 deletions(-) diff --git a/crates/pindakaas-build-macros/src/ipasir_up.h b/crates/pindakaas-build-macros/src/ipasir_up.h index 904c86f850..d450a890a9 100644 --- a/crates/pindakaas-build-macros/src/ipasir_up.h +++ b/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. diff --git a/crates/pindakaas-build-macros/src/lib.rs b/crates/pindakaas-build-macros/src/lib.rs index 39b8def46d..ad937f1a9b 100644 --- a/crates/pindakaas-build-macros/src/lib.rs +++ b/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, diff --git a/crates/pindakaas-cadical/src/ccadical_override.cpp b/crates/pindakaas-cadical/src/ccadical_override.cpp index c036f9cac7..851c56389a 100644 --- a/crates/pindakaas-cadical/src/ccadical_override.cpp +++ b/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) diff --git a/crates/pindakaas-cadical/src/ccadical_up.h b/crates/pindakaas-cadical/src/ccadical_up.h index 0dc153c4b5..e6ad8ec85b 100644 --- a/crates/pindakaas-cadical/src/ccadical_up.h +++ b/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); diff --git a/crates/pindakaas-cadical/vendor/cadical b/crates/pindakaas-cadical/vendor/cadical index 099b896410..d45b475de7 160000 --- a/crates/pindakaas-cadical/vendor/cadical +++ b/crates/pindakaas-cadical/vendor/cadical @@ -1 +1 @@ -Subproject commit 099b8964103fbadbb8d0f3f50e74c28dc68e2b52 +Subproject commit d45b475de71009e50c9c596eb062db76fc66e3c1 diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs index 7747770ae7..bdd2f72f0a 100644 --- a/crates/pindakaas/src/solver.rs +++ b/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 diff --git a/crates/pindakaas/src/solver/libloading.rs b/crates/pindakaas/src/solver/libloading.rs index 54870ecb16..175665b5c9 100644 --- a/crates/pindakaas/src/solver/libloading.rs +++ b/crates/pindakaas/src/solver/libloading.rs @@ -504,13 +504,14 @@ pub(crate) unsafe extern "C" fn ipasir_notify_new_decision_level_cb( state: *mut c_void, level: usize, + restart: bool, ) { let prop = &mut *(state as *mut IpasirPropStore); 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(