csp_solver/constraint/
implication.rs

1//! Reified implication constraint: `antecedent = a → consequent ∈ allowed`.
2//!
3//! Encodes the gestalt rule "if variable X takes value `a`, then variable Y
4//! must be drawn from the bitset `allowed`." Both variables share the same
5//! `Domain::Value` type. Used by recognizer-tier CSPs to enforce things like
6//! "if AltMode = TokenDispatch, all child engines must be one-pass-eligible."
7
8use crate::domain::Domain;
9use crate::variable::Variable;
10
11use super::traits::{Constraint, Revision, VarId};
12
13/// `antecedent = trigger → consequent ∈ allowed`.
14///
15/// When `antecedent` is bound to `trigger`, prune all values from
16/// `consequent` that are not in `allowed`. The antecedent is never
17/// pruned by this constraint — only the consequent.
18#[derive(Debug, Clone)]
19pub struct ImplicationConstraint<V: Clone + PartialEq + std::fmt::Debug> {
20    pub(crate) scope: [VarId; 2],
21    pub(crate) trigger: V,
22    pub(crate) allowed: Vec<V>,
23}
24
25impl<V: Clone + PartialEq + std::fmt::Debug> ImplicationConstraint<V> {
26    /// Build a new implication constraint.
27    ///
28    /// `antecedent` is the variable whose binding triggers the constraint;
29    /// `consequent` is the variable whose domain is filtered when triggered.
30    pub fn new(antecedent: VarId, consequent: VarId, trigger: V, allowed: Vec<V>) -> Self {
31        Self {
32            scope: [antecedent, consequent],
33            trigger,
34            allowed,
35        }
36    }
37
38    pub(crate) fn check_impl(&self, assignment: &[Option<V>]) -> bool {
39        let ai = self.scope[0] as usize;
40        let ci = self.scope[1] as usize;
41        match (&assignment[ai], &assignment[ci]) {
42            (Some(a), Some(c)) if *a == self.trigger => self.allowed.contains(c),
43            _ => true,
44        }
45    }
46
47    pub(crate) fn revise_impl<D: Domain<Value = V>>(
48        &self,
49        vars: &mut [Variable<D>],
50        depth: usize,
51    ) -> Revision {
52        let ai = self.scope[0] as usize;
53        let ci = self.scope[1] as usize;
54
55        // Trigger only fires when the antecedent is bound to `trigger`.
56        let antecedent_bound = vars[ai].domain.singleton_value();
57        let triggered = matches!(antecedent_bound.as_ref(), Some(v) if *v == self.trigger);
58
59        if !triggered {
60            return Revision::Unchanged;
61        }
62
63        // Antecedent is the trigger value — filter the consequent.
64        let mut changed = false;
65        let consequent_values: Vec<V> = vars[ci].domain.iter().collect();
66        for v in &consequent_values {
67            if !self.allowed.contains(v)
68                && vars[ci].prune(v, depth)
69            {
70                changed = true;
71            }
72        }
73
74        if vars[ci].domain.is_empty() {
75            return Revision::Unsatisfiable;
76        }
77
78        if changed {
79            Revision::Changed
80        } else {
81            Revision::Unchanged
82        }
83    }
84}
85
86impl<D: Domain> Constraint<D> for ImplicationConstraint<D::Value>
87where
88    D::Value: PartialEq,
89{
90    fn scope(&self) -> &[VarId] {
91        &self.scope
92    }
93    fn check(&self, assignment: &[Option<D::Value>]) -> bool {
94        self.check_impl(assignment)
95    }
96    fn revise(&self, vars: &mut [Variable<D>], depth: usize) -> Revision {
97        self.revise_impl(vars, depth)
98    }
99}
csp_solver/constraint/implication.rs

csp_solver/constraint/
implication.rs
