diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs index 993c2b5ea8..62994f84eb 100644 --- a/crates/pindakaas/src/solver.rs +++ b/crates/pindakaas/src/solver.rs @@ -138,8 +138,8 @@ pub trait Propagator { false } - /// Method called to notify the propagator about assignments to observed - /// variables. + /// Method called to notify the propagator about assignments of literals + /// concerning observed variables. /// /// The notification is not necessarily eager. It usually happens before the /// call of propagator callbacks and when a driving clause is leading to an @@ -147,9 +147,8 @@ pub trait Propagator { /// /// If [`persistent`] is set to `true`, then the assignment is known to /// persist through backtracking. - fn notify_assignment(&mut self, var: Var, val: bool, persistent: bool) { - let _ = var; - let _ = val; + fn notify_assignment(&mut self, lit: Lit, persistent: bool) { + let _ = lit; let _ = persistent; } fn notify_new_decision_level(&mut self) {} diff --git a/crates/pindakaas/src/solver/libloading.rs b/crates/pindakaas/src/solver/libloading.rs index 38be6865d4..51f3ecb928 100644 --- a/crates/pindakaas/src/solver/libloading.rs +++ b/crates/pindakaas/src/solver/libloading.rs @@ -386,8 +386,7 @@ pub(crate) unsafe extern "C" fn ipasir_notify_assignment_cb( ) { let prop = &mut *(state as *mut IpasirPropStore); let lit = crate::Lit(std::num::NonZeroI32::new(lit).unwrap()); - prop.prop - .notify_assignment(lit.var(), !lit.is_negated(), is_fixed) + prop.prop.notify_assignment(lit, is_fixed) } #[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_notify_new_decision_level_cb(state: *mut c_void) {