selen 0.15.5

Constraint Satisfaction Problem (CSP) solver
Documentation
# Phase 1 API Refactoring - Completion Report

**Date:** October 10, 2025  
**Status:** ✅ COMPLETED

## Overview

Phase 1 of the API refactoring has been successfully completed. We have created a unified constraint API with 30+ generic functions that eliminate type prefixes and provide a clean, composable interface for constraint programming.

## What Was Implemented

### 1. Core Infrastructure

**File:** `src/constraints/functions.rs` (680 lines)

Created a new module containing all generic constraint functions organized by category:

#### Arithmetic Operations (return `ExprBuilder` for composition)
- `add(x, y)` - Addition expression
- `sub(x, y)` - Subtraction expression  
- `mul(x, y)` - Multiplication expression
- `div(x, y)` - Division expression
- `modulo(x, y)` - Modulo expression

#### Comparison Constraints (available both as functions and runtime API methods)
- `eq(model, x, y)` - Equality constraint (or use `m.new(x.eq(y))`)
- `ne(model, x, y)` - Inequality constraint (or use `m.new(x.ne(y))`)
- `lt(model, x, y)` - Less than constraint (or use `m.new(x.lt(y))`)
- `le(model, x, y)` - Less than or equal constraint (or use `m.new(x.le(y))`)
- `gt(model, x, y)` - Greater than constraint (or use `m.new(x.gt(y))`)
- `ge(model, x, y)` - Greater than or equal constraint (or use `m.new(x.ge(y))`)

**Note:** The runtime API style (`m.new(x.eq(y))`) is preferred for its cleaner syntax.

#### Linear Constraints (generic via `LinearCoeff` trait)
- `lin_eq(model, coeffs, vars, constant)` - Linear equality
- `lin_le(model, coeffs, vars, constant)` - Linear less-than-or-equal
- `lin_ne(model, coeffs, vars, constant)` - Linear inequality

#### Reified Constraints
- `eq_reif(model, x, y, b)` - Reified equality
- `ne_reif(model, x, y, b)` - Reified inequality
- `lt_reif(model, x, y, b)` - Reified less than
- `le_reif(model, x, y, b)` - Reified less than or equal
- `gt_reif(model, x, y, b)` - Reified greater than
- `ge_reif(model, x, y, b)` - Reified greater than or equal
- `lin_eq_reif(model, coeffs, vars, constant, b)` - Reified linear equality
- `lin_le_reif(model, coeffs, vars, constant, b)` - Reified linear less-than-or-equal
- `lin_ne_reif(model, coeffs, vars, constant, b)` - Reified linear inequality

#### Logical Constraints
- `and(model, x, y, z)` - Logical AND
- `or(model, x, y, z)` - Logical OR
- `not(model, x, y)` - Logical NOT
- `xor(model, x, y, z)` - Logical XOR
- `implies(model, x, y)` - Logical implication

#### Global Constraints
- `alldiff(model, vars)` - All different constraint
- `alleq(model, vars)` - All equal constraint
- `min(model, vars, result)` - Minimum constraint
- `max(model, vars, result)` - Maximum constraint
- `sum(model, vars, result)` - Sum constraint
- `abs(model, x)` - Absolute value (returns VarId)
- `element(model, index, array, value)` - Element constraint

#### Stub Functions (marked with `todo!()` for Phase 2)
- `table(model, vars, tuples)`
- `gcc(model, vars, card_vars, covers)`
- `cumulative(model, starts, durations, demands, capacity)`
- `to_float(model, int_var)`
- `floor(model, float_var)`
- `ceil(model, float_var)`
- `round(model, float_var)`

### 2. Generic Programming

**LinearCoeff Trait:**
```rust
pub trait LinearCoeff: Copy + Clone + Into<Val> {
    fn post_lin_eq(model: &mut Model, coeffs: &[Self], vars: &[VarId], constant: Self);
    fn post_lin_le(model: &mut Model, coeffs: &[Self], vars: &[VarId], constant: Self);
    fn post_lin_ne(model: &[Self], vars: &[VarId], constant: Self);
    // ... reified versions
}
```

Implemented for both `i32` and `f64`, enabling:
```rust
// Integer linear constraint
lin_eq(&mut m, &[1, 2, 3], &[x, y, z], 10);

// Float linear constraint  
lin_eq(&mut m, &[1.0, 2.0, 3.0], &[x, y, z], 10.0);
```

### 3. API Design Principles Established

#### Explicit Constant Types
**Decision:** Always use explicit `int()` and `float()` for constants
```rust
// ✅ CORRECT - Explicit type
eq(&mut m, x, int(5));
eq(&mut m, y, float(3.14));

// ❌ WRONG - Implicit conversion (not supported)
eq(&mut m, x, 5);
```

#### Method Syntax for Non-Composable Constraints
**Decision:** Use `m.method()` for constraints that don't compose
```rust
// ✅ CORRECT - Method syntax
m.alldiff(&vars);
m.solve();

// ❌ WRONG - Standalone function (less ergonomic)
alldiff(&mut m, &vars);
```

#### Function Syntax for Composable Operations
**Decision:** Use standalone functions that return `ExprBuilder`
```rust
// ✅ CORRECT - Composable expressions
let expr = add(mul(x, int(2)), y);
m.new(expr.eq(z));

// Enables complex compositions
let expr = add(
    add(mul(x, int(10)), mul(y, int(20))),
    z
);
```

#### Runtime API for Constraint Posting (Preferred!)
**Decision:** Use `m.new(x.eq(y))` instead of `eq(&mut m, x, y)`
```rust
// ✅ PREFERRED - Runtime API (clean and fluent)
m.new(x.eq(y));
m.new(x.lt(int(10)));
m.new(add(x, y).eq(z));

// ❌ VERBOSE - Function API (still available but less preferred)
eq(&mut m, x, y);
lt(&mut m, x, int(10));
```

The runtime API is cleaner because:
- No need to pass `&mut m` to every constraint
- More fluent and readable: `x.eq(y)` reads naturally
- Consistent with expression building: `add(x, y).eq(z)`

#### Variable Naming Convention
**Decision:** Use short model names ('m' or 'mm' when conflicts)
```rust
// ✅ CORRECT - Short name
let mut m = Model::default();

// ✅ CORRECT - Avoid conflicts
let mut mm = Model::default();  // When 'm' is used for a variable
let m = mm.int(1, 9);  // m is a variable (letter M in puzzle)
```

### 4. Testing

Created comprehensive test suites:

**tests/test_new_api_linear.rs** (5 tests)
- `test_lin_eq_integer` - Integer linear equality
- `test_lin_le_integer` - Integer linear inequality
- `test_lin_eq_float` - Float linear equality
- `test_lin_eq_reif` - Reified linear constraints
- `test_generic_linear_with_comparison` - Mixed constraints

**tests/test_new_api_constants.rs** (6 tests)
- `test_eq_with_int_constant` - Integer constant equality
- `test_eq_with_float_constant` - Float constant equality
- `test_ne_with_constant` - Inequality with constant
- `test_comparison_with_constants` - Multiple comparisons
- `test_range_with_constants` - Range constraints
- `test_expression_with_constant` - Expressions with constants

**All 11 tests passing ✅**

### 5. Examples

Created 4 comprehensive examples demonstrating the new API:

**examples_backup/send_more_money_new_api.rs**
- Cryptarithmetic puzzle (SEND + MORE = MONEY)
- Demonstrates: `alldiff()`, `add()`, `mul()`, `eq()`, `int()` constants
- Uses method syntax and expression composition

**examples_backup/n_queens_new_api.rs**
- Classic N-Queens problem
- Demonstrates: `m.ints()`, `m.alldiff()`, `add()`, `sub()`, expression materialization
- Shows how to create auxiliary variables for expressions

**examples_backup/sudoku_4x4_new_api.rs**
- Simple 4x4 Sudoku solver
- Demonstrates: `m.ints()`, `m.alldiff()`, `eq()` with `int()` constants
- Clean constraint posting pattern

**examples_backup/zebra_puzzle_new_api.rs**
- Einstein's Riddle / Zebra Puzzle
- Demonstrates: `eq()`, `sub()`, `abs()`, complex constraint relationships
- Full-featured puzzle solver

## API Comparison

### Old API
```rust
// Type-specific methods, verbose
let x = model.int(1, 10);
let y = model.int(1, 10);
let sum = model.add(x, y);
model.int_lin_eq(&[1, 2, 3], &[x, y, z], 10);
model.float_lin_eq(&[1.0, 2.0], &[a, b], 5.0);
```

### New API
```rust
// Generic functions, composable
let x = m.int(1, 10);
let y = m.int(1, 10);
let sum_expr = add(x, y);
m.new(sum_expr.eq(int(15)));

// Generic linear constraints (no type prefix!)
lin_eq(&mut m, &[1, 2, 3], &[x, y, z], 10);      // Integer
lin_eq(&mut m, &[1.0, 2.0], &[a, b], 5.0);       // Float
```

## Key Achievements

### 1. Type Unification
✅ Eliminated type prefixes (`int_lin_eq` → `lin_eq`)  
✅ Generic dispatch via traits (`LinearCoeff`)  
✅ Single API for all numeric types

### 2. Composability
✅ Arithmetic operations return `ExprBuilder`  
✅ Expressions can be nested and composed  
✅ Clean separation: expressions vs constraints

### 3. Ergonomics
✅ Explicit constant types (`int(5)`, `float(3.14)`)  
✅ Method syntax for model operations (`m.alldiff()`)  
✅ Function syntax for expressions (`add()`, `mul()`)  
✅ Consistent naming conventions

### 4. Maintainability
✅ All functions in single module (`functions.rs`)  
✅ Organized by category with clear documentation  
✅ Easy to extend with new constraints

## Phase 1 Implementation Approach

**Strategy:** Create propagators directly (bypass AST)

All constraint functions in Phase 1 call the existing Model API methods directly:
```rust
pub fn lin_eq<T: LinearCoeff>(
    model: &mut Model,
    coeffs: &[T],
    vars: &[VarId],
    constant: T,
) {
    T::post_lin_eq(model, coeffs, vars, constant);
}
```

This approach:
- ✅ Gets the new API working quickly
- ✅ Maintains backward compatibility
- ✅ Allows testing and validation
- ⏭️ Will be replaced in Phase 2 with AST-based approach

## Next Steps: Phase 2

### Goal: AST-Based Constraint System

**Objective:** Route all constraints through the AST system to enable LP solver integration.

### Plan:
1. **Create AST nodes for all constraint types**
   - Extend `ConstraintKind` enum with all constraint variants
   - Add fields for coefficients, variables, constants

2. **Convert function implementations to create AST**
   ```rust
   // Phase 2 approach
   pub fn lin_eq<T: LinearCoeff>(
       model: &mut Model,
       coeffs: &[T],
       vars: &[VarId],
       constant: T,
   ) {
       let ast = ConstraintKind::LinearEq {
           coeffs: coeffs.to_vec(),
           vars: vars.to_vec(),
           constant,
       };
       model.post_constraint(ast);
   }
   ```

3. **Update propagator creation to extract from AST**
   - Model.post_constraint() creates AST
   - LP solver attempts to solve via AST
   - Falls back to propagators if needed

4. **Remove old Model API methods**
   - Clean up `src/constraints/api/` directory
   - Remove type-specific methods (43 methods)
   - Keep only new generic API

## Files Changed

### Created
- `src/constraints/functions.rs` (680 lines)
- `tests/test_new_api_linear.rs` (179 lines)
- `tests/test_new_api_constants.rs` (195 lines)
- `examples_backup/send_more_money_new_api.rs` (113 lines)
- `examples_backup/n_queens_new_api.rs` (124 lines)
- `examples_backup/sudoku_4x4_new_api.rs` (78 lines)
- `examples_backup/zebra_puzzle_new_api.rs` (168 lines)

### Modified
- `src/constraints/mod.rs` - Added `pub mod functions;`
- `src/api/prelude.rs` - Exported all new functions and traits

## Summary

Phase 1 is **complete and successful**. We have:

✅ Created a unified, generic constraint API  
✅ Eliminated type prefixes from function names  
✅ Established clear API design principles  
✅ Implemented 30+ generic constraint functions  
✅ Created comprehensive test coverage (11 tests)  
✅ Demonstrated usage with 4 real-world examples  
✅ Maintained backward compatibility  

The foundation is now in place for Phase 2, where we'll route all constraints through the AST system to enable full LP solver integration.

## API Style Guide

For future reference, the established conventions:

### Variable Creation
```rust
let x = m.int(min, max);           // Single integer
let vars = m.ints(n, min, max);    // Multiple integers
let f = m.float(min, max);         // Single float
let b = m.bool();                  // Boolean
```

### Constants
```rust
eq(&mut m, x, int(5));             // Integer constant
eq(&mut m, f, float(3.14));        // Float constant
```

### Expressions (composable)
```rust
let expr = add(x, y);              // x + y
let expr = mul(x, int(2));         // x * 2
let expr = add(mul(x, int(3)), y); // 3*x + y
```

### Constraints (non-composable)
```rust
m.alldiff(&vars);                  // All different
m.new(x.eq(y));                    // Equality (runtime API - preferred!)
lin_eq(&mut m, &coeffs, &vars, c); // Linear equation
```

### Posting Expressions (Runtime API - Preferred Style)
```rust
m.new(x.eq(y));                    // Variable equality
m.new(x.eq(int(5)));               // Equality with constant
m.new(expr.eq(result));            // Expression equality
m.new(x.lt(y));                    // Less than
m.new(add(x, y).eq(z));            // Post composed expression
```

---

**Phase 1: ✅ COMPLETE**  
**Ready for Phase 2: AST Integration**