From 190676adb1bd135823dc62e1bb82f8c085eaa276 Mon Sep 17 00:00:00 2001 From: "Jip J. Dekker" Date: Wed, 12 Jun 2024 22:19:32 +1000 Subject: [PATCH] Resolve one level of dispatch for IPASIR UP callbacks --- crates/pindakaas-derive/src/lib.rs | 75 +++++++++++------------ crates/pindakaas/src/linear/bdd.rs | 3 +- crates/pindakaas/src/solver.rs | 12 ++-- crates/pindakaas/src/solver/cadical.rs | 6 +- crates/pindakaas/src/solver/libloading.rs | 71 ++++++++++----------- 5 files changed, 79 insertions(+), 88 deletions(-) diff --git a/crates/pindakaas-derive/src/lib.rs b/crates/pindakaas-derive/src/lib.rs index f1744f681..711bcf15b 100644 --- a/crates/pindakaas-derive/src/lib.rs +++ b/crates/pindakaas-derive/src/lib.rs @@ -207,7 +207,9 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { #[cfg(feature = "ipasir-up")] pub(crate) struct #prop_ident { /// Rust Propagator Storage - prop: Box, + prop: *mut c_void, + drop_prop: fn(*mut c_void), + access_prop: fn(*mut c_void) -> *mut dyn std::any::Any, /// C Wrapper Object wrapper: *mut std::ffi::c_void, } @@ -216,38 +218,46 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { impl Drop for #prop_ident { fn drop(&mut self) { unsafe { #krate::ipasir_prop_release(self.wrapper) }; + (self.drop_prop)(self.prop); } } #[cfg(feature = "ipasir-up")] impl #prop_ident { - pub(crate) fn new(prop: Box, slv: *mut dyn crate::solver::SolvingActions) -> Self { + pub(crate) fn new(prop: P, slv: *mut dyn crate::solver::SolvingActions) -> Self { // Construct wrapping structures - let mut prop = Box::new(crate::solver::libloading::IpasirPropStore::new(prop, slv)); - let data = (&mut (*prop)) as *mut _; + let prop = crate::solver::libloading::IpasirPropStore::

::new(prop, slv); + let drop_prop = |x: *mut std::ffi::c_void| { + let prop = unsafe { Box::

::from_raw(x as *mut P) }; + drop(prop); + }; + let access_prop = |x: *mut std::ffi::c_void| { + x as *mut P as *mut dyn std::any::Any + }; + let data = Box::leak(Box::new(prop)) as *mut _ as *mut std::ffi::c_void; let wrapper = unsafe { #krate::ipasir_prop_init(data as *mut std::ffi::c_void) }; // Set function pointers for methods - unsafe { #krate::ipasir_prop_set_notify_assignment(wrapper, Some(crate::solver::libloading::ipasir_notify_assignment_cb)) }; - unsafe { #krate::ipasir_prop_set_notify_new_decision_level(wrapper, Some(crate::solver::libloading::ipasir_notify_new_decision_level_cb)) }; - unsafe { #krate::ipasir_prop_set_notify_backtrack(wrapper, Some(crate::solver::libloading::ipasir_notify_backtrack_cb)) }; - unsafe { #krate::ipasir_prop_set_check_model(wrapper, Some(crate::solver::libloading::ipasir_check_model_cb)) }; - unsafe { #krate::ipasir_prop_set_decide(wrapper, Some(crate::solver::libloading::ipasir_decide_cb)) }; - unsafe { #krate::ipasir_prop_set_propagate(wrapper, Some(crate::solver::libloading::ipasir_propagate_cb)) }; - unsafe { #krate::ipasir_prop_set_add_reason_clause_lit(wrapper, Some(crate::solver::libloading::ipasir_add_reason_clause_lit_cb)) }; - unsafe { #krate::ipasir_prop_set_has_external_clause(wrapper, Some(crate::solver::libloading::ipasir_has_external_clause_cb)) }; - unsafe { #krate::ipasir_prop_set_add_external_clause_lit(wrapper, Some(crate::solver::libloading::ipasir_add_external_clause_lit_cb)) }; + unsafe { #krate::ipasir_prop_set_notify_assignment(wrapper, Some(crate::solver::libloading::ipasir_notify_assignment_cb::

)) }; + unsafe { #krate::ipasir_prop_set_notify_new_decision_level(wrapper, Some(crate::solver::libloading::ipasir_notify_new_decision_level_cb::

)) }; + unsafe { #krate::ipasir_prop_set_notify_backtrack(wrapper, Some(crate::solver::libloading::ipasir_notify_backtrack_cb::

)) }; + unsafe { #krate::ipasir_prop_set_check_model(wrapper, Some(crate::solver::libloading::ipasir_check_model_cb::

)) }; + unsafe { #krate::ipasir_prop_set_decide(wrapper, Some(crate::solver::libloading::ipasir_decide_cb::

)) }; + unsafe { #krate::ipasir_prop_set_propagate(wrapper, Some(crate::solver::libloading::ipasir_propagate_cb::

)) }; + unsafe { #krate::ipasir_prop_set_add_reason_clause_lit(wrapper, Some(crate::solver::libloading::ipasir_add_reason_clause_lit_cb::

)) }; + unsafe { #krate::ipasir_prop_set_has_external_clause(wrapper, Some(crate::solver::libloading::ipasir_has_external_clause_cb::

)) }; + unsafe { #krate::ipasir_prop_set_add_external_clause_lit(wrapper, Some(crate::solver::libloading::ipasir_add_external_clause_lit_cb::

)) }; - Self { prop, wrapper, } + Self { prop: data, drop_prop, access_prop, wrapper, } } } #[cfg(feature = "ipasir-up")] impl crate::solver::PropagatingSolver for #ident { - fn set_external_propagator( + fn set_external_propagator( &mut self, - prop: Option>, - ) -> Option> { + prop: Option

, + ) { // Store old propagator (setting member to None) let old = #prop_member.take(); // Disconnect old propagator (if one was set) @@ -256,18 +266,9 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { } // If new propagator, set it now if let Some(p) = prop { - #prop_member = Some(Box::new(#prop_ident ::new(p, (self as *mut _)))); + #prop_member = Some(#prop_ident ::new(p, (self as *mut _))); unsafe { #krate::ipasir_connect_external_propagator( #ptr, #prop_member .as_ref().unwrap().wrapper ) }; } - // Return old propagator - if let Some(mut old) = old { - // Replace rust propagator with dummy to not interfere with Drop - let mut prop: Box = Box::new(crate::solver::libloading::NoProp{}); - std::mem::swap(&mut old.prop.prop, &mut prop); - Some(prop) - } else { - None - } } fn add_observed_var(&mut self, var: crate::Var){ @@ -284,14 +285,14 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { #[cfg(feature = "ipasir-up")] impl crate::solver::PropagatorAccess for #ident { fn propagator(&self) -> Option<&P> { - #prop_member.as_ref().map(|p| p.prop.prop.as_any().downcast_ref()).flatten() + #prop_member.as_ref().map(|p| unsafe { &*(p.access_prop)(p.prop) } .downcast_ref()).flatten() } } #[cfg(feature = "ipasir-up")] impl crate::solver::MutPropagatorAccess for #ident { fn propagator_mut(&mut self) -> Option<&mut P> { - #prop_member.as_mut().map(|p| p.prop.prop.as_mut_any().downcast_mut()).flatten() + #prop_member.as_ref().map(|p| unsafe { &mut *(p.access_prop)(p.prop) } .downcast_mut()).flatten() } } @@ -312,17 +313,17 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { ptr: *mut std::ffi::c_void, #[cfg(feature = "ipasir-up")] prop: Option<*mut std::ffi::c_void>, + #[cfg(feature = "ipasir-up")] + access_prop: Option *mut dyn std::any::Any>, } impl #ident { fn solver_solution_obj(&mut self) -> #sol_ident { #sol_ident { ptr: self.ptr, #[cfg(feature = "ipasir-up")] - prop: if let Some(p) = #prop_member .as_mut() { - Some((&mut (*p.prop)) as *mut _ as *mut std::ffi::c_void) - } else { - None - }, + prop: #prop_member .as_mut().map(|p| p.prop), + #[cfg(feature = "ipasir-up")] + access_prop: #prop_member .as_ref().map(|p| p.access_prop), } } } @@ -330,8 +331,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { impl crate::solver::PropagatorAccess for #sol_ident { fn propagator(&self) -> Option<&P> { if let Some(prop) = self.prop { - let prop = unsafe { &*(prop as *const crate::solver::libloading::IpasirPropStore) }; - prop.prop.as_any().downcast_ref() + unsafe { &*(self.access_prop.unwrap())(prop) }.downcast_ref() } else { None } @@ -341,8 +341,7 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream { impl crate::solver::MutPropagatorAccess for #sol_ident { fn propagator_mut(&mut self) -> Option<&mut P> { if let Some(prop) = self.prop { - let prop = unsafe { &mut *(prop as *mut crate::solver::libloading::IpasirPropStore) }; - prop.prop.as_mut_any().downcast_mut() + unsafe { &mut *(self.access_prop.unwrap())(prop) }.downcast_mut() } else { None } diff --git a/crates/pindakaas/src/linear/bdd.rs b/crates/pindakaas/src/linear/bdd.rs index c45dad820..c5c9a9d35 100755 --- a/crates/pindakaas/src/linear/bdd.rs +++ b/crates/pindakaas/src/linear/bdd.rs @@ -52,7 +52,8 @@ impl Encoder for BddEncoder { // TODO cannot avoid? #[allow(clippy::needless_collect)] - let ys = ys.into_iter() + let ys = ys + .into_iter() .map(|nodes| { let mut views = HashMap::new(); Rc::new(RefCell::new({ diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs index ce0570e1a..0e3f65aaa 100644 --- a/crates/pindakaas/src/solver.rs +++ b/crates/pindakaas/src/solver.rs @@ -101,18 +101,14 @@ where /// Set Propagator implementation which allows to learn, propagate and /// backtrack based on external constraints. /// - /// Only one Propagator can be connected. This Propagator is notified of all - /// changes to which it has subscribed, using the [`add_observed_var`] method. - /// - /// If a previous propagator was set, then it is returned. + /// Only one Propagator can be connected, any previous propagator will be + /// overriden. This Propagator is notified of all changes to which it has + /// subscribed, using the [`add_observed_var`] method. /// /// # Warning /// /// Calling this method automatically resets the observed variable set. - fn set_external_propagator( - &mut self, - prop: Option>, - ) -> Option>; + fn set_external_propagator(&mut self, prop: Option

); fn add_observed_var(&mut self, var: Var); fn remove_observed_var(&mut self, var: Var); diff --git a/crates/pindakaas/src/solver/cadical.rs b/crates/pindakaas/src/solver/cadical.rs index 0fe369e4f..7f2891c3f 100644 --- a/crates/pindakaas/src/solver/cadical.rs +++ b/crates/pindakaas/src/solver/cadical.rs @@ -24,7 +24,7 @@ pub struct Cadical { #[cfg(feature = "ipasir-up")] /// The external propagator called by the solver - prop: Option>, + prop: Option, } impl Default for Cadical { @@ -187,10 +187,10 @@ mod tests { } } - let p = Box::new(Dist2 { + let p = Dist2 { vars: vars.clone(), tmp: Vec::new(), - }); + }; slv.set_external_propagator(Some(p)); slv.add_clause(vars.clone().map_into()).unwrap(); for v in vars.clone() { diff --git a/crates/pindakaas/src/solver/libloading.rs b/crates/pindakaas/src/solver/libloading.rs index 934fd6a4a..42bdaae7e 100644 --- a/crates/pindakaas/src/solver/libloading.rs +++ b/crates/pindakaas/src/solver/libloading.rs @@ -1,11 +1,11 @@ +#[cfg(feature = "ipasir-up")] +use std::collections::VecDeque; use std::{ alloc::{self, Layout}, ffi::{c_char, c_int, c_void, CStr}, num::NonZeroI32, ptr, }; -#[cfg(feature = "ipasir-up")] -use std::{any::Any, collections::VecDeque}; use libloading::{Library, Symbol}; @@ -387,23 +387,9 @@ impl Iterator for ExplIter { } #[cfg(feature = "ipasir-up")] -#[derive(Debug, Clone, Copy)] -pub(crate) struct NoProp; - -#[cfg(feature = "ipasir-up")] -impl Propagator for NoProp { - fn as_any(&self) -> &dyn Any { - self - } - fn as_mut_any(&mut self) -> &mut dyn Any { - self - } -} - -#[cfg(feature = "ipasir-up")] -pub(crate) struct IpasirPropStore { +pub(crate) struct IpasirPropStore

{ /// Rust Propagator - pub(crate) prop: Box, + pub(crate) prop: P, /// IPASIR solver pointer pub(crate) slv: *mut dyn SolvingActions, /// Propagation queue @@ -416,8 +402,8 @@ pub(crate) struct IpasirPropStore { } #[cfg(feature = "ipasir-up")] -impl IpasirPropStore { - pub(crate) fn new(prop: Box, slv: *mut dyn SolvingActions) -> Self { +impl

IpasirPropStore

{ + pub(crate) fn new(prop: P, slv: *mut dyn SolvingActions) -> Self { Self { prop, slv, @@ -432,23 +418,28 @@ impl IpasirPropStore { // --- Callback functions for C propagator interface --- #[cfg(feature = "ipasir-up")] -pub(crate) unsafe extern "C" fn ipasir_notify_assignment_cb( +pub(crate) unsafe extern "C" fn ipasir_notify_assignment_cb( state: *mut c_void, lit: i32, is_fixed: bool, ) { - let prop = &mut *(state as *mut IpasirPropStore); + let prop = &mut *(state as *mut IpasirPropStore

); let lit = crate::Lit(std::num::NonZeroI32::new(lit).unwrap()); prop.prop.notify_assignment(lit, is_fixed) } #[cfg(feature = "ipasir-up")] -pub(crate) unsafe extern "C" fn ipasir_notify_new_decision_level_cb(state: *mut c_void) { - let prop = &mut *(state as *mut IpasirPropStore); +pub(crate) unsafe extern "C" fn ipasir_notify_new_decision_level_cb( + state: *mut c_void, +) { + let prop = &mut *(state as *mut IpasirPropStore

); prop.prop.notify_new_decision_level() } #[cfg(feature = "ipasir-up")] -pub(crate) unsafe extern "C" fn ipasir_notify_backtrack_cb(state: *mut c_void, level: usize) { - let prop = &mut *(state as *mut IpasirPropStore); +pub(crate) unsafe extern "C" fn ipasir_notify_backtrack_cb( + state: *mut c_void, + level: usize, +) { + let prop = &mut *(state as *mut IpasirPropStore

); prop.pqueue.clear(); prop.explaining = None; prop.rqueue.clear(); @@ -456,12 +447,12 @@ pub(crate) unsafe extern "C" fn ipasir_notify_backtrack_cb(state: *mut c_void, l prop.prop.notify_backtrack(level); } #[cfg(feature = "ipasir-up")] -pub(crate) unsafe extern "C" fn ipasir_check_model_cb( +pub(crate) unsafe extern "C" fn ipasir_check_model_cb( state: *mut c_void, len: usize, model: *const i32, ) -> bool { - let prop = &mut *(state as *mut IpasirPropStore); + let prop = &mut *(state as *mut IpasirPropStore

); let sol = if len > 0 { std::slice::from_raw_parts(model, len) } else { @@ -475,8 +466,8 @@ pub(crate) unsafe extern "C" fn ipasir_check_model_cb( prop.prop.check_model(&mut *prop.slv, &value) } #[cfg(feature = "ipasir-up")] -pub(crate) unsafe extern "C" fn ipasir_decide_cb(state: *mut c_void) -> i32 { - let prop = &mut *(state as *mut IpasirPropStore); +pub(crate) unsafe extern "C" fn ipasir_decide_cb(state: *mut c_void) -> i32 { + let prop = &mut *(state as *mut IpasirPropStore

); if let Some(l) = prop.prop.decide() { l.0.into() } else { @@ -484,8 +475,8 @@ pub(crate) unsafe extern "C" fn ipasir_decide_cb(state: *mut c_void) -> i32 { } } #[cfg(feature = "ipasir-up")] -pub(crate) unsafe extern "C" fn ipasir_propagate_cb(state: *mut c_void) -> i32 { - let prop = &mut *(state as *mut IpasirPropStore); +pub(crate) unsafe extern "C" fn ipasir_propagate_cb(state: *mut c_void) -> i32 { + let prop = &mut *(state as *mut IpasirPropStore

); if prop.pqueue.is_empty() { let slv = &mut *prop.slv; prop.pqueue = prop.prop.propagate(slv).into() @@ -497,11 +488,11 @@ pub(crate) unsafe extern "C" fn ipasir_propagate_cb(state: *mut c_void) -> i32 { } } #[cfg(feature = "ipasir-up")] -pub(crate) unsafe extern "C" fn ipasir_add_reason_clause_lit_cb( +pub(crate) unsafe extern "C" fn ipasir_add_reason_clause_lit_cb( state: *mut c_void, propagated_lit: i32, ) -> i32 { - let prop = &mut *(state as *mut IpasirPropStore); + let prop = &mut *(state as *mut IpasirPropStore

); let lit = crate::Lit(std::num::NonZeroI32::new(propagated_lit).unwrap()); debug_assert!(prop.explaining.is_none() || prop.explaining == Some(lit)); // TODO: Can this be prop.explaining.is_none()? @@ -518,14 +509,18 @@ pub(crate) unsafe extern "C" fn ipasir_add_reason_clause_lit_cb( } } #[cfg(feature = "ipasir-up")] -pub(crate) unsafe extern "C" fn ipasir_has_external_clause_cb(state: *mut c_void) -> bool { - let prop = &mut *(state as *mut IpasirPropStore); +pub(crate) unsafe extern "C" fn ipasir_has_external_clause_cb( + state: *mut c_void, +) -> bool { + let prop = &mut *(state as *mut IpasirPropStore

); prop.cqueue = prop.prop.add_external_clause(&mut *prop.slv).map(Vec::into); prop.cqueue.is_some() } #[cfg(feature = "ipasir-up")] -pub(crate) unsafe extern "C" fn ipasir_add_external_clause_lit_cb(state: *mut c_void) -> i32 { - let prop = &mut *(state as *mut IpasirPropStore); +pub(crate) unsafe extern "C" fn ipasir_add_external_clause_lit_cb( + state: *mut c_void, +) -> i32 { + let prop = &mut *(state as *mut IpasirPropStore

); if prop.cqueue.is_none() { debug_assert!(false); // This function shouldn't be called when "has_clause" returned false.