Add Variable Views visible in FlatZinc

crates/fzn-huub/Cargo.toml

@@ -12,7 +12,7 @@ keywords.workspace = true
 [dependencies]
 clap = { version = "4.4.18", features = ["derive"] }
 ctrlc = "3.4.4"
-flatzinc-serde = "0.2"
+flatzinc-serde = "0.3"
 humantime = "2.1.0"
 huub = { path = "../huub" }
 miette = { version = "7.2.0", features = ["fancy"] }

crates/fzn-huub/src/tracing.rs

@@ -150,6 +150,26 @@
 		}
 		false
 	}
+
+	#[inline]
+	fn check_int_vars(&mut self, field: &Field, value: &dyn fmt::Debug) -> bool {
+		if matches!(field.name(), "int_vars") {
+			let res: Result<Vec<usize>, _> = serde_json::from_str(&format!("{:?}", value));
+			if let Ok(vars) = res {
+				let mut v: Vec<String> = Vec::with_capacity(vars.len());
+				for i in vars {
+					if let Some(name) = self.int_reverse_map.get(i) {
+						v.push(name.to_string());
+					} else {
+						v.push(format!("IntVar({})", i));
+					}
+				}
+				self.inner.record_str(field, &v.join(", "));
+				return true;
+			}
+		}
+		false
+	}
 }
 
 impl<'a, V: Visit> Visit for LitNames<'a, V> {
@@ -188,6 +208,9 @@
 		if self.check_clause(field, value) {
 			return;
 		}
+		if self.check_int_vars(field, value) {
+			return;
+		}
 		self.inner.record_debug(field, value)
 	}
 }

crates/huub/Cargo.toml

@@ -11,7 +11,7 @@ keywords.workspace = true
 
 [dependencies]
 delegate = "0.12"
-flatzinc-serde = "0.2"
+flatzinc-serde = "0.3"
 index_vec = "0.1.3"
 itertools = "0.12.1"
 pindakaas = { git = "https://github.com/pindakaashq/pindakaas.git", features = [

crates/huub/src/helpers.rs

@@ -0,0 +1 @@
+pub(crate) mod linear_transform;

crates/huub/src/helpers/linear_transform.rs

@@ -0,0 +1,126 @@
+use std::ops::{Add, Mul, Neg};
+
+use crate::{IntVal, LitMeaning, NonZeroIntVal};
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
+pub struct LinearTransform {
+	pub(crate) scale: NonZeroIntVal,
+	pub(crate) offset: IntVal,
+}
+
+impl LinearTransform {
+	/// Creates a new linear transformation with the given scale and offset.
+	pub fn new(scale: NonZeroIntVal, offset: IntVal) -> Self {
+		Self { scale, offset }
+	}
+	/// Creates a new linear transformation with the given scale and no offset.
+	pub fn scaled(scale: NonZeroIntVal) -> Self {
+		Self { scale, offset: 0 }
+	}
+	/// Creates a new linear transformation with the given offset and no scale.
+	pub fn offset(offset: IntVal) -> Self {
+		Self {
+			scale: NonZeroIntVal::new(1).unwrap(),
+			offset,
+		}
+	}
+
+	pub(crate) fn positive_scale(&self) -> bool {
+		self.scale.get() > 0
+	}
+
+	/// Perform the linear transformation on a value.
+	pub fn transform(&self, val: IntVal) -> IntVal {
+		(val * self.scale.get()) + self.offset
+	}
+
+	/// Perform the reverse linear transformation on a value.
+	pub fn rev_transform(&self, val: IntVal) -> IntVal {
+		(val - self.offset) / self.scale.get()
+	}
+
+	/// Returns whether a value remains an integer after reversing the transformation.
+	pub fn rev_remains_integer(&self, val: IntVal) -> bool {
+		(val - self.offset) % self.scale.get() == 0
+	}
+
+	/// Perform the reverse linear tranformation for a LitMeanning request.
+	///
+	/// Note that this performs the correct rounding to maintain the meaning of the literal. When
+	/// equality literals are requested, None is returned when no such integer value exists.
+	pub fn rev_transform_lit(&self, mut lit: LitMeaning) -> Option<LitMeaning> {
+		let mut transformer = *self;
+		if !self.positive_scale() {
+			// Make positive by doing `*-1` on lit meaning and transformer
+			(lit, transformer) = match lit {
+				// -x >= i === x <= -i === x < -i + 1
+				LitMeaning::GreaterEq(i) => (LitMeaning::Less(-i + 1), -transformer),
+				// -x < i === x > -i === x >= -i + 1
+				LitMeaning::Less(i) => (LitMeaning::GreaterEq(-i + 1), -transformer),
+				_ => (lit, transformer),
+			};
+		}
+
+		match lit {
+			LitMeaning::Eq(i) => {
+				if transformer.rev_remains_integer(i) {
+					Some(LitMeaning::Eq(transformer.rev_transform(i)))
+				} else {
+					None
+				}
+			}
+			LitMeaning::NotEq(i) => {
+				if transformer.rev_remains_integer(i) {
+					Some(LitMeaning::NotEq(transformer.rev_transform(i)))
+				} else {
+					None
+				}
+			}
+			LitMeaning::GreaterEq(i) => Some(LitMeaning::GreaterEq(div_ceil(
+				i - transformer.offset,
+				transformer.scale,
+			))),
+			LitMeaning::Less(i) => Some(LitMeaning::Less(div_ceil(
+				i - transformer.offset,
+				transformer.scale,
+			))),
+		}
+	}
+}
+
+#[inline]
+fn div_ceil(a: IntVal, b: NonZeroIntVal) -> IntVal {
+	a / b.get() + (0 != a % b.get()) as IntVal
+}
+
+impl Neg for LinearTransform {
+	type Output = Self;
+	fn neg(self) -> Self::Output {
+		Self {
+			scale: NonZeroIntVal::new(-self.scale.get()).unwrap(),
+			offset: -self.offset,
+		}
+	}
+}
+
+impl Add<IntVal> for LinearTransform {
+	type Output = Self;
+
+	fn add(self, rhs: IntVal) -> Self::Output {
+		LinearTransform {
+			scale: self.scale,
+			offset: self.offset + rhs,
+		}
+	}
+}
+
+impl Mul<NonZeroIntVal> for LinearTransform {
+	type Output = Self;
+
+	fn mul(self, rhs: NonZeroIntVal) -> Self::Output {
+		LinearTransform {
+			scale: NonZeroIntVal::new(self.scale.get() * rhs.get()).unwrap(),
+			offset: self.offset * rhs.get(),
+		}
+	}
+}

crates/huub/src/lib.rs

@@ -1,12 +1,14 @@
+pub(crate) mod helpers;
 pub(crate) mod model;
 pub(crate) mod propagator;
 pub(crate) mod solver;
 #[cfg(test)]
 pub(crate) mod tests;
 
+pub use helpers::linear_transform::LinearTransform;
 pub use model::{
-	bool::BoolExpr, constraint::Constraint, flatzinc::FlatZincError, int::IntExpr,
-	reformulate::ReformulationError, Model, Variable,
+	bool::BoolExpr, constraint::Constraint, flatzinc::FlatZincError,
+	reformulate::ReformulationError, Model,
 };
 pub use pindakaas::solver::SlvTermSignal;
 use pindakaas::Lit as RawLit;

crates/huub/src/model.rs

@@ -14,13 +14,13 @@
 };
 
 use self::{
-	bool::{BoolExpr, BoolVar},
-	int::{IntExpr, IntVar},
+	bool::{BoolExpr, BoolView},
+	int::{IntVar, IntView},
 	reformulate::{ReformulationError, VariableMap},
 };
 use crate::{
 	model::int::IntVarDef,
-	solver::{engine::int_var::IntVar as SlvIntVar, view::SolverView, SatSolver},
+	solver::{engine::int_var::IntVar as SlvIntVar, SatSolver},
 	Constraint, Solver,
 };
 
@@ -34,18 +34,22 @@
 }
 
 impl Model {
-	pub fn new_bool_var(&mut self) -> BoolVar {
-		BoolVar(self.cnf.new_var())
+	pub fn new_bool_var(&mut self) -> BoolView {
+		BoolView::Lit(self.cnf.new_var().into())
 	}
 
-	pub fn new_bool_vars(&mut self, len: usize) -> Vec<BoolVar> {
-		self.cnf.next_var_range(len).unwrap().map(BoolVar).collect()
+	pub fn new_bool_vars(&mut self, len: usize) -> Vec<BoolView> {
+		self.cnf
+			.next_var_range(len)
+			.unwrap()
+			.map(|v| BoolView::Lit(v.into()))
+			.collect()
 	}
 
-	pub fn new_int_var(&mut self, domain: RangeList<i64>) -> IntVar {
+	pub fn new_int_var(&mut self, domain: RangeList<i64>) -> IntView {
 		let iv = IntVar(self.int_vars.len() as u32);
 		self.int_vars.push(IntVarDef::with_domain(domain));
-		iv
+		IntView::Var(iv)
 	}
 
 	pub fn new_int_vars(&mut self, len: usize, domain: RangeList<i64>) -> Vec<IntVar> {
@@ -78,7 +82,7 @@
 		for i in 0..self.int_vars.len() {
 			let var = &self.int_vars[i];
 			let view = SlvIntVar::new_in(&mut slv, var.domain.clone(), true); // TODO!
-			map.insert(Variable::Int(IntVar(i as u32)), SolverView::Int(view));
+			map.insert_int(IntVar(i as u32), view);
 		}
 
 		// Create constraint data structures within the solve
@@ -126,13 +130,18 @@
 	}
 }
 
-#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
-pub enum Variable {
-	Bool(BoolVar),
-	Int(IntVar),
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub enum ModelView {
+	Bool(BoolView),
+	Int(IntView),
 }
-impl From<BoolVar> for Variable {
-	fn from(value: BoolVar) -> Self {
+impl From<IntView> for ModelView {
+	fn from(value: IntView) -> Self {
+		Self::Int(value)
+	}
+}
+impl From<BoolView> for ModelView {
+	fn from(value: BoolView) -> Self {
 		Self::Bool(value)
 	}
 }