From 180c3dc426ce276425d4fedda6d3831a6cd8bd8e Mon Sep 17 00:00:00 2001
From: "Jip J. Dekker" <jip@dekker.one>
Date: Mon, 5 Aug 2024 21:55:04 +1000
Subject: [PATCH] Allow propagators to access solving actions in decide
 callback

This allows propagators to branch on new literals that the propagator
might (later) assign its own meaning to.
---
 crates/pindakaas/src/solver.rs            | 3 ++-
 crates/pindakaas/src/solver/libloading.rs | 7 +++++--
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/crates/pindakaas/src/solver.rs b/crates/pindakaas/src/solver.rs
index 0e3f65aaad..7747770ae7 100644
--- a/crates/pindakaas/src/solver.rs
+++ b/crates/pindakaas/src/solver.rs
@@ -173,7 +173,8 @@ pub trait Propagator {
 
 	/// Method called when the solver asks for the next decision literal. If it
 	/// returns None, the solver makes its own choice.
-	fn decide(&mut self) -> Option<Lit> {
+	fn decide(&mut self, slv: &mut dyn SolvingActions) -> Option<Lit> {
+		let _ = slv;
 		None
 	}
 
diff --git a/crates/pindakaas/src/solver/libloading.rs b/crates/pindakaas/src/solver/libloading.rs
index fc5230221c..b07c46546d 100644
--- a/crates/pindakaas/src/solver/libloading.rs
+++ b/crates/pindakaas/src/solver/libloading.rs
@@ -492,9 +492,12 @@ pub(crate) unsafe extern "C" fn ipasir_check_model_cb<P: Propagator, A: SolvingA
 	prop.prop.check_model(&mut prop.slv, &value)
 }
 #[cfg(feature = "ipasir-up")]
-pub(crate) unsafe extern "C" fn ipasir_decide_cb<P: Propagator, A>(state: *mut c_void) -> i32 {
+pub(crate) unsafe extern "C" fn ipasir_decide_cb<P: Propagator, A: SolvingActions>(
+	state: *mut c_void,
+) -> i32 {
 	let prop = &mut *(state as *mut IpasirPropStore<P, A>);
-	if let Some(l) = prop.prop.decide() {
+	let slv = &mut prop.slv;
+	if let Some(l) = prop.prop.decide(slv) {
 		l.0.into()
 	} else {
 		0