diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs index 4fcb32b3c9..64b6f73f99 100644 --- a/crates/pindakaas/src/solver.rs +++ b/crates/pindakaas/src/solver.rs @@ -107,12 +107,18 @@ pub trait Propagator { } /// Method called to notify the propagator about assignments to 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 assignment. - fn notify_assignment(&mut self, lit: Lit, is_fixed: bool) { - let _ = lit; - let _ = is_fixed; + /// 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 + /// assignment. + /// + /// 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; + let _ = persistent; } fn notify_new_decision_level(&mut self) {} fn notify_backtrack(&mut self, new_level: usize) { diff --git a/crates/pindakaas/src/solver/libloading.rs b/crates/pindakaas/src/solver/libloading.rs index 12d1f870d0..1029633192 100644 --- a/crates/pindakaas/src/solver/libloading.rs +++ b/crates/pindakaas/src/solver/libloading.rs @@ -344,7 +344,8 @@ 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, is_fixed) + prop.prop + .notify_assignment(lit.var(), !lit.is_negated(), is_fixed) } #[cfg(feature = "ipasir-up")] pub(crate) unsafe extern "C" fn ipasir_notify_new_decision_level_cb(state: *mut c_void) {