Resolve one level of dispatch for IPASIR UP callbacks

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<crate::solver::libloading::IpasirPropStore>,
+				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<dyn crate::solver::Propagator>, slv: *mut dyn crate::solver::SolvingActions) -> Self {
+				pub(crate) fn new<P: crate::solver::Propagator + 'static>(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::<P>::new(prop, slv);
+					let drop_prop = |x: *mut std::ffi::c_void| {
+						let prop = unsafe { Box::<P>::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::<P>)) };
+					unsafe { #krate::ipasir_prop_set_notify_new_decision_level(wrapper, Some(crate::solver::libloading::ipasir_notify_new_decision_level_cb::<P>)) };
+					unsafe { #krate::ipasir_prop_set_notify_backtrack(wrapper, Some(crate::solver::libloading::ipasir_notify_backtrack_cb::<P>)) };
+					unsafe { #krate::ipasir_prop_set_check_model(wrapper, Some(crate::solver::libloading::ipasir_check_model_cb::<P>)) };
+					unsafe { #krate::ipasir_prop_set_decide(wrapper, Some(crate::solver::libloading::ipasir_decide_cb::<P>)) };
+					unsafe { #krate::ipasir_prop_set_propagate(wrapper, Some(crate::solver::libloading::ipasir_propagate_cb::<P>)) };
+					unsafe { #krate::ipasir_prop_set_add_reason_clause_lit(wrapper, Some(crate::solver::libloading::ipasir_add_reason_clause_lit_cb::<P>)) };
+					unsafe { #krate::ipasir_prop_set_has_external_clause(wrapper, Some(crate::solver::libloading::ipasir_has_external_clause_cb::<P>)) };
+					unsafe { #krate::ipasir_prop_set_add_external_clause_lit(wrapper, Some(crate::solver::libloading::ipasir_add_external_clause_lit_cb::<P>)) };
 
-					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<P: crate::solver::Propagator + 'static>(
 					&mut self,
-					prop: Option<Box<dyn crate::solver::Propagator>>,
-				) -> Option<Box<dyn crate::solver::Propagator>> {
+					prop: Option<P>,
+				) {
 					// 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<dyn crate::solver::Propagator> = 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<P: crate::solver::Propagator + 'static>(&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<P: crate::solver::Propagator + 'static>(&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,26 +313,25 @@ 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<fn(*mut std::ffi::c_void) -> *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),
 					}
 				}
 			}
 			#[cfg(feature = "ipasir-up")]
 			impl crate::solver::PropagatorAccess for #sol_ident {
 				fn propagator<P: crate::solver::Propagator + 'static>(&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<P: crate::solver::Propagator + 'static>(&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
 					}

crates/pindakaas/src/linear/bdd.rs

@@ -52,7 +52,8 @@ impl<DB: ClauseDatabase> Encoder<DB, Linear> 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({

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<Box<dyn Propagator>>,
-	) -> Option<Box<dyn Propagator>>;
+	fn set_external_propagator<P: Propagator + 'static>(&mut self, prop: Option<P>);
 
 	fn add_observed_var(&mut self, var: Var);
 	fn remove_observed_var(&mut self, var: Var);

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<Box<CadicalProp>>,
+	prop: Option<CadicalProp>,
 }
 
 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() {

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<P> {
 	/// Rust Propagator
-	pub(crate) prop: Box<dyn Propagator>,
+	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<dyn Propagator>, slv: *mut dyn SolvingActions) -> Self {
+impl<P> IpasirPropStore<P> {
+	pub(crate) fn new(prop: P, slv: *mut dyn SolvingActions) -> Self {
 		Self {
 			prop,
 			slv,
@@ -432,36 +418,41 @@ 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<P: Propagator>(
 	state: *mut c_void,
 	lit: i32,
 	is_fixed: bool,
 ) {
-	let prop = &mut *(state as *mut IpasirPropStore);
+	let prop = &mut *(state as *mut IpasirPropStore<P>);
 	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<P: Propagator>(
+	state: *mut c_void,
+) {
+	let prop = &mut *(state as *mut IpasirPropStore<P>);
 	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<P: Propagator>(
+	state: *mut c_void,
+	level: usize,
+) {
+	let prop = &mut *(state as *mut IpasirPropStore<P>);
 	prop.pqueue.clear();
 	prop.explaining = None;
 	prop.rqueue.clear();
 	prop.cqueue = None;
 	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<P: Propagator>(
 	state: *mut c_void,
 	len: usize,
 	model: *const i32,
 ) -> bool {
-	let prop = &mut *(state as *mut IpasirPropStore);
+	let prop = &mut *(state as *mut IpasirPropStore<P>);
 	let sol = if len > 0 {
 		std::slice::from_raw_parts(model, len)
 	} else {
@@ -475,17 +466,17 @@ 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<P: Propagator>(state: *mut c_void) -> i32 {
+	let prop = &mut *(state as *mut IpasirPropStore<P>);
 	if let Some(l) = prop.prop.decide() {
 		l.0.into()
 	} else {
 		0
 	}
 }
 #[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<P: Propagator>(state: *mut c_void) -> i32 {
+	let prop = &mut *(state as *mut IpasirPropStore<P>);
 	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<P: Propagator>(
 	state: *mut c_void,
 	propagated_lit: i32,
 ) -> i32 {
-	let prop = &mut *(state as *mut IpasirPropStore);
+	let prop = &mut *(state as *mut IpasirPropStore<P>);
 	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<P: Propagator>(
+	state: *mut c_void,
+) -> bool {
+	let prop = &mut *(state as *mut IpasirPropStore<P>);
 	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<P: Propagator>(
+	state: *mut c_void,
+) -> i32 {
+	let prop = &mut *(state as *mut IpasirPropStore<P>);
 	if prop.cqueue.is_none() {
 		debug_assert!(false);
 		// This function shouldn't be called when "has_clause" returned false.