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(&self) -> Option<&P> { + #prop_member.as_ref().map(|p| p.prop.prop.as_any().downcast_ref()).flatten() + } + fn propagator_mut(&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>, ) -> Option>; + /// 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(&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(&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> { 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> { 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::().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 {