Give SolverActions access when calling check_model and add_external_c…

…lause

crates/pindakaas/src/solver.rs

@@ -160,8 +160,9 @@ pub trait Propagator {
 	/// Method called to check the found complete solution (after solution
 	/// reconstruction). If it returns false, the propagator must provide an
 	/// external clause during the next callback.
-	fn check_model(&mut self, value: &dyn Valuation) -> bool {
+	fn check_model(&mut self, slv: &mut dyn SolvingActions, value: &dyn Valuation) -> bool {
 		let _ = value;
+		let _ = slv;
 		true
 	}
 
@@ -189,7 +190,8 @@ pub trait Propagator {
 	}
 
 	/// Method to ask whether there is an external clause to add to the solver.
-	fn add_external_clause(&mut self) -> Option<Vec<Lit>> {
+	fn add_external_clause(&mut self, slv: &mut dyn SolvingActions) -> Option<Vec<Lit>> {
+		let _ = slv;
 		None
 	}
 

crates/pindakaas/src/solver/cadical.rs

@@ -100,7 +100,10 @@ mod tests {
 
 		use crate::{
 			helpers::tests::lits,
-			solver::{NextVarRange, PropagatingSolver, Propagator, PropagatorAccess, VarRange},
+			solver::{
+				NextVarRange, PropagatingSolver, Propagator, PropagatorAccess, SolvingActions,
+				VarRange,
+			},
 		};
 
 		let mut slv = Cadical::default();
@@ -115,7 +118,11 @@ mod tests {
 			fn is_lazy(&self) -> bool {
 				true
 			}
-			fn check_model(&mut self, model: &dyn crate::Valuation) -> bool {
+			fn check_model(
+				&mut self,
+				_slv: &mut dyn SolvingActions,
+				model: &dyn crate::Valuation,
+			) -> bool {
 				let mut vars = self.vars.clone();
 				while let Some(v) = vars.next() {
 					if model.value(v.into()).unwrap_or(true) {
@@ -129,7 +136,7 @@ mod tests {
 				}
 				self.tmp.is_empty()
 			}
-			fn add_external_clause(&mut self) -> Option<Vec<Lit>> {
+			fn add_external_clause(&mut self, _slv: &mut dyn SolvingActions) -> Option<Vec<Lit>> {
 				self.tmp.pop()
 			}
 
@@ -148,7 +155,7 @@ mod tests {
 		slv.set_external_propagator(Some(p));
 		slv.add_clause(vars.clone().map_into()).unwrap();
 		for v in vars.clone() {
-			slv.add_observed_var(v)
+			PropagatingSolver::add_observed_var(&mut slv, v)
 		}
 
 		let mut solns = Vec::new();

crates/pindakaas/src/solver/libloading.rs

@@ -420,7 +420,7 @@ pub(crate) unsafe extern "C" fn ipasir_check_model_cb(
 		.map(|&i| (Var(NonZeroI32::new(i.abs()).unwrap()), i >= 0))
 		.collect();
 	let value = |l: Lit| sol.get(&l.var()).copied();
-	prop.prop.check_model(&value)
+	prop.prop.check_model(&mut *prop.slv, &value)
 }
 #[cfg(feature = "ipasir-up")]
 pub(crate) unsafe extern "C" fn ipasir_decide_cb(state: *mut c_void) -> i32 {
@@ -468,7 +468,7 @@ pub(crate) unsafe extern "C" fn ipasir_add_reason_clause_lit_cb(
 #[cfg(feature = "ipasir-up")]
 pub(crate) unsafe extern "C" fn ipasir_has_external_clause_cb(state: *mut c_void) -> bool {
 	let prop = &mut *(state as *mut IpasirPropStore);
-	prop.cqueue = prop.prop.add_external_clause().map(Vec::into);
+	prop.cqueue = prop.prop.add_external_clause(&mut *prop.slv).map(Vec::into);
 	prop.cqueue.is_some()
 }
 #[cfg(feature = "ipasir-up")]
@@ -477,7 +477,7 @@ pub(crate) unsafe extern "C" fn ipasir_add_external_clause_lit_cb(state: *mut c_
 	if prop.cqueue.is_none() {
 		debug_assert!(false);
 		// This function shouldn't be called when "has_clause" returned false.
-		prop.cqueue = prop.prop.add_external_clause().map(Vec::into);
+		prop.cqueue = prop.prop.add_external_clause(&mut *prop.slv).map(Vec::into);
 	}
 	if let Some(queue) = &mut prop.cqueue {
 		if let Some(l) = queue.pop_front() {