From 6cd5d649789272de65a0e57916f4907bf313ff64 Mon Sep 17 00:00:00 2001
From: "Jip J. Dekker" <jip@dekker.one>
Date: Thu, 8 Feb 2024 13:28:37 +0100
Subject: [PATCH] Give (mutable) access to the set external propagator

---
 crates/pindakaas-derive/src/lib.rs        |  7 +++
 crates/pindakaas/src/solver.rs            | 61 ++++++++++++++++++++++-
 crates/pindakaas/src/solver/cadical.rs    | 10 ++++
 crates/pindakaas/src/solver/libloading.rs | 10 +++-
 4 files changed, 86 insertions(+), 2 deletions(-)

diff --git a/crates/pindakaas-derive/src/lib.rs b/crates/pindakaas-derive/src/lib.rs
index b46c0d49af..f993f40869 100644
--- a/crates/pindakaas-derive/src/lib.rs
+++ b/crates/pindakaas-derive/src/lib.rs
@@ -215,6 +215,13 @@ pub fn ipasir_solver_derive(input: TokenStream) -> TokenStream {
 					}
 				}
 
+				fn propagator<P: crate::solver::Propagator + 'static>(&self) -> Option<&P> {
+					#prop_member.as_ref().map(|p| p.prop.prop.as_any().downcast_ref()).flatten()
+				}
+				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()
+				}
+
 				fn add_observed_var(&mut self, var: crate::Var){
 					unsafe { #krate::ipasir_add_observed_var( #ptr, var.0.get()) };
 				}
diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs
index 64b6f73f99..2352be0b4f 100644
--- a/crates/pindakaas/src/solver.rs
+++ b/crates/pindakaas/src/solver.rs
@@ -1,4 +1,4 @@
-use std::num::NonZeroI32;
+use std::{any::Any, num::NonZeroI32};
 
 use crate::{helpers::VarRange, ClauseDatabase, Lit, Valuation, Var};
 
@@ -92,6 +92,18 @@ pub trait PropagatingSolver: Solver {
 		prop: Option<Box<dyn Propagator>>,
 	) -> Option<Box<dyn Propagator>>;
 
+	/// Access the external propagator given the to solver
+	///
+	/// This method will return [`None`] if no propagator is set, or if the
+	/// propagator is not of type [`P`].
+	fn propagator<P: Propagator + 'static>(&self) -> Option<&P>;
+
+	/// Get mutable access to the external propagator given the to solver
+	///
+	/// This method will return [`None`] if no propagator is set, or if the
+	/// propagator is not of type [`P`].
+	fn propagator_mut<P: Propagator + 'static>(&mut self) -> Option<&mut P>;
+
 	fn add_observed_var(&mut self, var: Var);
 	fn remove_observed_var(&mut self, var: Var);
 	fn reset_observed_vars(&mut self);
@@ -160,6 +172,53 @@ pub trait Propagator {
 	fn add_external_clause(&mut self) -> Option<Vec<Lit>> {
 		None
 	}
+
+	/// Method to help access to the propagator when given to the solver.
+	///
+	/// See [`PropagatingSolver::propagator`].
+	///
+	/// # Note
+	///
+	/// This method can generally be implemented as
+	/// ```rust
+	/// use std::any::Any;
+	/// use pindakaas::solver::Propagator;
+	///
+	/// struct A;
+	///
+	/// impl Propagator for A {
+	/// 	fn as_any(&self) -> &dyn Any {
+	/// 		self
+	/// 	}
+	///
+	/// #  fn as_mut_any(&mut self) -> &mut dyn Any { self }
+	/// }
+	///
+	/// ```
+	fn as_any(&self) -> &dyn Any;
+
+	/// Method to help access to the propagator when given to the solver.
+	///
+	/// See [`PropagatingSolver::propagator`].
+	///
+	/// # Note
+	///
+	/// This method can generally be implemented as
+	/// ```rust
+	/// use std::any::Any;
+	/// use pindakaas::solver::Propagator;
+	///
+	/// struct A;
+	///
+	/// impl Propagator for A {
+	/// 	fn as_mut_any(&mut self) -> &mut dyn Any {
+	/// 		self
+	/// 	}
+	/// #  fn as_any(&self) -> &dyn Any { self }
+	/// }
+	///
+	/// ```
+	fn as_mut_any(&mut self) -> &mut dyn Any;
 }
 
 #[cfg(feature = "ipasir-up")]
diff --git a/crates/pindakaas/src/solver/cadical.rs b/crates/pindakaas/src/solver/cadical.rs
index aeb480915d..db261fd0dd 100644
--- a/crates/pindakaas/src/solver/cadical.rs
+++ b/crates/pindakaas/src/solver/cadical.rs
@@ -94,6 +94,8 @@ mod tests {
 	#[cfg(feature = "ipasir-up")]
 	#[test]
 	fn test_ipasir_up() {
+		use std::any::Any;
+
 		use itertools::Itertools;
 
 		use crate::{
@@ -130,6 +132,13 @@ mod tests {
 			fn add_external_clause(&mut self) -> Option<Vec<Lit>> {
 				self.tmp.pop()
 			}
+
+			fn as_any(&self) -> &dyn Any {
+				self
+			}
+			fn as_mut_any(&mut self) -> &mut dyn Any {
+				self
+			}
 		}
 
 		let p = Box::new(Dist2 {
@@ -174,5 +183,6 @@ mod tests {
 				lits![-1, -2, -3, -4, 5],
 			]
 		);
+		assert!(slv.propagator::<Dist2>().unwrap().tmp.is_empty())
 	}
 }
diff --git a/crates/pindakaas/src/solver/libloading.rs b/crates/pindakaas/src/solver/libloading.rs
index 1029633192..f1cc502960 100644
--- a/crates/pindakaas/src/solver/libloading.rs
+++ b/crates/pindakaas/src/solver/libloading.rs
@@ -1,6 +1,7 @@
 #[cfg(feature = "ipasir-up")]
 use std::collections::VecDeque;
 use std::{
+	any::Any,
 	ffi::{c_char, c_int, c_void, CStr},
 	num::NonZeroI32,
 	ptr,
@@ -303,7 +304,14 @@ impl Iterator for ExplIter {
 pub(crate) struct NoProp;
 
 #[cfg(feature = "ipasir-up")]
-impl Propagator for NoProp {}
+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 {