Skip to content

Commit

Permalink
Give (mutable) access to the set external propagator
Browse files Browse the repository at this point in the history
  • Loading branch information
Dekker1 committed Feb 8, 2024
1 parent 4c94aa6 commit 6cd5d64
Show file tree
Hide file tree
Showing 4 changed files with 86 additions and 2 deletions.
7 changes: 7 additions & 0 deletions crates/pindakaas-derive/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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()) };
}
Expand Down
61 changes: 60 additions & 1 deletion crates/pindakaas/src/solver.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
use std::num::NonZeroI32;
use std::{any::Any, num::NonZeroI32};

use crate::{helpers::VarRange, ClauseDatabase, Lit, Valuation, Var};

Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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")]
Expand Down
10 changes: 10 additions & 0 deletions crates/pindakaas/src/solver/cadical.rs
Original file line number Diff line number Diff line change
Expand Up @@ -94,6 +94,8 @@ mod tests {
#[cfg(feature = "ipasir-up")]
#[test]
fn test_ipasir_up() {
use std::any::Any;

use itertools::Itertools;

use crate::{
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -174,5 +183,6 @@ mod tests {
lits![-1, -2, -3, -4, 5],
]
);
assert!(slv.propagator::<Dist2>().unwrap().tmp.is_empty())
}
}
10 changes: 9 additions & 1 deletion crates/pindakaas/src/solver/libloading.rs
Original file line number Diff line number Diff line change
@@ -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,
Expand Down Expand Up @@ -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 {
Expand Down

0 comments on commit 6cd5d64

Please sign in to comment.