count to accept variables, xor implemented

Author: radevgit

CHANGELOG.md

@@ -4,6 +4,7 @@ All notable changes to this project will be documented in this file.
 
 ## [0.14.0] - 2025-10-16
 - count(var, var) now uses Vies-s and can work with both const and vars
+- Boolean XOR implemented
 
 ## [0.12.8] - 2025-10-16
 - Introduced count_var() constraint for variable counts

README.md

@@ -60,6 +60,7 @@ m.gcc(&vars, values, counts);          // global cardinality constraint
 let and_result = m.bool_and(&[a, b]);  // a AND b
 let or_result = m.bool_or(&[a, b]);    // a OR b
 let not_result = m.bool_not(a);        // NOT a
+let xor_result = m.bool_xor(a, b);     // a XOR b
 m.implies(a, b);                       // a → b (if a then b)
 m.bool_clause(&[a, b], &[c]);          // a ∨ b ∨ ¬c (CNF clause)
 

src/constraints/api/boolean.rs

@@ -62,6 +62,24 @@ impl Model {
         result
     }
 
+    #[doc(hidden)]
+    /// Create a variable representing the boolean XOR of two operands.
+    /// Returns a variable that is 1 if exactly one operand is non-zero, 0 otherwise.
+    /// 
+    /// # Examples
+    /// ```
+    /// use selen::prelude::*;
+    /// let mut m = Model::default();
+    /// let a = m.bool();
+    /// let b = m.bool();
+    /// let xor_result = m.bool_xor(a, b);
+    /// ```
+    pub fn bool_xor(&mut self, x: VarId, y: VarId) -> VarId {
+        let result = self.bool(); // Create a boolean variable (0 or 1)
+        self.props.bool_xor(x, y, result);
+        result
+    }
+
     /// Post a boolean implication constraint: `a → b` (if a then b).
     /// 
     /// If `a` is true (1), then `b` must be true (1).

src/constraints/props/bool_logic.rs

@@ -269,3 +269,113 @@ impl Propagate for BoolNot {
             .chain(core::iter::once(self.operand))
     }
 }
+
+/// Boolean XOR constraint: `result = a XOR b`.
+/// This constraint enforces that the result variable equals the logical XOR of two boolean operands.
+/// XOR is true (1) when exactly one operand is true (non-zero).
+/// Variables are treated as boolean: 0 = false, non-zero = true.
+#[derive(Clone, Debug)]
+#[doc(hidden)]
+pub struct BoolXor {
+    x: VarId,
+    y: VarId,
+    result: VarId,
+}
+
+impl BoolXor {
+    pub fn new(x: VarId, y: VarId, result: VarId) -> Self {
+        Self { x, y, result }
+    }
+}
+
+impl Prune for BoolXor {
+    fn prune(&self, ctx: &mut Context) -> Option<()> {
+        // XOR truth table (treating as boolean: 0 = false, 1 = true):
+        // x | y | x XOR y
+        // --+---+--------
+        // 0 | 0 |   0
+        // 0 | 1 |   1
+        // 1 | 0 |   1
+        // 1 | 1 |   0
+        //
+        // So: result = 1 iff (x = 0 and y = 1) or (x = 1 and y = 0)
+        //     result = 0 iff (x = 0 and y = 0) or (x = 1 and y = 1)
+
+        let x_min = self.x.min(ctx);
+        let x_max = self.x.max(ctx);
+        let y_min = self.y.min(ctx);
+        let y_max = self.y.max(ctx);
+        let result_min = self.result.min(ctx);
+        let result_max = self.result.max(ctx);
+
+        // Case 1: result is fixed to 1 (must be true)
+        if result_min >= Val::ValI(1) {
+            // x XOR y must be true
+            // This means: (x=0 AND y=1) OR (x=1 AND y=0)
+            
+            // If x is definitely 0, then y must be definitely 1
+            if x_max <= Val::ValI(0) {
+                let _min = self.y.try_set_min(Val::ValI(1), ctx)?;
+            }
+            // If x is definitely 1 (>= 1), then y must be definitely 0
+            if x_min >= Val::ValI(1) {
+                let _max = self.y.try_set_max(Val::ValI(0), ctx)?;
+            }
+            // Similarly for y
+            if y_max <= Val::ValI(0) {
+                let _min = self.x.try_set_min(Val::ValI(1), ctx)?;
+            }
+            if y_min >= Val::ValI(1) {
+                let _max = self.x.try_set_max(Val::ValI(0), ctx)?;
+            }
+        }
+
+        // Case 2: result is fixed to 0 (must be false)
+        if result_max <= Val::ValI(0) {
+            // x XOR y must be false
+            // This means: (x=0 AND y=0) OR (x=1 AND y=1)
+            
+            // If x is definitely 0, then y must be definitely 0
+            if x_max <= Val::ValI(0) {
+                let _max = self.y.try_set_max(Val::ValI(0), ctx)?;
+            }
+            // If x is definitely 1, then y must be definitely 1
+            if x_min >= Val::ValI(1) {
+                let _min = self.y.try_set_min(Val::ValI(1), ctx)?;
+            }
+            // Similarly for y
+            if y_max <= Val::ValI(0) {
+                let _max = self.x.try_set_max(Val::ValI(0), ctx)?;
+            }
+            if y_min >= Val::ValI(1) {
+                let _min = self.x.try_set_min(Val::ValI(1), ctx)?;
+            }
+        }
+
+        // Case 3: Propagate from fixed x and y to result
+        // If both x and y are fixed (or determinable)
+        if x_min == x_max && y_min == y_max {
+            let x_bool = x_min >= Val::ValI(1);
+            let y_bool = y_min >= Val::ValI(1);
+            let xor_result = x_bool != y_bool; // XOR operation
+            
+            if xor_result {
+                let _min = self.result.try_set_min(Val::ValI(1), ctx)?;
+                let _max = self.result.try_set_max(Val::ValI(1), ctx)?;
+            } else {
+                let _min = self.result.try_set_min(Val::ValI(0), ctx)?;
+                let _max = self.result.try_set_max(Val::ValI(0), ctx)?;
+            }
+        }
+
+        Some(())
+    }
+}
+
+impl Propagate for BoolXor {
+    fn list_trigger_vars(&self) -> impl Iterator<Item = VarId> {
+        core::iter::once(self.result)
+            .chain(core::iter::once(self.x))
+            .chain(core::iter::once(self.y))
+    }
+}

src/constraints/props/mod.rs

@@ -1362,6 +1362,27 @@ impl Propagators {
         )
     }
 
+    pub fn bool_xor(&mut self, x: VarId, y: VarId, result: VarId) -> PropId {
+        use crate::optimization::constraint_metadata::{ConstraintData, ConstraintType, ViewInfo};
+
+        let x_info = ViewInfo::Variable { var_id: x };
+        let y_info = ViewInfo::Variable { var_id: y };
+        let result_info = ViewInfo::Variable { var_id: result };
+
+        let variables = vec![x, y, result];
+
+        let metadata = ConstraintData::NAry {
+            operands: vec![x_info, y_info, result_info],
+        };
+
+        self.push_new_prop_with_metadata(
+            self::bool_logic::BoolXor::new(x, y, result),
+            ConstraintType::BooleanXor,
+            variables,
+            metadata,
+        )
+    }
+
     // ═══════════════════════════════════════════════════════════════════════
     // 🔄 Reification Constraints
     // ═══════════════════════════════════════════════════════════════════════

src/optimization/constraint_metadata.rs

@@ -66,6 +66,8 @@ pub enum ConstraintType {
     BooleanOr,
     /// Boolean NOT constraint (result = NOT operand)
     BooleanNot,
+    /// Boolean XOR constraint (result = a XOR b)
+    BooleanXor,
     /// Reified equality constraint (b ⇔ (x = y))
     EqualityReified,
     /// Reified inequality constraint (b ⇔ (x ≠ y))
@@ -417,6 +419,7 @@ impl ConstraintRegistry {
                 ConstraintType::BooleanAnd |
                 ConstraintType::BooleanOr |
                 ConstraintType::BooleanNot |
+                ConstraintType::BooleanXor |
                 ConstraintType::AllDifferent | 
                 ConstraintType::AllEqual |
                 ConstraintType::Element |

tests/main_tests.rs

@@ -179,5 +179,8 @@ mod test_count_var;
 #[path = "../tests_all/test_count_view_flexibility.rs"]
 mod test_count_view_flexibility;
 
+#[path = "../tests_all/test_bool_xor.rs"]
+mod test_bool_xor;
+
 #[path = "../tests_all/test_element_computed_index.rs"]
 mod test_element_computed_index;