Add ability to search for literals for stronger explanations

crates/huub/src/actions.rs

@@ -1,3 +1,4 @@
+pub(crate) mod decision;
 pub(crate) mod explanation;
 pub(crate) mod initialization;
 pub(crate) mod inspection;

crates/huub/src/actions/decision.rs

@@ -0,0 +1,60 @@
+use crate::{
+	actions::{inspection::InspectionActions, trailing::TrailingActions},
+	solver::{
+		engine::int_var::IntVarRef,
+		view::{BoolViewInner, IntViewInner},
+	},
+	BoolView, IntView, LitMeaning,
+};
+
+pub(crate) trait DecisionActions: InspectionActions + TrailingActions {
+	fn get_int_lit(&mut self, var: IntView, mut meaning: LitMeaning) -> BoolView {
+		{
+			if let IntViewInner::Linear { transformer, .. }
+			| IntViewInner::Bool { transformer, .. } = var.0
+			{
+				if let Some(m) = transformer.rev_transform_lit(meaning) {
+					meaning = m;
+				} else {
+					return BoolView(BoolViewInner::Const(false));
+				}
+			}
+
+			match var.0 {
+				IntViewInner::VarRef(var) | IntViewInner::Linear { var, .. } => {
+					self.get_intref_lit(var, meaning)
+				}
+				IntViewInner::Const(c) => BoolView(BoolViewInner::Const(match meaning {
+					LitMeaning::Eq(i) => c == i,
+					LitMeaning::NotEq(i) => c != i,
+					LitMeaning::GreaterEq(i) => c >= i,
+					LitMeaning::Less(i) => c < i,
+				})),
+				IntViewInner::Bool { lit, .. } => {
+					let (meaning, negated) =
+						if matches!(meaning, LitMeaning::NotEq(_) | LitMeaning::Less(_)) {
+							(!meaning, true)
+						} else {
+							(meaning, false)
+						};
+					let bv = BoolView(match meaning {
+						LitMeaning::Eq(0) => BoolViewInner::Lit(!lit),
+						LitMeaning::Eq(1) => BoolViewInner::Lit(lit),
+						LitMeaning::Eq(_) => BoolViewInner::Const(false),
+						LitMeaning::GreaterEq(1) => BoolViewInner::Lit(lit),
+						LitMeaning::GreaterEq(i) if i > 1 => BoolViewInner::Const(false),
+						LitMeaning::GreaterEq(_) => BoolViewInner::Const(true),
+						_ => unreachable!(),
+					});
+					if negated {
+						!bv
+					} else {
+						bv
+					}
+				}
+			}
+		}
+	}
+
+	fn get_intref_lit(&mut self, var: IntVarRef, meaning: LitMeaning) -> BoolView;
+}

crates/huub/src/actions/explanation.rs

@@ -1,64 +1,9 @@
-use crate::{
-	actions::inspection::InspectionActions,
-	solver::{
-		engine::int_var::IntVarRef,
-		view::{BoolViewInner, IntViewInner},
-	},
-	BoolView, IntView, LitMeaning,
-};
+use crate::{actions::inspection::InspectionActions, BoolView, IntView, LitMeaning};
 
 pub(crate) trait ExplanationActions: InspectionActions {
 	fn try_int_lit(&self, var: IntView, meaning: LitMeaning) -> Option<BoolView>;
-	fn get_intref_lit(&mut self, var: IntVarRef, meaning: LitMeaning) -> BoolView;
-	fn get_int_lit(&mut self, var: IntView, mut meaning: LitMeaning) -> BoolView {
-		if let IntViewInner::Linear { transformer, .. } | IntViewInner::Bool { transformer, .. } =
-			var.0
-		{
-			if let Some(m) = transformer.rev_transform_lit(meaning) {
-				meaning = m;
-			} else {
-				return BoolView(BoolViewInner::Const(false));
-			}
-		}
-
-		match var.0 {
-			IntViewInner::VarRef(var) | IntViewInner::Linear { var, .. } => {
-				self.get_intref_lit(var, meaning)
-			}
-			IntViewInner::Const(c) => BoolView(BoolViewInner::Const(match meaning {
-				LitMeaning::Eq(i) => c == i,
-				LitMeaning::NotEq(i) => c != i,
-				LitMeaning::GreaterEq(i) => c >= i,
-				LitMeaning::Less(i) => c < i,
-			})),
-			IntViewInner::Bool { lit, .. } => {
-				let (meaning, negated) =
-					if matches!(meaning, LitMeaning::NotEq(_) | LitMeaning::Less(_)) {
-						(!meaning, true)
-					} else {
-						(meaning, false)
-					};
-				let bv = BoolView(match meaning {
-					LitMeaning::Eq(0) => BoolViewInner::Lit(!lit),
-					LitMeaning::Eq(1) => BoolViewInner::Lit(lit),
-					LitMeaning::Eq(_) => BoolViewInner::Const(false),
-					LitMeaning::GreaterEq(1) => BoolViewInner::Lit(lit),
-					LitMeaning::GreaterEq(i) if i > 1 => BoolViewInner::Const(false),
-					LitMeaning::GreaterEq(_) => BoolViewInner::Const(true),
-					_ => unreachable!(),
-				});
-				if negated {
-					!bv
-				} else {
-					bv
-				}
-			}
-		}
-	}
-	fn get_int_val_lit(&mut self, var: IntView) -> Option<BoolView> {
-		self.get_int_val(var)
-			.map(|v| self.get_int_lit(var, LitMeaning::Eq(v)))
-	}
+	fn get_int_lit_or_weaker(&mut self, var: IntView, meaning: LitMeaning) -> BoolView;
+	fn get_int_val_lit(&mut self, var: IntView) -> Option<BoolView>;
 	fn get_int_lower_bound_lit(&mut self, var: IntView) -> BoolView;
 	fn get_int_upper_bound_lit(&mut self, var: IntView) -> BoolView;
 }

crates/huub/src/actions/propagation.rs

@@ -1,10 +1,10 @@
 use crate::{
-	actions::explanation::ExplanationActions,
+	actions::{decision::DecisionActions, explanation::ExplanationActions},
 	propagator::{conflict::Conflict, reason::ReasonBuilder},
 	BoolView, IntVal, IntView,
 };
 
-pub(crate) trait PropagationActions: ExplanationActions {
+pub(crate) trait PropagationActions: ExplanationActions + DecisionActions {
 	fn set_bool_val(
 		&mut self,
 		bv: BoolView,

crates/huub/src/brancher.rs

@@ -3,7 +3,7 @@ use std::fmt::Debug;
 use pindakaas::Lit as RawLit;
 
 use crate::{
-	actions::{explanation::ExplanationActions, initialization::InitializationActions},
+	actions::{decision::DecisionActions, initialization::InitializationActions},
 	model::branching::{ValueSelection, VariableSelection},
 	solver::{
 		engine::trail::TrailedInt,
@@ -41,8 +41,8 @@ struct IntBrancherPoster {
 	val_sel: ValueSelection,
 }
 
-fn decide_bool<E: ExplanationActions>(
-	actions: &mut E,
+fn decide_bool<D: DecisionActions>(
+	actions: &mut D,
 	vars: &[RawLit],
 	var_sel: VariableSelection,
 	val_sel: ValueSelection,
@@ -92,8 +92,8 @@ fn decide_bool<E: ExplanationActions>(
 	})
 }
 
-fn decide_int<E: ExplanationActions>(
-	actions: &mut E,
+fn decide_int<D: DecisionActions>(
+	actions: &mut D,
 	vars: &mut [IntView],
 	var_sel: VariableSelection,
 	val_sel: ValueSelection,
@@ -178,7 +178,7 @@ fn decide_int<E: ExplanationActions>(
 }
 
 impl Brancher {
-	pub(crate) fn decide<E: ExplanationActions>(&mut self, actions: &mut E) -> Option<RawLit> {
+	pub(crate) fn decide<D: DecisionActions>(&mut self, actions: &mut D) -> Option<RawLit> {
 		match &mut self.vars {
 			BrancherVars::Bool(vars) => {
 				decide_bool(actions, vars, self.var_sel, self.val_sel, self.next)

crates/huub/src/model/constraint.rs

@@ -8,7 +8,7 @@ use pindakaas::{
 use rangelist::RangeList;
 
 use crate::{
-	actions::{explanation::ExplanationActions, inspection::InspectionActions},
+	actions::{decision::DecisionActions, inspection::InspectionActions},
 	helpers::{div_ceil, div_floor},
 	model::{
 		bool::BoolView,

crates/huub/src/model/reformulate.rs

@@ -7,8 +7,12 @@ use pindakaas::{
 use thiserror::Error;
 
 use crate::{
-	actions::explanation::ExplanationActions,
-	model::{bool, int, int::IntVar, ModelView},
+	actions::decision::DecisionActions,
+	model::{
+		bool,
+		int::{self, IntVar},
+		ModelView,
+	},
 	solver::{
 		view::{BoolView, BoolViewInner, IntViewInner, SolverView},
 		SatSolver,

crates/huub/src/propagator.rs

@@ -18,7 +18,7 @@ use crate::{
 	},
 	propagator::{conflict::Conflict, int_event::IntEvent},
 	solver::{
-		engine::{propagation_context::PropagationContext, trail::Trail, State},
+		engine::{solving_context::SolvingContext, trail::Trail, State},
 		poster::BoxedPropagator,
 	},
 	Conjunction,
@@ -73,9 +73,7 @@ pub(crate) trait Propagator<P: PropagationActions, E: ExplanationActions, T: Tra
 pub(crate) trait DynPropClone {
 	fn clone_dyn_prop(&self) -> BoxedPropagator;
 }
-impl<P: for<'a> Propagator<PropagationContext<'a>, State, Trail> + Clone + 'static> DynPropClone
-	for P
-{
+impl<P: for<'a> Propagator<SolvingContext<'a>, State, Trail> + Clone + 'static> DynPropClone for P {
 	fn clone_dyn_prop(&self) -> BoxedPropagator {
 		Box::new(self.clone())
 	}

crates/huub/src/solver.rs

@@ -21,7 +21,8 @@ use tracing::{debug, trace};
 
 use crate::{
 	actions::{
-		explanation::ExplanationActions, inspection::InspectionActions, trailing::TrailingActions,
+		decision::DecisionActions, explanation::ExplanationActions, inspection::InspectionActions,
+		trailing::TrailingActions,
 	},
 	solver::{
 		engine::{
@@ -150,7 +151,7 @@ where
 		let p = self.engine_mut().propagators.push(prop);
 		debug_assert_eq!(prop_ref, p);
 		let engine = self.engine_mut();
-		let p = engine.state.prop_priority.push(queue_pref.priority);
+		let p = engine.state.propagator_priority.push(queue_pref.priority);
 		debug_assert_eq!(prop_ref, p);
 		let p = self.engine_mut().state.enqueued.push(false);
 		debug_assert_eq!(prop_ref, p);
@@ -474,21 +475,11 @@ where
 	}
 }
 
-impl<Sol, Sat> ExplanationActions for Solver<Sat>
+impl<Sol, Sat> DecisionActions for Solver<Sat>
 where
 	Sol: PropagatorAccess + SatValuation,
 	Sat: SatSolver + SolverTrait<ValueFn = Sol>,
 {
-	delegate! {
-		to self.engine().state {
-			fn try_int_lit(&self, var: IntView, meaning: LitMeaning) -> Option<BoolView>;
-		}
-		to self.engine_mut().state {
-			fn get_int_lower_bound_lit(&mut self, var: IntView) -> BoolView;
-			fn get_int_upper_bound_lit(&mut self, var: IntView) -> BoolView;
-		}
-	}
-
 	fn get_intref_lit(&mut self, iv: IntVarRef, meaning: LitMeaning) -> BoolView {
 		// TODO: We currently copy the integer variable struct here to avoid
 		// borrowing issues. Hopefully the compiler sees that this is unnecessary,
@@ -520,6 +511,28 @@ where
 	}
 }
 
+impl<Sol, Sat> ExplanationActions for Solver<Sat>
+where
+	Sol: PropagatorAccess + SatValuation,
+	Sat: SatSolver + SolverTrait<ValueFn = Sol>,
+{
+	delegate! {
+		to self.engine().state {
+			fn try_int_lit(&self, var: IntView, meaning: LitMeaning) -> Option<BoolView>;
+		}
+		to self.engine_mut().state {
+			fn get_int_lower_bound_lit(&mut self, var: IntView) -> BoolView;
+			fn get_int_upper_bound_lit(&mut self, var: IntView) -> BoolView;
+			fn get_int_lit_or_weaker(&mut self, var: IntView, meaning: LitMeaning) -> BoolView;
+		}
+	}
+
+	fn get_int_val_lit(&mut self, var: IntView) -> Option<BoolView> {
+		let val = self.get_int_val(var)?;
+		Some(self.get_int_lit(var, LitMeaning::Eq(val)))
+	}
+}
+
 impl<Sol, Sat> InspectionActions for Solver<Sat>
 where
 	Sol: PropagatorAccess + SatValuation,