Use lower bounds of integer variables to determine solution values

crates/huub/src/solver.rs

@@ -26,7 +26,7 @@ use crate::{
 	},
 	solver::{
 		engine::{
-			int_var::{IntVarRef, LazyLitDef},
+			int_var::{IntVarRef, LazyLitDef, OrderStorage},
 			trace_new_lit,
 			trail::TrailedInt,
 			Engine, PropRef, SearchStatistics,
@@ -421,6 +421,15 @@ impl<Oracle: PropagatingSolver<Engine>> Solver<Oracle> {
 		};
 
 		let (engine, result) = self.oracle.solve_assuming(assumptions);
+		let get_int_val = |engine: &Engine, iv: IntVarRef| {
+			let var_def = &engine.state.int_vars[iv];
+			let val = var_def.get_lower_bound(&engine.state.trail);
+			debug_assert!(
+				matches!(var_def.order_encoding, OrderStorage::Lazy(_))
+					|| val == var_def.get_upper_bound(&engine.state.trail)
+			);
+			val
+		};
 		match result {
 			SatSolveResult::Satisfied(sol) => {
 				let wrapper: &dyn Valuation = &|x| match x {
@@ -429,15 +438,12 @@ impl<Oracle: PropagatingSolver<Engine>> Solver<Oracle> {
 						BoolViewInner::Const(b) => b,
 					}),
 					SolverView::Int(var) => Value::Int(match var.0 {
-						IntViewInner::VarRef(iv) => engine.state.int_vars[iv].get_value(&sol),
+						IntViewInner::VarRef(iv) => get_int_val(engine, iv),
 						IntViewInner::Const(i) => i,
 						IntViewInner::Linear {
 							transformer: transform,
 							var,
-						} => {
-							let val = engine.state.int_vars[var].get_value(&sol);
-							transform.transform(val)
-						}
+						} => transform.transform(get_int_val(engine, var)),
 						IntViewInner::Bool { transformer, lit } => {
 							transformer.transform(sol.value(lit) as IntVal)
 						}

crates/huub/src/solver/engine.rs

@@ -277,11 +277,11 @@ impl PropagatorExtension for Engine {
 		clause
 	}
 
-	#[tracing::instrument(level = "debug", skip(self, slv, model))]
+	#[tracing::instrument(level = "debug", skip(self, slv, _sol))]
 	fn check_solution(
 		&mut self,
 		slv: &mut dyn SolvingActions,
-		model: &dyn pindakaas::Valuation,
+		_sol: &dyn pindakaas::Valuation,
 	) -> bool {
 		debug_assert!(self.state.conflict.is_none());
 		// If there is a known conflict, return false
@@ -309,7 +309,6 @@ impl PropagatorExtension for Engine {
 					ctx.state.int_vars[r].order_encoding,
 					OrderStorage::Lazy(_)
 				));
-				debug_assert_eq!(lb, ctx.state.int_vars[r].get_value(model));
 
 				// Ensure the lazy literal for the upper bound exists
 				let ub_lit = ctx.get_intref_lit(r, LitMeaning::Less(lb + 1));

crates/huub/src/solver/engine/int_var.rs

@@ -8,10 +8,7 @@ use std::{
 };
 
 use itertools::Itertools;
-use pindakaas::{
-	solver::propagation::PropagatingSolver, Lit as RawLit, Valuation as SatValuation,
-	Var as RawVar, VarRange,
-};
+use pindakaas::{solver::propagation::PropagatingSolver, Lit as RawLit, Var as RawVar, VarRange};
 use rangelist::RangeList;
 
 use crate::{
@@ -374,38 +371,6 @@ impl IntVar {
 		}
 	}
 
-	pub(crate) fn get_value<V: SatValuation + ?Sized>(&self, model: &V) -> IntVal {
-		match &self.order_encoding {
-			OrderStorage::Eager { storage, .. } => {
-				let mut val_iter = self.domain.clone().into_iter().flatten();
-				for l in storage.clone() {
-					match model.value(l.into()) {
-						false => return val_iter.next().unwrap(),
-						true => {
-							let _ = val_iter.next();
-						}
-					}
-				}
-				*self.domain.upper_bound().unwrap()
-			}
-			OrderStorage::Lazy(storage) => {
-				let mut last_val = *self.domain.lower_bound().unwrap();
-				if storage.storage.is_empty() {
-					return last_val;
-				}
-				let mut i = storage.min_index as usize;
-				while model.value(storage.storage[i].var.into()) {
-					last_val = storage.storage[i].val;
-					if !storage.storage[i].has_next {
-						break;
-					}
-					i = storage.storage[i].next as usize;
-				}
-				last_val
-			}
-		}
-	}
-
 	/// Returns the boolean view associated with `< v` if it exists or weaker version otherwise.
 	///
 	/// ## Warning