Skip to content

Commit

Permalink
Allow propagators to access solving actions in decide callback
Browse files Browse the repository at this point in the history
This allows propagators to branch on new literals that the propagator
might (later) assign its own meaning to.
  • Loading branch information
Dekker1 committed Aug 5, 2024
1 parent dbded2b commit 180c3dc
Show file tree
Hide file tree
Showing 2 changed files with 7 additions and 3 deletions.
3 changes: 2 additions & 1 deletion crates/pindakaas/src/solver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -173,7 +173,8 @@ pub trait Propagator {

/// Method called when the solver asks for the next decision literal. If it
/// returns None, the solver makes its own choice.
fn decide(&mut self) -> Option<Lit> {
fn decide(&mut self, slv: &mut dyn SolvingActions) -> Option<Lit> {
let _ = slv;
None
}

Expand Down
7 changes: 5 additions & 2 deletions crates/pindakaas/src/solver/libloading.rs
Original file line number Diff line number Diff line change
Expand Up @@ -492,9 +492,12 @@ pub(crate) unsafe extern "C" fn ipasir_check_model_cb<P: Propagator, A: SolvingA
prop.prop.check_model(&mut prop.slv, &value)
}
#[cfg(feature = "ipasir-up")]
pub(crate) unsafe extern "C" fn ipasir_decide_cb<P: Propagator, A>(state: *mut c_void) -> i32 {
pub(crate) unsafe extern "C" fn ipasir_decide_cb<P: Propagator, A: SolvingActions>(
state: *mut c_void,
) -> i32 {
let prop = &mut *(state as *mut IpasirPropStore<P, A>);
if let Some(l) = prop.prop.decide() {
let slv = &mut prop.slv;
if let Some(l) = prop.prop.decide(slv) {
l.0.into()
} else {
0
Expand Down

0 comments on commit 180c3dc

Please sign in to comment.