From 596142da10082022e7528911f9f712d460ef95cf Mon Sep 17 00:00:00 2001
From: "Jip J. Dekker" <jip@dekker.one>
Date: Tue, 10 Sep 2024 17:27:13 +1000
Subject: [PATCH] Trail integer consequences before literal assignments

---
 crates/huub/src/solver/engine.rs              | 43 +++++++++++++------
 .../huub/src/solver/engine/solving_context.rs |  1 +
 2 files changed, 30 insertions(+), 14 deletions(-)

diff --git a/crates/huub/src/solver/engine.rs b/crates/huub/src/solver/engine.rs
index b81dd0fe..ba020598 100644
--- a/crates/huub/src/solver/engine.rs
+++ b/crates/huub/src/solver/engine.rs
@@ -145,14 +145,14 @@ impl IpasirPropagator for Engine {
 				return;
 			}
 		}
-		if self.state.trail.assign_sat(lit).is_some() {
+		if self.state.trail.get_sat_value(lit).is_some() || self.state.conflict.is_some() {
 			return;
 		}
 
-		// Enqueue propagators, if no conflict has been found
-		if self.state.conflict.is_none() {
-			self.state.enqueue_propagators(lit, None);
-		}
+		// Enqueue propagators and process integer consequences
+		self.state.enqueue_propagators(lit, None);
+		// Trail the SAT assignment
+		let _ = self.state.trail.assign_sat(lit).is_some();
 	}
 
 	fn notify_new_decision_level(&mut self) {
@@ -233,9 +233,6 @@ impl IpasirPropagator for Engine {
 				.collect::<Vec<i32>>(),
 			"propagate"
 		);
-		for &lit in queue.iter() {
-			self.state.enqueue_propagators(lit, None);
-		}
 		// Debug helper to ensure that any reason is based on known true literals
 		#[cfg(debug_assertions)]
 		{
@@ -243,16 +240,14 @@ impl IpasirPropagator for Engine {
 				if let Some(reason) = self.state.reason_map.get(lit).cloned() {
 					let clause: Vec<_> = reason.to_clause(&mut self.propagators, &mut self.state);
 					for l in &clause {
-						let val = self.state.trail.get_sat_value(!l);
-						if !val.unwrap_or(false) {
+						let val = self.state.reason_lit_known_positive(!l);
+						if !val {
 							tracing::error!(lit_prop = i32::from(*lit), lit_reason= i32::from(!l), reason_val = ?val, "invalid reason");
 						}
 						debug_assert!(
-							val.unwrap_or(false),
+							val,
 							"Literal {} in Reason for {} is {:?}, but should be known true",
-							!l,
-							lit,
-							val
+							!l, lit, val
 						);
 					}
 				}
@@ -547,6 +542,26 @@ impl State {
 		}
 	}
 
+	#[cfg(debug_assertions)]
+	fn reason_lit_known_positive(&self, lit: RawLit) -> bool {
+		if let Some(val) = self.trail.get_sat_value(lit) {
+			val
+		} else if let Some((iv, meaning)) = self.bool_to_int.get(lit.var()) {
+			let meaning = meaning
+				.map(|l| if lit.is_negated() { !l } else { l })
+				.unwrap_or_else(|| self.int_vars[iv].lit_meaning(lit));
+			let (lb, ub) = self.int_vars[iv].get_bounds(&self.trail);
+			match meaning {
+				LitMeaning::Eq(v) => lb == v && v == ub,
+				LitMeaning::NotEq(_) => false, // TODO: Is this possible?
+				LitMeaning::GreaterEq(v) => lb >= v,
+				LitMeaning::Less(v) => ub < v,
+			}
+		} else {
+			false
+		}
+	}
+
 	fn register_reason(&mut self, lit: RawLit, built_reason: Result<Reason, bool>) {
 		match built_reason {
 			Ok(reason) => {
diff --git a/crates/huub/src/solver/engine/solving_context.rs b/crates/huub/src/solver/engine/solving_context.rs
index f1baf123..df99f8e1 100644
--- a/crates/huub/src/solver/engine/solving_context.rs
+++ b/crates/huub/src/solver/engine/solving_context.rs
@@ -225,6 +225,7 @@ impl PropagationActions for SolvingContext<'_> {
 					trace!(lit = i32::from(propagated_lit), reason = ?reason, "propagate bool");
 					self.state.register_reason(propagated_lit, reason);
 					self.state.propagation_queue.push(propagated_lit);
+					self.state.enqueue_propagators(propagated_lit, None);
 					let prev = self.state.trail.assign_sat(propagated_lit);
 					debug_assert!(prev.is_none());
 					Ok(())