Update notify_assignment callback

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) {

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) {