feat(csp): Implement max/min expressions.

solver/src/model/lang.rs

@@ -6,6 +6,7 @@ pub mod expr;
 mod fixed;
 mod int;
 pub mod linear;
+pub(crate) mod max;
 pub mod reification;
 mod sym;
 mod validity_scope;

solver/src/model/lang/max.rs

@@ -0,0 +1,93 @@
+use crate::core::state::Term;
+use crate::core::{IntCst, SignedVar};
+use crate::model::lang::IAtom;
+use crate::reif::ReifExpr;
+use itertools::Itertools;
+use std::fmt::{Debug, Formatter};
+
+/// Constraint equivalent to `lhs = max { e | e \in rhs }
+pub struct EqMax {
+    lhs: IAtom,
+    rhs: Vec<IAtom>,
+}
+
+/// Constraint equivalent to `lhs = min { e | e \in rhs }
+pub struct EqMin {
+    lhs: IAtom,
+    rhs: Vec<IAtom>,
+}
+
+impl From<EqMax> for ReifExpr {
+    fn from(em: EqMax) -> Self {
+        // (lhs_var + lhs_cst)  =  max_i  {  var_i + cst_i }
+        // (lhs_var)  =  max_i  {  var_i + cst_i  - lhs_cst}
+        let lhs_var = SignedVar::plus(em.lhs.var.variable());
+        let lhs_cst = em.lhs.shift;
+        let rhs = em
+            .rhs
+            .iter()
+            .map(|term| NFEqMaxItem {
+                var: SignedVar::plus(term.var.variable()),
+                cst: term.shift - lhs_cst,
+            })
+            .sorted()
+            .collect_vec();
+
+        ReifExpr::EqMax(NFEqMax { lhs: lhs_var, rhs })
+    }
+}
+
+impl From<EqMin> for ReifExpr {
+    fn from(em: EqMin) -> Self {
+        // (lhs_var + lhs_cst)  =    min_i  {    var_i + cst_i }
+        // (lhs_var + lhs_cst)  =  - max_i  {  - var_i - cst_i }
+        // - lhs_var - lhs_cst  =    max_i  {  - var_i - cst_i }
+        // - lhs_var            =    max_i  {  - var_i - cst_i + lhs_cst}
+        let lhs_var = em.lhs.var.variable();
+        let lhs = SignedVar::minus(lhs_var);
+        let lhs_cst = em.lhs.shift;
+        let rhs = em
+            .rhs
+            .iter()
+            .map(|term| NFEqMaxItem {
+                var: SignedVar::minus(term.var.variable()),
+                cst: -term.shift + lhs_cst,
+            })
+            .sorted()
+            .collect_vec();
+
+        ReifExpr::EqMax(NFEqMax { lhs, rhs })
+    }
+}
+
+#[derive(Eq, PartialEq, Hash, Clone)]
+pub struct NFEqMax {
+    pub lhs: SignedVar,
+    pub rhs: Vec<NFEqMaxItem>,
+}
+
+impl Debug for NFEqMax {
+    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
+        write!(f, "{:?} = max ", self.lhs)?;
+        f.debug_set().entries(self.rhs.iter()).finish()
+    }
+}
+
+#[derive(Eq, PartialEq, Ord, PartialOrd, Hash, Clone)]
+pub struct NFEqMaxItem {
+    pub var: SignedVar,
+    pub cst: IntCst,
+}
+
+#[allow(clippy::comparison_chain)]
+impl Debug for NFEqMaxItem {
+    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
+        write!(f, "{:?}", self.var)?;
+        if self.cst > 0 {
+            write!(f, " + {}", self.cst)?;
+        } else if self.cst < 0 {
+            write!(f, " - {}", -self.cst)?;
+        }
+        Ok(())
+    }
+}

solver/src/reif/mod.rs

@@ -1,8 +1,9 @@
 use crate::core::literals::Disjunction;
 use crate::core::state::{Domains, OptDomain};
-use crate::core::{IntCst, Lit, VarRef};
+use crate::core::{IntCst, Lit, SignedVar, VarRef};
 use crate::model::lang::alternative::NFAlternative;
 use crate::model::lang::linear::NFLinearLeq;
+use crate::model::lang::max::NFEqMax;
 use crate::model::lang::ValidityScope;
 use crate::model::{Label, Model};
 use std::fmt::{Debug, Formatter};
@@ -30,6 +31,7 @@ pub enum ReifExpr {
     And(Vec<Lit>),
     Linear(NFLinearLeq),
     Alternative(NFAlternative),
+    EqMax(NFEqMax),
 }
 
 impl std::fmt::Display for ReifExpr {
@@ -44,7 +46,8 @@ impl std::fmt::Display for ReifExpr {
             ReifExpr::Or(or) => write!(f, "or{or:?}"),
             ReifExpr::And(and) => write!(f, "and{and:?}"),
             ReifExpr::Linear(l) => write!(f, "{l}"),
-            ReifExpr::Alternative(_) => todo!("Missing a way to explicitly opt out of reification"),
+            ReifExpr::EqMax(em) => write!(f, "{em:?}"),
+            ReifExpr::Alternative(alt) => write!(f, "{alt:?}"),
         }
     }
 }
@@ -71,13 +74,14 @@ impl ReifExpr {
             ),
             ReifExpr::Linear(lin) => lin.validity_scope(presence),
             ReifExpr::Alternative(alt) => ValidityScope::new([presence(alt.main)], []),
+            ReifExpr::EqMax(eq_max) => ValidityScope::new([presence(eq_max.lhs.variable())], []),
         }
     }
 
     /// Returns true iff a given expression can be negated.
     pub fn negatable(&self) -> bool {
         match self {
-            ReifExpr::Alternative(_) => false,
+            ReifExpr::Alternative(_) | ReifExpr::EqMax(_) => false,
             _ => true,
         }
     }
@@ -88,6 +92,14 @@ impl ReifExpr {
             OptDomain::Present(lb, ub) if lb == ub => lb,
             _ => panic!(),
         };
+        let sprez = |svar: SignedVar| prez(svar.variable());
+        let svalue = |svar: SignedVar| {
+            if svar.is_plus() {
+                value(svar.variable())
+            } else {
+                -value(svar.variable())
+            }
+        };
         match &self {
             ReifExpr::Lit(l) => {
                 if prez(l.variable()) {
@@ -179,6 +191,19 @@ impl ReifExpr {
                     Some(true)
                 }
             }
+            ReifExpr::EqMax(NFEqMax { lhs, rhs }) => {
+                if sprez(*lhs) {
+                    let left_value = svalue(*lhs);
+                    let right_value = rhs.iter().filter(|e| sprez(e.var)).map(|e| svalue(e.var) + e.cst).max();
+                    if let Some(right_value) = right_value {
+                        Some(left_value == right_value)
+                    } else {
+                        Some(false) // no value in the max while the lhs is present
+                    }
+                } else {
+                    Some(true)
+                }
+            }
         }
     }
 }
@@ -230,6 +255,7 @@ impl Not for ReifExpr {
             }
             ReifExpr::Linear(lin) => ReifExpr::Linear(!lin),
             ReifExpr::Alternative(_) => panic!("Alternative is a constraint and cannot be negated"),
+            ReifExpr::EqMax(_) => panic!("EqMax is a constraint and cannot be negated"),
         }
     }
 }

solver/src/solver/solver_impl.rs

@@ -285,7 +285,10 @@ impl<Lbl: Label> Solver<Lbl> {
             }
             ReifExpr::Alternative(a) => {
                 let prez = |v: VarRef| self.model.state.presence_literal(v);
-                assert!(self.model.entails(value), "Unsupported reified linear constraints.");
+                assert!(
+                    self.model.entails(value),
+                    "Unsupported reified alternative constraints."
+                );
                 assert_eq!(prez(a.main), prez(value.variable()));
 
                 let scope = prez(a.main);
@@ -346,6 +349,63 @@ impl<Lbl: Label> Solver<Lbl> {
                 });
                 Ok(())
             }
+            ReifExpr::EqMax(a) => {
+                let prez = |v: SignedVar| self.model.state.presence(v);
+                assert!(self.model.entails(value), "Unsupported reified eqmax constraints.");
+                assert_eq!(prez(a.lhs), prez(value.variable().into()));
+
+                let scope = prez(a.lhs);
+                let presences = a.rhs.iter().map(|alt| prez(alt.var)).collect_vec();
+                // at least one alternative must be present
+                self.add_clause(&presences, scope)?;
+
+                // POST  forall i    lhs >= rhs[i]   (scope: prez(rhs[i]))
+                for item in &a.rhs {
+                    let item_scope = self.model.state.presence(item.var);
+                    debug_assert!(self.model.state.implies(item_scope, scope));
+                    // a.lhs >= item.var + item.cst
+                    // a.lhs - item.var >= item.cst
+                    // item.var - a.lhs <= -item.cst
+                    let alt_value = self.model.get_tautology_of_scope(item_scope);
+                    if item.var.is_plus() {
+                        assert!(a.lhs.is_plus());
+                        self.post_constraint(&Constraint::Reified(
+                            ReifExpr::MaxDiff(DifferenceExpression::new(
+                                item.var.variable(),
+                                a.lhs.variable(),
+                                -item.cst,
+                            )),
+                            alt_value,
+                        ))?;
+                    } else {
+                        assert!(a.lhs.is_minus());
+                        // item.var - a.lhs <= -item.cst
+                        let x = item.var.variable();
+                        let y = a.lhs.variable();
+                        // (-x) - (-y) <= -item.cst
+                        // y - x <= -item.cst
+                        self.post_constraint(&Constraint::Reified(
+                            ReifExpr::MaxDiff(DifferenceExpression::new(y, x, -item.cst)),
+                            alt_value,
+                        ))?;
+                    }
+                }
+
+                let prez = |v: SignedVar| self.model.state.presence(v);
+
+                // POST  OR_i  (prez(rhs[i])  &&  rhs[i] >= lhs)    [scope: prez(lhs)]
+                self.reasoners.cp.add_propagator(AtLeastOneGeq {
+                    scope,
+                    lhs: a.lhs,
+                    elements: a
+                        .rhs
+                        .iter()
+                        .map(|elem| MaxElem::new(elem.var, elem.cst, prez(elem.var)))
+                        .collect_vec(),
+                });
+
+                Ok(())
+            }
         }
     }