Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Give (mutable) access to the set external propagator #37

Merged
merged 1 commit into from
Feb 8, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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: 61 additions & 0 deletions crates/pindakaas/src/solver.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
#[cfg(feature = "ipasir-up")]
use std::any::Any;
use std::num::NonZeroI32;

use crate::{helpers::VarRange, ClauseDatabase, Lit, Valuation, Var};
Expand Down Expand Up @@ -92,6 +94,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 +174,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())
}
}
11 changes: 9 additions & 2 deletions crates/pindakaas/src/solver/libloading.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
#[cfg(feature = "ipasir-up")]
use std::collections::VecDeque;
use std::{any::Any, collections::VecDeque};
use std::{
ffi::{c_char, c_int, c_void, CStr},
num::NonZeroI32,
Expand Down Expand Up @@ -303,7 +303,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