Further restructuring of the modelling layer

crates/fzn-huub/src/lib.rs

@@ -39,8 +39,11 @@ use std::{
 
 use flatzinc_serde::{FlatZinc, Literal, Method};
 use huub::{
-	FlatZincError, FlatZincStatistics, Goal, InitConfig, LitMeaning, ReformulationError,
-	SlvTermSignal, SolveResult, Solver, SolverView, Valuation, Value,
+	actions::DecisionActions,
+	flatzinc::{FlatZincError, FlatZincStatistics},
+	reformulate::{InitConfig, ReformulationError},
+	solver::{Goal, IntLitMeaning, SolveResult, Solver, Valuation, Value, View},
+	SlvTermSignal,
 };
 use pico_args::Arguments;
 use tracing::{subscriber::set_default, warn};
@@ -116,7 +119,7 @@ struct Solution<'a> {
 	/// Mapping from solver views to solution values
 	value: &'a dyn Valuation,
 	/// Mapping from FlatZinc identifiers to solver views
-	var_map: &'a UstrMap<SolverView>,
+	var_map: &'a UstrMap<View>,
 }
 
 /// Parse time duration for the time limit flag
@@ -188,21 +191,18 @@ where
 		})?;
 
 		// Convert FlatZinc model to internal Solver representation
-		let res = Solver::from_fzn(&fzn, &self.init_config());
+		let res = Solver::from_fzn::<Ustr, UstrMap<View>>(&fzn, &self.init_config());
 		// Resolve any errors that may have occurred during the conversion
-		let (mut slv, var_map, fzn_stats): (Solver, UstrMap<SolverView>, FlatZincStatistics) =
-			match res {
-				Err(FlatZincError::ReformulationError(
-					ReformulationError::TrivialUnsatisfiable,
-				)) => {
-					outputln!(self.stdout, "{}", FZN_UNSATISFIABLE);
-					return Ok(());
-				}
-				Err(err) => {
-					return Err(err.to_string());
-				}
-				Ok((slv, var_map, fzn_stats)) => (slv, var_map.into_iter().collect(), fzn_stats),
-			};
+		let (mut slv, var_map, fzn_stats): (Solver, UstrMap<View>, FlatZincStatistics) = match res {
+			Err(FlatZincError::ReformulationError(ReformulationError::TrivialUnsatisfiable)) => {
+				outputln!(self.stdout, "{}", FZN_UNSATISFIABLE);
+				return Ok(());
+			}
+			Err(err) => {
+				return Err(err.to_string());
+			}
+			Ok(x) => x,
+		};
 
 		if self.statistics {
 			let stats = slv.init_statistics();
@@ -228,13 +228,13 @@ where
 			let mut int_map = vec![ustr(""); slv.init_statistics().int_vars()];
 			for (name, v) in var_map.iter() {
 				match v {
-					SolverView::Bool(bv) => {
+					View::Bool(bv) => {
 						if let Some(info) = bv.reverse_map_info() {
 							let _ = lit_map.insert(info, LitName::BoolVar(*name, true));
 							let _ = lit_map.insert(-info, LitName::BoolVar(*name, false));
 						}
 					}
-					SolverView::Int(iv) => {
+					View::Int(iv) => {
 						let (pos, is_view) = iv.int_reverse_map_info();
 						if let Some(i) = pos {
 							if !is_view || int_map[i].is_empty() {
@@ -253,10 +253,10 @@ where
 							for (lit, meaning) in iv.lit_reverse_map_info(&slv) {
 								let _ = lit_map.entry(lit).or_insert_with(|| {
 									let (op, val) = match meaning {
-										LitMeaning::Eq(v) => ("=", v),
-										LitMeaning::NotEq(v) => ("!=", v),
-										LitMeaning::GreaterEq(v) => (">=", v),
-										LitMeaning::Less(v) => ("<", v),
+										IntLitMeaning::Eq(v) => ("=", v),
+										IntLitMeaning::NotEq(v) => ("!=", v),
+										IntLitMeaning::GreaterEq(v) => (">=", v),
+										IntLitMeaning::Less(v) => ("<", v),
 									};
 									LitName::BoolVar(format!("{name}{op}{val}").into(), true)
 								});
@@ -289,7 +289,7 @@ where
 					} else {
 						Goal::Maximize
 					},
-					if let SolverView::Int(iv) = var_map[ident] {
+					if let View::Int(iv) = var_map[ident] {
 						iv
 					} else {
 						todo!()
@@ -421,7 +421,7 @@ where
 					let Some(obj_val) = obj_val else {
 						unreachable!()
 					};
-					let obj_lit = slv.get_int_lit(obj, LitMeaning::Eq(obj_val));
+					let obj_lit = slv.get_int_lit(obj, IntLitMeaning::Eq(obj_val));
 					slv.add_clause([obj_lit]).unwrap();
 					// Ensure all following solutions are different from the first optimal
 					// solution

crates/fzn-huub/src/trace.rs

@@ -8,7 +8,7 @@ use std::{
 	sync::{Arc, Mutex},
 };
 
-use huub::{IntVal, LitMeaning};
+use huub::{solver::IntLitMeaning, IntVal};
 use tracing::{
 	field::{Field, Visit},
 	Event, Level, Subscriber,
@@ -55,7 +55,7 @@ pub(crate) enum LitName {
 	/// The tuple contains the index of the variable in the FlatZinc model (which
 	/// is used as the key in [`FmtLitFields::int_reverse_map`]), and
 	/// [`LitMeaning`] of the literal.
-	IntLit(usize, LitMeaning),
+	IntLit(usize, IntLitMeaning),
 }
 
 /// A visitor wrapper that ensures any fields containing literals are renamed
@@ -171,10 +171,10 @@ impl LitName {
 					&format!("int_var[{var}]")
 				};
 				match meaning {
-					LitMeaning::Eq(val) => format!("{var}={val}"),
-					LitMeaning::NotEq(val) => format!("{var}≠{val}"),
-					LitMeaning::GreaterEq(val) => format!("{var}≥{val}"),
-					LitMeaning::Less(val) => format!("{var}<{val}"),
+					IntLitMeaning::Eq(val) => format!("{var}={val}"),
+					IntLitMeaning::NotEq(val) => format!("{var}≠{val}"),
+					IntLitMeaning::GreaterEq(val) => format!("{var}≥{val}"),
+					IntLitMeaning::Less(val) => format!("{var}<{val}"),
 				}
 			}
 		}
@@ -342,9 +342,9 @@ impl RecordLazyLits {
 			self.lit,
 		) {
 			let meaning = if is_eq {
-				LitMeaning::Eq
+				IntLitMeaning::Eq
 			} else {
-				LitMeaning::Less
+				IntLitMeaning::Less
 			}(val);
 			let mut guard = lit_reverse_map.lock().unwrap();
 			let _ = guard.insert(lit, LitName::IntLit(iv, meaning.clone()));

crates/huub/src/actions.rs

@@ -8,23 +8,19 @@ use pindakaas::{AsDynClauseDatabase, ClauseDatabase};
 use crate::{
 	branchers::BoxedBrancher,
 	constraints::{BoxedPropagator, Conflict, LazyReason, ReasonBuilder},
-	model::{self, int::IntExpr},
+	reformulate::ReformulationError,
 	solver::{
-		activation_list::IntPropCond,
-		engine::PropRef,
-		int_var::IntVarRef,
-		queue::PriorityLevel,
-		trail::TrailedInt,
-		view::{BoolView, BoolViewInner, IntViewInner},
+		activation_list::IntPropCond, engine::PropRef, int_var::IntVarRef, queue::PriorityLevel,
+		trail::TrailedInt, BoolView, BoolViewInner, IntLitMeaning, IntView, IntViewInner, View,
 	},
-	IntSetVal, IntVal, IntView, LitMeaning, Model, ReformulationError, SolverView,
+	BoolDecision, IntDecision, IntSetVal, IntVal, Model,
 };
 
 /// Actions that can be performed during the initialization of branchers.
 pub trait BrancherInitActions: DecisionActions {
 	/// Ensure that any relevant decision variable are marked internally as a
 	/// decidable variable.
-	fn ensure_decidable(&mut self, view: SolverView);
+	fn ensure_decidable(&mut self, view: View);
 
 	/// Create a new trailed integer value with the given initial value.
 	fn new_trailed_int(&mut self, init: IntVal) -> TrailedInt;
@@ -39,18 +35,18 @@ pub trait BrancherInitActions: DecisionActions {
 pub trait ConstraintInitActions {
 	/// Schedule the simplify method of the calling constraint when the given
 	/// boolean expression changes.
-	fn simplify_on_change_bool(&mut self, var: model::bool::BoolView);
+	fn simplify_on_change_bool(&mut self, var: BoolDecision);
 
 	/// Schedule the simplify method of the calling constraint when the given
 	/// integer expression changes.
-	fn simplify_on_change_int(&mut self, var: IntExpr);
+	fn simplify_on_change_int(&mut self, var: IntDecision);
 }
 
 /// Actions that can be performed by a [`crate::branchers::Brancher`] when
 /// making search decisions.
 pub trait DecisionActions: InspectionActions {
 	/// Get (or create) a literal for the given integer view with the given meaning.
-	fn get_int_lit(&mut self, var: IntView, mut meaning: LitMeaning) -> BoolView {
+	fn get_int_lit(&mut self, var: IntView, mut meaning: IntLitMeaning) -> BoolView {
 		{
 			if let IntViewInner::Linear { transformer, .. }
 			| IntViewInner::Bool { transformer, .. } = var.0
@@ -66,25 +62,25 @@ pub trait DecisionActions: InspectionActions {
 					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,
+					IntLitMeaning::Eq(i) => c == i,
+					IntLitMeaning::NotEq(i) => c != i,
+					IntLitMeaning::GreaterEq(i) => c >= i,
+					IntLitMeaning::Less(i) => c < i,
 				})),
 				IntViewInner::Bool { lit, .. } => {
 					let (meaning, negated) =
-						if matches!(meaning, LitMeaning::NotEq(_) | LitMeaning::Less(_)) {
+						if matches!(meaning, IntLitMeaning::NotEq(_) | IntLitMeaning::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),
+						IntLitMeaning::Eq(0) => BoolViewInner::Lit(!lit),
+						IntLitMeaning::Eq(1) => BoolViewInner::Lit(lit),
+						IntLitMeaning::Eq(_) => BoolViewInner::Const(false),
+						IntLitMeaning::GreaterEq(1) => BoolViewInner::Lit(lit),
+						IntLitMeaning::GreaterEq(i) if i > 1 => BoolViewInner::Const(false),
+						IntLitMeaning::GreaterEq(_) => BoolViewInner::Const(true),
 						_ => unreachable!(),
 					});
 					if negated {
@@ -98,7 +94,7 @@ pub trait DecisionActions: InspectionActions {
 	}
 
 	/// Get (or create) a literal for the given referenced integer variable with the given meaning.
-	fn get_intref_lit(&mut self, var: IntVarRef, meaning: LitMeaning) -> BoolView;
+	fn get_intref_lit(&mut self, var: IntVarRef, meaning: IntLitMeaning) -> BoolView;
 
 	/// Returns the number of conflicts up to this point in the search process.
 	fn get_num_conflicts(&self) -> u64;
@@ -109,12 +105,16 @@ pub trait DecisionActions: InspectionActions {
 pub trait ExplanationActions: InspectionActions {
 	/// Get a Boolean view that represents the given meaning (that is currently
 	/// `true`) on the integer view, if it already exists.
-	fn try_int_lit(&self, var: IntView, meaning: LitMeaning) -> Option<BoolView>;
+	fn try_int_lit(&self, var: IntView, meaning: IntLitMeaning) -> Option<BoolView>;
 
 	/// Get a Boolean view that represents the given meaning (that is currently
 	/// `true`) on the integer view, or a relaxation if the literal does not yet
 	/// exist.
-	fn get_int_lit_relaxed(&mut self, var: IntView, meaning: LitMeaning) -> (BoolView, LitMeaning);
+	fn get_int_lit_relaxed(
+		&mut self,
+		var: IntView,
+		meaning: IntLitMeaning,
+	) -> (BoolView, IntLitMeaning);
 
 	/// Get the Boolean view that represents the current assignment of the integer
 	/// view, or `None` if the integer view is not assigned.
@@ -235,11 +235,11 @@ pub trait PropagatorInitActions: AsDynClauseDatabase + ClauseDatabase + Decision
 pub trait ReformulationActions: PropagatorInitActions {
 	/// Lookup the solver [`BoolView`] to which the given model
 	/// [`model::bool::BoolView`] maps.
-	fn get_solver_bool(&mut self, bv: model::bool::BoolView) -> BoolView;
+	fn get_solver_bool(&mut self, bv: BoolDecision) -> BoolView;
 
 	/// Lookup the solver [`IntExpr`] to which the given model
 	/// [`model::int::IntView`] maps.
-	fn get_solver_int(&mut self, iv: IntExpr) -> IntView;
+	fn get_solver_int(&mut self, iv: IntDecision) -> IntView;
 
 	/// Create a new Boolean decision variable to use in the encoding.
 	fn new_bool_var(&mut self) -> BoolView;
@@ -254,25 +254,25 @@ pub trait SimplificationActions {
 		Model: AddAssign<C>;
 
 	/// Check whether a given integer view can take a given value.
-	fn check_int_in_domain(&self, var: IntExpr, val: IntVal) -> bool;
+	fn check_int_in_domain(&self, var: IntDecision, val: IntVal) -> bool;
 
 	/// Get the current value of a [`BoolView`], if it has been assigned.
-	fn get_bool_val(&self, bv: model::bool::BoolView) -> Option<bool>;
+	fn get_bool_val(&self, bv: BoolDecision) -> Option<bool>;
 
 	/// Get the minimum value that an integer view is guaranteed to take.
-	fn get_int_lower_bound(&self, var: IntExpr) -> IntVal;
+	fn get_int_lower_bound(&self, var: IntDecision) -> IntVal;
 
 	/// Get the maximum value that an integer view is guaranteed to take.
-	fn get_int_upper_bound(&self, var: IntExpr) -> IntVal;
+	fn get_int_upper_bound(&self, var: IntDecision) -> IntVal;
 
 	/// Convenience method to get both the lower and upper bounds of an integer
 	/// view.
-	fn get_int_bounds(&self, var: IntExpr) -> (IntVal, IntVal) {
+	fn get_int_bounds(&self, var: IntDecision) -> (IntVal, IntVal) {
 		(self.get_int_lower_bound(var), self.get_int_upper_bound(var))
 	}
 
 	/// Get the current value of an integer view, if it has been assigned.
-	fn get_int_val(&self, var: IntExpr) -> Option<IntVal> {
+	fn get_int_val(&self, var: IntDecision) -> Option<IntVal> {
 		let (lb, ub) = self.get_int_bounds(var);
 		if lb == ub {
 			Some(lb)
@@ -285,35 +285,43 @@ pub trait SimplificationActions {
 	///
 	/// Note that it is possible to enforce that a boolean view is `false` by
 	/// negating the view, i.e. `!bv`.
-	fn set_bool(&mut self, bv: model::bool::BoolView) -> Result<(), ReformulationError>;
+	fn set_bool(&mut self, bv: BoolDecision) -> Result<(), ReformulationError>;
 
 	/// Enforce that the given integer expression takes a value in in the given
 	/// set.
 	fn set_int_in_set(
 		&mut self,
-		var: IntExpr,
+		var: IntDecision,
 		values: &IntSetVal,
 	) -> Result<(), ReformulationError>;
 
 	/// Enforce that a an integer view takes a value that is greater or equal to
 	/// `val`.
-	fn set_int_lower_bound(&mut self, var: IntExpr, val: IntVal) -> Result<(), ReformulationError>;
+	fn set_int_lower_bound(
+		&mut self,
+		var: IntDecision,
+		val: IntVal,
+	) -> Result<(), ReformulationError>;
 
 	/// Enforce that a an integer view takes a value that is less or equal to
 	/// `val`.
-	fn set_int_upper_bound(&mut self, var: IntExpr, val: IntVal) -> Result<(), ReformulationError>;
+	fn set_int_upper_bound(
+		&mut self,
+		var: IntDecision,
+		val: IntVal,
+	) -> Result<(), ReformulationError>;
 
 	/// Enforce that a an integer view takes a value `val`.
-	fn set_int_val(&mut self, var: IntExpr, val: IntVal) -> Result<(), ReformulationError>;
+	fn set_int_val(&mut self, var: IntDecision, val: IntVal) -> Result<(), ReformulationError>;
 
 	/// Enforce that a an integer view cannot take a value `val`.
-	fn set_int_not_eq(&mut self, var: IntExpr, val: IntVal) -> Result<(), ReformulationError>;
+	fn set_int_not_eq(&mut self, var: IntDecision, val: IntVal) -> Result<(), ReformulationError>;
 
 	/// Enforce that a given integer expression cannot take any of the values in
 	/// the given set.
 	fn set_int_not_in_set(
 		&mut self,
-		var: IntExpr,
+		var: IntDecision,
 		values: &IntSetVal,
 	) -> Result<(), ReformulationError>;
 }