IPASIR-UP: Use literals in the notify_assignment callback

crates/pindakaas/src/solver.rs

@@ -138,18 +138,17 @@ 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
 	/// 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;
+	fn notify_assignment(&mut self, lit: Lit, persistent: bool) {
+		let _ = lit;
 		let _ = persistent;
 	}
 	fn notify_new_decision_level(&mut self) {}

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