additional reification constraints

Author: radevgit

CHANGELOG.md

@@ -2,6 +2,22 @@
 
 All notable changes to this project will be documented in this file.
 
+## [Unreleased]
+### Added
+- Reified comparison constraints for FlatZinc Phase 2 integration:
+  - `int_lt_reif(x, y, b)` - Reified less-than: b ⇔ (x < y)
+  - `int_le_reif(x, y, b)` - Reified less-or-equal: b ⇔ (x ≤ y)
+  - `int_gt_reif(x, y, b)` - Reified greater-than: b ⇔ (x > y)
+  - `int_ge_reif(x, y, b)` - Reified greater-or-equal: b ⇔ (x ≥ y)
+- Comprehensive integration tests for Phase 2 constraints (12 tests, all passing)
+- Example demonstrating reification comparison constraints with 5 use cases
+- Documentation: `docs/development/PHASE2_REIFICATION_COMPARISON.md`
+
+### Fixed
+- Critical bug: Reification constraints were being removed during constraint optimization
+  - Added all reification constraint types to `constraint_types_to_optimize` list
+  - Ensures reification propagators are preserved during `prepare_for_search()`
+
 ## [0.8.6] - 2025-10-01
 - Linear Constraint Helpers
 

docs/development/PHASE2_REIFICATION_COMPARISON.md

@@ -0,0 +1,254 @@
+# Phase 2 FlatZinc Integration - Reification Comparison Constraints
+
+## Summary
+
+This document describes the implementation of reified comparison constraints for FlatZinc Phase 2 integration.
+
+## Implementation Date
+
+October 1, 2025
+
+## What Was Implemented
+
+### New Reification Constraints
+
+Added four new reified comparison constraints to complement the existing `int_eq_reif` and `int_ne_reif`:
+
+1. **`int_lt_reif(x, y, b)`** - Reified less-than: `b ⇔ (x < y)`
+2. **`int_le_reif(x, y, b)`** - Reified less-or-equal: `b ⇔ (x ≤ y)`
+3. **`int_gt_reif(x, y, b)`** - Reified greater-than: `b ⇔ (x > y)`
+4. **`int_ge_reif(x, y, b)`** - Reified greater-or-equal: `b ⇔ (x ≥ y)`
+
+### How Reification Works
+
+A reified constraint `b ⇔ C` creates a bidirectional implication:
+- If `b = 1` (true), then constraint `C` must hold
+- If `b = 0` (false), then constraint `C` must NOT hold
+- If `C` holds, then `b` must be 1
+- If `C` does not hold, then `b` must be 0
+
+### Propagation Strategy
+
+All reification propagators use **bidirectional propagation** without early returns:
+
+**Direction 1: From variable domains → infer boolean**
+- If the constraint is definitely true (domains force it), set `b = 1`
+- If the constraint is definitely false (domains prevent it), set `b = 0`
+
+**Direction 2: From boolean → enforce constraint**
+- If `b = 1`, enforce the constraint on the variables
+- If `b = 0`, enforce the negation of the constraint
+
+This design ensures:
+- No dependency on constraint posting order
+- Deterministic behavior regardless of propagation scheduling
+- Proper interaction with other constraints (bool_clause, linear, etc.)
+
+## Files Modified
+
+### Core Implementation
+- `src/constraints/props/reification.rs` - Added 4 new propagator structs
+- `src/constraints/props/mod.rs` - Added registration methods and fixed optimization bug
+- `src/model/constraints.rs` - Added 4 public API methods
+- `src/optimization/constraint_metadata.rs` - Added 4 new constraint types
+
+### Testing
+- `tests/test_phase2_integration.rs` - Created 12 comprehensive integration tests
+  - All tests passing ✅
+
+### Documentation
+- `examples/reification_comparison.rs` - Comprehensive examples demonstrating:
+  - Conditional constraints (if-then-else logic)
+  - Maximum computation using reification
+  - Counting constraints
+  - Partial ordering constraints
+  - Range membership checking
+
+## Critical Bug Fix
+
+### Problem
+The `optimize_universal_constraint_order()` function was removing reification constraints during optimization because they weren't in the `constraint_types_to_optimize` list. This caused reification propagators to be deleted before search started.
+
+### Symptoms
+- Reification propagators were created successfully
+- They were registered in the dependency graph
+- But they disappeared during `prepare_for_search()`
+- Tests failed with incorrect solutions
+- No errors or warnings were generated
+
+### Root Cause
+The optimization function clears `self.state` and rebuilds it with only the constraints in the optimization list:
+
+```rust
+// Reorder propagators based on priority
+self.state.clear();  // ← CLEARS ALL PROPAGATORS
+for &(prop_idx, _, _) in &constraint_priorities {
+    self.state.push(original_state[prop_idx].clone());  // ← Only adds optimized ones!
+}
+```
+
+### Solution
+Added all 6 reification constraint types to the `constraint_types_to_optimize` array:
+
+```rust
+let constraint_types_to_optimize = [
+    // ... existing types ...
+    ConstraintType::EqualityReified,
+    ConstraintType::InequalityReified,
+    ConstraintType::LessThanReified,
+    ConstraintType::LessEqualReified,
+    ConstraintType::GreaterThanReified,
+    ConstraintType::GreaterEqualReified,
+];
+```
+
+## Test Results
+
+All 12 integration tests pass consistently:
+
+```
+running 12 tests
+test test_cnf_with_linear_le ... ok
+test test_cnf_with_linear_eq ... ok
+test test_multiple_linear_with_clause ... ok
+test test_reified_linear_eq ... ok
+test test_linear_eq_with_bool_clause ... ok
+test test_3sat_with_linear ... ok
+test test_reified_ne_with_clause ... ok
+test test_negative_coeff_with_clause ... ok
+test test_linear_le_with_bool_clause ... ok
+test test_chained_reifications ... ok
+test test_reified_linear_eq_false ... ok
+test test_large_integration ... ok
+
+test result: ok. 12 passed; 0 failed
+```
+
+## Usage Examples
+
+### Basic Reification
+
+```rust
+use selen::prelude::*;
+
+let mut m = Model::default();
+let x = m.int(0, 10);
+let y = m.int(0, 10);
+let b = m.bool();
+
+// b will be 1 iff x < y
+m.int_lt_reif(x, y, b);
+```
+
+### Conditional Constraints
+
+```rust
+// If x > 5, then y = 10, else y = 0
+let x = m.int(0, 10);
+let y = m.int(0, 10);
+let b = m.bool();
+let five = m.int(5, 5);
+
+m.int_gt_reif(x, five, b);
+
+let y_eq_10 = m.bool();
+let y_eq_0 = m.bool();
+let ten = m.int(10, 10);
+let zero = m.int(0, 0);
+
+m.int_eq_reif(y, ten, y_eq_10);
+m.int_eq_reif(y, zero, y_eq_0);
+
+// b → y_eq_10 and ¬b → y_eq_0
+m.bool_clause(&[y_eq_10], &[b]);
+m.bool_clause(&[b, y_eq_0], &[]);
+```
+
+### Counting
+
+```rust
+// Count how many of x, y, z are greater than 5
+let x = m.int(0, 10);
+let y = m.int(0, 10);
+let z = m.int(0, 10);
+let five = m.int(5, 5);
+
+let x_gt_5 = m.bool();
+let y_gt_5 = m.bool();
+let z_gt_5 = m.bool();
+
+m.int_gt_reif(x, five, x_gt_5);
+m.int_gt_reif(y, five, y_gt_5);
+m.int_gt_reif(z, five, z_gt_5);
+
+// Require exactly 2 to be > 5
+m.int_lin_eq(&[1, 1, 1], &[x_gt_5, y_gt_5, z_gt_5], 2);
+```
+
+## Design Decisions
+
+### Why Bidirectional Propagation Without Early Returns?
+
+The original implementation used early returns after checking one direction:
+
+```rust
+// OLD - BAD
+if x_max < y_min {
+    self.b.try_set_min(Val::ValI(1), ctx)?;
+    return Some(());  // ← Early return
+}
+```
+
+This caused non-deterministic failures when constraints were posted in certain orders. The fix removes early returns and always checks all directions:
+
+```rust
+// NEW - GOOD
+if x_max < y_min {
+    self.b.try_set_min(Val::ValI(1), ctx)?;
+}
+// Continue to check other directions...
+```
+
+This ensures the propagator makes progress regardless of when it runs or what other constraints have propagated.
+
+### Why Include Reification in Optimization?
+
+Reification constraints can be expensive to propagate, so including them in constraint optimization allows the solver to:
+- Schedule them appropriately relative to other constraints
+- Prioritize them based on variable connectivity
+- Maintain consistency with the optimization framework
+
+Without inclusion in optimization, they would be silently removed, causing subtle and hard-to-debug failures.
+
+## API Completeness
+
+All six comparison reification constraints are now available:
+
+| Constraint | Meaning | API Method |
+|-----------|---------|-----------|
+| `b ⇔ (x = y)` | Equality | `int_eq_reif(x, y, b)` ✅ |
+| `b ⇔ (x ≠ y)` | Inequality | `int_ne_reif(x, y, b)` ✅ |
+| `b ⇔ (x < y)` | Less than | `int_lt_reif(x, y, b)` ✅ |
+| `b ⇔ (x ≤ y)` | Less or equal | `int_le_reif(x, y, b)` ✅ |
+| `b ⇔ (x > y)` | Greater than | `int_gt_reif(x, y, b)` ✅ |
+| `b ⇔ (x ≥ y)` | Greater or equal | `int_ge_reif(x, y, b)` ✅ |
+
+## Next Steps
+
+### Immediate
+- ✅ Run full test suite to ensure no regressions
+- ✅ Document the implementation
+- Commit changes with clear message
+
+### Future Phase 2 Work
+- Implement more FlatZinc global constraints
+- Add set constraints
+- Implement float constraints
+- Create FlatZinc parser integration tests
+
+## References
+
+- FlatZinc specification: https://www.minizinc.org/doc-2.5.5/en/fzn-spec.html
+- Reification documentation: `docs/development/ZINC_REIFICATION_FIX.md`
+- Integration tests: `tests/test_phase2_integration.rs`
+- Examples: `examples/reification_comparison.rs`