diff --git a/crates/huub/src/model.rs b/crates/huub/src/model.rs index c0a26a67..5204af2c 100644 --- a/crates/huub/src/model.rs +++ b/crates/huub/src/model.rs @@ -6,6 +6,7 @@ mod reformulate; use std::ops::AddAssign; use flatzinc_serde::RangeList; +use itertools::Itertools; use pindakaas::{ solver::{PropagatorAccess, Solver as SolverTrait}, ClauseDatabase, Cnf, Lit as RawLit, Valuation as SatValuation, Var as RawVar, @@ -18,13 +19,13 @@ use self::{ }; use crate::{ model::{int::IntVarDef, reformulate::ReifContext}, - propagator::{all_different::AllDifferentValue, linear::LinearLE}, + propagator::{all_different::AllDifferentValue, int_lin_le::LinearLE}, solver::{ engine::int_var::IntVar as SlvIntVar, view::{BoolViewInner, SolverView}, SatSolver, }, - Solver, + IntVal, Solver, }; #[derive(Debug, Default)] @@ -96,7 +97,8 @@ impl ClauseDatabase for Model { pub enum Constraint { Clause(Vec), AllDifferent(Vec), - LinearLE(Vec, Vec, i64), + IntLinLessEq(Vec, Vec, IntVal), + IntLinEq(Vec, Vec, IntVal), } impl Constraint { @@ -130,12 +132,37 @@ impl Constraint { .collect(); slv.add_propagator(AllDifferentValue::new(vars)); } - Constraint::LinearLE(coeffs, vars, c) => { + Constraint::IntLinLessEq(coeffs, vars, c) => { + let vars: Vec<_> = vars + .iter() + .zip_eq(coeffs.iter()) + .map(|(v, &c)| { + v.to_arg( + if c >= 0 { + ReifContext::Pos + } else { + ReifContext::Neg + }, + slv, + map, + ) + }) + .collect(); + slv.add_propagator(LinearLE::new(coeffs, vars, *c)); + } + Constraint::IntLinEq(coeffs, vars, c) => { let vars: Vec<_> = vars .iter() .map(|v| v.to_arg(ReifContext::Mixed, slv, map)) .collect(); - slv.add_propagator(LinearLE::new(coeffs, vars, c)); + // coeffs * vars <= c + slv.add_propagator(LinearLE::new(coeffs, vars.clone(), *c)); + // coeffs * vars >= c <=> -coeffs * vars <= -c + slv.add_propagator(LinearLE::new( + &coeffs.iter().map(|c| -c).collect_vec(), + vars, + -c, + )) } } } diff --git a/crates/huub/src/model/flatzinc.rs b/crates/huub/src/model/flatzinc.rs index e5ccbed1..810a51dd 100644 --- a/crates/huub/src/model/flatzinc.rs +++ b/crates/huub/src/model/flatzinc.rs @@ -60,7 +60,8 @@ impl Model { }); } } - "int_linear_le" => { + "int_lin_le" | "int_lin_eq" => { + let is_eq = c.id.deref() == "int_lin_eq"; if let [coeffs, vars, rhs] = c.args.as_slice() { let coeffs = arg_array(fzn, coeffs)?; let vars = arg_array(fzn, vars)?; @@ -84,10 +85,14 @@ impl Model { .iter() .map(|l| lit_int(fzn, &mut prb, &mut map, l)) .collect(); - prb += Constraint::LinearLE(coeffs?, vars?, *rhs); + prb += if is_eq { + Constraint::IntLinEq + } else { + Constraint::IntLinLessEq + }(coeffs?, vars?, *rhs); } else { return Err(FlatZincError::InvalidNumArgs { - name: "int_linear_le", + name: if is_eq { "int_lin_eq" } else { "int_linear_le" }, found: c.args.len(), expected: 3, }); diff --git a/crates/huub/src/model/int.rs b/crates/huub/src/model/int.rs index 8806ab0d..b4431719 100644 --- a/crates/huub/src/model/int.rs +++ b/crates/huub/src/model/int.rs @@ -10,13 +10,13 @@ use crate::{ view::{IntView, IntViewInner, SolverView}, SatSolver, }, - Solver, Variable, + IntVal, Solver, Variable, }; #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub enum IntExpr { Var(IntVar), - Val(i64), + Val(IntVal), } impl IntExpr { @@ -47,5 +47,5 @@ pub struct IntVar(pub(crate) u32); #[derive(Debug)] pub(crate) struct IntVarDef { - pub(crate) domain: RangeList, + pub(crate) domain: RangeList, } diff --git a/crates/huub/src/propagator.rs b/crates/huub/src/propagator.rs index 11af8d91..02f163e4 100644 --- a/crates/huub/src/propagator.rs +++ b/crates/huub/src/propagator.rs @@ -1,7 +1,7 @@ pub(crate) mod all_different; pub(crate) mod conflict; pub(crate) mod int_event; -pub(crate) mod linear; +pub(crate) mod int_lin_le; pub(crate) mod reason; use std::fmt::Debug; diff --git a/crates/huub/src/propagator/linear.rs b/crates/huub/src/propagator/int_lin_le.rs similarity index 93% rename from crates/huub/src/propagator/linear.rs rename to crates/huub/src/propagator/int_lin_le.rs index 6c59b3f5..7e212cc0 100644 --- a/crates/huub/src/propagator/linear.rs +++ b/crates/huub/src/propagator/int_lin_le.rs @@ -14,7 +14,7 @@ use crate::{ #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub(crate) struct LinearLE { vars: Vec, // Variables in the linear inequality - rhs: i64, // Lower bound of the linear inequality + rhs: IntVal, // Lower bound of the linear inequality action_list: Vec, // List of variables that have been modified since the last propagation } @@ -22,10 +22,9 @@ impl LinearLE { pub(crate) fn new, VI: IntoIterator>( coeffs: &[IntVal], vars: VI, - rhs: &IntVal, + mut max_sum: IntVal, ) -> Self { let vars: Vec = vars.into_iter().map(Into::into).collect(); - let mut max_sum = *rhs; let scaled_vars: Vec = vars.iter() .enumerate() @@ -127,7 +126,7 @@ mod tests { Cnf, }; - use crate::{propagator::linear::LinearLE, solver::engine::int_var::IntVar, Solver, Value}; + use crate::{propagator::int_lin_le::LinearLE, solver::engine::int_var::IntVar, Solver, Value}; #[test] fn test_linear_le_sat() { @@ -136,7 +135,7 @@ mod tests { let b = IntVar::new_in(&mut slv, RangeList::from_iter([1..=2]), true); let c = IntVar::new_in(&mut slv, RangeList::from_iter([1..=2]), true); - slv.add_propagator(LinearLE::new(&[2, 1, 1], vec![a, b, c], &10)); + slv.add_propagator(LinearLE::new(&[2, 1, 1], vec![a, b, c], 10)); let result = slv.solve(|val| { let Value::Int(a_val) = val(a.into()).unwrap() else { panic!() @@ -159,7 +158,7 @@ mod tests { let b = IntVar::new_in(&mut slv, RangeList::from_iter([1..=4]), true); let c = IntVar::new_in(&mut slv, RangeList::from_iter([1..=4]), true); - slv.add_propagator(LinearLE::new(&[2, 1, 1], vec![a, b, c], &3)); + slv.add_propagator(LinearLE::new(&[2, 1, 1], vec![a, b, c], 3)); assert_eq!(slv.solve(|_| {}), SolveResult::Unsat) } @@ -170,7 +169,7 @@ mod tests { let b = IntVar::new_in(&mut slv, RangeList::from_iter([1..=4]), true); let c = IntVar::new_in(&mut slv, RangeList::from_iter([1..=4]), true); - slv.add_propagator(LinearLE::new(&[-2, -1, -1], vec![a, b, c], &-3)); + slv.add_propagator(LinearLE::new(&[-2, -1, -1], vec![a, b, c], -3)); let result = slv.solve(|val| { let Value::Int(a_val) = val(a.into()).unwrap() else { panic!() @@ -193,7 +192,7 @@ mod tests { let b = IntVar::new_in(&mut slv, RangeList::from_iter([1..=2]), true); let c = IntVar::new_in(&mut slv, RangeList::from_iter([1..=2]), true); - slv.add_propagator(LinearLE::new(&[-2, -1, -1], vec![a, b, c], &-10)); + slv.add_propagator(LinearLE::new(&[-2, -1, -1], vec![a, b, c], -10)); assert_eq!(slv.solve(|_| {}), SolveResult::Unsat) } } diff --git a/crates/huub/src/solver/engine/int_var.rs b/crates/huub/src/solver/engine/int_var.rs index 32caf582..82b12903 100644 --- a/crates/huub/src/solver/engine/int_var.rs +++ b/crates/huub/src/solver/engine/int_var.rs @@ -55,7 +55,7 @@ impl IntVar { Sat: SatSolver + SolverTrait, >( slv: &mut Solver, - domain: RangeList, + domain: RangeList, direct_encoding: bool, ) -> IntView { let orig_domain_len = (&domain) @@ -122,11 +122,11 @@ impl IntVar { let direct_offset = self.orig_domain_len - 1; let meaning = if offset < direct_offset { - LitMeaning::GreaterEq(*self.orig_domain.lower_bound().unwrap() + 1 + offset as i64) + LitMeaning::GreaterEq(*self.orig_domain.lower_bound().unwrap() + 1 + offset as IntVal) } else { debug_assert!(self.has_direct); let offset = offset - direct_offset; - LitMeaning::Eq(*self.orig_domain.lower_bound().unwrap() + 1 + offset as i64) + LitMeaning::Eq(*self.orig_domain.lower_bound().unwrap() + 1 + offset as IntVal) }; if lit.is_negated() { !meaning @@ -211,7 +211,7 @@ impl IntVar { BoolView(BoolViewInner::Lit(if negate { !lit } else { lit })) } - pub(crate) fn get_value(&self, model: &V) -> i64 { + pub(crate) fn get_value(&self, model: &V) -> IntVal { let mut val_iter = self.orig_domain.clone().into_iter().flatten(); for l in self.order_vars() { match model.value(l.into()) { @@ -228,10 +228,10 @@ impl IntVar { #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub enum LitMeaning { - Eq(i64), - NotEq(i64), - GreaterEq(i64), - Less(i64), + Eq(IntVal), + NotEq(IntVal), + GreaterEq(IntVal), + Less(IntVal), } impl Not for LitMeaning {