diff --git a/CHANGELOG.md b/CHANGELOG.md index 0f61036..c2554c9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,8 +2,11 @@ All notable changes to this project will be documented in this file. +## [0.9.0] - 2025-10-03 +- **Removed**: FlatZinc parser and integration (moved to [Zelen](https://github.com/radevgit/zelen) + ## [0.8.7] - 2025-10-03 -- FlatZinc Parser +- FlatZinc Parser (deprecated - moved to Zelen in v0.9.0) ## [0.8.6] - 2025-10-01 - Linear Constraint Helpers diff --git a/Cargo.lock b/Cargo.lock index 7b10eda..2f8dc60 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -4,4 +4,4 @@ version = 4 [[package]] name = "selen" -version = "0.8.7" +version = "0.9.0" diff --git a/Cargo.toml b/Cargo.toml index bd46c0b..d3e0cf8 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "selen" -version = "0.8.7" +version = "0.9.0" edition = "2024" description = "Constraint Satisfaction Problem (CSP) solver" rust-version = "1.88" diff --git a/README.md b/README.md index 7113e43..3cb75c6 100644 --- a/README.md +++ b/README.md @@ -45,23 +45,23 @@ post!(m, x * y == int(12)); // x * y == 12 post!(m, z / y != int(0)); // z / y != 0 ``` -**Import FlatZinc `.fzn` file** +**FlatZinc/MiniZinc Support** + +For FlatZinc `.fzn` file support, use the separate [Zelen](https://github.com/radevgit/zelen) crate: ```rust -use selen::prelude::*; +use zelen::prelude::*; let mut model = Model::default(); model.from_flatzinc_file("puzzle.fzn")?; let solution = model.solve()?; -println!("Solution: {:?}", solution); ``` - ## Installation Add this to your `Cargo.toml`: ```toml [dependencies] -selen = "0.8.7" +selen = "0.9" ``` ## Examples diff --git a/examples/flatzinc_simple.rs b/examples/flatzinc_simple.rs deleted file mode 100644 index 0669a01..0000000 --- a/examples/flatzinc_simple.rs +++ /dev/null @@ -1,68 +0,0 @@ -//! Example: Simple FlatZinc test - -use selen::prelude::*; - -fn main() { - // Test 1: Simple variable declaration - println!("Test 1: Simple variable declaration"); - { - let fzn = r#" - var 1..10: x; - var 1..10: y; - solve satisfy; - "#; - - let mut model = Model::default(); - match model.from_flatzinc_str(fzn) { - Ok(_) => println!("✓ Parsed successfully"), - Err(e) => println!("✗ Parse error: {}", e), - } - } - - // Test 2: Simple constraint - println!("\nTest 2: Simple constraint with int_eq"); - { - let fzn = r#" - var 1..3: x; - var 1..3: y; - constraint int_eq(x, 1); - solve satisfy; - "#; - - let mut model = Model::default(); - match model.from_flatzinc_str(fzn) { - Ok(_) => { - println!("✓ Parsed successfully"); - match model.solve() { - Ok(_) => println!("✓ Solved successfully"), - Err(e) => println!("✗ Solve error: {:?}", e), - } - } - Err(e) => println!("✗ Parse error: {}", e), - } - } - - // Test 3: all_different - println!("\nTest 3: all_different constraint"); - { - let fzn = r#" - var 1..3: x; - var 1..3: y; - var 1..3: z; - constraint all_different([x, y, z]); - solve satisfy; - "#; - - let mut model = Model::default(); - match model.from_flatzinc_str(fzn) { - Ok(_) => { - println!("✓ Parsed successfully"); - match model.solve() { - Ok(_) => println!("✓ Solved successfully"), - Err(e) => println!("✗ Solve error: {:?}", e), - } - } - Err(e) => println!("✗ Parse error: {}", e), - } - } -} diff --git a/src/flatzinc/ast.rs b/src/flatzinc/ast.rs deleted file mode 100644 index c4db8ab..0000000 --- a/src/flatzinc/ast.rs +++ /dev/null @@ -1,167 +0,0 @@ -//! Abstract Syntax Tree (AST) for FlatZinc -//! -//! Represents the parsed structure of a FlatZinc model. - -use crate::flatzinc::tokenizer::Location; - -/// A complete FlatZinc model -#[derive(Debug, Clone)] -pub struct FlatZincModel { - pub predicates: Vec, - pub var_decls: Vec, - pub constraints: Vec, - pub solve_goal: SolveGoal, -} - -/// Predicate declaration -#[derive(Debug, Clone)] -pub struct PredicateDecl { - pub name: String, - pub params: Vec, - pub location: Location, -} - -/// Predicate parameter -#[derive(Debug, Clone)] -pub struct PredParam { - pub param_type: Type, - pub name: String, -} - -/// Variable declaration -#[derive(Debug, Clone)] -pub struct VarDecl { - pub var_type: Type, - pub name: String, - pub annotations: Vec, - pub init_value: Option, - pub location: Location, -} - -/// Type in FlatZinc -#[derive(Debug, Clone, PartialEq)] -pub enum Type { - /// Basic types - Bool, - Int, - Float, - - /// Integer range: int_min..int_max - IntRange(i64, i64), - - /// Integer set: {1, 2, 3} - IntSet(Vec), - - /// Float range: float_min..float_max - FloatRange(f64, f64), - - /// Set of int - SetOfInt, - - /// Set with specific domain - SetRange(i64, i64), - - /// Array type: array[index_set] of element_type - Array { - index_sets: Vec, - element_type: Box, - }, - - /// Variable type (var before the actual type) - Var(Box), -} - -/// Index set for arrays -#[derive(Debug, Clone, PartialEq)] -pub enum IndexSet { - /// 1..n - Range(i64, i64), - - /// Explicit set - Set(Vec), -} - -/// Constraint statement -#[derive(Debug, Clone)] -pub struct Constraint { - pub predicate: String, - pub args: Vec, - pub annotations: Vec, - pub location: Location, -} - -/// Solve goal -#[derive(Debug, Clone)] -pub enum SolveGoal { - Satisfy { - annotations: Vec, - }, - Minimize { - objective: Expr, - annotations: Vec, - }, - Maximize { - objective: Expr, - annotations: Vec, - }, -} - -/// Expression -#[derive(Debug, Clone)] -pub enum Expr { - /// Boolean literal - BoolLit(bool), - - /// Integer literal - IntLit(i64), - - /// Float literal - FloatLit(f64), - - /// String literal - StringLit(String), - - /// Identifier (variable reference) - Ident(String), - - /// Array literal: [1, 2, 3] - ArrayLit(Vec), - - /// Set literal: {1, 2, 3} - SetLit(Vec), - - /// Integer range: 1..10 - Range(Box, Box), - - /// Array access: arr[idx] - ArrayAccess { - array: Box, - index: Box, - }, -} - -/// Annotation (e.g., :: output_var) -#[derive(Debug, Clone)] -pub struct Annotation { - pub name: String, - pub args: Vec, -} - -impl FlatZincModel { - pub fn new() -> Self { - FlatZincModel { - predicates: Vec::new(), - var_decls: Vec::new(), - constraints: Vec::new(), - solve_goal: SolveGoal::Satisfy { - annotations: Vec::new(), - }, - } - } -} - -impl Default for FlatZincModel { - fn default() -> Self { - Self::new() - } -} diff --git a/src/flatzinc/error.rs b/src/flatzinc/error.rs deleted file mode 100644 index 9cf5576..0000000 --- a/src/flatzinc/error.rs +++ /dev/null @@ -1,71 +0,0 @@ -//! Error types for FlatZinc parsing and integration - -use std::fmt; - -/// Result type for FlatZinc operations -pub type FlatZincResult = Result; - -/// Errors that can occur during FlatZinc parsing and mapping -#[derive(Debug, Clone)] -pub enum FlatZincError { - /// I/O error reading file - IoError(String), - - /// Lexical error during tokenization - LexError { - message: String, - line: usize, - column: usize, - }, - - /// Syntax error during parsing - ParseError { - message: String, - line: usize, - column: usize, - }, - - /// Semantic error during AST to Model mapping - MapError { - message: String, - line: Option, - column: Option, - }, - - /// Unsupported FlatZinc feature - UnsupportedFeature { - feature: String, - line: Option, - column: Option, - }, -} - -impl fmt::Display for FlatZincError { - fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - match self { - FlatZincError::IoError(msg) => write!(f, "I/O Error: {}", msg), - FlatZincError::LexError { message, line, column } => { - write!(f, "Lexical Error at line {}, column {}: {}", line, column, message) - } - FlatZincError::ParseError { message, line, column } => { - write!(f, "Parse Error at line {}, column {}: {}", line, column, message) - } - FlatZincError::MapError { message, line, column } => { - match (line, column) { - (Some(l), Some(c)) => write!(f, "Mapping Error at line {}, column {}: {}", l, c, message), - _ => write!(f, "Mapping Error: {}", message), - } - } - FlatZincError::UnsupportedFeature { feature, line, column } => { - match (line, column) { - (Some(l), Some(c)) => { - write!(f, "Unsupported Feature '{}' at line {}, column {}", feature, l, c) - } - _ => write!(f, "Unsupported Feature '{}'", feature), - } - } - } - } -} - -impl std::error::Error for FlatZincError {} diff --git a/src/flatzinc/mapper.rs b/src/flatzinc/mapper.rs deleted file mode 100644 index 6f27c3e..0000000 --- a/src/flatzinc/mapper.rs +++ /dev/null @@ -1,542 +0,0 @@ -//! AST to Selen Model Mapper -//! -//! Converts FlatZinc AST into a Selen constraint model. - -use crate::flatzinc::ast::*; -use crate::flatzinc::error::{FlatZincError, FlatZincResult}; -use crate::prelude::Model; -use crate::variables::VarId; -use crate::runtime_api::{VarIdExt, ModelExt}; -use std::collections::HashMap; - -// Sub-modules for organization -mod constraints; -mod helpers; - -// Re-export is not needed as methods are already on MappingContext - -/// Context for mapping AST to Model -pub struct MappingContext<'a> { - pub(super) model: &'a mut Model, - pub(super) var_map: HashMap, - /// Maps array names to their variable lists - pub(super) array_map: HashMap>, - /// Maps parameter array names to their constant integer values - pub(super) param_int_arrays: HashMap>, - /// Maps parameter array names to their constant boolean values - pub(super) param_bool_arrays: HashMap>, - /// Inferred bounds for unbounded integer variables - pub(super) unbounded_int_bounds: (i32, i32), -} - -impl<'a> MappingContext<'a> { - pub fn new(model: &'a mut Model, unbounded_bounds: (i32, i32)) -> Self { - MappingContext { - model, - var_map: HashMap::new(), - array_map: HashMap::new(), - param_int_arrays: HashMap::new(), - param_bool_arrays: HashMap::new(), - unbounded_int_bounds: unbounded_bounds, - } - } - - /// Map variable declarations to Selen variables - fn map_var_decl(&mut self, decl: &VarDecl) -> FlatZincResult<()> { - let var_id = match &decl.var_type { - Type::Var(inner_type) => match **inner_type { - Type::Bool => self.model.bool(), - Type::Int => { - // Unbounded integer variables are approximated using inferred bounds - // from other bounded variables in the model - let (min_bound, max_bound) = self.unbounded_int_bounds; - self.model.int(min_bound, max_bound) - } - Type::IntRange(min, max) => { - // Validate domain size against Selen's SparseSet limit - // Use checked arithmetic to handle potential overflow - let domain_size = match max.checked_sub(min) { - Some(diff) => match diff.checked_add(1) { - Some(size) => size as u64, - None => u64::MAX, // Overflow means it's too large - }, - None => u64::MAX, // Overflow means it's too large - }; - - const MAX_DOMAIN: u64 = crate::variables::domain::MAX_SPARSE_SET_DOMAIN_SIZE; - if domain_size > MAX_DOMAIN { - // For very large domains, use domain inference instead of failing - // This handles cases like [0, 999999999] by using inferred bounds - // from other variables in the model - eprintln!( - "Warning: Variable '{}' has very large domain [{}, {}] with size {}. \ - Using inferred bounds [{}, {}] instead.", - decl.name, min, max, domain_size, - self.unbounded_int_bounds.0, self.unbounded_int_bounds.1 - ); - let (min_bound, max_bound) = self.unbounded_int_bounds; - self.model.int(min_bound, max_bound) - } else { - self.model.int(min as i32, max as i32) - } - } - Type::IntSet(ref values) => { - if values.is_empty() { - return Err(FlatZincError::MapError { - message: format!("Empty domain for variable {}", decl.name), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - } - let min = *values.iter().min().unwrap(); - let max = *values.iter().max().unwrap(); - // TODO: Handle sparse domains more efficiently - self.model.int(min as i32, max as i32) - } - Type::Float => self.model.float(f64::NEG_INFINITY, f64::INFINITY), - Type::FloatRange(min, max) => self.model.float(min, max), - _ => { - return Err(FlatZincError::UnsupportedFeature { - feature: format!("Variable type: {:?}", inner_type), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - } - }, - Type::Array { index_sets, element_type } => { - // Three cases for array declarations: - // 1. Parameter arrays: array [1..n] of int: coeffs = [1, 2, 3]; - // 2. Variable arrays (collect): array [...] = [var1, var2, ...] - // 3. Variable arrays (create): array [1..n] of var int: arr - - // Check if this is a parameter array (non-var type with initialization) - if let Some(ref init) = decl.init_value { - // Detect parameter integer arrays - match **element_type { - Type::Int | Type::IntRange(..) | Type::IntSet(..) => { - // This is a parameter int array: array [1..n] of int: name = [values]; - if let Expr::ArrayLit(elements) = init { - let values: Result, _> = elements.iter() - .map(|e| self.extract_int(e)) - .collect(); - - if let Ok(int_values) = values { - self.param_int_arrays.insert(decl.name.clone(), int_values); - return Ok(()); // Parameter arrays don't create variables - } - } - } - Type::Bool => { - // This is a parameter bool array: array [1..n] of bool: name = [values]; - if let Expr::ArrayLit(elements) = init { - let values: Result, _> = elements.iter() - .map(|e| match e { - Expr::BoolLit(b) => Ok(*b), - _ => Err(FlatZincError::MapError { - message: "Expected boolean literal in bool array".to_string(), - line: Some(decl.location.line), - column: Some(decl.location.column), - }), - }) - .collect(); - - if let Ok(bool_values) = values { - self.param_bool_arrays.insert(decl.name.clone(), bool_values); - return Ok(()); // Parameter arrays don't create variables - } - } - } - _ => {} - } - } - - // If not a parameter array, handle as variable array - if let Some(ref init) = decl.init_value { - // Case 2: Array collects existing variables/constants - match init { - Expr::ArrayLit(elements) => { - let mut var_ids = Vec::new(); - for elem in elements { - match elem { - Expr::Ident(name) => { - // Reference to existing variable - let var_id = self.var_map.get(name).ok_or_else(|| { - FlatZincError::MapError { - message: format!("Undefined variable '{}' in array", name), - line: Some(decl.location.line), - column: Some(decl.location.column), - } - })?; - var_ids.push(*var_id); - } - Expr::IntLit(val) => { - // Constant integer - create a fixed variable - let const_var = self.model.int(*val as i32, *val as i32); - var_ids.push(const_var); - } - Expr::BoolLit(b) => { - // Constant boolean - create a fixed variable (0 or 1) - let val = if *b { 1 } else { 0 }; - let const_var = self.model.int(val, val); - var_ids.push(const_var); - } - Expr::Range(start, end) => { - // Range expression: expand [1..10] to [1,2,3,...,10] - let start_val = match **start { - Expr::IntLit(v) => v, - _ => return Err(FlatZincError::MapError { - message: "Range start must be integer literal".to_string(), - line: Some(decl.location.line), - column: Some(decl.location.column), - }), - }; - let end_val = match **end { - Expr::IntLit(v) => v, - _ => return Err(FlatZincError::MapError { - message: "Range end must be integer literal".to_string(), - line: Some(decl.location.line), - column: Some(decl.location.column), - }), - }; - // Expand range into individual constants - for val in start_val..=end_val { - let const_var = self.model.int(val as i32, val as i32); - var_ids.push(const_var); - } - } - Expr::SetLit(values) => { - // Set literal in array: {1, 2, 3} - currently not supported - // FlatZinc uses sets, but Selen doesn't have set variables yet - // For now, we'll skip/ignore set elements or create a placeholder - // This allows parsing to continue for files with set literals - return Err(FlatZincError::UnsupportedFeature { - feature: format!("Set literals in arrays not yet supported. Found set with {} elements", values.len()), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - } - Expr::ArrayAccess { array, index } => { - // Array access in array literal: x[1] - // Evaluate the array access to get the variable - let var = self.evaluate_array_access(array, index)?; - var_ids.push(var); - } - _ => { - return Err(FlatZincError::UnsupportedFeature { - feature: format!("Array element expression: {:?}", elem), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - } - } - } - // Store the array mapping - self.array_map.insert(decl.name.clone(), var_ids); - return Ok(()); // Arrays don't create new variables - } - _ => { - return Err(FlatZincError::UnsupportedFeature { - feature: format!("Array initialization: {:?}", init), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - } - } - } else { - // Case 2: Create new array of variables (no initialization) - // e.g., array [1..5] of var 1..5: animal - match **element_type { - Type::Var(ref inner) => { - match **inner { - Type::IntRange(min, max) => { - // Determine array size from index_sets - // For now, assume single index set [1..n] - let size = if let Some(IndexSet::Range(start, end)) = index_sets.first() { - (end - start + 1) as usize - } else { - return Err(FlatZincError::UnsupportedFeature { - feature: "Array with complex index sets".to_string(), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - }; - - // Create variables for each array element - let var_ids: Vec = (0..size) - .map(|_| self.model.int(min as i32, max as i32)) - .collect(); - - self.array_map.insert(decl.name.clone(), var_ids); - return Ok(()); - } - Type::Int => { - // Unbounded integer arrays are approximated using inferred bounds - let (min_bound, max_bound) = self.unbounded_int_bounds; - - let size = if let Some(IndexSet::Range(start, end)) = index_sets.first() { - (end - start + 1) as usize - } else { - return Err(FlatZincError::UnsupportedFeature { - feature: "Array with complex index sets".to_string(), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - }; - - let var_ids: Vec = (0..size) - .map(|_| self.model.int(min_bound, max_bound)) - .collect(); - - self.array_map.insert(decl.name.clone(), var_ids); - return Ok(()); - } - Type::Bool => { - // Boolean array: array [1..n] of var bool: flags - let size = if let Some(IndexSet::Range(start, end)) = index_sets.first() { - (end - start + 1) as usize - } else { - return Err(FlatZincError::UnsupportedFeature { - feature: "Array with complex index sets".to_string(), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - }; - - let var_ids: Vec = (0..size) - .map(|_| self.model.bool()) - .collect(); - - self.array_map.insert(decl.name.clone(), var_ids); - return Ok(()); - } - _ => { - return Err(FlatZincError::UnsupportedFeature { - feature: format!("Array element type: {:?}", inner), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - } - } - } - Type::Bool => { - // Non-var boolean arrays: array [1..n] of bool (should be parameter arrays) - // These should have been caught earlier as parameter arrays if initialized - return Err(FlatZincError::UnsupportedFeature { - feature: "Non-variable boolean arrays without initialization".to_string(), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - } - _ => { - return Err(FlatZincError::UnsupportedFeature { - feature: format!("Array element type: {:?}", element_type), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - } - } - } - } - _ => { - return Err(FlatZincError::MapError { - message: format!("Unexpected variable type: {:?}", decl.var_type), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - } - }; - - // Handle initialization - if let Some(ref init) = decl.init_value { - match init { - Expr::IntLit(val) => { - self.model.new(var_id.eq(*val as i32)); - } - Expr::BoolLit(val) => { - self.model.new(var_id.eq(if *val { 1 } else { 0 })); - } - Expr::FloatLit(val) => { - self.model.new(var_id.eq(*val)); - } - Expr::Ident(var_name) => { - // Variable-to-variable initialization: var int: c4 = M; - // Post an equality constraint: c4 = M - let source_var = self.var_map.get(var_name).ok_or_else(|| { - FlatZincError::MapError { - message: format!("Variable '{}' not found for initialization", var_name), - line: Some(decl.location.line), - column: Some(decl.location.column), - } - })?; - self.model.new(var_id.eq(*source_var)); - } - Expr::ArrayAccess { array, index } => { - // Array element initialization: var int: x = arr[3]; - // Evaluate the array access and post an equality constraint - let source_var = self.evaluate_array_access(array, index)?; - self.model.new(var_id.eq(source_var)); - } - _ => { - return Err(FlatZincError::MapError { - message: format!("Complex initialization not yet supported: {:?}", init), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - } - } - } - - self.var_map.insert(decl.name.clone(), var_id); - Ok(()) - } - - /// Map a constraint to Selen constraint - fn map_constraint(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - match constraint.predicate.as_str() { - "int_eq" => self.map_int_eq(constraint), - "int_ne" => self.map_int_ne(constraint), - "int_lt" => self.map_int_lt(constraint), - "int_le" => self.map_int_le(constraint), - "int_gt" => self.map_int_gt(constraint), - "int_ge" => self.map_int_ge(constraint), - "int_lin_eq" => self.map_int_lin_eq(constraint), - "int_lin_le" => self.map_int_lin_le(constraint), - "int_lin_ne" => self.map_int_lin_ne(constraint), - "int_lin_eq_reif" => self.map_int_lin_eq_reif(constraint), - "int_lin_le_reif" => self.map_int_lin_le_reif(constraint), - "fzn_all_different_int" | "all_different_int" | "all_different" => self.map_all_different(constraint), - "sort" => self.map_sort(constraint), - "table_int" => self.map_table_int(constraint), - "table_bool" => self.map_table_bool(constraint), - "lex_less" | "lex_less_int" => self.map_lex_less(constraint), - "lex_lesseq" | "lex_lesseq_int" => self.map_lex_lesseq(constraint), - "nvalue" => self.map_nvalue(constraint), - "fixed_fzn_cumulative" | "cumulative" => self.map_fixed_fzn_cumulative(constraint), - "var_fzn_cumulative" => self.map_var_fzn_cumulative(constraint), - "int_eq_reif" => self.map_int_eq_reif(constraint), - "int_ne_reif" => self.map_int_ne_reif(constraint), - "int_lt_reif" => self.map_int_lt_reif(constraint), - "int_le_reif" => self.map_int_le_reif(constraint), - "int_gt_reif" => self.map_int_gt_reif(constraint), - "int_ge_reif" => self.map_int_ge_reif(constraint), - "bool_clause" => self.map_bool_clause(constraint), - // Array aggregations - "array_int_minimum" | "minimum_int" => self.map_array_int_minimum(constraint), - "array_int_maximum" | "maximum_int" => self.map_array_int_maximum(constraint), - "array_bool_and" => self.map_array_bool_and(constraint), - "array_bool_or" => self.map_array_bool_or(constraint), - // Bool-int conversion - "bool2int" => self.map_bool2int(constraint), - "bool_eq_reif" => self.map_bool_eq_reif(constraint), - // Count constraints - "count_eq" | "count" => self.map_count_eq(constraint), - // Element constraints (array indexing) - "array_var_int_element" => self.map_array_var_int_element(constraint), - "array_int_element" => self.map_array_int_element(constraint), - "array_var_bool_element" => self.map_array_var_bool_element(constraint), - "array_bool_element" => self.map_array_bool_element(constraint), - // Arithmetic operations - "int_abs" => self.map_int_abs(constraint), - "int_plus" => self.map_int_plus(constraint), - "int_minus" => self.map_int_minus(constraint), - "int_times" => self.map_int_times(constraint), - "int_div" => self.map_int_div(constraint), - "int_mod" => self.map_int_mod(constraint), - "int_max" => self.map_int_max(constraint), - "int_min" => self.map_int_min(constraint), - // Boolean constraints - "bool_le" => self.map_bool_le(constraint), - "bool_le_reif" => self.map_bool_le_reif(constraint), - "bool_eq" => self.map_bool_eq(constraint), - "bool_not" => self.map_bool_not(constraint), - "bool_xor" => self.map_bool_xor(constraint), - // Set constraints - "set_in_reif" => self.map_set_in_reif(constraint), - "set_in" => self.map_set_in(constraint), - // Global cardinality - "global_cardinality" => self.map_global_cardinality(constraint), - "global_cardinality_low_up_closed" => self.map_global_cardinality_low_up_closed(constraint), - _ => { - Err(FlatZincError::UnsupportedFeature { - feature: format!("Constraint: {}", constraint.predicate), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }) - } - } - } -} - -/// Infer reasonable bounds for unbounded integer variables by scanning the model -fn infer_unbounded_int_bounds(ast: &FlatZincModel) -> (i32, i32) { - let mut min_bound = 0i32; - let mut max_bound = 0i32; - let mut found_any = false; - - // Scan all variable declarations to find bounded integer ranges - for var_decl in &ast.var_decls { - match &var_decl.var_type { - Type::Var(inner_type) => { - if let Type::IntRange(min, max) = **inner_type { - min_bound = min_bound.min(min as i32); - max_bound = max_bound.max(max as i32); - found_any = true; - } - } - Type::Array { element_type, .. } => { - if let Type::Var(inner) = &**element_type { - if let Type::IntRange(min, max) = **inner { - min_bound = min_bound.min(min as i32); - max_bound = max_bound.max(max as i32); - found_any = true; - } - } - } - _ => {} - } - } - - // If we found bounded variables, expand their range slightly for safety - if found_any { - // Expand by 10x or at least to ±100 - let range = max_bound - min_bound; - let expansion = range.max(100); - const MAX_BOUND: i32 = (crate::variables::domain::MAX_SPARSE_SET_DOMAIN_SIZE / 2) as i32; - min_bound = (min_bound - expansion).max(-MAX_BOUND); - max_bound = (max_bound + expansion).min(MAX_BOUND); - (min_bound, max_bound) - } else { - // No bounded variables found, use default reasonable range - const DEFAULT_BOUND: i32 = (crate::variables::domain::MAX_SPARSE_SET_DOMAIN_SIZE / 2) as i32; - (-DEFAULT_BOUND, DEFAULT_BOUND) - } -} - -/// Map FlatZinc AST to an existing Selen Model -pub fn map_to_model_mut(ast: FlatZincModel, model: &mut Model) -> FlatZincResult<()> { - // First pass: infer reasonable bounds for unbounded variables - let unbounded_bounds = infer_unbounded_int_bounds(&ast); - - let mut ctx = MappingContext::new(model, unbounded_bounds); - - // Map variable declarations - for var_decl in &ast.var_decls { - ctx.map_var_decl(var_decl)?; - } - - // Map constraints - for constraint in &ast.constraints { - ctx.map_constraint(constraint)?; - } - - // TODO: Handle solve goal (minimize/maximize) - - Ok(()) -} - -/// Map FlatZinc AST to a new Selen Model -pub fn map_to_model(ast: FlatZincModel) -> FlatZincResult { - let mut model = Model::default(); - map_to_model_mut(ast, &mut model)?; - Ok(model) -} diff --git a/src/flatzinc/mapper/constraint_mappers.rs b/src/flatzinc/mapper/constraint_mappers.rs deleted file mode 100644 index 0eef83a..0000000 --- a/src/flatzinc/mapper/constraint_mappers.rs +++ /dev/null @@ -1,1147 +0,0 @@ -//! Constraint mapping functions -//! -//! Maps individual FlatZinc constraint predicates to Selen constraints. -//! -//! ## Organization -//! -//! This file contains constraint mappers organized by category: -//! -//! 1. **Comparison Constraints** (lines ~15-220) -//! - int_eq, int_ne, int_lt, int_le, int_gt, int_ge -//! -//! 2. **Linear Constraints** (lines ~220-300) -//! - int_lin_eq, int_lin_le, int_lin_ne -//! -//! 3. **Global Constraints** (lines ~300-315) -//! - all_different -//! -//! 4. **Reified Constraints** (lines ~315-545) -//! - int_eq_reif, int_ne_reif, int_lt_reif, int_le_reif, int_gt_reif, int_ge_reif -//! -//! 5. **Boolean Constraints** (lines ~545-690) -//! - bool_clause, array_bool_and, array_bool_or, bool2int, bool_le -//! -//! 6. **Array Constraints** (lines ~575-645) -//! - array_int_minimum, array_int_maximum -//! -//! 7. **Counting Constraints** (lines ~690-720) -//! - count_eq -//! -//! 8. **Element Constraints** (lines ~720-900) -//! - array_var_int_element, array_int_element, array_var_bool_element, array_bool_element -//! -//! 9. **Arithmetic Constraints** (lines ~900-1100) -//! - int_abs, int_plus, int_minus, int_times, int_div, int_mod, int_max, int_min -//! -//! TODO: Consider splitting into separate modules when file exceeds ~1500 lines - -use crate::flatzinc::ast::*; -use crate::flatzinc::error::{FlatZincError, FlatZincResult}; -use crate::flatzinc::mapper::MappingContext; -use crate::runtime_api::{VarIdExt, ModelExt}; -use crate::variables::VarId; - -impl<'a> MappingContext<'a> { - // ═════════════════════════════════════════════════════════════════════════ - // 📊 COMPARISON CONSTRAINTS - // ═════════════════════════════════════════════════════════════════════════ - - /// Map int_eq constraint: x = y or x = constant - pub(super) fn map_int_eq(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "int_eq requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - // Handle both: int_eq(var, const) and int_eq(const, var) - match (&constraint.args[0], &constraint.args[1]) { - // var = var - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - self.model.new(x.eq(y)); - } - // var = const - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::IntLit(val)) => { - let x = self.get_var(&constraint.args[0])?; - self.model.new(x.eq(*val as i32)); - } - // const = var (swap to var = const) - (Expr::IntLit(val), Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let y = self.get_var(&constraint.args[1])?; - self.model.new(y.eq(*val as i32)); - } - _ => { - return Err(FlatZincError::MapError { - message: "Unsupported argument types for int_eq".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - } - - Ok(()) - } - - pub(super) fn map_int_ne(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "int_ne requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - match (&constraint.args[0], &constraint.args[1]) { - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - self.model.new(x.ne(y)); - } - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::IntLit(val)) => { - let x = self.get_var(&constraint.args[0])?; - self.model.new(x.ne(*val as i32)); - } - (Expr::IntLit(val), Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let y = self.get_var(&constraint.args[1])?; - self.model.new(y.ne(*val as i32)); - } - _ => { - return Err(FlatZincError::MapError { - message: "Unsupported argument types for int_ne".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - } - Ok(()) - } - - pub(super) fn map_int_lt(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "int_lt requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - match (&constraint.args[0], &constraint.args[1]) { - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - self.model.new(x.lt(y)); - } - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::IntLit(val)) => { - let x = self.get_var(&constraint.args[0])?; - self.model.new(x.lt(*val as i32)); - } - (Expr::IntLit(val), Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let y = self.get_var(&constraint.args[1])?; - self.model.new(y.gt(*val as i32)); // const < var => var > const - } - _ => { - return Err(FlatZincError::MapError { - message: "Unsupported argument types for int_lt".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - } - Ok(()) - } - - pub(super) fn map_int_le(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "int_le requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - match (&constraint.args[0], &constraint.args[1]) { - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - self.model.new(x.le(y)); - } - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::IntLit(val)) => { - let x = self.get_var(&constraint.args[0])?; - self.model.new(x.le(*val as i32)); - } - (Expr::IntLit(val), Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let y = self.get_var(&constraint.args[1])?; - self.model.new(y.ge(*val as i32)); // const <= var => var >= const - } - _ => { - return Err(FlatZincError::MapError { - message: "Unsupported argument types for int_le".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - } - Ok(()) - } - - pub(super) fn map_int_gt(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "int_gt requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - match (&constraint.args[0], &constraint.args[1]) { - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - self.model.new(x.gt(y)); - } - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::IntLit(val)) => { - let x = self.get_var(&constraint.args[0])?; - self.model.new(x.gt(*val as i32)); - } - (Expr::IntLit(val), Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let y = self.get_var(&constraint.args[1])?; - self.model.new(y.lt(*val as i32)); // const > var => var < const - } - _ => { - return Err(FlatZincError::MapError { - message: "Unsupported argument types for int_gt".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - } - Ok(()) - } - - pub(super) fn map_int_ge(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "int_ge requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - match (&constraint.args[0], &constraint.args[1]) { - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - self.model.new(x.ge(y)); - } - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::IntLit(val)) => { - let x = self.get_var(&constraint.args[0])?; - self.model.new(x.ge(*val as i32)); - } - (Expr::IntLit(val), Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let y = self.get_var(&constraint.args[1])?; - self.model.new(y.le(*val as i32)); // const >= var => var <= const - } - _ => { - return Err(FlatZincError::MapError { - message: "Unsupported argument types for int_ge".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - } - Ok(()) - } - - /// Map int_lin_eq: Σ(coeffs[i] * vars[i]) = constant - pub(super) fn map_int_lin_eq(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_lin_eq requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let coeffs = self.extract_int_array(&constraint.args[0])?; - let var_ids = self.extract_var_array(&constraint.args[1])?; - let constant = self.extract_int(&constraint.args[2])?; - - // Create sum using Model's API - let scaled_vars: Vec = coeffs - .iter() - .zip(var_ids.iter()) - .map(|(&coeff, &var)| self.model.mul(var, crate::variables::Val::ValI(coeff))) - .collect(); - - let sum_var = self.model.sum(&scaled_vars); - self.model.new(sum_var.eq(constant)); - Ok(()) - } - - /// Map int_lin_le: Σ(coeffs[i] * vars[i]) ≤ constant - pub(super) fn map_int_lin_le(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_lin_le requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let coeffs = self.extract_int_array(&constraint.args[0])?; - let var_ids = self.extract_var_array(&constraint.args[1])?; - let constant = self.extract_int(&constraint.args[2])?; - - let scaled_vars: Vec = coeffs - .iter() - .zip(var_ids.iter()) - .map(|(&coeff, &var)| self.model.mul(var, crate::variables::Val::ValI(coeff))) - .collect(); - - let sum_var = self.model.sum(&scaled_vars); - self.model.new(sum_var.le(constant)); - Ok(()) - } - - /// Map int_lin_ne: Σ(coeffs[i] * vars[i]) ≠ constant - pub(super) fn map_int_lin_ne(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_lin_ne requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let coeffs = self.extract_int_array(&constraint.args[0])?; - let var_ids = self.extract_var_array(&constraint.args[1])?; - let constant = self.extract_int(&constraint.args[2])?; - - let scaled_vars: Vec = coeffs - .iter() - .zip(var_ids.iter()) - .map(|(&coeff, &var)| self.model.mul(var, crate::variables::Val::ValI(coeff))) - .collect(); - - let sum_var = self.model.sum(&scaled_vars); - - // Use runtime API to post not-equals constraint: sum ≠ constant - self.model.c(sum_var).ne(constant); - Ok(()) - } - - // ═════════════════════════════════════════════════════════════════════════ - // 🌐 GLOBAL CONSTRAINTS - // ═════════════════════════════════════════════════════════════════════════ - - /// Map all_different constraint - pub(super) fn map_all_different(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 1 { - return Err(FlatZincError::MapError { - message: "all_different requires 1 argument (array of variables)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let var_ids = self.extract_var_array(&constraint.args[0])?; - self.model.alldiff(&var_ids); - Ok(()) - } - - // ═════════════════════════════════════════════════════════════════════════ - // 🔄 REIFIED CONSTRAINTS - // ═════════════════════════════════════════════════════════════════════════ - - /// Map int_eq_reif: b ⇔ (x = y) - pub(super) fn map_int_eq_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_eq_reif requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let b = self.get_var(&constraint.args[2])?; - - match (&constraint.args[0], &constraint.args[1]) { - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - self.model.int_eq_reif(x, y, b); - } - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::IntLit(val)) => { - let x = self.get_var(&constraint.args[0])?; - let const_var = self.model.int(*val as i32, *val as i32); - self.model.int_eq_reif(x, const_var, b); - } - (Expr::IntLit(val), Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let y = self.get_var(&constraint.args[1])?; - let const_var = self.model.int(*val as i32, *val as i32); - self.model.int_eq_reif(const_var, y, b); - } - _ => { - return Err(FlatZincError::MapError { - message: "Unsupported argument types for int_eq_reif".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - } - Ok(()) - } - - pub(super) fn map_int_ne_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_ne_reif requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let b = self.get_var(&constraint.args[2])?; - - match (&constraint.args[0], &constraint.args[1]) { - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - self.model.int_ne_reif(x, y, b); - } - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::IntLit(val)) => { - let x = self.get_var(&constraint.args[0])?; - let const_var = self.model.int(*val as i32, *val as i32); - self.model.int_ne_reif(x, const_var, b); - } - (Expr::IntLit(val), Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let y = self.get_var(&constraint.args[1])?; - let const_var = self.model.int(*val as i32, *val as i32); - self.model.int_ne_reif(const_var, y, b); - } - _ => { - return Err(FlatZincError::MapError { - message: "Unsupported argument types for int_ne_reif".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - } - Ok(()) - } - - pub(super) fn map_int_lt_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_lt_reif requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let b = self.get_var(&constraint.args[2])?; - - match (&constraint.args[0], &constraint.args[1]) { - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - self.model.int_lt_reif(x, y, b); - } - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::IntLit(val)) => { - let x = self.get_var(&constraint.args[0])?; - let const_var = self.model.int(*val as i32, *val as i32); - self.model.int_lt_reif(x, const_var, b); - } - (Expr::IntLit(val), Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let y = self.get_var(&constraint.args[1])?; - let const_var = self.model.int(*val as i32, *val as i32); - self.model.int_lt_reif(const_var, y, b); - } - _ => { - return Err(FlatZincError::MapError { - message: "Unsupported argument types for int_lt_reif".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - } - Ok(()) - } - - pub(super) fn map_int_le_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_le_reif requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let b = self.get_var(&constraint.args[2])?; - - match (&constraint.args[0], &constraint.args[1]) { - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - self.model.int_le_reif(x, y, b); - } - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::IntLit(val)) => { - let x = self.get_var(&constraint.args[0])?; - let const_var = self.model.int(*val as i32, *val as i32); - self.model.int_le_reif(x, const_var, b); - } - (Expr::IntLit(val), Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let y = self.get_var(&constraint.args[1])?; - let const_var = self.model.int(*val as i32, *val as i32); - self.model.int_le_reif(const_var, y, b); - } - _ => { - return Err(FlatZincError::MapError { - message: "Unsupported argument types for int_le_reif".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - } - Ok(()) - } - - pub(super) fn map_int_gt_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_gt_reif requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let b = self.get_var(&constraint.args[2])?; - - match (&constraint.args[0], &constraint.args[1]) { - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - self.model.int_gt_reif(x, y, b); - } - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::IntLit(val)) => { - let x = self.get_var(&constraint.args[0])?; - let const_var = self.model.int(*val as i32, *val as i32); - self.model.int_gt_reif(x, const_var, b); - } - (Expr::IntLit(val), Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let y = self.get_var(&constraint.args[1])?; - let const_var = self.model.int(*val as i32, *val as i32); - self.model.int_gt_reif(const_var, y, b); - } - _ => { - return Err(FlatZincError::MapError { - message: "Unsupported argument types for int_gt_reif".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - } - Ok(()) - } - - pub(super) fn map_int_ge_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_ge_reif requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let b = self.get_var(&constraint.args[2])?; - - match (&constraint.args[0], &constraint.args[1]) { - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - self.model.int_ge_reif(x, y, b); - } - (Expr::Ident(_) | Expr::ArrayAccess { .. }, Expr::IntLit(val)) => { - let x = self.get_var(&constraint.args[0])?; - let const_var = self.model.int(*val as i32, *val as i32); - self.model.int_ge_reif(x, const_var, b); - } - (Expr::IntLit(val), Expr::Ident(_) | Expr::ArrayAccess { .. }) => { - let y = self.get_var(&constraint.args[1])?; - let const_var = self.model.int(*val as i32, *val as i32); - self.model.int_ge_reif(const_var, y, b); - } - _ => { - return Err(FlatZincError::MapError { - message: "Unsupported argument types for int_ge_reif".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - } - Ok(()) - } - - /// Map bool_clause: (∨ pos[i]) ∨ (∨ ¬neg[i]) - pub(super) fn map_bool_clause(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "bool_clause requires 2 arguments (positive and negative literals)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let pos_vars = self.extract_var_array(&constraint.args[0])?; - let neg_vars = self.extract_var_array(&constraint.args[1])?; - - // Build clause: (∨ pos[i]) ∨ (∨ ¬neg[i]) - // For negated literals, create: (1 - var) which gives NOT - let mut all_literals = pos_vars; - - for &var in &neg_vars { - // Create (1 - var) for negation (since bool is 0/1) - let one_minus_var = self.model.sub(crate::variables::Val::ValI(1), var); - all_literals.push(one_minus_var); - } - - if !all_literals.is_empty() { - let clause_result = self.model.bool_or(&all_literals); - // The clause must be true - self.model.new(clause_result.eq(1)); - } - - Ok(()) - } - - /// Map array_int_minimum: min = minimum(array) - pub(super) fn map_array_int_minimum(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "array_int_minimum requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let min_var = self.get_var(&constraint.args[0])?; - let arr_vars = self.extract_var_array(&constraint.args[1])?; - let min_result = self.model.min(&arr_vars).map_err(|e| FlatZincError::MapError { - message: format!("Failed to create min: {}", e), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - })?; - self.model.new(min_var.eq(min_result)); - Ok(()) - } - - /// Map array_int_maximum: max = maximum(array) - pub(super) fn map_array_int_maximum(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "array_int_maximum requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let max_var = self.get_var(&constraint.args[0])?; - let arr_vars = self.extract_var_array(&constraint.args[1])?; - let max_result = self.model.max(&arr_vars).map_err(|e| FlatZincError::MapError { - message: format!("Failed to create max: {}", e), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - })?; - self.model.new(max_var.eq(max_result)); - Ok(()) - } - - /// Map array_bool_and: result = AND of all array elements - pub(super) fn map_array_bool_and(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "array_bool_and requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let arr_vars = self.extract_var_array(&constraint.args[0])?; - let result_var = self.get_var(&constraint.args[1])?; - - // result = AND of all elements: result ⇔ (x[0] ∧ x[1] ∧ ... ∧ x[n]) - if arr_vars.is_empty() { - // Empty array: result = true - self.model.new(result_var.eq(1)); - } else if arr_vars.len() == 1 { - self.model.new(result_var.eq(arr_vars[0])); - } else { - // Use Model's bool_and for n-ary conjunction - let and_result = self.model.bool_and(&arr_vars); - self.model.new(result_var.eq(and_result)); - } - Ok(()) - } - - /// Map array_bool_or: result = OR of all array elements - pub(super) fn map_array_bool_or(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "array_bool_or requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let arr_vars = self.extract_var_array(&constraint.args[0])?; - let result_var = self.get_var(&constraint.args[1])?; - - // result = OR of all elements: result ⇔ (x[0] ∨ x[1] ∨ ... ∨ x[n]) - if arr_vars.is_empty() { - // Empty array: result = false - self.model.new(result_var.eq(0)); - } else if arr_vars.len() == 1 { - self.model.new(result_var.eq(arr_vars[0])); - } else { - // Use Model's bool_or for n-ary disjunction - let or_result = self.model.bool_or(&arr_vars); - self.model.new(result_var.eq(or_result)); - } - Ok(()) - } - - /// Map bool2int: int_var = bool_var (bool is 0/1) - pub(super) fn map_bool2int(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "bool2int requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let bool_var = self.get_var(&constraint.args[0])?; - let int_var = self.get_var(&constraint.args[1])?; - // bool2int: int_var = bool_var (bool is 0/1 in Selen) - self.model.new(int_var.eq(bool_var)); - Ok(()) - } - - /// Map count_eq: count = |{i : array[i] = value}| - pub(super) fn map_count_eq(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "count_eq requires 3 arguments (array, value, count)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let arr_vars = self.extract_var_array(&constraint.args[0])?; - let value = self.extract_int(&constraint.args[1])?; - let count_var = self.get_var(&constraint.args[2])?; - - // Use Selen's count constraint - self.model.count(&arr_vars, value, count_var); - Ok(()) - } - - /// Map array_var_int_element: array[index] = value - /// FlatZinc signature: array_var_int_element(index, array, value) - /// Note: FlatZinc uses 1-based indexing, Selen uses 0-based - pub(super) fn map_array_var_int_element(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "array_var_int_element requires 3 arguments (index, array, value)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - // Get index variable (1-based in FlatZinc) - let index_1based = self.get_var(&constraint.args[0])?; - - // Convert to 0-based index for Selen - // Create: index_0based = index_1based - 1 - let index_0based = self.model.sub(index_1based, crate::variables::Val::ValI(1)); - - // Get array - let array = self.extract_var_array(&constraint.args[1])?; - - // Get value (can be variable or constant) - let value = match &constraint.args[2] { - Expr::Ident(_) => self.get_var(&constraint.args[2])?, - Expr::IntLit(val) => { - // Convert constant to fixed variable - self.model.int(*val as i32, *val as i32) - } - _ => { - return Err(FlatZincError::MapError { - message: "Unsupported value type in array_var_int_element".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - }; - - // Apply element constraint: array[index_0based] = value - self.model.elem(&array, index_0based, value); - Ok(()) - } - - /// Map array_int_element: array[index] = value (with constant array) - /// FlatZinc signature: array_int_element(index, array, value) - /// Note: FlatZinc uses 1-based indexing, Selen uses 0-based - pub(super) fn map_array_int_element(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "array_int_element requires 3 arguments (index, array, value)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - // Get index variable (1-based in FlatZinc) - let index_1based = self.get_var(&constraint.args[0])?; - - // Convert to 0-based index for Selen - let index_0based = self.model.sub(index_1based, crate::variables::Val::ValI(1)); - - // Get array of constants and convert to fixed variables - let const_array = self.extract_int_array(&constraint.args[1])?; - let array: Vec = const_array.iter() - .map(|&val| self.model.int(val, val)) - .collect(); - - // Get value (can be variable or constant) - let value = match &constraint.args[2] { - Expr::Ident(_) => self.get_var(&constraint.args[2])?, - Expr::IntLit(val) => { - self.model.int(*val as i32, *val as i32) - } - _ => { - return Err(FlatZincError::MapError { - message: "Unsupported value type in array_int_element".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - }; - - // Apply element constraint: array[index_0based] = value - self.model.elem(&array, index_0based, value); - Ok(()) - } - - /// Map array_var_bool_element: array[index] = value (boolean version) - /// FlatZinc signature: array_var_bool_element(index, array, value) - /// Note: FlatZinc uses 1-based indexing, Selen uses 0-based - pub(super) fn map_array_var_bool_element(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "array_var_bool_element requires 3 arguments (index, array, value)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - // Get index variable (1-based in FlatZinc) - let index_1based = self.get_var(&constraint.args[0])?; - - // Convert to 0-based index for Selen - let index_0based = self.model.sub(index_1based, crate::variables::Val::ValI(1)); - - // Get array (booleans are represented as 0/1 variables) - let array = self.extract_var_array(&constraint.args[1])?; - - // Get value (can be variable or constant) - let value = match &constraint.args[2] { - Expr::Ident(_) => self.get_var(&constraint.args[2])?, - Expr::BoolLit(b) => { - let val = if *b { 1 } else { 0 }; - self.model.int(val, val) - } - _ => { - return Err(FlatZincError::MapError { - message: "Unsupported value type in array_var_bool_element".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - }; - - // Apply element constraint: array[index_0based] = value - self.model.elem(&array, index_0based, value); - Ok(()) - } - - /// Map array_bool_element: array[index] = value (with constant boolean array) - /// FlatZinc signature: array_bool_element(index, array, value) - /// Note: FlatZinc uses 1-based indexing, Selen uses 0-based - pub(super) fn map_array_bool_element(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "array_bool_element requires 3 arguments (index, array, value)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - // Get index variable (1-based in FlatZinc) - let index_1based = self.get_var(&constraint.args[0])?; - - // Convert to 0-based index for Selen - let index_0based = self.model.sub(index_1based, crate::variables::Val::ValI(1)); - - // Get array of boolean constants and convert to 0/1 fixed variables - let array: Vec = if let Expr::ArrayLit(elements) = &constraint.args[1] { - elements.iter() - .map(|elem| { - if let Expr::BoolLit(b) = elem { - let val = if *b { 1 } else { 0 }; - Ok(self.model.int(val, val)) - } else { - Err(FlatZincError::MapError { - message: "Expected boolean literal in array_bool_element array".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }) - } - }) - .collect::>>()? - } else { - return Err(FlatZincError::MapError { - message: "Expected array literal in array_bool_element".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - }; - - // Get value (can be variable or constant) - let value = match &constraint.args[2] { - Expr::Ident(_) => self.get_var(&constraint.args[2])?, - Expr::BoolLit(b) => { - let val = if *b { 1 } else { 0 }; - self.model.int(val, val) - } - _ => { - return Err(FlatZincError::MapError { - message: "Unsupported value type in array_bool_element".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - }; - - // Apply element constraint: array[index_0based] = value - self.model.elem(&array, index_0based, value); - Ok(()) - } - - // ═════════════════════════════════════════════════════════════════════════ - // ➕ ARITHMETIC CONSTRAINTS - // ═════════════════════════════════════════════════════════════════════════ - - /// Map int_abs: result = |x| - /// FlatZinc signature: int_abs(x, result) - pub(super) fn map_int_abs(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "int_abs requires 2 arguments (x, result)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var(&constraint.args[0])?; - let result = self.get_var(&constraint.args[1])?; - - // Use Selen's abs constraint - let abs_x = self.model.abs(x); - - // Constrain result to equal abs(x) - self.model.new(abs_x.eq(result)); - Ok(()) - } - - /// Map int_plus: z = x + y - /// FlatZinc signature: int_plus(x, y, z) - pub(super) fn map_int_plus(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_plus requires 3 arguments (x, y, z)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - let z = self.get_var(&constraint.args[2])?; - - // Use Selen's add constraint: z = x + y - let sum = self.model.add(x, y); - self.model.new(sum.eq(z)); - Ok(()) - } - - /// Map int_minus: z = x - y - /// FlatZinc signature: int_minus(x, y, z) - pub(super) fn map_int_minus(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_minus requires 3 arguments (x, y, z)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - let z = self.get_var(&constraint.args[2])?; - - // Use Selen's sub constraint: z = x - y - let diff = self.model.sub(x, y); - self.model.new(diff.eq(z)); - Ok(()) - } - - /// Map int_times: z = x * y - /// FlatZinc signature: int_times(x, y, z) - pub(super) fn map_int_times(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_times requires 3 arguments (x, y, z)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - let z = self.get_var(&constraint.args[2])?; - - // Use Selen's mul constraint: z = x * y - let product = self.model.mul(x, y); - self.model.new(product.eq(z)); - Ok(()) - } - - /// Map int_div: z = x / y - /// FlatZinc signature: int_div(x, y, z) - pub(super) fn map_int_div(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_div requires 3 arguments (x, y, z)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - let z = self.get_var(&constraint.args[2])?; - - // Use Selen's div constraint: z = x / y - let quotient = self.model.div(x, y); - self.model.new(quotient.eq(z)); - Ok(()) - } - - /// Map int_mod: z = x mod y - /// FlatZinc signature: int_mod(x, y, z) - pub(super) fn map_int_mod(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_mod requires 3 arguments (x, y, z)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - let z = self.get_var(&constraint.args[2])?; - - // Use Selen's mod constraint: z = x mod y - let remainder = self.model.modulo(x, y); - self.model.new(remainder.eq(z)); - Ok(()) - } - - /// Map int_max: z = max(x, y) - /// FlatZinc signature: int_max(x, y, z) - pub(super) fn map_int_max(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_max requires 3 arguments (x, y, z)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - let z = self.get_var(&constraint.args[2])?; - - // Use Selen's max constraint: z = max([x, y]) - let max_xy = self.model.max(&[x, y]) - .map_err(|e| FlatZincError::MapError { - message: format!("Error creating max constraint: {}", e), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - })?; - self.model.new(max_xy.eq(z)); - Ok(()) - } - - /// Map int_min: z = min(x, y) - /// FlatZinc signature: int_min(x, y, z) - pub(super) fn map_int_min(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_min requires 3 arguments (x, y, z)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - let z = self.get_var(&constraint.args[2])?; - - // Use Selen's min constraint: z = min([x, y]) - let min_xy = self.model.min(&[x, y]) - .map_err(|e| FlatZincError::MapError { - message: format!("Error creating min constraint: {}", e), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - })?; - self.model.new(min_xy.eq(z)); - Ok(()) - } - - /// Map bool_le: x <= y for boolean variables - /// FlatZinc signature: bool_le(x, y) - pub(super) fn map_bool_le(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "bool_le requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - - // For boolean variables: x <= y is equivalent to (not x) or y - // Which is the same as x => y (implication) - self.model.new(x.le(y)); - Ok(()) - } -} diff --git a/src/flatzinc/mapper/constraints/arithmetic.rs b/src/flatzinc/mapper/constraints/arithmetic.rs deleted file mode 100644 index c06382c..0000000 --- a/src/flatzinc/mapper/constraints/arithmetic.rs +++ /dev/null @@ -1,197 +0,0 @@ -//! Arithmetic constraint mappers -//! -//! Maps FlatZinc arithmetic constraints (int_plus, int_minus, int_times, int_div, int_mod, int_abs, int_min, int_max) -//! to Selen constraint model. - -use crate::flatzinc::ast::*; -use crate::flatzinc::error::{FlatZincError, FlatZincResult}; -use crate::flatzinc::mapper::MappingContext; -use crate::runtime_api::{VarIdExt, ModelExt}; - -impl<'a> MappingContext<'a> { - /// Map int_abs: result = |x| - /// FlatZinc signature: int_abs(x, result) - pub(in crate::flatzinc::mapper) fn map_int_abs(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "int_abs requires 2 arguments (x, result)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let result = self.get_var_or_const(&constraint.args[1])?; - - // Use Selen's abs constraint - let abs_x = self.model.abs(x); - - // Constrain result to equal abs(x) - self.model.new(abs_x.eq(result)); - Ok(()) - } - - /// Map int_plus: z = x + y - /// FlatZinc signature: int_plus(x, y, z) - /// Accepts variables, literals, or array access for all arguments - pub(in crate::flatzinc::mapper) fn map_int_plus(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_plus requires 3 arguments (x, y, z)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - let z = self.get_var_or_const(&constraint.args[2])?; - - // Use Selen's add constraint: z = x + y - let sum = self.model.add(x, y); - self.model.new(sum.eq(z)); - Ok(()) - } - - /// Map int_minus: z = x - y - /// FlatZinc signature: int_minus(x, y, z) - /// Accepts variables, literals, or array access for all arguments - pub(in crate::flatzinc::mapper) fn map_int_minus(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_minus requires 3 arguments (x, y, z)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - let z = self.get_var_or_const(&constraint.args[2])?; - - // Use Selen's sub constraint: z = x - y - let diff = self.model.sub(x, y); - self.model.new(diff.eq(z)); - Ok(()) - } - - /// Map int_times: z = x * y - /// FlatZinc signature: int_times(x, y, z) - /// Accepts variables, literals, or array access for all arguments - pub(in crate::flatzinc::mapper) fn map_int_times(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_times requires 3 arguments (x, y, z)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - let z = self.get_var_or_const(&constraint.args[2])?; - - // Use Selen's mul constraint: z = x * y - let product = self.model.mul(x, y); - self.model.new(product.eq(z)); - Ok(()) - } - - /// Map int_div: z = x / y - /// FlatZinc signature: int_div(x, y, z) - /// Accepts variables, literals, or array access for all arguments - pub(in crate::flatzinc::mapper) fn map_int_div(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_div requires 3 arguments (x, y, z)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - let z = self.get_var_or_const(&constraint.args[2])?; - - // Use Selen's div constraint: z = x / y - let quotient = self.model.div(x, y); - self.model.new(quotient.eq(z)); - Ok(()) - } - - /// Map int_mod: z = x mod y - /// FlatZinc signature: int_mod(x, y, z) - /// Accepts variables, literals, or array access for all arguments - pub(in crate::flatzinc::mapper) fn map_int_mod(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_mod requires 3 arguments (x, y, z)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - let z = self.get_var_or_const(&constraint.args[2])?; - - // Use Selen's mod constraint: z = x mod y - let remainder = self.model.modulo(x, y); - self.model.new(remainder.eq(z)); - Ok(()) - } - - /// Map int_max: z = max(x, y) - /// FlatZinc signature: int_max(x, y, z) - /// Accepts variables, literals, or array access for all arguments - pub(in crate::flatzinc::mapper) fn map_int_max(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_max requires 3 arguments (x, y, z)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - let z = self.get_var_or_const(&constraint.args[2])?; - - // Use Selen's max constraint: z = max([x, y]) - let max_xy = self.model.max(&[x, y]) - .map_err(|e| FlatZincError::MapError { - message: format!("Error creating max constraint: {}", e), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - })?; - self.model.new(max_xy.eq(z)); - Ok(()) - } - - /// Map int_min: z = min(x, y) - /// FlatZinc signature: int_min(x, y, z) - /// Accepts variables, literals, or array access for all arguments - pub(in crate::flatzinc::mapper) fn map_int_min(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_min requires 3 arguments (x, y, z)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - let z = self.get_var_or_const(&constraint.args[2])?; - - // Use Selen's min constraint: z = min([x, y]) - let min_xy = self.model.min(&[x, y]) - .map_err(|e| FlatZincError::MapError { - message: format!("Error creating min constraint: {}", e), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - })?; - self.model.new(min_xy.eq(z)); - Ok(()) - } -} diff --git a/src/flatzinc/mapper/constraints/array.rs b/src/flatzinc/mapper/constraints/array.rs deleted file mode 100644 index abbe529..0000000 --- a/src/flatzinc/mapper/constraints/array.rs +++ /dev/null @@ -1,53 +0,0 @@ -//! Array constraint mappers -//! -//! Maps FlatZinc array constraints (array_int_minimum, array_int_maximum) -//! to Selen constraint model. - -use crate::flatzinc::ast::*; -use crate::flatzinc::error::{FlatZincError, FlatZincResult}; -use crate::flatzinc::mapper::MappingContext; -use crate::runtime_api::{VarIdExt, ModelExt}; - -impl<'a> MappingContext<'a> { - /// Map array_int_minimum: min = minimum(array) - pub(in crate::flatzinc::mapper) fn map_array_int_minimum(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "array_int_minimum requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let min_var = self.get_var_or_const(&constraint.args[0])?; - let arr_vars = self.extract_var_array(&constraint.args[1])?; - let min_result = self.model.min(&arr_vars).map_err(|e| FlatZincError::MapError { - message: format!("Failed to create min: {}", e), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - })?; - self.model.new(min_var.eq(min_result)); - Ok(()) - } - - /// Map array_int_maximum: max = maximum(array) - pub(in crate::flatzinc::mapper) fn map_array_int_maximum(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "array_int_maximum requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let max_var = self.get_var_or_const(&constraint.args[0])?; - let arr_vars = self.extract_var_array(&constraint.args[1])?; - let max_result = self.model.max(&arr_vars).map_err(|e| FlatZincError::MapError { - message: format!("Failed to create max: {}", e), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - })?; - self.model.new(max_var.eq(max_result)); - Ok(()) - } -} diff --git a/src/flatzinc/mapper/constraints/boolean.rs b/src/flatzinc/mapper/constraints/boolean.rs deleted file mode 100644 index 288c5fc..0000000 --- a/src/flatzinc/mapper/constraints/boolean.rs +++ /dev/null @@ -1,236 +0,0 @@ -//! Boolean constraint mappers -//! -//! Maps FlatZinc boolean constraints (bool_clause, array_bool_and, array_bool_or, bool2int, bool_le) -//! to Selen constraint model. - -use crate::flatzinc::ast::*; -use crate::flatzinc::error::{FlatZincError, FlatZincResult}; -use crate::flatzinc::mapper::MappingContext; -use crate::runtime_api::{VarIdExt, ModelExt}; - -impl<'a> MappingContext<'a> { - /// Map bool_clause: (∨ pos[i]) ∨ (∨ ¬neg[i]) - pub(in crate::flatzinc::mapper) fn map_bool_clause(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "bool_clause requires 2 arguments (positive and negative literals)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let pos_vars = self.extract_var_array(&constraint.args[0])?; - let neg_vars = self.extract_var_array(&constraint.args[1])?; - - // Build clause: (∨ pos[i]) ∨ (∨ ¬neg[i]) - // For negated literals, create: (1 - var) which gives NOT - let mut all_literals = pos_vars; - - for &var in &neg_vars { - // Create (1 - var) for negation (since bool is 0/1) - let one_minus_var = self.model.sub(crate::variables::Val::ValI(1), var); - all_literals.push(one_minus_var); - } - - if !all_literals.is_empty() { - let clause_result = self.model.bool_or(&all_literals); - // The clause must be true - self.model.new(clause_result.eq(1)); - } - - Ok(()) - } - - /// Map array_bool_and: result = AND of all array elements - pub(in crate::flatzinc::mapper) fn map_array_bool_and(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "array_bool_and requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let arr_vars = self.extract_var_array(&constraint.args[0])?; - let result_var = self.get_var_or_const(&constraint.args[1])?; - - // result = AND of all elements: result ⇔ (x[0] ∧ x[1] ∧ ... ∧ x[n]) - if arr_vars.is_empty() { - // Empty array: result = true - self.model.new(result_var.eq(1)); - } else if arr_vars.len() == 1 { - self.model.new(result_var.eq(arr_vars[0])); - } else { - // Use Model's bool_and for n-ary conjunction - let and_result = self.model.bool_and(&arr_vars); - self.model.new(result_var.eq(and_result)); - } - Ok(()) - } - - /// Map array_bool_or: result = OR of all array elements - pub(in crate::flatzinc::mapper) fn map_array_bool_or(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "array_bool_or requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let arr_vars = self.extract_var_array(&constraint.args[0])?; - let result_var = self.get_var_or_const(&constraint.args[1])?; - - // result = OR of all elements: result ⇔ (x[0] ∨ x[1] ∨ ... ∨ x[n]) - if arr_vars.is_empty() { - // Empty array: result = false - self.model.new(result_var.eq(0)); - } else if arr_vars.len() == 1 { - self.model.new(result_var.eq(arr_vars[0])); - } else { - // Use Model's bool_or for n-ary disjunction - let or_result = self.model.bool_or(&arr_vars); - self.model.new(result_var.eq(or_result)); - } - Ok(()) - } - - /// Map bool2int: int_var = bool_var (bool is 0/1) - pub(in crate::flatzinc::mapper) fn map_bool2int(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "bool2int requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let bool_var = self.get_var_or_const(&constraint.args[0])?; - let int_var = self.get_var_or_const(&constraint.args[1])?; - // bool2int: int_var = bool_var (bool is 0/1 in Selen) - self.model.new(int_var.eq(bool_var)); - Ok(()) - } - - /// Map bool_le: x <= y for boolean variables - /// FlatZinc signature: bool_le(x, y) - pub(in crate::flatzinc::mapper) fn map_bool_le(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "bool_le requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - - // For boolean variables: x <= y is equivalent to (not x) or y - // Which is the same as x => y (implication) - self.model.new(x.le(y)); - Ok(()) - } - - /// Map bool_eq_reif: r ⇔ (x = y) for boolean variables - /// FlatZinc signature: bool_eq_reif(x, y, r) - pub(in crate::flatzinc::mapper) fn map_bool_eq_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "bool_eq_reif requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - let r = self.get_var_or_const(&constraint.args[2])?; - - // For booleans (0/1): r ⇔ (x = y) - // Since booleans are represented as 0/1 integers in Selen, we can use int_eq_reif - self.model.int_eq_reif(x, y, r); - Ok(()) - } - - /// Map bool_eq: x = y for boolean variables - /// FlatZinc signature: bool_eq(x, y) - pub(in crate::flatzinc::mapper) fn map_bool_eq(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "bool_eq requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - - // x = y for booleans - self.model.new(x.eq(y)); - Ok(()) - } - - /// Map bool_le_reif: r ⇔ (x ≤ y) for boolean variables - /// FlatZinc signature: bool_le_reif(x, y, r) - pub(in crate::flatzinc::mapper) fn map_bool_le_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "bool_le_reif requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - let r = self.get_var_or_const(&constraint.args[2])?; - - // For booleans (0/1): r ⇔ (x ≤ y) - self.model.int_le_reif(x, y, r); - Ok(()) - } - - /// Map bool_not: y = ¬x for boolean variables - /// FlatZinc signature: bool_not(x, y) - pub(in crate::flatzinc::mapper) fn map_bool_not(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "bool_not requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - - // y = NOT x → y = 1 - x (for boolean 0/1) - let not_x = self.model.sub(crate::variables::Val::ValI(1), x); - self.model.new(y.eq(not_x)); - Ok(()) - } - - /// Map bool_xor: z = x XOR y for boolean variables - /// FlatZinc signature: bool_xor(x, y, z) - pub(in crate::flatzinc::mapper) fn map_bool_xor(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "bool_xor requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - let z = self.get_var_or_const(&constraint.args[2])?; - - // z = x XOR y - // For booleans: x XOR y = (x + y) mod 2 = x + y - 2*(x*y) - // Or equivalently: z ⇔ (x ≠ y) - self.model.int_ne_reif(x, y, z); - Ok(()) - } -} diff --git a/src/flatzinc/mapper/constraints/comparison.rs b/src/flatzinc/mapper/constraints/comparison.rs deleted file mode 100644 index ec684f1..0000000 --- a/src/flatzinc/mapper/constraints/comparison.rs +++ /dev/null @@ -1,114 +0,0 @@ -//! Comparison constraint mappers -//! -//! Maps FlatZinc comparison constraints (int_eq, int_ne, int_lt, int_le, int_gt, int_ge) -//! to Selen constraint model. - -use crate::flatzinc::ast::*; -use crate::flatzinc::error::{FlatZincError, FlatZincResult}; -use crate::flatzinc::mapper::MappingContext; -use crate::runtime_api::{VarIdExt, ModelExt}; - -impl<'a> MappingContext<'a> { - /// Map int_eq constraint: x = y - /// Supports variables, array access, and integer literals for both arguments - pub(in crate::flatzinc::mapper) fn map_int_eq(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "int_eq requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - self.model.new(x.eq(y)); - - Ok(()) - } - - /// Map int_ne constraint: x ≠ y - /// Supports variables, array access, and integer literals for both arguments - pub(in crate::flatzinc::mapper) fn map_int_ne(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "int_ne requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - self.model.new(x.ne(y)); - Ok(()) - } - - /// Map int_lt constraint: x < y - /// Supports variables, array access, and integer literals for both arguments - pub(in crate::flatzinc::mapper) fn map_int_lt(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "int_lt requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - self.model.new(x.lt(y)); - Ok(()) - } - - /// Map int_le constraint: x ≤ y - /// Supports variables, array access, and integer literals for both arguments - pub(in crate::flatzinc::mapper) fn map_int_le(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "int_le requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - self.model.new(x.le(y)); - Ok(()) - } - - /// Map int_gt constraint: x > y - /// Supports variables, array access, and integer literals for both arguments - pub(in crate::flatzinc::mapper) fn map_int_gt(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "int_gt requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - self.model.new(x.gt(y)); - Ok(()) - } - - /// Map int_ge constraint: x ≥ y - /// Supports variables, array access, and integer literals for both arguments - pub(in crate::flatzinc::mapper) fn map_int_ge(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "int_ge requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - self.model.new(x.ge(y)); - Ok(()) - } -} diff --git a/src/flatzinc/mapper/constraints/counting.rs b/src/flatzinc/mapper/constraints/counting.rs deleted file mode 100644 index 24fd8b9..0000000 --- a/src/flatzinc/mapper/constraints/counting.rs +++ /dev/null @@ -1,30 +0,0 @@ -//! Counting constraint mappers -//! -//! Maps FlatZinc counting constraints (count_eq) to Selen constraint model. - -use crate::flatzinc::ast::*; -use crate::flatzinc::error::{FlatZincError, FlatZincResult}; -use crate::flatzinc::mapper::MappingContext; -use crate::runtime_api::ModelExt; - -impl<'a> MappingContext<'a> { - /// Map count_eq: count = |{i : array[i] = value}| - /// Also used for count/3 which has the same signature - pub(in crate::flatzinc::mapper) fn map_count_eq(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "count_eq requires 3 arguments (array, value, count)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let arr_vars = self.extract_var_array(&constraint.args[0])?; - let value = self.extract_int(&constraint.args[1])?; - let count_var = self.get_var_or_const(&constraint.args[2])?; - - // Use Selen's count constraint - self.model.count(&arr_vars, value, count_var); - Ok(()) - } -} diff --git a/src/flatzinc/mapper/constraints/element.rs b/src/flatzinc/mapper/constraints/element.rs deleted file mode 100644 index a57e052..0000000 --- a/src/flatzinc/mapper/constraints/element.rs +++ /dev/null @@ -1,161 +0,0 @@ -//! Element constraint mappers -//! -//! Maps FlatZinc element constraints (array access constraints) to Selen constraint model. -//! Element constraints express: array[index] = value - -use crate::flatzinc::ast::*; -use crate::flatzinc::error::{FlatZincError, FlatZincResult}; -use crate::flatzinc::mapper::MappingContext; -use crate::runtime_api::ModelExt; -use crate::variables::VarId; - -impl<'a> MappingContext<'a> { - /// Map array_var_int_element: array[index] = value - /// FlatZinc signature: array_var_int_element(index, array, value) - /// Note: FlatZinc uses 1-based indexing, Selen uses 0-based - pub(in crate::flatzinc::mapper) fn map_array_var_int_element(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "array_var_int_element requires 3 arguments (index, array, value)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - // Get index variable (1-based in FlatZinc) - // Supports: variables, array access (x[i]), integer literals - let index_1based = self.get_var_or_const(&constraint.args[0])?; - - // Convert to 0-based index for Selen - // Create: index_0based = index_1based - 1 - let index_0based = self.model.sub(index_1based, crate::variables::Val::ValI(1)); - - // Get array - let array = self.extract_var_array(&constraint.args[1])?; - - // Get value (can be variable, array access, or constant) - // Supports: variables, array access (y[j]), integer literals - let value = self.get_var_or_const(&constraint.args[2])?; - - // Apply element constraint: array[index_0based] = value - self.model.elem(&array, index_0based, value); - Ok(()) - } - - /// Map array_int_element: array[index] = value (with constant array) - /// FlatZinc signature: array_int_element(index, array, value) - /// Note: FlatZinc uses 1-based indexing, Selen uses 0-based - pub(in crate::flatzinc::mapper) fn map_array_int_element(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "array_int_element requires 3 arguments (index, array, value)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - // Get index variable (1-based in FlatZinc) - // Supports: variables, array access (x[i]), integer literals - let index_1based = self.get_var_or_const(&constraint.args[0])?; - - // Convert to 0-based index for Selen - let index_0based = self.model.sub(index_1based, crate::variables::Val::ValI(1)); - - // Get array of constants and convert to fixed variables - let const_array = self.extract_int_array(&constraint.args[1])?; - let array: Vec = const_array.iter() - .map(|&val| self.model.int(val, val)) - .collect(); - - // Get value (can be variable, array access, or constant) - // Supports: variables, array access (y[j]), integer literals - let value = self.get_var_or_const(&constraint.args[2])?; - - // Apply element constraint: array[index_0based] = value - self.model.elem(&array, index_0based, value); - Ok(()) - } - - /// Map array_var_bool_element: array[index] = value (boolean version) - /// FlatZinc signature: array_var_bool_element(index, array, value) - /// Note: FlatZinc uses 1-based indexing, Selen uses 0-based - pub(in crate::flatzinc::mapper) fn map_array_var_bool_element(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "array_var_bool_element requires 3 arguments (index, array, value)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - // Get index variable (1-based in FlatZinc) - // Supports: variables, array access (x[i]), integer literals - let index_1based = self.get_var_or_const(&constraint.args[0])?; - - // Convert to 0-based index for Selen - let index_0based = self.model.sub(index_1based, crate::variables::Val::ValI(1)); - - // Get array (booleans are represented as 0/1 variables) - let array = self.extract_var_array(&constraint.args[1])?; - - // Get value (can be variable, array access, or constant) - // Supports: variables, array access (y[j]), boolean literals - let value = self.get_var_or_const(&constraint.args[2])?; - - // Apply element constraint: array[index_0based] = value - self.model.elem(&array, index_0based, value); - Ok(()) - } - - /// Map array_bool_element: array[index] = value (with constant boolean array) - /// FlatZinc signature: array_bool_element(index, array, value) - /// Note: FlatZinc uses 1-based indexing, Selen uses 0-based - pub(in crate::flatzinc::mapper) fn map_array_bool_element(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "array_bool_element requires 3 arguments (index, array, value)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - // Get index variable (1-based in FlatZinc) - // Supports: variables, array access (x[i]), integer literals - let index_1based = self.get_var_or_const(&constraint.args[0])?; - - // Convert to 0-based index for Selen - let index_0based = self.model.sub(index_1based, crate::variables::Val::ValI(1)); - - // Get array of boolean constants and convert to 0/1 fixed variables - let array: Vec = if let Expr::ArrayLit(elements) = &constraint.args[1] { - elements.iter() - .map(|elem| { - if let Expr::BoolLit(b) = elem { - let val = if *b { 1 } else { 0 }; - Ok(self.model.int(val, val)) - } else { - Err(FlatZincError::MapError { - message: "Expected boolean literal in array_bool_element array".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }) - } - }) - .collect::>>()? - } else { - return Err(FlatZincError::MapError { - message: "Expected array literal in array_bool_element".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - }; - - // Get value (can be variable, array access, or constant) - // Supports: variables, array access (y[j]), boolean literals - let value = self.get_var_or_const(&constraint.args[2])?; - - // Apply element constraint: array[index_0based] = value - self.model.elem(&array, index_0based, value); - Ok(()) - } -} diff --git a/src/flatzinc/mapper/constraints/global.rs b/src/flatzinc/mapper/constraints/global.rs deleted file mode 100644 index 2859d13..0000000 --- a/src/flatzinc/mapper/constraints/global.rs +++ /dev/null @@ -1,704 +0,0 @@ -//! Global constraint mappers -//! -//! Maps FlatZinc global constraints (all_different, sort, table, lex_less, nvalue) to Selen constraint model. - -use crate::flatzinc::ast::*; -use crate::flatzinc::error::{FlatZincError, FlatZincResult}; -use crate::flatzinc::mapper::MappingContext; -use crate::runtime_api::{ModelExt, VarIdExt}; - -impl<'a> MappingContext<'a> { - /// Map all_different constraint - pub(in crate::flatzinc::mapper) fn map_all_different(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 1 { - return Err(FlatZincError::MapError { - message: "all_different requires 1 argument (array of variables)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let var_ids = self.extract_var_array(&constraint.args[0])?; - self.model.alldiff(&var_ids); - Ok(()) - } - - /// Map sort constraint: y is the sorted version of x - /// FlatZinc signature: sort(x, y) - /// - /// Decomposition: - /// 1. y contains the same values as x (they are permutations) - /// 2. y is sorted: y[i] <= y[i+1] for all i - /// - /// Implementation strategy: - /// - For each element in y, it must equal some element in x - /// - y must be in non-decreasing order - /// - Use global_cardinality to ensure same multiset - pub(in crate::flatzinc::mapper) fn map_sort(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "sort requires 2 arguments (unsorted array, sorted array)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.extract_var_array(&constraint.args[0])?; - let y = self.extract_var_array(&constraint.args[1])?; - - if x.len() != y.len() { - return Err(FlatZincError::MapError { - message: format!( - "sort: arrays must have same length (x: {}, y: {})", - x.len(), - y.len() - ), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let n = x.len(); - - // Constraint 1: y is sorted (non-decreasing order) - // y[i] <= y[i+1] for all i - for i in 0..n.saturating_sub(1) { - self.model.new(y[i].le(&y[i + 1])); - } - - // Constraint 2: y is a permutation of x - // For each value that appears in the union of domains: - // count(x, value) = count(y, value) - // - // Since we don't have direct access to domains, we use a simpler approach: - // For small arrays, ensure each y[i] equals some x[j] using element-like constraints - // For larger arrays, we rely on the combined constraints being sufficient - - if n <= 10 { - // For small arrays, add explicit channeling constraints - // Each y[i] must equal at least one x[j] - for &yi in &y { - // Create: (yi = x[0]) OR (yi = x[1]) OR ... OR (yi = x[n-1]) - let mut equality_vars = Vec::new(); - for &xj in &x { - let bi = self.model.bool(); - self.model.int_eq_reif(yi, xj, bi); - equality_vars.push(bi); - } - let or_result = self.model.bool_or(&equality_vars); - self.model.new(or_result.eq(1)); - } - - // Similarly for x: each x[j] must equal at least one y[i] - for &xj in &x { - let mut equality_vars = Vec::new(); - for &yi in &y { - let bi = self.model.bool(); - self.model.int_eq_reif(xj, yi, bi); - equality_vars.push(bi); - } - let or_result = self.model.bool_or(&equality_vars); - self.model.new(or_result.eq(1)); - } - } - // For larger arrays, the sorting constraint + domain pruning should be sufficient - // A more efficient implementation would use proper channeling or element constraints - - Ok(()) - } - - /// Map table_int constraint: tuple(x) must be in table t - /// FlatZinc signature: table_int(array[int] of var int: x, array[int, int] of int: t) - /// - /// The table t is a 2D array where each row is a valid tuple. - /// Decomposition: Create boolean for each row, at least one must be true - pub(in crate::flatzinc::mapper) fn map_table_int(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "table_int requires 2 arguments (variable array, table)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.extract_var_array(&constraint.args[0])?; - let arity = x.len(); - - // Extract the table: 2D array of integers - // The table format is a flat array representing rows - let table_data = self.extract_int_array(&constraint.args[1])?; - - if table_data.is_empty() { - // Empty table means no valid tuples - unsatisfiable - let false_var = self.model.int(0, 0); - self.model.new(false_var.eq(1)); // Force failure - return Ok(()); - } - - if table_data.len() % arity != 0 { - return Err(FlatZincError::MapError { - message: format!( - "table_int: table size {} is not a multiple of arity {}", - table_data.len(), - arity - ), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let num_rows = table_data.len() / arity; - - // For each row in the table, create a boolean indicating if x matches this row - let mut row_matches = Vec::new(); - - for row_idx in 0..num_rows { - // Create booleans for each position match - let mut position_matches = Vec::new(); - - for col_idx in 0..arity { - let table_value = table_data[row_idx * arity + col_idx]; - let var = x[col_idx]; - - // Create: b_i ↔ (x[i] = table_value) - let b = self.model.bool(); - let const_var = self.model.int(table_value, table_value); - self.model.int_eq_reif(var, const_var, b); - position_matches.push(b); - } - - // All positions must match for this row - let row_match = self.model.bool_and(&position_matches); - row_matches.push(row_match); - } - - // At least one row must match - let any_row_matches = self.model.bool_or(&row_matches); - self.model.new(any_row_matches.eq(1)); - - Ok(()) - } - - /// Map table_bool constraint: tuple(x) must be in table t - /// FlatZinc signature: table_bool(array[int] of var bool: x, array[int, int] of bool: t) - pub(in crate::flatzinc::mapper) fn map_table_bool(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "table_bool requires 2 arguments (variable array, table)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.extract_var_array(&constraint.args[0])?; - let arity = x.len(); - - // Extract the table: 2D array of booleans - let table_data = self.extract_bool_array(&constraint.args[1])?; - - if table_data.is_empty() { - // Empty table means no valid tuples - unsatisfiable - let false_var = self.model.int(0, 0); - self.model.new(false_var.eq(1)); // Force failure - return Ok(()); - } - - if table_data.len() % arity != 0 { - return Err(FlatZincError::MapError { - message: format!( - "table_bool: table size {} is not a multiple of arity {}", - table_data.len(), - arity - ), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let num_rows = table_data.len() / arity; - - // For each row in the table, create a boolean indicating if x matches this row - let mut row_matches = Vec::new(); - - for row_idx in 0..num_rows { - // Create booleans for each position match - let mut position_matches = Vec::new(); - - for col_idx in 0..arity { - let table_value = table_data[row_idx * arity + col_idx]; - let var = x[col_idx]; - - // Create: b_i ↔ (x[i] = table_value) - let b = self.model.bool(); - let const_var = self.model.int(table_value as i32, table_value as i32); - self.model.int_eq_reif(var, const_var, b); - position_matches.push(b); - } - - // All positions must match for this row - let row_match = self.model.bool_and(&position_matches); - row_matches.push(row_match); - } - - // At least one row must match - let any_row_matches = self.model.bool_or(&row_matches); - self.model.new(any_row_matches.eq(1)); - - Ok(()) - } - - /// Map lex_less constraint: x <_lex y (lexicographic strict ordering) - /// FlatZinc signature: lex_less(array[int] of var int: x, array[int] of var int: y) - /// - /// Decomposition: x <_lex y iff ∃i: (∀j FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "lex_less requires 2 arguments (two arrays)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.extract_var_array(&constraint.args[0])?; - let y = self.extract_var_array(&constraint.args[1])?; - - if x.len() != y.len() { - return Err(FlatZincError::MapError { - message: format!( - "lex_less: arrays must have same length (x: {}, y: {})", - x.len(), - y.len() - ), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let n = x.len(); - - if n == 0 { - // Empty arrays: x <_lex y is false - let false_var = self.model.int(0, 0); - self.model.new(false_var.eq(1)); // Force failure - return Ok(()); - } - - // Decomposition: For each position i, create a boolean indicating: - // "x is less than y starting at position i" - // meaning: all previous positions are equal AND x[i] < y[i] - - let mut position_less = Vec::new(); - - for i in 0..n { - let mut conditions = Vec::new(); - - // All previous positions must be equal - for j in 0..i { - let eq_b = self.model.bool(); - self.model.int_eq_reif(x[j], y[j], eq_b); - conditions.push(eq_b); - } - - // At position i, x[i] < y[i] - let lt_b = self.model.bool(); - self.model.int_lt_reif(x[i], y[i], lt_b); - conditions.push(lt_b); - - // All conditions must hold - let pos_less = self.model.bool_and(&conditions); - position_less.push(pos_less); - } - - // At least one position must satisfy the "less" condition - let lex_less_holds = self.model.bool_or(&position_less); - self.model.new(lex_less_holds.eq(1)); - - Ok(()) - } - - /// Map lex_lesseq constraint: x ≤_lex y (lexicographic ordering) - /// FlatZinc signature: lex_lesseq(array[int] of var int: x, array[int] of var int: y) - /// - /// Decomposition: x ≤_lex y iff (x = y) ∨ (x <_lex y) - pub(in crate::flatzinc::mapper) fn map_lex_lesseq(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "lex_lesseq requires 2 arguments (two arrays)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.extract_var_array(&constraint.args[0])?; - let y = self.extract_var_array(&constraint.args[1])?; - - if x.len() != y.len() { - return Err(FlatZincError::MapError { - message: format!( - "lex_lesseq: arrays must have same length (x: {}, y: {})", - x.len(), - y.len() - ), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let n = x.len(); - - if n == 0 { - // Empty arrays: x ≤_lex y is true (equal) - return Ok(()); - } - - // Decomposition: For each position i, create a boolean indicating: - // "x is less than or equal to y starting at position i" - // Two cases: - // 1. All previous positions equal AND x[i] < y[i] (strictly less) - // 2. All positions equal (equal case) - - let mut position_conditions = Vec::new(); - - // Case 1: Strictly less at some position - for i in 0..n { - let mut conditions = Vec::new(); - - // All previous positions must be equal - for j in 0..i { - let eq_b = self.model.bool(); - self.model.int_eq_reif(x[j], y[j], eq_b); - conditions.push(eq_b); - } - - // At position i, x[i] < y[i] - let lt_b = self.model.bool(); - self.model.int_lt_reif(x[i], y[i], lt_b); - conditions.push(lt_b); - - // All conditions must hold - let pos_less = self.model.bool_and(&conditions); - position_conditions.push(pos_less); - } - - // Case 2: Complete equality - let mut all_equal_conditions = Vec::new(); - for i in 0..n { - let eq_b = self.model.bool(); - self.model.int_eq_reif(x[i], y[i], eq_b); - all_equal_conditions.push(eq_b); - } - let all_equal = self.model.bool_and(&all_equal_conditions); - position_conditions.push(all_equal); - - // At least one condition must hold (less at some position OR completely equal) - let lex_lesseq_holds = self.model.bool_or(&position_conditions); - self.model.new(lex_lesseq_holds.eq(1)); - - Ok(()) - } - - /// Map nvalue constraint: n = |{x[i] : i ∈ indices}| (count distinct values) - /// FlatZinc signature: nvalue(var int: n, array[int] of var int: x) - /// - /// Decomposition: For each potential value v in the union of domains, - /// create a boolean indicating if v appears in x, then sum these booleans. - pub(in crate::flatzinc::mapper) fn map_nvalue(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "nvalue requires 2 arguments (result variable, array)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let n = self.get_var_or_const(&constraint.args[0])?; - let x = self.extract_var_array(&constraint.args[1])?; - - if x.is_empty() { - // Empty array has 0 distinct values - let zero = self.model.int(0, 0); - self.model.new(n.eq(zero)); - return Ok(()); - } - - // Get union of all possible values (approximate by using a reasonable range) - // We'll use the model's domain bounds - // For simplicity, iterate through a reasonable range of values - - // Get min/max bounds from unbounded_int_bounds in context - let (min_bound, max_bound) = self.unbounded_int_bounds; - - // Limit the range to avoid excessive computation - const MAX_RANGE: i32 = 1000; - let range = (max_bound - min_bound).min(MAX_RANGE); - - if range > MAX_RANGE { - // For very large domains, use a different approach - // Create a boolean for each array element pair to check distinctness - // This is O(n²) but works for any domain size - - // Not implemented yet - fall back to unsupported - return Err(FlatZincError::UnsupportedFeature { - feature: "nvalue with very large domains (>1000)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - // For each potential value, create a boolean indicating if it appears in x - let mut value_present_bools = Vec::new(); - - for value in min_bound..=max_bound { - // Create: b_v ↔ (∃i: x[i] = value) - let mut any_equal = Vec::new(); - - for &xi in &x { - let eq_b = self.model.bool(); - let const_var = self.model.int(value, value); - self.model.int_eq_reif(xi, const_var, eq_b); - any_equal.push(eq_b); - } - - // At least one element equals this value - let value_present = self.model.bool_or(&any_equal); - value_present_bools.push(value_present); - } - - // Sum the booleans to get the count of distinct values - let sum = self.model.sum(&value_present_bools); - self.model.new(n.eq(sum)); - - Ok(()) - } - - /// Map fixed_fzn_cumulative constraint: cumulative scheduling with fixed capacity - /// FlatZinc signature: fixed_fzn_cumulative(array[int] of var int: s, array[int] of int: d, - /// array[int] of int: r, int: b) - /// - /// Parameters: - /// - s[i]: start time of task i (variable) - /// - d[i]: duration of task i (constant) - /// - r[i]: resource requirement of task i (constant) - /// - b: resource capacity bound (constant) - /// - /// Constraint: At any time t, sum of resources used by overlapping tasks ≤ b - /// Task i is active at time t if: s[i] ≤ t < s[i] + d[i] - /// - /// Decomposition: For each relevant time point t, ensure resource usage ≤ b - pub(in crate::flatzinc::mapper) fn map_fixed_fzn_cumulative(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 4 { - return Err(FlatZincError::MapError { - message: "fixed_fzn_cumulative requires 4 arguments (starts, durations, resources, bound)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let starts = self.extract_var_array(&constraint.args[0])?; - let durations = self.extract_int_array(&constraint.args[1])?; - let resources = self.extract_int_array(&constraint.args[2])?; - let capacity = self.extract_int(&constraint.args[3])?; - - let n_tasks = starts.len(); - - if durations.len() != n_tasks || resources.len() != n_tasks { - return Err(FlatZincError::MapError { - message: format!( - "fixed_fzn_cumulative: array lengths must match (starts: {}, durations: {}, resources: {})", - n_tasks, durations.len(), resources.len() - ), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - // Skip tasks with zero duration or zero resource requirement - let mut active_tasks = Vec::new(); - for i in 0..n_tasks { - if durations[i] > 0 && resources[i] > 0 { - active_tasks.push(i); - } - } - - if active_tasks.is_empty() { - return Ok(()); // No active tasks, constraint trivially satisfied - } - - // Determine time horizon: compute reasonable bounds - // Time points to check: from min possible start to max possible end - let (min_time, max_time) = self.unbounded_int_bounds; - - // Limit time points to avoid excessive constraints (max 200 time points) - const MAX_TIME_POINTS: i32 = 200; - let time_range = max_time - min_time + 1; - - if time_range > MAX_TIME_POINTS { - // For large time horizons, use a simplified check on a subset of time points - // Sample time points evenly across the range - let step = time_range / MAX_TIME_POINTS; - for t_idx in 0..MAX_TIME_POINTS { - let t = min_time + t_idx * step; - self.add_cumulative_constraint_at_time(&starts, &durations, &resources, capacity, t, &active_tasks)?; - } - } else { - // For small time horizons, check every time point - for t in min_time..=max_time { - self.add_cumulative_constraint_at_time(&starts, &durations, &resources, capacity, t, &active_tasks)?; - } - } - - Ok(()) - } - - /// Map var_fzn_cumulative constraint: cumulative scheduling with variable capacity - /// FlatZinc signature: var_fzn_cumulative(array[int] of var int: s, array[int] of int: d, - /// array[int] of int: r, var int: b) - /// - /// Same as fixed_fzn_cumulative but with variable capacity b - pub(in crate::flatzinc::mapper) fn map_var_fzn_cumulative(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 4 { - return Err(FlatZincError::MapError { - message: "var_fzn_cumulative requires 4 arguments (starts, durations, resources, bound)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let starts = self.extract_var_array(&constraint.args[0])?; - let durations = self.extract_int_array(&constraint.args[1])?; - let resources = self.extract_int_array(&constraint.args[2])?; - let capacity_var = self.get_var_or_const(&constraint.args[3])?; - - let n_tasks = starts.len(); - - if durations.len() != n_tasks || resources.len() != n_tasks { - return Err(FlatZincError::MapError { - message: format!( - "var_fzn_cumulative: array lengths must match (starts: {}, durations: {}, resources: {})", - n_tasks, durations.len(), resources.len() - ), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - // Skip tasks with zero duration or zero resource requirement - let mut active_tasks = Vec::new(); - for i in 0..n_tasks { - if durations[i] > 0 && resources[i] > 0 { - active_tasks.push(i); - } - } - - if active_tasks.is_empty() { - return Ok(()); // No active tasks, constraint trivially satisfied - } - - // Determine time horizon - let (min_time, max_time) = self.unbounded_int_bounds; - - // Limit time points to avoid excessive constraints - const MAX_TIME_POINTS: i32 = 200; - let time_range = max_time - min_time + 1; - - if time_range > MAX_TIME_POINTS { - let step = time_range / MAX_TIME_POINTS; - for t_idx in 0..MAX_TIME_POINTS { - let t = min_time + t_idx * step; - self.add_var_cumulative_constraint_at_time(&starts, &durations, &resources, capacity_var, t, &active_tasks)?; - } - } else { - for t in min_time..=max_time { - self.add_var_cumulative_constraint_at_time(&starts, &durations, &resources, capacity_var, t, &active_tasks)?; - } - } - - Ok(()) - } - - /// Helper: Add cumulative constraint at specific time point t (fixed capacity) - fn add_cumulative_constraint_at_time( - &mut self, - starts: &[crate::variables::VarId], - durations: &[i32], - resources: &[i32], - capacity: i32, - t: i32, - active_tasks: &[usize], - ) -> FlatZincResult<()> { - // For each task i, create boolean: active_i ↔ (s[i] ≤ t < s[i] + d[i]) - let mut resource_usage_terms = Vec::new(); - - for &i in active_tasks { - // Task i is active at time t if: s[i] ≤ t AND t < s[i] + d[i] - // Which is: s[i] ≤ t AND s[i] + d[i] > t - - let t_const = self.model.int(t, t); - let end_time_i = durations[i]; // s[i] + d[i] - - // b1 ↔ (s[i] ≤ t) - let b1 = self.model.bool(); - self.model.int_le_reif(starts[i], t_const, b1); - - // b2 ↔ (s[i] + d[i] > t) which is (s[i] > t - d[i]) - let b2 = self.model.bool(); - let t_minus_d = self.model.int(t - end_time_i + 1, t - end_time_i + 1); - self.model.int_ge_reif(starts[i], t_minus_d, b2); - - // active_i = b1 AND b2 - let active_i = self.model.bool_and(&[b1, b2]); - - // If task i is active, it uses resources[i] - // resource_usage += active_i * resources[i] - let usage_i = self.model.mul(active_i, crate::variables::Val::ValI(resources[i])); - resource_usage_terms.push(usage_i); - } - - if !resource_usage_terms.is_empty() { - // Sum of resource usage at time t must be ≤ capacity - let total_usage = self.model.sum(&resource_usage_terms); - let capacity_var = self.model.int(capacity, capacity); - self.model.new(total_usage.le(capacity_var)); - } - - Ok(()) - } - - /// Helper: Add cumulative constraint at specific time point t (variable capacity) - fn add_var_cumulative_constraint_at_time( - &mut self, - starts: &[crate::variables::VarId], - durations: &[i32], - resources: &[i32], - capacity_var: crate::variables::VarId, - t: i32, - active_tasks: &[usize], - ) -> FlatZincResult<()> { - // Same as fixed version but use capacity_var instead of creating constant - let mut resource_usage_terms = Vec::new(); - - for &i in active_tasks { - let t_const = self.model.int(t, t); - let end_time_i = durations[i]; - - let b1 = self.model.bool(); - self.model.int_le_reif(starts[i], t_const, b1); - - let b2 = self.model.bool(); - let t_minus_d = self.model.int(t - end_time_i + 1, t - end_time_i + 1); - self.model.int_ge_reif(starts[i], t_minus_d, b2); - - let active_i = self.model.bool_and(&[b1, b2]); - let usage_i = self.model.mul(active_i, crate::variables::Val::ValI(resources[i])); - resource_usage_terms.push(usage_i); - } - - if !resource_usage_terms.is_empty() { - let total_usage = self.model.sum(&resource_usage_terms); - self.model.new(total_usage.le(capacity_var)); - } - - Ok(()) - } -} diff --git a/src/flatzinc/mapper/constraints/global_cardinality.rs b/src/flatzinc/mapper/constraints/global_cardinality.rs deleted file mode 100644 index 57292b4..0000000 --- a/src/flatzinc/mapper/constraints/global_cardinality.rs +++ /dev/null @@ -1,123 +0,0 @@ -//! Global cardinality constraint mappers -//! -//! Maps FlatZinc global cardinality constraint to Selen constraint model. - -use crate::flatzinc::ast::*; -use crate::flatzinc::error::{FlatZincError, FlatZincResult}; -use crate::flatzinc::mapper::MappingContext; -use crate::runtime_api::ModelExt; - -impl<'a> MappingContext<'a> { - /// Map global_cardinality: For each value[i], count occurrences in vars array - /// FlatZinc signature: global_cardinality(vars, values, counts) - /// - /// Where: - /// - vars: array of variables to count in - /// - values: array of values to count (must be constants) - /// - counts: array of count variables (one per value) - /// - /// Constraint: For each i, counts[i] = |{j : vars[j] = values[i]}| - pub(in crate::flatzinc::mapper) fn map_global_cardinality(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "global_cardinality requires 3 arguments (vars, values, counts)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - // Extract the variables array - let vars = self.extract_var_array(&constraint.args[0])?; - - // Extract the values array (must be constants) - let values = self.extract_int_array(&constraint.args[1])?; - - // Extract the counts array (variables or constants) - let counts = self.extract_var_array(&constraint.args[2])?; - - // Verify arrays have compatible sizes - if values.len() != counts.len() { - return Err(FlatZincError::MapError { - message: format!( - "global_cardinality: values array length ({}) must match counts array length ({})", - values.len(), - counts.len() - ), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - // For each value, create a count constraint - for (&value, &count_var) in values.iter().zip(counts.iter()) { - // Use Selen's count constraint: count(vars, value, count_var) - // This constrains: count_var = |{j : vars[j] = value}| - self.model.count(&vars, value, count_var); - } - - Ok(()) - } - - /// Map global_cardinality_low_up_closed: Count with bounds on counts - /// FlatZinc signature: global_cardinality_low_up_closed(vars, values, low, up) - /// - /// Where: - /// - vars: array of variables to count in - /// - values: array of values to count (must be constants) - /// - low: array of lower bounds for counts - /// - up: array of upper bounds for counts - /// - /// Constraint: For each i, low[i] <= |{j : vars[j] = values[i]}| <= up[i] - pub(in crate::flatzinc::mapper) fn map_global_cardinality_low_up_closed(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 4 { - return Err(FlatZincError::MapError { - message: "global_cardinality_low_up_closed requires 4 arguments (vars, values, low, up)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - // Extract the variables array - let vars = self.extract_var_array(&constraint.args[0])?; - - // Extract the values array (must be constants) - let values = self.extract_int_array(&constraint.args[1])?; - - // Extract the low bounds array - let low = self.extract_int_array(&constraint.args[2])?; - - // Extract the up bounds array - let up = self.extract_int_array(&constraint.args[3])?; - - // Verify arrays have compatible sizes - if values.len() != low.len() || values.len() != up.len() { - return Err(FlatZincError::MapError { - message: format!( - "global_cardinality_low_up_closed: arrays must have same length (values: {}, low: {}, up: {})", - values.len(), - low.len(), - up.len() - ), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - // For each value, create a count variable and constrain it with bounds - for i in 0..values.len() { - let value = values[i]; - let low_bound = low[i]; - let up_bound = up[i]; - - // Create a variable to hold the count with appropriate bounds - let count_var = self.model.int(low_bound, up_bound); - - // Use Selen's count constraint: count(vars, value, count_var) - // This constrains: count_var = |{j : vars[j] = value}| - // The count_var's domain already enforces low_bound <= count_var <= up_bound - self.model.count(&vars, value, count_var); - } - - Ok(()) - } -} diff --git a/src/flatzinc/mapper/constraints/linear.rs b/src/flatzinc/mapper/constraints/linear.rs deleted file mode 100644 index 4068273..0000000 --- a/src/flatzinc/mapper/constraints/linear.rs +++ /dev/null @@ -1,152 +0,0 @@ -//! Linear constraint mappers -//! -//! Maps FlatZinc linear constraints (int_lin_eq, int_lin_le, int_lin_ne) -//! to Selen constraint model. - -use crate::flatzinc::ast::*; -use crate::flatzinc::error::{FlatZincError, FlatZincResult}; -use crate::flatzinc::mapper::MappingContext; -use crate::runtime_api::{VarIdExt, ModelExt}; -use crate::variables::VarId; - -impl<'a> MappingContext<'a> { - /// Map int_lin_eq: Σ(coeffs[i] * vars[i]) = constant - pub(in crate::flatzinc::mapper) fn map_int_lin_eq(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_lin_eq requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let coeffs = self.extract_int_array(&constraint.args[0])?; - let var_ids = self.extract_var_array(&constraint.args[1])?; - let constant = self.extract_int(&constraint.args[2])?; - - // Create sum using Model's API - let scaled_vars: Vec = coeffs - .iter() - .zip(var_ids.iter()) - .map(|(&coeff, &var)| self.model.mul(var, crate::variables::Val::ValI(coeff))) - .collect(); - - let sum_var = self.model.sum(&scaled_vars); - self.model.new(sum_var.eq(constant)); - Ok(()) - } - - /// Map int_lin_le: Σ(coeffs[i] * vars[i]) ≤ constant - pub(in crate::flatzinc::mapper) fn map_int_lin_le(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_lin_le requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let coeffs = self.extract_int_array(&constraint.args[0])?; - let var_ids = self.extract_var_array(&constraint.args[1])?; - let constant = self.extract_int(&constraint.args[2])?; - - let scaled_vars: Vec = coeffs - .iter() - .zip(var_ids.iter()) - .map(|(&coeff, &var)| self.model.mul(var, crate::variables::Val::ValI(coeff))) - .collect(); - - let sum_var = self.model.sum(&scaled_vars); - self.model.new(sum_var.le(constant)); - Ok(()) - } - - /// Map int_lin_ne: Σ(coeffs[i] * vars[i]) ≠ constant - pub(in crate::flatzinc::mapper) fn map_int_lin_ne(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_lin_ne requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let coeffs = self.extract_int_array(&constraint.args[0])?; - let var_ids = self.extract_var_array(&constraint.args[1])?; - let constant = self.extract_int(&constraint.args[2])?; - - let scaled_vars: Vec = coeffs - .iter() - .zip(var_ids.iter()) - .map(|(&coeff, &var)| self.model.mul(var, crate::variables::Val::ValI(coeff))) - .collect(); - - let sum_var = self.model.sum(&scaled_vars); - - // Use runtime API to post not-equals constraint: sum ≠ constant - self.model.c(sum_var).ne(constant); - Ok(()) - } - - /// Map int_lin_eq_reif: b ⇔ (Σ(coeffs[i] * vars[i]) = constant) - pub(in crate::flatzinc::mapper) fn map_int_lin_eq_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 4 { - return Err(FlatZincError::MapError { - message: "int_lin_eq_reif requires 4 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let coeffs = self.extract_int_array(&constraint.args[0])?; - let var_ids = self.extract_var_array(&constraint.args[1])?; - let constant = self.extract_int(&constraint.args[2])?; - let b = self.get_var_or_const(&constraint.args[3])?; - - // Create sum: Σ(coeffs[i] * vars[i]) - let scaled_vars: Vec = coeffs - .iter() - .zip(var_ids.iter()) - .map(|(&coeff, &var)| self.model.mul(var, crate::variables::Val::ValI(coeff))) - .collect(); - - let sum_var = self.model.sum(&scaled_vars); - - // Create reified constraint: b ⇔ (sum = constant) - // Use Selen's int_eq_reif: b ⇔ (sum = constant_var) - let const_var = self.model.int(constant, constant); - self.model.int_eq_reif(sum_var, const_var, b); - Ok(()) - } - - /// Map int_lin_le_reif: b ⇔ (Σ(coeffs[i] * vars[i]) ≤ constant) - pub(in crate::flatzinc::mapper) fn map_int_lin_le_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 4 { - return Err(FlatZincError::MapError { - message: "int_lin_le_reif requires 4 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let coeffs = self.extract_int_array(&constraint.args[0])?; - let var_ids = self.extract_var_array(&constraint.args[1])?; - let constant = self.extract_int(&constraint.args[2])?; - let b = self.get_var_or_const(&constraint.args[3])?; - - // Create sum: Σ(coeffs[i] * vars[i]) - let scaled_vars: Vec = coeffs - .iter() - .zip(var_ids.iter()) - .map(|(&coeff, &var)| self.model.mul(var, crate::variables::Val::ValI(coeff))) - .collect(); - - let sum_var = self.model.sum(&scaled_vars); - - // Create reified constraint: b ⇔ (sum ≤ constant) - // Use Selen's int_le_reif: b ⇔ (sum ≤ constant_var) - let const_var = self.model.int(constant, constant); - self.model.int_le_reif(sum_var, const_var, b); - Ok(()) - } -} diff --git a/src/flatzinc/mapper/constraints/mod.rs b/src/flatzinc/mapper/constraints/mod.rs deleted file mode 100644 index 2a71679..0000000 --- a/src/flatzinc/mapper/constraints/mod.rs +++ /dev/null @@ -1,15 +0,0 @@ -//! Constraint mapping modules -//! -//! This module organizes FlatZinc constraint mappers by category. - -pub(super) mod comparison; -pub(super) mod linear; -pub(super) mod global; -pub(super) mod reified; -pub(super) mod boolean; -pub(super) mod array; -pub(super) mod element; -pub(super) mod arithmetic; -pub(super) mod counting; -pub(super) mod set; -pub(super) mod global_cardinality; diff --git a/src/flatzinc/mapper/constraints/reified.rs b/src/flatzinc/mapper/constraints/reified.rs deleted file mode 100644 index e800a8d..0000000 --- a/src/flatzinc/mapper/constraints/reified.rs +++ /dev/null @@ -1,108 +0,0 @@ -//! Reified constraint mappers -//! -//! Maps FlatZinc reified constraints (*_reif) to Selen constraint model. -//! Reified constraints have the form: b ⇔ (constraint) - -use crate::flatzinc::ast::*; -use crate::flatzinc::error::{FlatZincError, FlatZincResult}; -use crate::flatzinc::mapper::MappingContext; -use crate::runtime_api::ModelExt; - -impl<'a> MappingContext<'a> { - /// Map int_eq_reif: b ⇔ (x = y) - pub(in crate::flatzinc::mapper) fn map_int_eq_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_eq_reif requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - let b = self.get_var_or_const(&constraint.args[2])?; - self.model.int_eq_reif(x, y, b); - Ok(()) - } - - pub(in crate::flatzinc::mapper) fn map_int_ne_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_ne_reif requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - let b = self.get_var_or_const(&constraint.args[2])?; - self.model.int_ne_reif(x, y, b); - Ok(()) - } - - pub(in crate::flatzinc::mapper) fn map_int_lt_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_lt_reif requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - let b = self.get_var_or_const(&constraint.args[2])?; - self.model.int_lt_reif(x, y, b); - Ok(()) - } - - pub(in crate::flatzinc::mapper) fn map_int_le_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_le_reif requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - let b = self.get_var_or_const(&constraint.args[2])?; - self.model.int_le_reif(x, y, b); - Ok(()) - } - - pub(in crate::flatzinc::mapper) fn map_int_gt_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_gt_reif requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - let b = self.get_var_or_const(&constraint.args[2])?; - self.model.int_gt_reif(x, y, b); - Ok(()) - } - - pub(in crate::flatzinc::mapper) fn map_int_ge_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_ge_reif requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var_or_const(&constraint.args[0])?; - let y = self.get_var_or_const(&constraint.args[1])?; - let b = self.get_var_or_const(&constraint.args[2])?; - self.model.int_ge_reif(x, y, b); - Ok(()) - } -} diff --git a/src/flatzinc/mapper/constraints/set.rs b/src/flatzinc/mapper/constraints/set.rs deleted file mode 100644 index 61b6913..0000000 --- a/src/flatzinc/mapper/constraints/set.rs +++ /dev/null @@ -1,157 +0,0 @@ -//! Set constraint mappers -//! -//! Maps FlatZinc set constraints to Selen constraint model. - -use crate::flatzinc::ast::*; -use crate::flatzinc::error::{FlatZincError, FlatZincResult}; -use crate::flatzinc::mapper::MappingContext; -use crate::runtime_api::{VarIdExt, ModelExt}; - -impl<'a> MappingContext<'a> { - /// Map set_in_reif: b ⇔ (value ∈ set) - /// FlatZinc signature: set_in_reif(value, set, b) - /// - /// Where: - /// - value: int variable or literal - /// - set: set literal {1,2,3} or range 1..10 - /// - b: boolean variable indicating membership - pub(in crate::flatzinc::mapper) fn map_set_in_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "set_in_reif requires 3 arguments (value, set, bool)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - // Get the value (can be variable or constant) - let value = self.get_var_or_const(&constraint.args[0])?; - - // Get the boolean result variable - let b = self.get_var_or_const(&constraint.args[2])?; - - // Parse the set (can be SetLit or Range) - match &constraint.args[1] { - Expr::Range(min_expr, max_expr) => { - // Handle range like 1..10 - let min = self.extract_int(min_expr)?; - let max = self.extract_int(max_expr)?; - - // b ⇔ (value ∈ [min, max]) - // This is equivalent to: b ⇔ (value >= min AND value <= max) - // We can decompose into: (value >= min) AND (value <= max) ⇔ b - - // Create: b1 ⇔ (value >= min) - let min_var = self.model.int(min, min); - let b1 = self.model.bool(); - self.model.int_ge_reif(value, min_var, b1); - - // Create: b2 ⇔ (value <= max) - let max_var = self.model.int(max, max); - let b2 = self.model.bool(); - self.model.int_le_reif(value, max_var, b2); - - // Create: b ⇔ (b1 AND b2) - let and_result = self.model.bool_and(&[b1, b2]); - self.model.new(b.eq(and_result)); - - Ok(()) - } - Expr::SetLit(elements) => { - // Handle explicit set like {1, 2, 3} - // b ⇔ (value = elements[0] OR value = elements[1] OR ...) - - if elements.is_empty() { - // Empty set: b must be false - self.model.new(b.eq(0)); - return Ok(()); - } - - // Create b_i ⇔ (value = element[i]) for each element - let mut membership_vars = Vec::new(); - for elem in elements { - let elem_val = self.extract_int(elem)?; - let elem_var = self.model.int(elem_val, elem_val); - let bi = self.model.bool(); - self.model.int_eq_reif(value, elem_var, bi); - membership_vars.push(bi); - } - - // b ⇔ OR of all membership variables - let or_result = self.model.bool_or(&membership_vars); - self.model.new(b.eq(or_result)); - - Ok(()) - } - _ => Err(FlatZincError::MapError { - message: format!("Unsupported set type in set_in_reif: {:?}", constraint.args[1]), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }), - } - } - - /// Map set_in: value ∈ set (non-reified version) - /// FlatZinc signature: set_in(value, set) - pub(in crate::flatzinc::mapper) fn map_set_in(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "set_in requires 2 arguments (value, set)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - // Get the value - let value = self.get_var_or_const(&constraint.args[0])?; - - // Parse the set - match &constraint.args[1] { - Expr::Range(min_expr, max_expr) => { - // Handle range like 1..10 - let min = self.extract_int(min_expr)?; - let max = self.extract_int(max_expr)?; - - // value ∈ [min, max] => (value >= min) AND (value <= max) - self.model.new(value.ge(min)); - self.model.new(value.le(max)); - - Ok(()) - } - Expr::SetLit(elements) => { - // Handle explicit set like {1, 2, 3} - // value ∈ {e1, e2, ...} => (value = e1) OR (value = e2) OR ... - - if elements.is_empty() { - // Empty set: contradiction - return Err(FlatZincError::MapError { - message: "set_in with empty set is unsatisfiable".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - // Create (value = element[i]) for each element - let mut membership_vars = Vec::new(); - for elem in elements { - let elem_val = self.extract_int(elem)?; - let elem_var = self.model.int(elem_val, elem_val); - let bi = self.model.bool(); - self.model.int_eq_reif(value, elem_var, bi); - membership_vars.push(bi); - } - - // At least one must be true - let or_result = self.model.bool_or(&membership_vars); - self.model.new(or_result.eq(1)); - - Ok(()) - } - _ => Err(FlatZincError::MapError { - message: format!("Unsupported set type in set_in: {:?}", constraint.args[1]), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }), - } - } -} diff --git a/src/flatzinc/mapper/helpers.rs b/src/flatzinc/mapper/helpers.rs deleted file mode 100644 index 76c1d0f..0000000 --- a/src/flatzinc/mapper/helpers.rs +++ /dev/null @@ -1,326 +0,0 @@ -//! Helper functions for extracting values from FlatZinc AST expressions - -use crate::flatzinc::ast::*; -use crate::flatzinc::error::{FlatZincError, FlatZincResult}; -use crate::flatzinc::mapper::MappingContext; -use crate::variables::VarId; - -impl<'a> MappingContext<'a> { - /// Evaluate array access expression: array[index] - /// - /// Resolves expressions like `x[1]` by: - /// 1. Looking up the array variable `x` in array_map - /// 2. Converting the FlatZinc 1-based index to 0-based - /// 3. Returning the VarId at that position - pub(super) fn evaluate_array_access( - &self, - array_expr: &Expr, - index_expr: &Expr, - ) -> FlatZincResult { - // Get the array name - let array_name = match array_expr { - Expr::Ident(name) => name, - _ => { - return Err(FlatZincError::MapError { - message: format!("Array access requires identifier, got: {:?}", array_expr), - line: None, - column: None, - }); - } - }; - - // Get the array - let array = self.array_map.get(array_name).ok_or_else(|| { - FlatZincError::MapError { - message: format!("Unknown array: {}", array_name), - line: None, - column: None, - } - })?; - - // Get the index (1-based in FlatZinc) - let index_1based = match index_expr { - Expr::IntLit(val) => *val as usize, - _ => { - return Err(FlatZincError::MapError { - message: format!("Array index must be integer literal, got: {:?}", index_expr), - line: None, - column: None, - }); - } - }; - - // Convert to 0-based and bounds check - if index_1based < 1 { - return Err(FlatZincError::MapError { - message: format!("Array index must be >= 1, got: {}", index_1based), - line: None, - column: None, - }); - } - let index_0based = index_1based - 1; - - if index_0based >= array.len() { - return Err(FlatZincError::MapError { - message: format!( - "Array index {} out of bounds for array '{}' of length {}", - index_1based, - array_name, - array.len() - ), - line: None, - column: None, - }); - } - - Ok(array[index_0based]) - } - - /// Get a variable by identifier or array access - pub(super) fn get_var(&self, expr: &Expr) -> FlatZincResult { - match expr { - Expr::Ident(name) => { - self.var_map.get(name).copied().ok_or_else(|| { - FlatZincError::MapError { - message: format!("Unknown variable: {}", name), - line: None, - column: None, - } - }) - } - Expr::ArrayAccess { array, index } => { - // Handle array access like x[1] - self.evaluate_array_access(array, index) - } - _ => Err(FlatZincError::MapError { - message: format!("Expected variable identifier or array access, got: {:?}", expr), - line: None, - column: None, - }), - } - } - - /// Get a variable or convert a constant to a fixed variable - /// Handles: variables, array access, integer literals, boolean literals - pub(super) fn get_var_or_const(&mut self, expr: &Expr) -> FlatZincResult { - match expr { - Expr::Ident(name) => { - self.var_map.get(name).copied().ok_or_else(|| { - FlatZincError::MapError { - message: format!("Unknown variable: {}", name), - line: None, - column: None, - } - }) - } - Expr::ArrayAccess { array, index } => { - // Handle array access like x[1] - self.evaluate_array_access(array, index) - } - Expr::IntLit(val) => { - // Convert constant to fixed variable - Ok(self.model.int(*val as i32, *val as i32)) - } - Expr::BoolLit(b) => { - // Convert boolean to 0/1 fixed variable - let val = if *b { 1 } else { 0 }; - Ok(self.model.int(val, val)) - } - _ => Err(FlatZincError::MapError { - message: format!("Unsupported expression type: {:?}", expr), - line: None, - column: None, - }), - } - } - - /// Extract an integer value from an expression - pub(super) fn extract_int(&self, expr: &Expr) -> FlatZincResult { - match expr { - Expr::IntLit(val) => Ok(*val as i32), - Expr::Ident(name) => { - // Could be a parameter - for now, just error - Err(FlatZincError::MapError { - message: format!("Expected integer literal, got identifier: {}", name), - line: None, - column: None, - }) - } - _ => Err(FlatZincError::MapError { - message: "Expected integer literal".to_string(), - line: None, - column: None, - }), - } - } - - /// Extract an array of integers from an expression - /// - /// Handles: - /// - Inline array literals: [1, 2, 3] - /// - Parameter array identifiers: col_left (references previously declared parameter array) - pub(super) fn extract_int_array(&self, expr: &Expr) -> FlatZincResult> { - match expr { - Expr::ArrayLit(elements) => { - elements.iter().map(|e| self.extract_int(e)).collect() - } - Expr::Ident(name) => { - // Look up parameter array by name - self.param_int_arrays.get(name) - .cloned() - .ok_or_else(|| FlatZincError::MapError { - message: format!("Parameter array '{}' not found (expected array of integers)", name), - line: None, - column: None, - }) - } - _ => Err(FlatZincError::MapError { - message: "Expected array of integers or array identifier".to_string(), - line: None, - column: None, - }), - } - } - - /// Extract a boolean value from an expression - pub(super) fn extract_bool(&self, expr: &Expr) -> FlatZincResult { - match expr { - Expr::BoolLit(val) => Ok(*val), - Expr::IntLit(val) => Ok(*val != 0), // Treat 0 as false, non-zero as true - Expr::Ident(name) => { - // Could be a parameter - for now, just error - Err(FlatZincError::MapError { - message: format!("Expected boolean literal, got identifier: {}", name), - line: None, - column: None, - }) - } - _ => Err(FlatZincError::MapError { - message: "Expected boolean literal".to_string(), - line: None, - column: None, - }), - } - } - - /// Extract an array of booleans from an expression - /// - /// Handles: - /// - Inline array literals: [true, false, true] - /// - Parameter array identifiers: flags (references previously declared parameter array) - pub(super) fn extract_bool_array(&self, expr: &Expr) -> FlatZincResult> { - match expr { - Expr::ArrayLit(elements) => { - elements.iter().map(|e| self.extract_bool(e)).collect() - } - Expr::Ident(name) => { - // Look up parameter array by name - self.param_bool_arrays.get(name) - .cloned() - .ok_or_else(|| FlatZincError::MapError { - message: format!("Parameter array '{}' not found (expected array of booleans)", name), - line: None, - column: None, - }) - } - _ => Err(FlatZincError::MapError { - message: "Expected array of booleans or array identifier".to_string(), - line: None, - column: None, - }), - } - } - - /// Extract an array of variables from an expression - /// - /// Handles: - /// - Array literals like `[x, y, z]` (may contain variables, array access, or integer constants) - /// - Array identifiers that reference previously declared arrays - /// - Single variable identifiers (treated as single-element array) - pub(super) fn extract_var_array(&mut self, expr: &Expr) -> FlatZincResult> { - match expr { - Expr::ArrayLit(elements) => { - // Handle array literals that may contain variables, array access, or integer constants - let mut var_ids = Vec::new(); - for elem in elements { - match elem { - Expr::Ident(name) => { - // Variable reference - let var_id = self.var_map.get(name).copied().ok_or_else(|| { - FlatZincError::MapError { - message: format!("Unknown variable: {}", name), - line: None, - column: None, - } - })?; - var_ids.push(var_id); - } - Expr::IntLit(val) => { - // Constant integer - create a fixed variable - let const_var = self.model.int(*val as i32, *val as i32); - var_ids.push(const_var); - } - Expr::BoolLit(b) => { - // Constant boolean - create a fixed variable (0 or 1) - let val = if *b { 1 } else { 0 }; - let const_var = self.model.int(val, val); - var_ids.push(const_var); - } - Expr::ArrayAccess { array, index } => { - // Array element access like x[1] - let var_id = self.evaluate_array_access(array, index)?; - var_ids.push(var_id); - } - _ => { - return Err(FlatZincError::MapError { - message: format!("Unsupported array element: {:?}", elem), - line: None, - column: None, - }); - } - } - } - Ok(var_ids) - } - Expr::Ident(name) => { - // First check if it's an array variable - if let Some(arr) = self.array_map.get(name) { - return Ok(arr.clone()); - } - - // Check if it's a parameter int array - create constant VarIds - if let Some(int_values) = self.param_int_arrays.get(name) { - let var_ids: Vec = int_values.iter() - .map(|&val| self.model.int(val, val)) - .collect(); - return Ok(var_ids); - } - - // Check if it's a parameter bool array - create constant VarIds - if let Some(bool_values) = self.param_bool_arrays.get(name) { - let var_ids: Vec = bool_values.iter() - .map(|&b| { - let val = if b { 1 } else { 0 }; - self.model.int(val, val) - }) - .collect(); - return Ok(var_ids); - } - - // Otherwise treat as single variable - Ok(vec![self.var_map.get(name).copied().ok_or_else(|| { - FlatZincError::MapError { - message: format!("Unknown variable or array: {}", name), - line: None, - column: None, - } - })?]) - } - _ => Err(FlatZincError::MapError { - message: "Expected array of variables".to_string(), - line: None, - column: None, - }), - } - } -} diff --git a/src/flatzinc/mapper_old_backup.rs b/src/flatzinc/mapper_old_backup.rs deleted file mode 100644 index 9eada4c..0000000 --- a/src/flatzinc/mapper_old_backup.rs +++ /dev/null @@ -1,798 +0,0 @@ -//! AST to Selen Model Mapper -//! -//! Converts FlatZinc AST into a Selen constraint model. - -use crate::flatzinc::ast::*; -use crate::flatzinc::error::{FlatZincError, FlatZincResult}; -use crate::prelude::Model; -use crate::variables::VarId; -use crate::runtime_api::{VarIdExt, ModelExt}; -use std::collections::HashMap; - -/// Context for mapping AST to Model -pub struct MappingContext<'a> { - model: &'a mut Model, - var_map: HashMap, - /// Maps array names to their variable lists - array_map: HashMap>, -} - -impl<'a> MappingContext<'a> { - pub fn new(model: &'a mut Model) -> Self { - MappingContext { - model, - var_map: HashMap::new(), - array_map: HashMap::new(), - } - } - - /// Map variable declarations to Selen variables - fn map_var_decl(&mut self, decl: &VarDecl) -> FlatZincResult<()> { - let var_id = match &decl.var_type { - Type::Var(inner_type) => match **inner_type { - Type::Bool => self.model.bool(), - Type::Int => self.model.int(i32::MIN, i32::MAX), - Type::IntRange(min, max) => { - self.model.int(min as i32, max as i32) - } - Type::IntSet(ref values) => { - if values.is_empty() { - return Err(FlatZincError::MapError { - message: format!("Empty domain for variable {}", decl.name), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - } - let min = *values.iter().min().unwrap(); - let max = *values.iter().max().unwrap(); - // TODO: Handle sparse domains more efficiently - self.model.int(min as i32, max as i32) - } - Type::Float => self.model.float(f64::NEG_INFINITY, f64::INFINITY), - Type::FloatRange(min, max) => self.model.float(min, max), - _ => { - return Err(FlatZincError::UnsupportedFeature { - feature: format!("Variable type: {:?}", inner_type), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - } - }, - Type::Array { index_sets, element_type } => { - // Two cases for array variables: - // 1. Collecting existing variables: array [...] = [var1, var2, ...] - // 2. Creating new array of variables: array [1..n] of var int: arr - - if let Some(ref init) = decl.init_value { - // Case 1: Array collects existing variables/constants - match init { - Expr::ArrayLit(elements) => { - let mut var_ids = Vec::new(); - for elem in elements { - match elem { - Expr::Ident(name) => { - // Reference to existing variable - let var_id = self.var_map.get(name).ok_or_else(|| { - FlatZincError::MapError { - message: format!("Undefined variable '{}' in array", name), - line: Some(decl.location.line), - column: Some(decl.location.column), - } - })?; - var_ids.push(*var_id); - } - Expr::IntLit(val) => { - // Constant integer - create a fixed variable - let const_var = self.model.int(*val as i32, *val as i32); - var_ids.push(const_var); - } - _ => { - return Err(FlatZincError::UnsupportedFeature { - feature: format!("Array element expression: {:?}", elem), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - } - } - } - // Store the array mapping - self.array_map.insert(decl.name.clone(), var_ids); - return Ok(()); // Arrays don't create new variables - } - _ => { - return Err(FlatZincError::UnsupportedFeature { - feature: format!("Array initialization: {:?}", init), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - } - } - } else { - // Case 2: Create new array of variables (no initialization) - // e.g., array [1..5] of var 1..5: animal - match **element_type { - Type::Var(ref inner) => { - match **inner { - Type::IntRange(min, max) => { - // Determine array size from index_sets - // For now, assume single index set [1..n] - let size = if let Some(IndexSet::Range(start, end)) = index_sets.first() { - (end - start + 1) as usize - } else { - return Err(FlatZincError::UnsupportedFeature { - feature: "Array with complex index sets".to_string(), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - }; - - // Create variables for each array element - let var_ids: Vec = (0..size) - .map(|_| self.model.int(min as i32, max as i32)) - .collect(); - - self.array_map.insert(decl.name.clone(), var_ids); - return Ok(()); - } - Type::Int => { - // Full integer domain - let size = if let Some(IndexSet::Range(start, end)) = index_sets.first() { - (end - start + 1) as usize - } else { - return Err(FlatZincError::UnsupportedFeature { - feature: "Array with complex index sets".to_string(), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - }; - - let var_ids: Vec = (0..size) - .map(|_| self.model.int(i32::MIN, i32::MAX)) - .collect(); - - self.array_map.insert(decl.name.clone(), var_ids); - return Ok(()); - } - _ => { - return Err(FlatZincError::UnsupportedFeature { - feature: format!("Array element type: {:?}", inner), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - } - } - } - _ => { - return Err(FlatZincError::UnsupportedFeature { - feature: format!("Array element type: {:?}", element_type), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - } - } - } - } - _ => { - return Err(FlatZincError::MapError { - message: format!("Unexpected variable type: {:?}", decl.var_type), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - } - }; - - // Handle initialization - if let Some(ref init) = decl.init_value { - match init { - Expr::IntLit(val) => { - self.model.new(var_id.eq(*val as i32)); - } - Expr::BoolLit(val) => { - self.model.new(var_id.eq(if *val { 1 } else { 0 })); - } - Expr::FloatLit(val) => { - self.model.new(var_id.eq(*val)); - } - _ => { - return Err(FlatZincError::MapError { - message: "Complex initialization not yet supported".to_string(), - line: Some(decl.location.line), - column: Some(decl.location.column), - }); - } - } - } - - self.var_map.insert(decl.name.clone(), var_id); - Ok(()) - } - - /// Map a constraint to Selen constraint - fn map_constraint(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - match constraint.predicate.as_str() { - "int_eq" => self.map_int_eq(constraint), - "int_ne" => self.map_int_ne(constraint), - "int_lt" => self.map_int_lt(constraint), - "int_le" => self.map_int_le(constraint), - "int_gt" => self.map_int_gt(constraint), - "int_ge" => self.map_int_ge(constraint), - "int_lin_eq" => self.map_int_lin_eq(constraint), - "int_lin_le" => self.map_int_lin_le(constraint), - "int_lin_ne" => self.map_int_lin_ne(constraint), - "fzn_all_different_int" | "all_different_int" | "all_different" => self.map_all_different(constraint), - "int_eq_reif" => self.map_int_eq_reif(constraint), - "int_ne_reif" => self.map_int_ne_reif(constraint), - "int_lt_reif" => self.map_int_lt_reif(constraint), - "int_le_reif" => self.map_int_le_reif(constraint), - "int_gt_reif" => self.map_int_gt_reif(constraint), - "int_ge_reif" => self.map_int_ge_reif(constraint), - "bool_clause" => self.map_bool_clause(constraint), - // Array aggregations - "array_int_minimum" => self.map_array_int_minimum(constraint), - "array_int_maximum" => self.map_array_int_maximum(constraint), - "array_bool_and" => self.map_array_bool_and(constraint), - "array_bool_or" => self.map_array_bool_or(constraint), - // Bool-int conversion - "bool2int" => self.map_bool2int(constraint), - // Count constraints - "count_eq" => self.map_count_eq(constraint), - _ => { - Err(FlatZincError::UnsupportedFeature { - feature: format!("Constraint: {}", constraint.predicate), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }) - } - } - } - - fn get_var(&self, expr: &Expr) -> FlatZincResult { - match expr { - Expr::Ident(name) => { - self.var_map.get(name).copied().ok_or_else(|| { - FlatZincError::MapError { - message: format!("Unknown variable: {}", name), - line: None, - column: None, - } - }) - } - _ => Err(FlatZincError::MapError { - message: "Expected variable identifier".to_string(), - line: None, - column: None, - }), - } - } - - fn map_int_eq(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "int_eq requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var(&constraint.args[0])?; - - match &constraint.args[1] { - Expr::Ident(_) => { - let y = self.get_var(&constraint.args[1])?; - self.model.new(x.eq(y)); - } - Expr::IntLit(val) => { - self.model.new(x.eq(*val as i32)); - } - _ => { - return Err(FlatZincError::MapError { - message: "Unsupported argument type for int_eq".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - } - - Ok(()) - } - - fn map_int_ne(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "int_ne requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - self.model.new(x.ne(y)); - Ok(()) - } - - fn map_int_lt(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "int_lt requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - self.model.new(x.lt(y)); - Ok(()) - } - - fn map_int_le(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "int_le requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - self.model.new(x.le(y)); - Ok(()) - } - - fn map_int_gt(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "int_gt requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - self.model.new(x.gt(y)); - Ok(()) - } - - fn map_int_ge(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "int_ge requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - self.model.new(x.ge(y)); - Ok(()) - } - - fn map_int_lin_eq(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - // int_lin_eq([coeffs], [vars], constant) - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_lin_eq requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let coeffs = self.extract_int_array(&constraint.args[0])?; - let var_ids = self.extract_var_array(&constraint.args[1])?; - let constant = self.extract_int(&constraint.args[2])?; - - if coeffs.len() != var_ids.len() { - return Err(FlatZincError::MapError { - message: "Coefficient and variable array lengths must match".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - self.model.int_lin_eq(&coeffs, &var_ids, constant); - Ok(()) - } - - fn map_int_lin_le(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - // int_lin_le([coeffs], [vars], constant) - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_lin_le requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let coeffs = self.extract_int_array(&constraint.args[0])?; - let var_ids = self.extract_var_array(&constraint.args[1])?; - let constant = self.extract_int(&constraint.args[2])?; - - self.model.int_lin_le(&coeffs, &var_ids, constant); - Ok(()) - } - - fn map_int_lin_ne(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - // int_lin_ne([coeffs], [vars], constant) - // Decompose as: sum(coeffs[i] * vars[i]) ≠ constant - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_lin_ne requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let coeffs = self.extract_int_array(&constraint.args[0])?; - let var_ids = self.extract_var_array(&constraint.args[1])?; - let constant = self.extract_int(&constraint.args[2])?; - - // Create sum using Model's API - let scaled_vars: Vec = coeffs - .iter() - .zip(var_ids.iter()) - .map(|(&coeff, &var)| self.model.mul(var, crate::variables::Val::ValI(coeff))) - .collect(); - - let sum_var = self.model.sum(&scaled_vars); - - // Use runtime API to post not-equals constraint: sum ≠ constant - use crate::runtime_api::ModelExt; - self.model.c(sum_var).ne(constant); - Ok(()) - } - - fn map_all_different(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 1 { - return Err(FlatZincError::MapError { - message: "all_different requires 1 argument (array of variables)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let var_ids = self.extract_var_array(&constraint.args[0])?; - self.model.alldiff(&var_ids); - Ok(()) - } - - fn map_int_eq_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_eq_reif requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - let b = self.get_var(&constraint.args[2])?; - self.model.int_eq_reif(x, y, b); - Ok(()) - } - - fn map_int_ne_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_ne_reif requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - let b = self.get_var(&constraint.args[2])?; - self.model.int_ne_reif(x, y, b); - Ok(()) - } - - fn map_int_lt_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_lt_reif requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - let b = self.get_var(&constraint.args[2])?; - self.model.int_lt_reif(x, y, b); - Ok(()) - } - - fn map_int_le_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_le_reif requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - let b = self.get_var(&constraint.args[2])?; - self.model.int_le_reif(x, y, b); - Ok(()) - } - - fn map_int_gt_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_gt_reif requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - let b = self.get_var(&constraint.args[2])?; - self.model.int_gt_reif(x, y, b); - Ok(()) - } - - fn map_int_ge_reif(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "int_ge_reif requires 3 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let x = self.get_var(&constraint.args[0])?; - let y = self.get_var(&constraint.args[1])?; - let b = self.get_var(&constraint.args[2])?; - self.model.int_ge_reif(x, y, b); - Ok(()) - } - - fn map_bool_clause(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "bool_clause requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let pos = self.extract_var_array(&constraint.args[0])?; - let neg = self.extract_var_array(&constraint.args[1])?; - self.model.bool_clause(&pos, &neg); - Ok(()) - } - - fn extract_int(&self, expr: &Expr) -> FlatZincResult { - match expr { - Expr::IntLit(val) => Ok(*val as i32), - _ => Err(FlatZincError::MapError { - message: "Expected integer literal".to_string(), - line: None, - column: None, - }), - } - } - - fn map_array_int_minimum(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "array_int_minimum requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let min_var = self.get_var(&constraint.args[0])?; - let arr_vars = self.extract_var_array(&constraint.args[1])?; - let min_result = self.model.min(&arr_vars).map_err(|e| FlatZincError::MapError { - message: format!("Failed to create min: {}", e), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - })?; - self.model.new(min_var.eq(min_result)); - Ok(()) - } - - fn map_array_int_maximum(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "array_int_maximum requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let max_var = self.get_var(&constraint.args[0])?; - let arr_vars = self.extract_var_array(&constraint.args[1])?; - let max_result = self.model.max(&arr_vars).map_err(|e| FlatZincError::MapError { - message: format!("Failed to create max: {}", e), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - })?; - self.model.new(max_var.eq(max_result)); - Ok(()) - } - - fn map_array_bool_and(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "array_bool_and requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let arr_vars = self.extract_var_array(&constraint.args[0])?; - let result_var = self.get_var(&constraint.args[1])?; - - // result = AND of all elements: result ⇔ (x[0] ∧ x[1] ∧ ... ∧ x[n]) - if arr_vars.is_empty() { - // Empty array: result = true - self.model.new(result_var.eq(1)); - } else if arr_vars.len() == 1 { - self.model.new(result_var.eq(arr_vars[0])); - } else { - // Use Model's bool_and for n-ary conjunction - let and_result = self.model.bool_and(&arr_vars); - self.model.new(result_var.eq(and_result)); - } - Ok(()) - } - - fn map_array_bool_or(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "array_bool_or requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let arr_vars = self.extract_var_array(&constraint.args[0])?; - let result_var = self.get_var(&constraint.args[1])?; - - // result = OR of all elements: result ⇔ (x[0] ∨ x[1] ∨ ... ∨ x[n]) - if arr_vars.is_empty() { - // Empty array: result = false - self.model.new(result_var.eq(0)); - } else if arr_vars.len() == 1 { - self.model.new(result_var.eq(arr_vars[0])); - } else { - // Use Model's bool_or for n-ary disjunction - let or_result = self.model.bool_or(&arr_vars); - self.model.new(result_var.eq(or_result)); - } - Ok(()) - } - - fn map_bool2int(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 2 { - return Err(FlatZincError::MapError { - message: "bool2int requires 2 arguments".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let bool_var = self.get_var(&constraint.args[0])?; - let int_var = self.get_var(&constraint.args[1])?; - // bool2int: int_var = bool_var (bool is 0/1 in Selen) - self.model.new(int_var.eq(bool_var)); - Ok(()) - } - - fn map_count_eq(&mut self, constraint: &Constraint) -> FlatZincResult<()> { - if constraint.args.len() != 3 { - return Err(FlatZincError::MapError { - message: "count_eq requires 3 arguments (array, value, count)".to_string(), - line: Some(constraint.location.line), - column: Some(constraint.location.column), - }); - } - - let arr_vars = self.extract_var_array(&constraint.args[0])?; - let value = self.extract_int(&constraint.args[1])?; - let count_var = self.get_var(&constraint.args[2])?; - - // Use Selen's count constraint - use crate::runtime_api::ModelExt; - self.model.count(&arr_vars, value, count_var); - Ok(()) - } - - fn extract_int_array(&self, expr: &Expr) -> FlatZincResult> { - match expr { - Expr::ArrayLit(elements) => { - elements.iter().map(|e| self.extract_int(e)).collect() - } - _ => Err(FlatZincError::MapError { - message: "Expected array of integers".to_string(), - line: None, - column: None, - }), - } - } - - fn extract_var_array(&mut self, expr: &Expr) -> FlatZincResult> { - match expr { - Expr::ArrayLit(elements) => { - // Handle array literals that may contain variables or integer constants - let mut var_ids = Vec::new(); - for elem in elements { - match elem { - Expr::Ident(name) => { - // Variable reference - let var_id = self.var_map.get(name).copied().ok_or_else(|| { - FlatZincError::MapError { - message: format!("Unknown variable: {}", name), - line: None, - column: None, - } - })?; - var_ids.push(var_id); - } - Expr::IntLit(val) => { - // Constant integer - create a fixed variable - let const_var = self.model.int(*val as i32, *val as i32); - var_ids.push(const_var); - } - _ => { - return Err(FlatZincError::MapError { - message: format!("Unsupported array element: {:?}", elem), - line: None, - column: None, - }); - } - } - } - Ok(var_ids) - } - Expr::Ident(name) => { - // First check if it's an array variable - if let Some(arr) = self.array_map.get(name) { - return Ok(arr.clone()); - } - // Otherwise treat as single variable - Ok(vec![self.var_map.get(name).copied().ok_or_else(|| { - FlatZincError::MapError { - message: format!("Unknown variable or array: {}", name), - line: None, - column: None, - } - })?]) - } - _ => Err(FlatZincError::MapError { - message: "Expected array of variables".to_string(), - line: None, - column: None, - }), - } - } -} - -/// Map FlatZinc AST to an existing Selen Model -pub fn map_to_model_mut(ast: FlatZincModel, model: &mut Model) -> FlatZincResult<()> { - let mut ctx = MappingContext::new(model); - - // Map variable declarations - for var_decl in &ast.var_decls { - ctx.map_var_decl(var_decl)?; - } - - // Map constraints - for constraint in &ast.constraints { - ctx.map_constraint(constraint)?; - } - - // TODO: Handle solve goal (minimize/maximize) - - Ok(()) -} diff --git a/src/flatzinc/mod.rs b/src/flatzinc/mod.rs deleted file mode 100644 index 3bf0fba..0000000 --- a/src/flatzinc/mod.rs +++ /dev/null @@ -1,70 +0,0 @@ -//! FlatZinc Parser and Integration -//! -//! This module provides functionality to parse FlatZinc files and integrate them with Selen's solver. -//! -//! # FlatZinc Format -//! -//! FlatZinc is a low-level solver input language used by the MiniZinc constraint modeling language. -//! It consists of: -//! - Predicate declarations -//! - Variable declarations (var, array) -//! - Constraint statements -//! - Solve goals (satisfy, minimize, maximize) -//! - Output specifications -//! -//! # Modules -//! -//! - `tokenizer`: Lexical analysis - converts text to tokens -//! - `ast`: Abstract Syntax Tree structures -//! - `parser`: Recursive-descent parser -//! - `mapper`: Maps AST to Selen Model -//! - `error`: Error types and handling -//! - `output`: FlatZinc output formatter -//! -//! # Example -//! -//! ```ignore -//! use selen::prelude::*; -//! -//! let fzn_code = r#" -//! var 1..10: x; -//! var 1..10: y; -//! constraint int_eq(x, y); -//! solve satisfy; -//! "#; -//! -//! let mut model = Model::default(); -//! model.from_flatzinc_str(fzn_code)?; -//! match model.solve() { -//! Ok(solution) => println!("Solution found!"), -//! Err(e) => println!("No solution: {:?}", e), -//! } -//! ``` - -mod error; -mod tokenizer; -mod ast; -mod parser; -mod mapper; -mod output; - -pub use error::{FlatZincError, FlatZincResult}; -pub use output::format_solution; - -use crate::prelude::Model; - -/// Parse FlatZinc tokens into AST and map to an existing Model. -/// -/// This is an internal function used by Model::from_flatzinc_* methods. -pub(crate) fn parse_and_map(content: &str, model: &mut Model) -> FlatZincResult<()> { - // Step 1: Tokenize - let tokens = tokenizer::tokenize(content)?; - - // Step 2: Parse into AST - let ast = parser::parse(tokens)?; - - // Step 3: Map AST to the provided Model - mapper::map_to_model_mut(ast, model)?; - - Ok(()) -} diff --git a/src/flatzinc/output.rs b/src/flatzinc/output.rs deleted file mode 100644 index b7c6023..0000000 --- a/src/flatzinc/output.rs +++ /dev/null @@ -1,41 +0,0 @@ -//! FlatZinc Output Formatter -//! -//! Formats solution results according to FlatZinc output specification. - -use crate::variables::{Val, VarId}; -use std::collections::HashMap; - -/// Format a solution in FlatZinc output format -pub fn format_solution( - solution: &HashMap, - var_names: &HashMap, -) -> String { - let mut output = String::new(); - - // Sort variables by name for consistent output - let mut sorted_vars: Vec<_> = var_names.iter().collect(); - sorted_vars.sort_by_key(|(_, name)| name.as_str()); - - for (var_id, name) in sorted_vars { - if let Some(val) = solution.get(var_id) { - let value_str = match val { - Val::ValI(i) => i.to_string(), - Val::ValF(f) => f.to_string(), - }; - output.push_str(&format!("{} = {};\n", name, value_str)); - } - } - - output.push_str("----------\n"); - output -} - -/// Format "no solution" message -pub fn format_no_solution() -> String { - "=====UNSATISFIABLE=====\n".to_string() -} - -/// Format "unknown" message (solver could not determine satisfiability) -pub fn format_unknown() -> String { - "=====UNKNOWN=====\n".to_string() -} diff --git a/src/flatzinc/parser.rs b/src/flatzinc/parser.rs deleted file mode 100644 index 1e3d619..0000000 --- a/src/flatzinc/parser.rs +++ /dev/null @@ -1,547 +0,0 @@ -//! FlatZinc Parser -//! -//! Recursive-descent parser that converts tokens into an AST. - -use crate::flatzinc::ast::*; -use crate::flatzinc::error::{FlatZincError, FlatZincResult}; -use crate::flatzinc::tokenizer::{Token, TokenType, Location}; - -/// Parser state -pub struct Parser { - tokens: Vec, - position: usize, -} - -impl Parser { - pub fn new(tokens: Vec) -> Self { - Parser { tokens, position: 0 } - } - - fn current(&self) -> &Token { - self.tokens.get(self.position).unwrap_or(&self.tokens[self.tokens.len() - 1]) - } - - fn peek(&self) -> &TokenType { - &self.current().token_type - } - - fn location(&self) -> Location { - self.current().location - } - - fn advance(&mut self) -> &Token { - let token = &self.tokens[self.position]; - if !matches!(token.token_type, TokenType::Eof) { - self.position += 1; - } - token - } - - fn expect(&mut self, expected: TokenType) -> FlatZincResult<()> { - if std::mem::discriminant(self.peek()) == std::mem::discriminant(&expected) { - self.advance(); - Ok(()) - } else { - let loc = self.location(); - Err(FlatZincError::ParseError { - message: format!("Expected {:?}, found {:?}", expected, self.peek()), - line: loc.line, - column: loc.column, - }) - } - } - - fn match_token(&mut self, token_type: &TokenType) -> bool { - if std::mem::discriminant(self.peek()) == std::mem::discriminant(token_type) { - self.advance(); - true - } else { - false - } - } - - /// Parse the entire FlatZinc model - pub fn parse_model(&mut self) -> FlatZincResult { - let mut model = FlatZincModel::new(); - - while !matches!(self.peek(), TokenType::Eof) { - match self.peek() { - TokenType::Predicate => { - model.predicates.push(self.parse_predicate()?); - } - TokenType::Var | TokenType::Array | TokenType::Bool | TokenType::Int | TokenType::Float => { - model.var_decls.push(self.parse_var_decl()?); - } - TokenType::Constraint => { - model.constraints.push(self.parse_constraint()?); - } - TokenType::Solve => { - model.solve_goal = self.parse_solve()?; - } - _ => { - let loc = self.location(); - return Err(FlatZincError::ParseError { - message: format!("Unexpected token: {:?}", self.peek()), - line: loc.line, - column: loc.column, - }); - } - } - } - - Ok(model) - } - - fn parse_predicate(&mut self) -> FlatZincResult { - let loc = self.location(); - self.expect(TokenType::Predicate)?; - - let name = if let TokenType::Identifier(s) = self.peek() { - let n = s.clone(); - self.advance(); - n - } else { - return Err(FlatZincError::ParseError { - message: "Expected predicate name".to_string(), - line: loc.line, - column: loc.column, - }); - }; - - self.expect(TokenType::LeftParen)?; - let params = self.parse_pred_params()?; - self.expect(TokenType::RightParen)?; - self.expect(TokenType::Semicolon)?; - - Ok(PredicateDecl { name, params, location: loc }) - } - - fn parse_pred_params(&mut self) -> FlatZincResult> { - let mut params = Vec::new(); - - if matches!(self.peek(), TokenType::RightParen) { - return Ok(params); - } - - loop { - let param_type = self.parse_type()?; - self.expect(TokenType::Colon)?; - - let name = if let TokenType::Identifier(s) = self.peek() { - let n = s.clone(); - self.advance(); - n - } else { - let loc = self.location(); - return Err(FlatZincError::ParseError { - message: "Expected parameter name".to_string(), - line: loc.line, - column: loc.column, - }); - }; - - params.push(PredParam { param_type, name }); - - if !self.match_token(&TokenType::Comma) { - break; - } - } - - Ok(params) - } - - fn parse_var_decl(&mut self) -> FlatZincResult { - let loc = self.location(); - let var_type = self.parse_type()?; - self.expect(TokenType::Colon)?; - - let name = if let TokenType::Identifier(s) = self.peek() { - let n = s.clone(); - self.advance(); - n - } else { - return Err(FlatZincError::ParseError { - message: "Expected variable name".to_string(), - line: loc.line, - column: loc.column, - }); - }; - - let annotations = self.parse_annotations()?; - - let init_value = if self.match_token(&TokenType::Equals) { - Some(self.parse_expr()?) - } else { - None - }; - - self.expect(TokenType::Semicolon)?; - - Ok(VarDecl { - var_type, - name, - annotations, - init_value, - location: loc, - }) - } - - fn parse_type(&mut self) -> FlatZincResult { - // Handle 'var' prefix - let is_var = self.match_token(&TokenType::Var); - - let base_type = match self.peek() { - TokenType::Bool => { - self.advance(); - Type::Bool - } - TokenType::Int => { - self.advance(); - Type::Int - } - TokenType::Float => { - self.advance(); - Type::Float - } - TokenType::IntLiteral(min) => { - let min_val = *min; - self.advance(); - self.expect(TokenType::DoubleDot)?; - if let TokenType::IntLiteral(max) = self.peek() { - let max_val = *max; - self.advance(); - Type::IntRange(min_val, max_val) - } else { - let loc = self.location(); - return Err(FlatZincError::ParseError { - message: "Expected integer for range upper bound".to_string(), - line: loc.line, - column: loc.column, - }); - } - } - TokenType::LeftBrace => { - self.advance(); - let values = self.parse_int_set()?; - self.expect(TokenType::RightBrace)?; - Type::IntSet(values) - } - TokenType::Set => { - self.advance(); - self.expect(TokenType::Of)?; - // TODO: Handle set types more completely - self.expect(TokenType::Int)?; - Type::SetOfInt - } - TokenType::Array => { - self.advance(); - self.expect(TokenType::LeftBracket)?; - let index_sets = self.parse_index_sets()?; - self.expect(TokenType::RightBracket)?; - self.expect(TokenType::Of)?; - let element_type = Box::new(self.parse_type()?); - Type::Array { index_sets, element_type } - } - _ => { - let loc = self.location(); - return Err(FlatZincError::ParseError { - message: format!("Expected type, found {:?}", self.peek()), - line: loc.line, - column: loc.column, - }); - } - }; - - if is_var { - Ok(Type::Var(Box::new(base_type))) - } else { - Ok(base_type) - } - } - - fn parse_int_set(&mut self) -> FlatZincResult> { - let mut values = Vec::new(); - - if matches!(self.peek(), TokenType::RightBrace) { - return Ok(values); - } - - loop { - if let TokenType::IntLiteral(val) = self.peek() { - values.push(*val); - self.advance(); - } else { - let loc = self.location(); - return Err(FlatZincError::ParseError { - message: "Expected integer in set".to_string(), - line: loc.line, - column: loc.column, - }); - } - - if !self.match_token(&TokenType::Comma) { - break; - } - } - - Ok(values) - } - - fn parse_index_sets(&mut self) -> FlatZincResult> { - let mut index_sets = Vec::new(); - - loop { - // Handle 'int' as index set type (for predicate declarations) - if let TokenType::Int = self.peek() { - self.advance(); - index_sets.push(IndexSet::Range(1, 1000000)); // Arbitrary large range for 'int' - } - // Handle numeric range like 1..8 OR single integer like [1] (meaning 1..1) - else if let TokenType::IntLiteral(min) = self.peek() { - let min_val = *min; - self.advance(); - - // Check if there's a range operator (..) - if self.match_token(&TokenType::DoubleDot) { - // It's a range: min..max - if let TokenType::IntLiteral(max) = self.peek() { - let max_val = *max; - self.advance(); - index_sets.push(IndexSet::Range(min_val, max_val)); - } else { - let loc = self.location(); - return Err(FlatZincError::ParseError { - message: "Expected integer for index range upper bound".to_string(), - line: loc.line, - column: loc.column, - }); - } - } else { - // It's a single integer: treat as range 1..min_val - // This handles array[1] or array[N] syntax - index_sets.push(IndexSet::Range(1, min_val)); - } - } else { - break; - } - - if !self.match_token(&TokenType::Comma) { - break; - } - } - - Ok(index_sets) - } - - fn parse_constraint(&mut self) -> FlatZincResult { - let loc = self.location(); - self.expect(TokenType::Constraint)?; - - let predicate = if let TokenType::Identifier(s) = self.peek() { - let n = s.clone(); - self.advance(); - n - } else { - return Err(FlatZincError::ParseError { - message: "Expected constraint predicate name".to_string(), - line: loc.line, - column: loc.column, - }); - }; - - self.expect(TokenType::LeftParen)?; - let args = self.parse_exprs()?; - self.expect(TokenType::RightParen)?; - - let annotations = self.parse_annotations()?; - self.expect(TokenType::Semicolon)?; - - Ok(Constraint { - predicate, - args, - annotations, - location: loc, - }) - } - - fn parse_solve(&mut self) -> FlatZincResult { - self.expect(TokenType::Solve)?; - - // Parse annotations that come before the goal (e.g., solve :: int_search(...) satisfy) - let annotations = self.parse_annotations()?; - - let goal = match self.peek() { - TokenType::Satisfy => { - self.advance(); - SolveGoal::Satisfy { annotations } - } - TokenType::Minimize => { - self.advance(); - let objective = self.parse_expr()?; - SolveGoal::Minimize { objective, annotations } - } - TokenType::Maximize => { - self.advance(); - let objective = self.parse_expr()?; - SolveGoal::Maximize { objective, annotations } - } - _ => { - let loc = self.location(); - return Err(FlatZincError::ParseError { - message: "Expected satisfy, minimize, or maximize".to_string(), - line: loc.line, - column: loc.column, - }); - } - }; - - self.expect(TokenType::Semicolon)?; - Ok(goal) - } - - fn parse_annotations(&mut self) -> FlatZincResult> { - let mut annotations = Vec::new(); - - while self.match_token(&TokenType::DoubleColon) { - if let TokenType::Identifier(name) = self.peek() { - let ann_name = name.clone(); - self.advance(); - - let args = if self.match_token(&TokenType::LeftParen) { - let exprs = self.parse_exprs()?; - self.expect(TokenType::RightParen)?; - exprs - } else { - Vec::new() - }; - - annotations.push(Annotation { name: ann_name, args }); - } - } - - Ok(annotations) - } - - fn parse_exprs(&mut self) -> FlatZincResult> { - let mut exprs = Vec::new(); - - if matches!(self.peek(), TokenType::RightParen) { - return Ok(exprs); - } - - loop { - exprs.push(self.parse_expr()?); - if !self.match_token(&TokenType::Comma) { - break; - } - } - - Ok(exprs) - } - - fn parse_expr(&mut self) -> FlatZincResult { - match self.peek() { - TokenType::True => { - self.advance(); - Ok(Expr::BoolLit(true)) - } - TokenType::False => { - self.advance(); - Ok(Expr::BoolLit(false)) - } - TokenType::IntLiteral(val) => { - let v = *val; - self.advance(); - - // Check for range - if self.match_token(&TokenType::DoubleDot) { - if let TokenType::IntLiteral(max) = self.peek() { - let max_val = *max; - self.advance(); - Ok(Expr::Range(Box::new(Expr::IntLit(v)), Box::new(Expr::IntLit(max_val)))) - } else { - Ok(Expr::IntLit(v)) - } - } else { - Ok(Expr::IntLit(v)) - } - } - TokenType::FloatLiteral(val) => { - let v = *val; - self.advance(); - Ok(Expr::FloatLit(v)) - } - TokenType::StringLiteral(s) => { - let string = s.clone(); - self.advance(); - Ok(Expr::StringLit(string)) - } - TokenType::Identifier(name) => { - let id = name.clone(); - self.advance(); - - // Check for array access - if self.match_token(&TokenType::LeftBracket) { - let index = self.parse_expr()?; - self.expect(TokenType::RightBracket)?; - Ok(Expr::ArrayAccess { - array: Box::new(Expr::Ident(id)), - index: Box::new(index), - }) - } else { - Ok(Expr::Ident(id)) - } - } - TokenType::LeftBracket => { - self.advance(); - let elements = self.parse_exprs()?; - self.expect(TokenType::RightBracket)?; - Ok(Expr::ArrayLit(elements)) - } - TokenType::LeftBrace => { - self.advance(); - let elements = self.parse_exprs()?; - self.expect(TokenType::RightBrace)?; - Ok(Expr::SetLit(elements)) - } - _ => { - let loc = self.location(); - Err(FlatZincError::ParseError { - message: format!("Unexpected token in expression: {:?}", self.peek()), - line: loc.line, - column: loc.column, - }) - } - } - } -} - -/// Parse a token stream into an AST -pub fn parse(tokens: Vec) -> FlatZincResult { - let mut parser = Parser::new(tokens); - parser.parse_model() -} - -#[cfg(test)] -mod tests { - use super::*; - use crate::flatzinc::tokenizer::tokenize; - - #[test] - fn test_parse_simple_var() { - let input = "var 1..10: x;\nsolve satisfy;"; - let tokens = tokenize(input).unwrap(); - let ast = parse(tokens).unwrap(); - assert_eq!(ast.var_decls.len(), 1); - assert_eq!(ast.var_decls[0].name, "x"); - } - - #[test] - fn test_parse_constraint() { - let input = "var 1..10: x;\nconstraint int_eq(x, 5);\nsolve satisfy;"; - let tokens = tokenize(input).unwrap(); - let ast = parse(tokens).unwrap(); - assert_eq!(ast.constraints.len(), 1); - assert_eq!(ast.constraints[0].predicate, "int_eq"); - } -} diff --git a/src/flatzinc/tokenizer.rs b/src/flatzinc/tokenizer.rs deleted file mode 100644 index 5863e7e..0000000 --- a/src/flatzinc/tokenizer.rs +++ /dev/null @@ -1,431 +0,0 @@ -//! FlatZinc Tokenizer (Lexer) -//! -//! Converts FlatZinc source text into a stream of tokens with location tracking. - -use crate::flatzinc::error::{FlatZincError, FlatZincResult}; - -/// Source location for error reporting -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub struct Location { - pub line: usize, - pub column: usize, -} - -impl Location { - pub fn new(line: usize, column: usize) -> Self { - Location { line, column } - } -} - -/// Token types in FlatZinc grammar -#[derive(Debug, Clone, PartialEq)] -pub enum TokenType { - // Keywords - Predicate, - Var, - Array, - Of, - Constraint, - Solve, - Satisfy, - Minimize, - Maximize, - Int, - Bool, - Float, - Set, - True, - False, - - // Identifiers and literals - Identifier(String), - IntLiteral(i64), - FloatLiteral(f64), - StringLiteral(String), - - // Operators and punctuation - DoubleColon, // :: - Colon, // : - Semicolon, // ; - Comma, // , - Dot, // . - DoubleDot, // .. - LeftParen, // ( - RightParen, // ) - LeftBracket, // [ - RightBracket, // ] - LeftBrace, // { - RightBrace, // } - Equals, // = - - // End of file - Eof, -} - -/// Token with location information -#[derive(Debug, Clone, PartialEq)] -pub struct Token { - pub token_type: TokenType, - pub location: Location, -} - -impl Token { - pub fn new(token_type: TokenType, location: Location) -> Self { - Token { token_type, location } - } -} - -/// Tokenizer state -pub struct Tokenizer { - input: Vec, - position: usize, - line: usize, - column: usize, -} - -impl Tokenizer { - pub fn new(input: &str) -> Self { - Tokenizer { - input: input.chars().collect(), - position: 0, - line: 1, - column: 1, - } - } - - fn current_location(&self) -> Location { - Location::new(self.line, self.column) - } - - fn peek(&self) -> Option { - self.input.get(self.position).copied() - } - - fn peek_ahead(&self, offset: usize) -> Option { - self.input.get(self.position + offset).copied() - } - - fn advance(&mut self) -> Option { - if let Some(ch) = self.input.get(self.position) { - self.position += 1; - if *ch == '\n' { - self.line += 1; - self.column = 1; - } else { - self.column += 1; - } - Some(*ch) - } else { - None - } - } - - fn skip_whitespace(&mut self) { - while let Some(ch) = self.peek() { - if ch.is_whitespace() { - self.advance(); - } else { - break; - } - } - } - - fn skip_line_comment(&mut self) { - // Skip until end of line - while let Some(ch) = self.peek() { - self.advance(); - if ch == '\n' { - break; - } - } - } - - fn skip_block_comment(&mut self) -> FlatZincResult<()> { - let start_loc = self.current_location(); - self.advance(); // skip '/' - self.advance(); // skip '*' - - loop { - match self.peek() { - None => { - return Err(FlatZincError::LexError { - message: "Unterminated block comment".to_string(), - line: start_loc.line, - column: start_loc.column, - }); - } - Some('*') if self.peek_ahead(1) == Some('/') => { - self.advance(); // skip '*' - self.advance(); // skip '/' - break; - } - Some(_) => { - self.advance(); - } - } - } - Ok(()) - } - - fn read_identifier(&mut self) -> String { - let mut result = String::new(); - while let Some(ch) = self.peek() { - if ch.is_alphanumeric() || ch == '_' { - result.push(ch); - self.advance(); - } else { - break; - } - } - result - } - - fn read_number(&mut self) -> FlatZincResult { - let start_loc = self.current_location(); - let mut num_str = String::new(); - let mut is_float = false; - - // Handle negative sign - if self.peek() == Some('-') { - num_str.push('-'); - self.advance(); - } - - // Read digits - while let Some(ch) = self.peek() { - if ch.is_ascii_digit() { - num_str.push(ch); - self.advance(); - } else if ch == '.' && !is_float && self.peek_ahead(1).map_or(false, |c| c.is_ascii_digit()) { - is_float = true; - num_str.push(ch); - self.advance(); - } else if ch == 'e' || ch == 'E' { - is_float = true; - num_str.push(ch); - self.advance(); - // Handle optional +/- after 'e' - if let Some('+') | Some('-') = self.peek() { - num_str.push(self.advance().unwrap()); - } - } else { - break; - } - } - - if is_float { - num_str.parse::() - .map(TokenType::FloatLiteral) - .map_err(|_| FlatZincError::LexError { - message: format!("Invalid float literal: {}", num_str), - line: start_loc.line, - column: start_loc.column, - }) - } else { - num_str.parse::() - .map(TokenType::IntLiteral) - .map_err(|_| FlatZincError::LexError { - message: format!("Invalid integer literal: {}", num_str), - line: start_loc.line, - column: start_loc.column, - }) - } - } - - fn read_string(&mut self) -> FlatZincResult { - let start_loc = self.current_location(); - self.advance(); // skip opening quote - - let mut result = String::new(); - loop { - match self.peek() { - None | Some('\n') => { - return Err(FlatZincError::LexError { - message: "Unterminated string literal".to_string(), - line: start_loc.line, - column: start_loc.column, - }); - } - Some('"') => { - self.advance(); - break; - } - Some('\\') => { - self.advance(); - match self.peek() { - Some('n') => { result.push('\n'); self.advance(); } - Some('t') => { result.push('\t'); self.advance(); } - Some('\\') => { result.push('\\'); self.advance(); } - Some('"') => { result.push('"'); self.advance(); } - _ => { - return Err(FlatZincError::LexError { - message: "Invalid escape sequence".to_string(), - line: self.line, - column: self.column, - }); - } - } - } - Some(ch) => { - result.push(ch); - self.advance(); - } - } - } - Ok(result) - } - - pub fn next_token(&mut self) -> FlatZincResult { - self.skip_whitespace(); - - // Handle comments - while self.peek() == Some('%') || (self.peek() == Some('/') && self.peek_ahead(1) == Some('*')) { - if self.peek() == Some('%') { - self.skip_line_comment(); - } else { - self.skip_block_comment()?; - } - self.skip_whitespace(); - } - - let loc = self.current_location(); - - match self.peek() { - None => Ok(Token::new(TokenType::Eof, loc)), - - Some(ch) if ch.is_alphabetic() || ch == '_' => { - let ident = self.read_identifier(); - let token_type = match ident.as_str() { - "predicate" => TokenType::Predicate, - "var" => TokenType::Var, - "array" => TokenType::Array, - "of" => TokenType::Of, - "constraint" => TokenType::Constraint, - "solve" => TokenType::Solve, - "satisfy" => TokenType::Satisfy, - "minimize" => TokenType::Minimize, - "maximize" => TokenType::Maximize, - "int" => TokenType::Int, - "bool" => TokenType::Bool, - "float" => TokenType::Float, - "set" => TokenType::Set, - "true" => TokenType::True, - "false" => TokenType::False, - _ => TokenType::Identifier(ident), - }; - Ok(Token::new(token_type, loc)) - } - - Some(ch) if ch.is_ascii_digit() => { - let token_type = self.read_number()?; - Ok(Token::new(token_type, loc)) - } - - Some('-') if self.peek_ahead(1).map_or(false, |c| c.is_ascii_digit()) => { - let token_type = self.read_number()?; - Ok(Token::new(token_type, loc)) - } - - Some('"') => { - let string = self.read_string()?; - Ok(Token::new(TokenType::StringLiteral(string), loc)) - } - - Some(':') => { - self.advance(); - if self.peek() == Some(':') { - self.advance(); - Ok(Token::new(TokenType::DoubleColon, loc)) - } else { - Ok(Token::new(TokenType::Colon, loc)) - } - } - - Some('.') => { - self.advance(); - if self.peek() == Some('.') { - self.advance(); - Ok(Token::new(TokenType::DoubleDot, loc)) - } else { - Ok(Token::new(TokenType::Dot, loc)) - } - } - - Some(';') => { self.advance(); Ok(Token::new(TokenType::Semicolon, loc)) } - Some(',') => { self.advance(); Ok(Token::new(TokenType::Comma, loc)) } - Some('(') => { self.advance(); Ok(Token::new(TokenType::LeftParen, loc)) } - Some(')') => { self.advance(); Ok(Token::new(TokenType::RightParen, loc)) } - Some('[') => { self.advance(); Ok(Token::new(TokenType::LeftBracket, loc)) } - Some(']') => { self.advance(); Ok(Token::new(TokenType::RightBracket, loc)) } - Some('{') => { self.advance(); Ok(Token::new(TokenType::LeftBrace, loc)) } - Some('}') => { self.advance(); Ok(Token::new(TokenType::RightBrace, loc)) } - Some('=') => { self.advance(); Ok(Token::new(TokenType::Equals, loc)) } - - Some(ch) => { - Err(FlatZincError::LexError { - message: format!("Unexpected character: '{}'", ch), - line: loc.line, - column: loc.column, - }) - } - } - } -} - -/// Tokenize a FlatZinc source string -pub fn tokenize(input: &str) -> FlatZincResult> { - let mut tokenizer = Tokenizer::new(input); - let mut tokens = Vec::new(); - - loop { - let token = tokenizer.next_token()?; - let is_eof = matches!(token.token_type, TokenType::Eof); - tokens.push(token); - if is_eof { - break; - } - } - - Ok(tokens) -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_tokenize_keywords() { - let input = "var int bool predicate constraint solve satisfy"; - let tokens = tokenize(input).unwrap(); - assert_eq!(tokens.len(), 8); // 7 keywords + EOF - assert!(matches!(tokens[0].token_type, TokenType::Var)); - assert!(matches!(tokens[1].token_type, TokenType::Int)); - assert!(matches!(tokens[2].token_type, TokenType::Bool)); - } - - #[test] - fn test_tokenize_numbers() { - let input = "42 -17 3.14 -2.5 1e10"; - let tokens = tokenize(input).unwrap(); - assert!(matches!(tokens[0].token_type, TokenType::IntLiteral(42))); - assert!(matches!(tokens[1].token_type, TokenType::IntLiteral(-17))); - assert!(matches!(tokens[2].token_type, TokenType::FloatLiteral(_))); - } - - #[test] - fn test_tokenize_identifiers() { - let input = "x y_1 foo_bar INT____00001"; - let tokens = tokenize(input).unwrap(); - assert_eq!(tokens.len(), 5); // 4 identifiers + EOF - } - - #[test] - fn test_tokenize_comment() { - let input = "var x; % this is a comment\nvar y;"; - let tokens = tokenize(input).unwrap(); - // Should skip comment - assert!(matches!(tokens[0].token_type, TokenType::Var)); - assert!(matches!(tokens[2].token_type, TokenType::Semicolon)); - assert!(matches!(tokens[3].token_type, TokenType::Var)); - } -} diff --git a/src/lib.rs b/src/lib.rs index 328a648..45b8d8d 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -244,9 +244,6 @@ pub mod api; pub mod prelude; pub mod runtime_api; -// FlatZinc integration -pub mod flatzinc; - // Development and testing modules #[doc(hidden)] pub mod benchmarks; diff --git a/src/model/flatzinc_integration.rs b/src/model/flatzinc_integration.rs deleted file mode 100644 index a257a6b..0000000 --- a/src/model/flatzinc_integration.rs +++ /dev/null @@ -1,72 +0,0 @@ -//! FlatZinc integration methods for Model - -use crate::prelude::Model; -use crate::flatzinc::{parse_and_map, FlatZincResult}; -use std::fs; -use std::path::Path; - -impl Model { - /// Import a FlatZinc file into this model. - /// - /// This allows you to configure the model (memory limits, timeout, etc.) before - /// importing the FlatZinc problem. - /// - /// # Arguments - /// - /// * `path` - Path to the `.fzn` file - /// - /// # Returns - /// - /// `Ok(())` if successful, or a `FlatZincError` if parsing or mapping fails. - /// - /// # Example - /// - /// ```ignore - /// use selen::prelude::*; - /// - /// // Configure model first - /// let mut model = Model::default() - /// .with_timeout_seconds(30); - /// - /// model.from_flatzinc_file("problem.fzn")?; - /// let solution = model.solve()?; - /// ``` - pub fn from_flatzinc_file>(&mut self, path: P) -> FlatZincResult<()> { - let content = fs::read_to_string(path) - .map_err(|e| crate::flatzinc::FlatZincError::IoError(e.to_string()))?; - self.from_flatzinc_str(&content) - } - - /// Import FlatZinc source code into this model. - /// - /// This allows you to configure the model (memory limits, timeout, etc.) before - /// importing the FlatZinc problem. - /// - /// # Arguments - /// - /// * `content` - FlatZinc source code as a string - /// - /// # Returns - /// - /// `Ok(())` if successful, or a `FlatZincError` if parsing or mapping fails. - /// - /// # Example - /// - /// ```ignore - /// use selen::prelude::*; - /// - /// let fzn = r#" - /// var 1..10: x; - /// var 1..10: y; - /// constraint int_eq(x, y); - /// solve satisfy; - /// "#; - /// - /// let mut model = Model::default(); - /// model.from_flatzinc_str(fzn)?; - /// let solution = model.solve()?; - /// ``` - pub fn from_flatzinc_str(&mut self, content: &str) -> FlatZincResult<()> { - parse_and_map(content, self) - } -} diff --git a/src/model/mod.rs b/src/model/mod.rs index a9d0620..b53a06c 100644 --- a/src/model/mod.rs +++ b/src/model/mod.rs @@ -11,7 +11,6 @@ mod factory_internal; // Internal variable creation methods pub mod constraints; pub mod solving; pub mod precision; -mod flatzinc_integration; // FlatZinc import methods // Re-export everything for backward compatibility pub use core::*; \ No newline at end of file diff --git a/src/prelude.rs b/src/prelude.rs index fd6b410..eaae6bb 100644 --- a/src/prelude.rs +++ b/src/prelude.rs @@ -5,6 +5,3 @@ // Re-export everything from the new API prelude pub use crate::api::prelude::*; -// Re-export FlatZinc types and utilities -pub use crate::flatzinc::{FlatZincError, FlatZincResult, format_solution}; - diff --git a/tests/test_flatzinc_batch_01.rs b/tests/test_flatzinc_batch_01.rs deleted file mode 100644 index d353a12..0000000 --- a/tests/test_flatzinc_batch_01.rs +++ /dev/null @@ -1,138 +0,0 @@ -//! Test FlatZinc parser - Batch 01: Simple arithmetic puzzles -//! Tests files that are likely to have basic constraints - -use selen::prelude::*; -use std::path::Path; - -#[test] -#[ignore] -fn test_batch_01_simple_arithmetic() { - let examples_dir = Path::new("zinc/ortools"); - - if !examples_dir.exists() { - println!("Skipping test - examples directory not found"); - return; - } - - let test_files = vec![ - "1d_rubiks_cube.fzn", - "2DPacking.fzn", - "3_coins.fzn", - "3_jugs2_all.fzn", - "3_jugs2.fzn", - "3_jugs.fzn", - "50_puzzle.fzn", - "5x5_puzzle.fzn", - "99_bottles_of_beer.fzn", - "abbott.fzn", - "abc_endview.fzn", - "abpuzzle.fzn", - "added_corner.fzn", - "adjacency_matrix_from_degrees.fzn", - "ages2.fzn", - "alien.fzn", - "alldifferent_consecutive_values.fzn", - "alldifferent_cst.fzn", - "alldifferent_except_0.fzn", - "alldifferent_interval.fzn", - "all_different_modulo.fzn", - "alldifferent_modulo.fzn", - "alldifferent_on_intersection.fzn", - "alldifferent_same_value.fzn", - "alldifferent_soft.fzn", - "all_differ_from_at_least_k_pos.fzn", - "all_equal_me.fzn", - "all_interval1.fzn", - "all_interval2.fzn", - "all_interval3.fzn", - "all_interval4.fzn", - "all_interval5.fzn", - "all_interval6.fzn", - "all_interval.fzn", - "all_min_dist.fzn", - "allocating_developments.fzn", - "all_paths_graph.fzn", - "allperm.fzn", - "alpha.fzn", - "among_diff_0.fzn", - "among_interval.fzn", - "among_low_up.fzn", - "among_modulo.fzn", - "among_seq.fzn", - "and.fzn", - "another_kind_of_magic_square.fzn", - "antisymmetric.fzn", - "a_puzzle.fzn", - "arch_friends.fzn", - "argmax.fzn", - "arith.fzn", - "arithmetic_ring.fzn", - "arith_or.fzn", - "arith_sliding.fzn", - "a_round_of_golf.fzn", - "arrow.fzn", - "artificial_intelligence.fzn", - "assign_and_counts.fzn", - "assign_and_nvalues.fzn", - "assignment2_2.fzn", - "assignment2.fzn", - "assignment3.fzn", - "assignment4.fzn", - "assignment5.fzn", - "assignment6.fzn", - "assignment.fzn", - "atom_smasher.fzn", - "averbach_1.2.fzn", - "averbach_1.3.fzn", - "averbach_1.4.fzn", - "averbach_1.5.fzn", - "averback_1.4.fzn", - "babysitting.fzn", - "balanced_brackets.fzn", - "balanced_matrix.fzn", - "balance.fzn", - "balance_interval.fzn", - "balance_modulo.fzn", - "bales_of_hay.fzn", - "bank_card.fzn", - "battleships10.fzn", - "battleships_1.fzn", - "battleships_2.fzn", - "battleships_3.fzn", - "battleships_4.fzn", - "battleships_5.fzn", - ]; - - let mut success = 0; - let mut failed = 0; - let mut not_found = 0; - - println!("\n=== Batch 01: Simple Arithmetic Puzzles ===\n"); - - for filename in &test_files { - let filepath = examples_dir.join(filename); - - if !filepath.exists() { - println!("⊘ {}", filename); - not_found += 1; - continue; - } - - let mut model = Model::default(); - match model.from_flatzinc_file(&filepath) { - Ok(_) => { - println!("✓ {}", filename); - success += 1; - } - Err(e) => { - println!("✗ {} - {}", filename, e); - failed += 1; - } - } - } - - println!("\nResults: {} success, {} failed, {} not found", success, failed, not_found); - println!("Success rate: {}/{} ({:.1}%)", - success, test_files.len() - not_found, - 100.0 * success as f64 / (test_files.len() - not_found) as f64); -} diff --git a/tests/test_flatzinc_batch_02.rs b/tests/test_flatzinc_batch_02.rs deleted file mode 100644 index 22c835f..0000000 --- a/tests/test_flatzinc_batch_02.rs +++ /dev/null @@ -1,140 +0,0 @@ -//! Test FlatZinc parser - Batch 02: Sudoku and grid puzzles -//! Tests sudoku variants and similar grid-based puzzles - -use selen::prelude::*; -use std::path::Path; - -#[test] -#[ignore] -fn test_batch_02_sudoku() { - let examples_dir = Path::new("zinc/ortools"); - - if !examples_dir.exists() { - println!("Skipping test - examples directory not found"); - return; - } - - let test_files = vec![ - "battleships_6.fzn", - "battleships_7.fzn", - "battleships_8.fzn", - "battleships_9.fzn", - "best_shuffle.fzn", - "between_min_max.fzn", - "binary_matrix2array.fzn", - "binary_tree.fzn", - "binero.fzn", - "bin_packing2.fzn", - "bin_packing_me.fzn", - "birthdays_2010.fzn", - "birthdays_coins.fzn", - "bit_vector1.fzn", - "blending_problem.fzn", - "blocksworld_instance_1.fzn", - "blocksworld_instance_2.fzn", - "blueberry_muffins.fzn", - "bobs_sale.fzn", - "bokus_competition.fzn", - "book_buy.fzn", - "bpp.fzn", - "breaking_news.fzn", - "bridges_to_somewhere.fzn", - "broken_weights.fzn", - "buckets.fzn", - "bug_unsat.fzn", - "building_a_house2.fzn", - "building_a_house.fzn", - "building_a_house_model.fzn", - "building_blocks.fzn", - "bus.fzn", - "bus_scheduling_csplib.fzn", - "bus_scheduling.fzn", - "calculs_d_enfer.fzn", - "calvin_puzzle.fzn", - "candles.fzn", - "capital_budget2.fzn", - "cardinality_atleast.fzn", - "cardinality_atmost.fzn", - "car.fzn", - "car_painting.fzn", - "catalan_numbers.fzn", - "change.fzn", - "change_pair.fzn", - "checker_puzzle.fzn", - "chessset.fzn", - "choose_your_crew.fzn", - "circling_squares.fzn", - "circuit_path.fzn", - "circuit_test.fzn", - "circular_change.fzn", - "clock_triplets.fzn", - "coins3.fzn", - "coins_41_58.fzn", - "coins.fzn", - "coins_grid.fzn", - "coins_problem.fzn", - "collatz2.fzn", - "collatz.fzn", - "coloring_ip.fzn", - "color_simple.fzn", - "col_sum_puzzle.fzn", - "combinatorial_auction.fzn", - "common.fzn", - "common_interval.fzn", - "cond_lex_cost.fzn", - "cond_lex_less.fzn", - "config.fzn", - "congress.fzn", - "connected.fzn", - "consecutive_digits.fzn", - "consecutive_values.fzn", - "constraint.fzn", - "contains_array.fzn", - "contiguity_regular.fzn", - "contractor_costs.fzn", - "correspondence.fzn", - "costas_array.fzn", - "count_ctr.fzn", - "counts.fzn", - "crew.fzn", - "critical_path1.fzn", - "crossbar.fzn", - "crossfigure.fzn", - "crossword2.fzn", - ]; - - let mut success = 0; - let mut failed = 0; - let mut not_found = 0; - - println!("\n=== Batch 02: Sudoku Puzzles ===\n"); - - for filename in &test_files { - let filepath = examples_dir.join(filename); - - if !filepath.exists() { - println!("⊘ {}", filename); - not_found += 1; - continue; - } - - let mut model = Model::default(); - match model.from_flatzinc_file(&filepath) { - Ok(_) => { - println!("✓ {}", filename); - success += 1; - } - Err(e) => { - println!("✗ {} - {}", filename, e); - failed += 1; - } - } - } - - println!("\nResults: {} success, {} failed, {} not found", success, failed, not_found); - if success + failed > 0 { - println!("Success rate: {}/{} ({:.1}%)", - success, success + failed, - 100.0 * success as f64 / (success + failed) as f64); - } -} diff --git a/tests/test_flatzinc_batch_03.rs b/tests/test_flatzinc_batch_03.rs deleted file mode 100644 index 78daeda..0000000 --- a/tests/test_flatzinc_batch_03.rs +++ /dev/null @@ -1,140 +0,0 @@ -//! Test FlatZinc parser - Batch 03: Logic puzzles -//! Tests zebra, einstein, and other logic puzzles - -use selen::prelude::*; -use std::path::Path; - -#[test] -#[ignore] -fn test_batch_03_logic_puzzles() { - let examples_dir = Path::new("zinc/ortools"); - - if !examples_dir.exists() { - println!("Skipping test - examples directory not found"); - return; - } - - let test_files = vec![ - "crossword_bratko.fzn", - "crossword.fzn", - "crowd.fzn", - "crypta.fzn", - "crypto.fzn", - "crypto_ip.fzn", - "cube_sum.fzn", - "cumulative_test.fzn", - "cumulative_test_mats_carlsson.fzn", - "curious_set_of_integers.fzn", - "cur_num.fzn", - "cutstock.fzn", - "cutting_stock_winston.fzn", - "cycle_test2.fzn", - "czech_logical_labyrinth.fzn", - "debruijn2d_2.fzn", - "debruijn2d_3.fzn", - "debruijn2d.fzn", - "debruijn2.fzn", - "debruijn_binary.fzn", - "debruijn_mike_winter2.fzn", - "debruijn_mike_winter3.fzn", - "debruijn_no_repetition.fzn", - "decision_tree_binary.fzn", - "decreasing_me.fzn", - "defending_castle.fzn", - "dennys_menu.fzn", - "derangement.fzn", - "devils_word.fzn", - "diet1.fzn", - "differs_from_at_least_k_pos.fzn", - "diffn_me.fzn", - "digital_roots.fzn", - "digits_of_the_square.fzn", - "dimes.fzn", - "dinner.fzn", - "disjunctive.fzn", - "distance_between.fzn", - "distance_change.fzn", - "dividing_the_spoils.fzn", - "divisible_by_7.fzn", - "divisible_by_9_trough_1.fzn", - "domain_constraint.fzn", - "domain.fzn", - "donald.fzn", - "dqueens.fzn", - "drinking_game.fzn", - "dudeney_bishop_placement1.fzn", - "dudeney_bishop_placement2.fzn", - "dudeney_numbers.fzn", - "earthlin.fzn", - "egg_basket.fzn", - "einav_puzzle.fzn", - "ein_ein_ein_ein_vier.fzn", - "einstein_hurlimann.fzn", - "einstein_opl.fzn", - "element_greatereq.fzn", - "element_lesseq.fzn", - "element_matrix.fzn", - "elementn.fzn", - "element_product.fzn", - "elements_alldifferent.fzn", - "elements.fzn", - "element_sparse.fzn", - "elevator_6_3.fzn", - "elevator_8_4.fzn", - "eliza_pseudonym7.fzn", - "enclosed_tiles.fzn", - "enigma_1000.fzn", - "enigma_1001.fzn", - "enigma_1293.fzn", - "enigma_1530.fzn", - "enigma_1535.fzn", - "enigma_1553.fzn", - "enigma_1555.fzn", - "enigma_1557.fzn", - "enigma_1568.fzn", - "enigma_1570.fzn", - "enigma_1573.fzn", - "enigma_1574.fzn", - "enigma_1575.fzn", - "enigma_1576.fzn", - "enigma_1577.fzn", - "enigma_843.fzn", - "enigma_birthday_magic.fzn", - "enigma_circular_chain.fzn", - ]; - - let mut success = 0; - let mut failed = 0; - let mut not_found = 0; - - println!("\n=== Batch 03: Logic Puzzles ===\n"); - - for filename in &test_files { - let filepath = examples_dir.join(filename); - - if !filepath.exists() { - println!("⊘ {}", filename); - not_found += 1; - continue; - } - - let mut model = Model::default(); - match model.from_flatzinc_file(&filepath) { - Ok(_) => { - println!("✓ {}", filename); - success += 1; - } - Err(e) => { - println!("✗ {} - {}", filename, e); - failed += 1; - } - } - } - - println!("\nResults: {} success, {} failed, {} not found", success, failed, not_found); - if success + failed > 0 { - println!("Success rate: {}/{} ({:.1}%)", - success, success + failed, - 100.0 * success as f64 / (success + failed) as f64); - } -} diff --git a/tests/test_flatzinc_batch_04.rs b/tests/test_flatzinc_batch_04.rs deleted file mode 100644 index bd872f1..0000000 --- a/tests/test_flatzinc_batch_04.rs +++ /dev/null @@ -1,140 +0,0 @@ -//! Test FlatZinc parser - Batch 04: N-Queens variants -//! Tests various N-Queens problems - -use selen::prelude::*; -use std::path::Path; - -#[test] -#[ignore] -fn test_batch_04_queens() { - let examples_dir = Path::new("zinc/ortools"); - - if !examples_dir.exists() { - println!("Skipping test - examples directory not found"); - return; - } - - let test_files = vec![ - "enigma_counting_pennies.fzn", - "enigma_eighteen.fzn", - "enigma_eight_times2.fzn", - "enigma_eight_times.fzn", - "enigma_five_fives.fzn", - "enigma.fzn", - "enigma_planets.fzn", - "enigma_portuguese_squares.fzn", - "eq10.fzn", - "eq20.fzn", - "equal_sized_groups.fzn", - "equivalent.fzn", - "ett_ett_ett_ett_ett__fem.fzn", - "euler_18.fzn", - "euler_1.fzn", - "euler_2.fzn", - "euler_30.fzn", - "euler_39.fzn", - "euler_52.fzn", - "euler_6.fzn", - "euler_9.fzn", - "evens2.fzn", - "evens.fzn", - "evision.fzn", - "exact_cover_dlx.fzn", - "exact_cover_dlx_matrix.fzn", - "exodus.fzn", - "facility_location_problem.fzn", - "factorial.fzn", - "factory_planning_instance.fzn", - "fairies.fzn", - "fair_split_into_3_groups.fzn", - "family.fzn", - "family_riddle.fzn", - "fancy.fzn", - "farm_puzzle0.fzn", - "farm_puzzle.fzn", - "fib_test2.fzn", - "fill_a_pix.fzn", - "filling_table_with_ticks.fzn", - "fill_in_the_squares.fzn", - "five_brigades.fzn", - "five_floors.fzn", - "five.fzn", - "fixed_charge.fzn", - "fix_points.fzn", - "fizz_buzz.fzn", - "football.fzn", - "four_islands.fzn", - "four_power.fzn", - "fractions.fzn", - "franklin_8x8_magic_square.fzn", - "freight_transfer.fzn", - "full_adder.fzn", - "furniture_moving.fzn", - "futoshiki.fzn", - "gap.fzn", - "gardner_prime_puzzle.fzn", - "gardner_sum_square.fzn", - "generalized_knapsack_problem.fzn", - "general_store.fzn", - "giapetto.fzn", - "global_cardinality_no_loop.fzn", - "global_cardinality_table.fzn", - "global_cardinality_with_costs.fzn", - "global_contiguity.fzn", - "golomb.fzn", - "graceful_labeling.fzn", - "graph_degree_sequence.fzn", - "gray_code.fzn", - "greatest_combination.fzn", - "grid_puzzle.fzn", - "grime_puzzle.fzn", - "grocery2.fzn", - "grocery.fzn", - "guards_and_apples2.fzn", - "guards_and_apples.fzn", - "gunport_problem1.fzn", - "gunport_problem2.fzn", - "hamming_distance.fzn", - "hanging_weights.fzn", - "hardy_1729.fzn", - "heterosquare.fzn", - "hidato_exists.fzn", - "hidato.fzn", - "hidato_table2.fzn", - ]; - - let mut success = 0; - let mut failed = 0; - let mut not_found = 0; - - println!("\n=== Batch 04: N-Queens Variants ===\n"); - - for filename in &test_files { - let filepath = examples_dir.join(filename); - - if !filepath.exists() { - println!("⊘ {}", filename); - not_found += 1; - continue; - } - - let mut model = Model::default(); - match model.from_flatzinc_file(&filepath) { - Ok(_) => { - println!("✓ {}", filename); - success += 1; - } - Err(e) => { - println!("✗ {} - {}", filename, e); - failed += 1; - } - } - } - - println!("\nResults: {} success, {} failed, {} not found", success, failed, not_found); - if success + failed > 0 { - println!("Success rate: {}/{} ({:.1}%)", - success, success + failed, - 100.0 * success as f64 / (success + failed) as f64); - } -} diff --git a/tests/test_flatzinc_batch_05.rs b/tests/test_flatzinc_batch_05.rs deleted file mode 100644 index 4ab07a4..0000000 --- a/tests/test_flatzinc_batch_05.rs +++ /dev/null @@ -1,140 +0,0 @@ -//! Test FlatZinc parser - Batch 05: Magic sequences and numbers -//! Tests magic sequence and magic square problems - -use selen::prelude::*; -use std::path::Path; - -#[test] -#[ignore] -fn test_batch_05_magic() { - let examples_dir = Path::new("zinc/ortools"); - - if !examples_dir.exists() { - println!("Skipping test - examples directory not found"); - return; - } - - let test_files = vec![ - "hidato_table.fzn", - "high_iq_problem.fzn", - "hitchcock_transporation_problem.fzn", - "hitting_set.fzn", - "home_improvement.fzn", - "honey_division.fzn", - "houses.fzn", - "how_old_am_i.fzn", - "huey_dewey_louie.fzn", - "hundred_doors_optimized_array.fzn", - "hundred_fowls.fzn", - "ice_cream.fzn", - "imply.fzn", - "increasing_except_0.fzn", - "indexed_sum.fzn", - "inflexions.fzn", - "in_interval.fzn", - "in_relation.fzn", - "in_set.fzn", - "integer_programming1.fzn", - "inter_distance.fzn", - "int_value_precede.fzn", - "inverse_within_range.fzn", - "investment_problem.fzn", - "investment_problem_mip.fzn", - "isbn.fzn", - "itemset_mining.fzn", - "ith_pos_different_from_0.fzn", - "jive_turkeys.fzn", - "jobshop2x2.fzn", - "jobs_puzzle.fzn", - "joshua.fzn", - "jssp.fzn", - "just_forgotten.fzn", - "K4P2GracefulGraph2.fzn", - "K4P2GracefulGraph.fzn", - "kakuro2.fzn", - "kakuro.fzn", - "k_alldifferent.fzn", - "kaprekars_constant2.fzn", - "kaprekars_constant_3.fzn", - "kaprekars_constant_8.fzn", - "kaprekars_constant.fzn", - "kenken2.fzn", - "killer_sudoku2.fzn", - "killer_sudoku.fzn", - "kiselman_semigroup_problem.fzn", - "knapsack1.fzn", - "knapsack2.fzn", - "knapsack_investments.fzn", - "knapsack_rosetta_code_01.fzn", - "knapsack_rosetta_code_bounded.fzn", - "knapsack_rosetta_code_unbounded_int.fzn", - "knight_path.fzn", - "kntdom.fzn", - "kqueens.fzn", - "k_same.fzn", - "k_same_modulo.fzn", - "labeled_dice.fzn", - "lager.fzn", - "lams_problem.fzn", - "langford2.fzn", - "langford.fzn", - "latin_square_card_puzzle.fzn", - "latin_square.fzn", - "latin_squares_fd.fzn", - "lccoin.fzn", - "least_diff.fzn", - "lecture_series.fzn", - "lectures.fzn", - "letter_square.fzn", - "lex2_me.fzn", - "lex_alldifferent.fzn", - "lex_between.fzn", - "lex_chain_less.fzn", - "lex_different.fzn", - "lex_greater_me.fzn", - "lichtenstein_coloring.fzn", - "life.fzn", - "lightmeal2.fzn", - "lightmeal.fzn", - "lights.fzn", - "limerick_primes2.fzn", - "limerick_primes.fzn", - "locker.fzn", - "logical_design.fzn", - ]; - - let mut success = 0; - let mut failed = 0; - let mut not_found = 0; - - println!("\n=== Batch 05: Magic Sequences and Squares ===\n"); - - for filename in &test_files { - let filepath = examples_dir.join(filename); - - if !filepath.exists() { - println!("⊘ {}", filename); - not_found += 1; - continue; - } - - let mut model = Model::default(); - match model.from_flatzinc_file(&filepath) { - Ok(_) => { - println!("✓ {}", filename); - success += 1; - } - Err(e) => { - println!("✗ {} - {}", filename, e); - failed += 1; - } - } - } - - println!("\nResults: {} success, {} failed, {} not found", success, failed, not_found); - if success + failed > 0 { - println!("Success rate: {}/{} ({:.1}%)", - success, success + failed, - 100.0 * success as f64 / (success + failed) as f64); - } -} diff --git a/tests/test_flatzinc_batch_06.rs b/tests/test_flatzinc_batch_06.rs deleted file mode 100644 index 41d5897..0000000 --- a/tests/test_flatzinc_batch_06.rs +++ /dev/null @@ -1,140 +0,0 @@ -//! Test FlatZinc parser - Batch 06: Scheduling and planning -//! Tests scheduling and job shop problems - -use selen::prelude::*; -use std::path::Path; - -#[test] -#[ignore] -fn test_batch_06_scheduling() { - let examples_dir = Path::new("zinc/ortools"); - - if !examples_dir.exists() { - println!("Skipping test - examples directory not found"); - return; - } - - let test_files = vec![ - "logic_puzzle_aop.fzn", - "longest_change.fzn", - "lucky_number.fzn", - "M12.fzn", - "magic3.fzn", - "magic4.fzn", - "magic.fzn", - "magic_modulo_number.fzn", - "magic_sequence2.fzn", - "magic_sequence3.fzn", - "magic_sequence4.fzn", - "magic_sequence.fzn", - "magicsq_3.fzn", - "magicsq_4.fzn", - "magicsq_5.fzn", - "magic_square_frenicle_form.fzn", - "magic_square.fzn", - "magic_squares_and_cards.fzn", - "mamas_age.fzn", - "mango_puzzle.fzn", - "map2.fzn", - "map_coloring_with_costs.fzn", - "map.fzn", - "map_stuckey.fzn", - "marathon2.fzn", - "marathon.fzn", - "matchmaker.fzn", - "matrix2num.fzn", - "max_cut.fzn", - "maxflow.fzn", - "max_flow_taha.fzn", - "max_flow_winston1.fzn", - "maximal_independent_sets.fzn", - "maximum_density_still_life.fzn", - "maximum_modulo.fzn", - "maximum_subarray.fzn", - "max_index.fzn", - "max_m_in_row.fzn", - "max_n.fzn", - "max_nvalue.fzn", - "max_size_set_of_consecutive_var.fzn", - "mceverywhere.fzn", - "message_sending.fzn", - "mfasp.fzn", - "mfvsp.fzn", - "minesweeper_0.fzn", - "minesweeper_1.fzn", - "minesweeper_2.fzn", - "minesweeper_3.fzn", - "minesweeper_4.fzn", - "minesweeper_5.fzn", - "minesweeper_6.fzn", - "minesweeper_7.fzn", - "minesweeper_8.fzn", - "minesweeper_9.fzn", - "minesweeper_basic3.fzn", - "minesweeper_basic4.fzn", - "minesweeper_basic4x4.fzn", - "minesweeper_config_page2.fzn", - "minesweeper_config_page3.fzn", - "minesweeper.fzn", - "minesweeper_german_Lakshtanov.fzn", - "minesweeper_inverse.fzn", - "minesweeper_splitter.fzn", - "minesweeper_wire.fzn", - "minimum_except_0.fzn", - "minimum_greater_than.fzn", - "minimum_modulo.fzn", - "minimum_weight_alldifferent.fzn", - "min_index.fzn", - "min_n.fzn", - "min_nvalue.fzn", - "misp.fzn", - "missing_digit.fzn", - "mixing_party.fzn", - "money_change.fzn", - "monkey_coconuts.fzn", - "monks_and_doors.fzn", - "movie_stars.fzn", - "mr_smith.fzn", - "multidimknapsack_simple.fzn", - "multipl.fzn", - "murder.fzn", - "music_men.fzn", - "mvcp.fzn", - "my_precedence.fzn", - ]; - - let mut success = 0; - let mut failed = 0; - let mut not_found = 0; - - println!("\n=== Batch 06: Scheduling and Planning ===\n"); - - for filename in &test_files { - let filepath = examples_dir.join(filename); - - if !filepath.exists() { - println!("⊘ {}", filename); - not_found += 1; - continue; - } - - let mut model = Model::default(); - match model.from_flatzinc_file(&filepath) { - Ok(_) => { - println!("✓ {}", filename); - success += 1; - } - Err(e) => { - println!("✗ {} - {}", filename, e); - failed += 1; - } - } - } - - println!("\nResults: {} success, {} failed, {} not found", success, failed, not_found); - if success + failed > 0 { - println!("Success rate: {}/{} ({:.1}%)", - success, success + failed, - 100.0 * success as f64 / (success + failed) as f64); - } -} diff --git a/tests/test_flatzinc_batch_07.rs b/tests/test_flatzinc_batch_07.rs deleted file mode 100644 index 55b3fee..0000000 --- a/tests/test_flatzinc_batch_07.rs +++ /dev/null @@ -1,140 +0,0 @@ -//! Test FlatZinc parser - Batch 07: Graph problems -//! Tests graph coloring, paths, and graph-based puzzles - -use selen::prelude::*; -use std::path::Path; - -#[test] -#[ignore] -fn test_batch_07_graph() { - let examples_dir = Path::new("zinc/ortools"); - - if !examples_dir.exists() { - println!("Skipping test - examples directory not found"); - return; - } - - let test_files = vec![ - "nadel.fzn", - "narcissistic_numbers.fzn", - "n_change.fzn", - "nchange.fzn", - "newspaper0.fzn", - "newspaper.fzn", - "next_element.fzn", - "next_greater_element.fzn", - "nim.fzn", - "nine_digit_arrangement.fzn", - "nine_to_one_equals_100.fzn", - "non_dominating_queens.fzn", - "nonogram_create_automaton2.fzn", - "nonogram.fzn", - "nontransitive_dice.fzn", - "no_solve_item.fzn", - "not_all_equal.fzn", - "no_three_in_line.fzn", - "not_in.fzn", - "npair.fzn", - "n_puzzle.fzn", - "n_puzzle_table.fzn", - "number_generation.fzn", - "number_of_days.fzn", - "number_of_regions.fzn", - "number_puzzle.fzn", - "number_square.fzn", - "numeric_keypad.fzn", - "OandX.fzn", - "olympic.fzn", - "onroad.fzn", - "open_alldifferent.fzn", - "open_among.fzn", - "open_atleast.fzn", - "open_atmost.fzn", - "open_global_cardinality.fzn", - "open_global_cardinality_low_up.fzn", - "optimal_picking_elements_from_each_list.fzn", - "organize_day.fzn", - "or_matching2.fzn", - "or_matching.fzn", - "or_matching_orig.fzn", - "or_matching_xxx.fzn", - "ormat_game.fzn", - "ormat_game_generate.fzn", - "ormat_game_mip_problem1.fzn", - "ormat_game_mip_problem2.fzn", - "ormat_game_mip_problem3.fzn", - "ormat_game_mip_problem4.fzn", - "ormat_game_mip_problem5.fzn", - "ormat_game_mip_problem6.fzn", - "ormat_game_problem1.fzn", - "ormat_game_problem2.fzn", - "ormat_game_problem3.fzn", - "ormat_game_problem4.fzn", - "ormat_game_problem5.fzn", - "ormat_game_problem6.fzn", - "or_seating.fzn", - "orth_link_ori_siz_end.fzn", - "orth_on_the_ground.fzn", - "oss.fzn", - "packing.fzn", - "pair_divides_the_sum.fzn", - "pairwise_sum_of_n_numbers.fzn", - "pandigital_numbers.fzn", - "parallel_resistors.fzn", - "partial_latin_square.fzn", - "partition.fzn", - "partition_into_subset_of_equal_values2.fzn", - "partition_into_subset_of_equal_values3.fzn", - "partition_into_subset_of_equal_values.fzn", - "partitions.fzn", - "path_from_to.fzn", - "patient_no_21.fzn", - "pchange.fzn", - "peacableArmyOfQueens.fzn", - "penguin.fzn", - "perfect_shuffle.fzn", - "perfect_square_sequence.fzn", - "perfsq2.fzn", - "perfsq.fzn", - "period.fzn", - "permutation_number.fzn", - "pert.fzn", - "photo.fzn", - "photo_hkj2_data1.fzn", - ]; - - let mut success = 0; - let mut failed = 0; - let mut not_found = 0; - - println!("\n=== Batch 07: Graph Problems ===\n"); - - for filename in &test_files { - let filepath = examples_dir.join(filename); - - if !filepath.exists() { - println!("⊘ {}", filename); - not_found += 1; - continue; - } - - let mut model = Model::default(); - match model.from_flatzinc_file(&filepath) { - Ok(_) => { - println!("✓ {}", filename); - success += 1; - } - Err(e) => { - println!("✗ {} - {}", filename, e); - failed += 1; - } - } - } - - println!("\nResults: {} success, {} failed, {} not found", success, failed, not_found); - if success + failed > 0 { - println!("Success rate: {}/{} ({:.1}%)", - success, success + failed, - 100.0 * success as f64 / (success + failed) as f64); - } -} diff --git a/tests/test_flatzinc_batch_08.rs b/tests/test_flatzinc_batch_08.rs deleted file mode 100644 index 7337d35..0000000 --- a/tests/test_flatzinc_batch_08.rs +++ /dev/null @@ -1,140 +0,0 @@ -//! Test FlatZinc parser - Batch 08: Assignment and matching -//! Tests assignment, stable marriage, and matching problems - -use selen::prelude::*; -use std::path::Path; - -#[test] -#[ignore] -fn test_batch_08_assignment() { - let examples_dir = Path::new("zinc/ortools"); - - if !examples_dir.exists() { - println!("Skipping test - examples directory not found"); - return; - } - - let test_files = vec![ - "photo_hkj2_data2.fzn", - "photo_hkj.fzn", - "picking_teams.fzn", - "pigeon_hole2.fzn", - "pigeon_hole.fzn", - "pilgrim.fzn", - "place_number.fzn", - "pool_ball_triangles.fzn", - "popsicle_stand.fzn", - "post_office_problem2.fzn", - "post_office_problem.fzn", - "power.fzn", - "prime.fzn", - "prime_looking.fzn", - "product_configuration.fzn", - "product_ctr.fzn", - "product_fd.fzn", - "product_lp.fzn", - "product_test.fzn", - "public_school_problem.fzn", - "puzzle1.fzn", - "pyramid_of_numbers.fzn", - "pythagoras.fzn", - "quasiGroup3Idempotent.fzn", - "quasiGroup3NonIdempotent.fzn", - "quasiGroup4Idempotent.fzn", - "quasiGroup4NonIdempotent.fzn", - "quasiGroup5Idempotent.fzn", - "quasiGroup5NonIdempotent.fzn", - "quasiGroup6.fzn", - "quasiGroup7.fzn", - "quasigroup_completion.fzn", - "quasigroup_completion_gcc.fzn", - "quasigroup_completion_gomes_demo1.fzn", - "quasigroup_completion_gomes_demo2.fzn", - "quasigroup_completion_gomes_demo3.fzn", - "quasigroup_completion_gomes_demo4.fzn", - "quasigroup_completion_gomes_demo5.fzn", - "quasigroup_completion_gomes_shmoys_p3.fzn", - "quasigroup_completion_gomes_shmoys_p7.fzn", - "quasigroup_completion_martin_lynce.fzn", - "quasigroup_qg5.fzn", - "queen_cp2.fzn", - "queen_ip.fzn", - "queens3.fzn", - "queens4.fzn", - "queens_ip.fzn", - "queens_viz.fzn", - "radiation.fzn", - "range_ctr.fzn", - "raven_puzzle.fzn", - "rectangle_from_line_segments.fzn", - "regular_test.fzn", - "rehearsal.fzn", - "relative_sizes.fzn", - "relief_mission.fzn", - "remainder_puzzle2.fzn", - "remainder_puzzle.fzn", - "remarkable_sequence.fzn", - "reveal_the_mapping.fzn", - "rock_star_dressing_problem.fzn", - "rogo3.fzn", - "rogo.fzn", - "rook_path.fzn", - "rookwise_chain.fzn", - "roots_test.fzn", - "rostering.fzn", - "rot13.fzn", - "rotation.fzn", - "runs.fzn", - "safe_cracking.fzn", - "same_and_global_cardinality.fzn", - "same_and_global_cardinality_low_up.fzn", - "same.fzn", - "same_interval.fzn", - "same_modulo.fzn", - "sangraal.fzn", - "sat.fzn", - "satisfy.fzn", - "scene_allocation.fzn", - "schedule1.fzn", - "schedule2.fzn", - "scheduling_bratko2.fzn", - "scheduling_bratko.fzn", - "scheduling_chip.fzn", - "scheduling_speakers.fzn", - ]; - - let mut success = 0; - let mut failed = 0; - let mut not_found = 0; - - println!("\n=== Batch 08: Assignment and Matching ===\n"); - - for filename in &test_files { - let filepath = examples_dir.join(filename); - - if !filepath.exists() { - println!("⊘ {}", filename); - not_found += 1; - continue; - } - - let mut model = Model::default(); - match model.from_flatzinc_file(&filepath) { - Ok(_) => { - println!("✓ {}", filename); - success += 1; - } - Err(e) => { - println!("✗ {} - {}", filename, e); - failed += 1; - } - } - } - - println!("\nResults: {} success, {} failed, {} not found", success, failed, not_found); - if success + failed > 0 { - println!("Success rate: {}/{} ({:.1}%)", - success, success + failed, - 100.0 * success as f64 / (success + failed) as f64); - } -} diff --git a/tests/test_flatzinc_batch_09.rs b/tests/test_flatzinc_batch_09.rs deleted file mode 100644 index cd41e4f..0000000 --- a/tests/test_flatzinc_batch_09.rs +++ /dev/null @@ -1,140 +0,0 @@ -//! Test FlatZinc parser - Batch 09: Knapsack and optimization -//! Tests knapsack variants and optimization problems - -use selen::prelude::*; -use std::path::Path; - -#[test] -#[ignore] -fn test_batch_09_knapsack() { - let examples_dir = Path::new("zinc/ortools"); - - if !examples_dir.exists() { - println!("Skipping test - examples directory not found"); - return; - } - - let test_files = vec![ - "seating_plan.fzn", - "seating_row1.fzn", - "seating_row.fzn", - "seating_table.fzn", - "secret_santa2.fzn", - "secret_santa.fzn", - "seg_fault.fzn", - "self_referential_quiz.fzn", - "send_more_money2.fzn", - "send_more_money_any_base.fzn", - "send_more_money.fzn", - "send_more_money_ip.fzn", - "send_most_money.fzn", - "sequence_2_3.fzn", - "seseman2.fzn", - "seseman.fzn", - "set_covering2.fzn", - "set_covering3.fzn", - "set_covering4b.fzn", - "set_covering4.fzn", - "set_covering5.fzn", - "set_covering6.fzn", - "set_covering_deployment.fzn", - "set_covering.fzn", - "set_covering_skiena.fzn", - "set_packing.fzn", - "seven11.fzn", - "shift.fzn", - "shopping_basket2.fzn", - "shopping_basket5.fzn", - "shopping_basket6.fzn", - "shopping_basket.fzn", - "shopping.fzn", - "shortest_path1.fzn", - "shortest_path2.fzn", - "sicherman_dice.fzn", - "simple_sat.fzn", - "singHoist2.fzn", - "ski_assignment_problem.fzn", - "skyscraper.fzn", - "sliding_sum_me.fzn", - "sliding_time_window_from_start.fzn", - "sliding_time_window.fzn", - "smooth.fzn", - "smuggler_knapsack.fzn", - "smullyan_knights_knaves.fzn", - "smullyan_knights_knaves_normals_bahava.fzn", - "smullyan_knights_knaves_normals.fzn", - "smullyan_lion_and_unicorn.fzn", - "smullyan_portia.fzn", - "soccer_puzzle.fzn", - "social_golfers1.fzn", - "soft_all_equal_ctr.fzn", - "soft_same_var.fzn", - "solitaire_battleship.fzn", - "sonet_problem.fzn", - "sort_permutation.fzn", - "spinning_disks.fzn", - "sportsScheduling.fzn", - "spp.fzn", - "spy_girls.fzn", - "square_root_of_wonderful.fzn", - "squeens.fzn", - "stable_marriage3_random10.fzn", - "stable_marriage3_random200.fzn", - "stable_marriage3_random50.fzn", - "stable_marriage.fzn", - "stamp_licking.fzn", - "state_name_puzzle.fzn", - "stretch_circuit.fzn", - "stretch_path.fzn", - "strictly_decreasing.fzn", - "strimko2.fzn", - "stuckey_assignment.fzn", - "stuckey_seesaw.fzn", - "subsequence.fzn", - "subsequence_sum.fzn", - "subset_sum.fzn", - "successive_number_problem.fzn", - "sudoku_25x25_250.fzn", - "sudoku_alldifferent.fzn", - "sudoku.fzn", - "sudoku_gcc.fzn", - "sudoku_ip.fzn", - "sudoku_pi_2008.fzn", - "sudoku_pi_2010.fzn", - ]; - - let mut success = 0; - let mut failed = 0; - let mut not_found = 0; - - println!("\n=== Batch 09: Knapsack and Optimization ===\n"); - - for filename in &test_files { - let filepath = examples_dir.join(filename); - - if !filepath.exists() { - println!("⊘ {}", filename); - not_found += 1; - continue; - } - - let mut model = Model::default(); - match model.from_flatzinc_file(&filepath) { - Ok(_) => { - println!("✓ {}", filename); - success += 1; - } - Err(e) => { - println!("✗ {} - {}", filename, e); - failed += 1; - } - } - } - - println!("\nResults: {} success, {} failed, {} not found", success, failed, not_found); - if success + failed > 0 { - println!("Success rate: {}/{} ({:.1}%)", - success, success + failed, - 100.0 * success as f64 / (success + failed) as f64); - } -} diff --git a/tests/test_flatzinc_batch_10.rs b/tests/test_flatzinc_batch_10.rs deleted file mode 100644 index 1d19a7f..0000000 --- a/tests/test_flatzinc_batch_10.rs +++ /dev/null @@ -1,135 +0,0 @@ -//! Test FlatZinc parser - Batch 10: Miscellaneous puzzles -//! Tests various other puzzles and problems - -use selen::prelude::*; -use std::path::Path; - -#[test] -#[ignore] -fn test_batch_10_misc() { - let examples_dir = Path::new("zinc/ortools"); - - if !examples_dir.exists() { - println!("Skipping test - examples directory not found"); - return; - } - - let test_files = vec![ - "sudoku_pi_2011.fzn", - "sudoku_pi.fzn", - "sum_ctr.fzn", - "sum_free.fzn", - "sum_of_weights_of_distinct_values.fzn", - "sum_to_100.fzn", - "survivor.fzn", - "survo_puzzle.fzn", - "symmetric_alldifferent.fzn", - "symmetry_breaking.fzn", - "table_of_numbers.fzn", - "talent.fzn", - "talisman_square.fzn", - "tank.fzn", - "tea_mixing.fzn", - "template_design.fzn", - "temporal_reasoning.fzn", - "tenpenki_1.fzn", - "tenpenki_2.fzn", - "tenpenki_3.fzn", - "tenpenki_4.fzn", - "tenpenki_5.fzn", - "tenpenki_6.fzn", - "test.fzn", - "the_bomb.fzn", - "the_family_puzzle.fzn", - "three_digit.fzn", - "tickTackToe.fzn", - "timeslots_for_songs.fzn", - "timetabling.fzn", - "timpkin.fzn", - "tobacco.fzn", - "tomography.fzn", - "tomography_n_colors.fzn", - "torn_number.fzn", - "touching_numbers.fzn", - "traffic_lights.fzn", - "traffic_lights_table.fzn", - "transportation2.fzn", - "transportation.fzn", - "transpose.fzn", - "transshipment.fzn", - "trial12.fzn", - "trial1.fzn", - "trial2.fzn", - "trial3.fzn", - "trial4.fzn", - "trial5.fzn", - "trial6.fzn", - "tripuzzle1.fzn", - "tripuzzle2.fzn", - "trucking.fzn", - "tsp_circuit.fzn", - "tsp.fzn", - "tunapalooza.fzn", - "twelve.fzn", - "twin_letters.fzn", - "two_cube_calendar.fzn", - "two_dimensional_channels.fzn", - "uzbekian_puzzle.fzn", - "vingt_cinq_cinq_trente.fzn", - "warehouses.fzn", - "war_or_peace.fzn", - "water_buckets1.fzn", - "wedding_optimal_chart.fzn", - "weighted_sum.fzn", - "were2.fzn", - "were4.fzn", - "who_killed_agatha.fzn", - "wolf_goat_cabbage.fzn", - "wolf_goat_cabbage_lp.fzn", - "word_golf.fzn", - "word_square.fzn", - "work_shift_problem.fzn", - "wwr.fzn", - "xkcd_among_diff_0.fzn", - "xkcd.fzn", - "young_tableaux.fzn", - "zebra.fzn", - "zebra_inverse.fzn", - "zebra_ip.fzn", - ]; - - let mut success = 0; - let mut failed = 0; - let mut not_found = 0; - - println!("\n=== Batch 10: Miscellaneous Puzzles ===\n"); - - for filename in &test_files { - let filepath = examples_dir.join(filename); - - if !filepath.exists() { - println!("⊘ {}", filename); - not_found += 1; - continue; - } - - let mut model = Model::default(); - match model.from_flatzinc_file(&filepath) { - Ok(_) => { - println!("✓ {}", filename); - success += 1; - } - Err(e) => { - println!("✗ {} - {}", filename, e); - failed += 1; - } - } - } - - println!("\nResults: {} success, {} failed, {} not found", success, failed, not_found); - if success + failed > 0 { - println!("Success rate: {}/{} ({:.1}%)", - success, success + failed, - 100.0 * success as f64 / (success + failed) as f64); - } -} diff --git a/tests/test_flatzinc_examples.rs b/tests/test_flatzinc_examples.rs deleted file mode 100644 index ffc0c87..0000000 --- a/tests/test_flatzinc_examples.rs +++ /dev/null @@ -1,172 +0,0 @@ -//! Test FlatZinc parser on example files -//! -//! This test only runs when the example FlatZinc files are present in the source tree. -//! It will be skipped in packaged builds where these files are not included. - -use selen::prelude::*; -use std::path::Path; - -/// Test parsing a selection of FlatZinc example files -/// This helps ensure the parser handles real-world FlatZinc correctly -#[test] -#[ignore] -fn test_parse_flatzinc_examples() { - let examples_dir = Path::new("zinc/ortools"); - - // Skip test if examples directory doesn't exist (e.g., in packaged builds) - if !examples_dir.exists() { - println!("Skipping FlatZinc examples test - examples directory not found"); - return; - } - - // Selection of diverse FlatZinc files to test - let test_files = vec![ - // Simple puzzles - "send_more_money.fzn", - "magic_sequence.fzn", - "n_queens.fzn", - "sudoku.fzn", - "zebra.fzn", - - // Scheduling/planning - "JobShop2x2.fzn", - "scheduling_speakers.fzn", - - // Logic puzzles - "einstein_opl.fzn", - "who_killed_agatha.fzn", - "smullyan_knights_knaves.fzn", - - // Graph problems - "graph_coloring.fzn", - "stable_marriage.fzn", - - // Arithmetic puzzles - "alphametic.fzn", - "crypta.fzn", - "grocery.fzn", - - // Constraint variety - "all_interval.fzn", - "langford.fzn", - "perfect_square_sequence.fzn", - - // Optimization - "knapsack.fzn", - "diet.fzn", - - // Other - "coins.fzn", - "crossword.fzn", - "nonogram.fzn", - "minesweeper.fzn", - "traffic_lights.fzn", - ]; - - let mut results = Vec::new(); - let mut parse_success = 0; - let mut parse_fail = 0; - let mut file_not_found = 0; - - println!("\n=== Testing FlatZinc Parser on Example Files ===\n"); - - for filename in test_files { - let filepath = examples_dir.join(filename); - - if !filepath.exists() { - println!("⊘ {}: File not found", filename); - file_not_found += 1; - results.push((filename, "not_found")); - continue; - } - - let mut model = Model::default(); - match model.from_flatzinc_file(&filepath) { - Ok(_) => { - println!("✓ {}: Parsed successfully", filename); - parse_success += 1; - results.push((filename, "success")); - } - Err(e) => { - println!("✗ {}: Parse error - {}", filename, e); - parse_fail += 1; - results.push((filename, "failed")); - - // Print first few lines of file for debugging - if let Ok(content) = std::fs::read_to_string(&filepath) { - let preview: String = content.lines().take(10).collect::>().join("\n"); - println!(" First 10 lines:"); - for line in preview.lines() { - println!(" {}", line); - } - } - } - } - } - - println!("\n=== Summary ==="); - println!("✓ Parsed successfully: {}", parse_success); - println!("✗ Parse failures: {}", parse_fail); - println!("⊘ Files not found: {}", file_not_found); - println!("Total tested: {}", results.len()); - - // Calculate success rate (excluding files not found) - let tested = parse_success + parse_fail; - if tested > 0 { - let success_rate = (parse_success as f64 / tested as f64) * 100.0; - println!("Success rate: {:.1}%", success_rate); - - // We expect at least 50% success rate for real FlatZinc files - // Some may fail due to unsupported constraints, which is expected - assert!( - success_rate >= 30.0, - "Success rate too low: {:.1}%. Expected at least 30%", - success_rate - ); - } - - // List all failures for reference - if parse_fail > 0 { - println!("\nFailed files:"); - for (filename, status) in &results { - if *status == "failed" { - println!(" - {}", filename); - } - } - } -} - -/// Test that we can parse and solve a simple example -#[test] -#[ignore] -fn test_solve_simple_example() { - let examples_dir = Path::new("zinc/ortools"); - - // Skip test if examples directory doesn't exist - if !examples_dir.exists() { - println!("Skipping solve example test - examples directory not found"); - return; - } - - // Test with send_more_money if available - let filepath = examples_dir.join("send_more_money.fzn"); - if !filepath.exists() { - println!("Skipping - send_more_money.fzn not found"); - return; - } - - let mut model = Model::default(); - model.from_flatzinc_file(&filepath).expect("Should parse send_more_money.fzn"); - - // Try to solve it (may or may not find solution depending on constraints) - match model.solve() { - Ok(_solution) => { - println!("✓ Found solution for send_more_money"); - // We can't access variable values without the var_map, but we know it solved - } - Err(e) => { - println!("Note: Could not solve send_more_money: {:?}", e); - // This is OK - we're mainly testing parsing, not solving - } - } -} diff --git a/tests/test_flatzinc_integration.rs b/tests/test_flatzinc_integration.rs deleted file mode 100644 index 50c61db..0000000 --- a/tests/test_flatzinc_integration.rs +++ /dev/null @@ -1,172 +0,0 @@ -//! Integration tests for FlatZinc parser and model import - -use selen::prelude::*; - -#[cfg(test)] -#[ignore] -mod flatzinc_integration { - use super::*; - - #[test] - fn test_simple_variable_declaration() { - let fzn = r#" - var 1..10: x; - var 1..10: y; - solve satisfy; - "#; - - let mut model = Model::default(); - let result = model.from_flatzinc_str(fzn); - assert!(result.is_ok(), "Failed to parse simple FlatZinc: {:?}", result); - } - - #[test] - fn test_simple_constraint() { - // Test int_eq with variable and literal - let fzn = r#" -var 1..10: x; -constraint int_eq(x, x); -solve satisfy; -"#; - - let mut model = Model::default(); - model.from_flatzinc_str(fzn).expect("Should parse variable-to-variable equality"); - assert!(model.solve().is_ok()); - - // Test int_ne with two variables - let fzn2 = r#" -var 1..5: a; -var 1..5: b; -constraint int_ne(a, b); -solve satisfy; -"#; - let mut model2 = Model::default(); - model2.from_flatzinc_str(fzn2).expect("Should parse int_ne"); - assert!(model2.solve().is_ok()); - } - - #[test] - fn test_alldiff_constraint() { - let fzn = r#" - var 1..3: x; - var 1..3: y; - var 1..3: z; - constraint all_different([x, y, z]); - solve satisfy; - "#; - - let mut model = Model::default(); - model.from_flatzinc_str(fzn).unwrap(); - - let solution = model.solve(); - assert!(solution.is_ok(), "Should find a solution with all_different"); - } - - #[test] - fn test_linear_eq_constraint() { - let fzn = r#" - var 1..10: x; - var 1..10: y; - constraint int_lin_eq([1, 1], [x, y], 10); - solve satisfy; - "#; - - let mut model = Model::default(); - model.from_flatzinc_str(fzn).unwrap(); - - let solution = model.solve(); - assert!(solution.is_ok(), "Should find a solution for x + y = 10"); - } - - #[test] - fn test_linear_ne_constraint() { - let fzn = r#" - var 1..10: x; - var 1..10: y; - constraint int_lin_ne([1, 1], [x, y], 10); - solve satisfy; - "#; - - let mut model = Model::default(); - model.from_flatzinc_str(fzn).unwrap(); - - let solution = model.solve(); - assert!(solution.is_ok(), "Should find a solution for x + y ≠ 10"); - } - - #[test] - fn test_reification_constraint() { - let fzn = r#" - var 1..10: x; - var 1..10: y; - var bool: b; - constraint int_eq_reif(x, y, b); - solve satisfy; - "#; - - let mut model = Model::default(); - model.from_flatzinc_str(fzn).unwrap(); - - let solution = model.solve(); - assert!(solution.is_ok(), "Should find a solution with reification"); - } - - #[test] - fn test_from_file() { - use std::fs::File; - use std::io::Write; - - let fzn = r#" - var 1..5: x; - var 1..5: y; - constraint int_lt(x, y); - solve satisfy; - "#; - - // Create a temporary file - let temp_path = "/tmp/test_flatzinc.fzn"; - let mut file = File::create(temp_path).unwrap(); - file.write_all(fzn.as_bytes()).unwrap(); - file.sync_all().unwrap(); - drop(file); - - // Test from_flatzinc_file - let mut model = Model::default(); - let result = model.from_flatzinc_file(temp_path); - assert!(result.is_ok(), "Failed to load FlatZinc from file: {:?}", result); - - // Clean up - std::fs::remove_file(temp_path).ok(); - } - - #[test] - fn test_parse_error_reporting() { - let fzn = r#" - var 1..10 x; % Missing colon - solve satisfy; - "#; - - let mut model = Model::default(); - let result = model.from_flatzinc_str(fzn); - assert!(result.is_err(), "Should fail on invalid syntax"); - - if let Err(e) = result { - let error_msg = format!("{}", e); - assert!(error_msg.contains("line") || error_msg.contains("column"), - "Error should include location info: {}", error_msg); - } - } - - #[test] - fn test_unsupported_constraint() { - let fzn = r#" - var 1..10: x; - constraint some_unsupported_constraint(x); - solve satisfy; - "#; - - let mut model = Model::default(); - let result = model.from_flatzinc_str(fzn); - assert!(result.is_err(), "Should fail on unsupported constraint"); - } -} diff --git a/tests/test_flatzinc_mapper_features.rs b/tests/test_flatzinc_mapper_features.rs deleted file mode 100644 index 3af7acc..0000000 --- a/tests/test_flatzinc_mapper_features.rs +++ /dev/null @@ -1,386 +0,0 @@ -//! Test coverage for FlatZinc mapper features -//! -//! Tests the recently implemented features: -//! - Array element access in constraints (x[1], s[2], etc.) -//! - Variable initialization (var int: x = y;) -//! - Array element constraints (array_var_int_element, etc.) -//! - Domain size validation - -use selen::prelude::*; - -/// Helper function to test FlatZinc input -fn test_flatzinc(input: &str) -> FlatZincResult { - let mut model = Model::default(); - model.from_flatzinc_str(input)?; - Ok(model) -} - -/// Helper to test that FlatZinc input parses and solves successfully -fn assert_solves(input: &str, description: &str) { - let model = test_flatzinc(input).expect(&format!("Failed to parse: {}", description)); - let solution = model.solve(); - assert!(solution.is_ok(), "{} - should find a solution", description); -} - -/// Helper to test that FlatZinc input fails with an error -fn assert_fails(input: &str, expected_msg: &str, description: &str) { - let result = test_flatzinc(input); - assert!(result.is_err(), "{} - should fail", description); - let err_msg = format!("{:?}", result.unwrap_err()); - assert!(err_msg.contains(expected_msg), - "{} - error should contain '{}', got: {}", description, expected_msg, err_msg); -} - -// ============================================================================ -// Array Element Access Tests -// ============================================================================ - -#[test] -fn test_array_access_in_constraint_args() { - // Test that array element access like x[1] works in constraint arguments - let input = r#" -array [1..3] of var 0..10: x; -constraint int_eq(x[1], 5); -constraint int_eq(x[2], x[3]); -solve satisfy; -"#; - - assert_solves(input, "Array access in constraint args"); -} - -#[test] -fn test_array_access_in_linear_constraint() { - // Test array access in int_lin_eq constraint (common pattern) - let input = r#" -array [1..4] of var 0..10: s; -constraint int_lin_eq([1, -1], [s[1], s[2]], 3); -constraint int_lin_le([1, 1], [s[3], s[4]], 10); -solve satisfy; -"#; - - assert_solves(input, "Array access in linear constraints"); -} - -#[test] -fn test_array_access_mixed_with_variables() { - // Test mixing array access with direct variable references - let input = r#" -var 0..10: x; -array [1..2] of var 0..10: arr; -constraint int_lin_eq([1, 1, -1], [x, arr[1], arr[2]], 0); -solve satisfy; -"#; - - assert_solves(input, "Mixed array access and variables"); -} - -#[test] -fn test_array_access_bounds_checking() { - // Test that out-of-bounds array access is caught - let input = r#" -array [1..3] of var 0..10: x; -constraint int_eq(x[5], 0); -solve satisfy; -"#; - - assert_fails(input, "out of bounds", "Out-of-bounds array access"); -} - -#[test] -fn test_array_access_zero_index() { - // Test that 0-based indexing is rejected (FlatZinc uses 1-based) - let input = r#" -array [1..3] of var 0..10: x; -constraint int_eq(x[0], 5); -solve satisfy; -"#; - - assert_fails(input, "must be >= 1", "Zero-based array access"); -} - -#[test] -fn test_nested_array_in_all_different() { - // Test array access in all_different constraint - let input = r#" -array [1..4] of var 1..4: x; -constraint fzn_all_different_int([x[1], x[2], x[3], x[4]]); -solve satisfy; -"#; - - assert_solves(input, "Array access in all_different"); -} - -#[test] -fn test_array_access_with_nonexistent_array() { - // Test error handling when array doesn't exist - let input = r#" -var 0..10: x; -constraint int_eq(nonexistent[1], x); -solve satisfy; -"#; - - assert_fails(input, "Unknown array", "Nonexistent array access"); -} - -// ============================================================================ -// Variable Initialization Tests -// ============================================================================ - -#[test] -fn test_variable_initialization_to_variable() { - // Test var int: x = y; pattern - let input = r#" -var 1..9: M; -var 1..9: c4 = M; -constraint int_eq(M, 5); -solve satisfy; -"#; - - assert_solves(input, "Variable-to-variable initialization"); -} - -#[test] -fn test_variable_initialization_to_literal() { - // Test existing literal initialization still works - let input = r#" -var 1..10: x = 5; -constraint int_eq(x, 5); -solve satisfy; -"#; - - assert_solves(input, "Literal initialization"); -} - -#[test] -fn test_variable_initialization_order() { - // Test that variable must be declared before being used in initialization - let input = r#" -var 1..10: x = y; -var 1..10: y; -solve satisfy; -"#; - - assert_fails(input, "not found", "Variable initialization before declaration"); -} - -#[test] -fn test_bool_variable_initialization() { - // Test bool variable initialization using int_eq (bool is 0/1) - let input = r#" -var bool: b1; -var bool: b2 = b1; -constraint int_eq(b1, 1); -solve satisfy; -"#; - - assert_solves(input, "Bool variable initialization"); -} - -// ============================================================================ -// Array Element Constraint Tests -// ============================================================================ - -#[test] -fn test_array_var_int_element() { - // Test array_var_int_element constraint (variable array, variable index) - let input = r#" -array [1..5] of var 1..10: arr; -var 1..5: idx; -var 1..10: val; -constraint array_var_int_element(idx, arr, val); -constraint int_eq(idx, 3); -constraint int_eq(val, 7); -solve satisfy; -"#; - - assert_solves(input, "array_var_int_element constraint"); -} - -#[test] -fn test_array_int_element() { - // Test array_int_element constraint (constant array inline) - let input = r#" -var 1..5: idx; -var 10..50: val; -constraint array_int_element(idx, [10, 20, 30, 40, 50], val); -constraint int_eq(idx, 2); -solve satisfy; -"#; - - assert_solves(input, "array_int_element constraint"); -} - -// Note: array_var_bool_element test removed - constraint works but finding solution is slow -// The feature is tested indirectly through other tests - -#[test] -fn test_array_bool_element() { - // Test array_bool_element constraint (constant bool array inline) - let input = r#" -var 1..3: idx; -var bool: val; -constraint array_bool_element(idx, [false, true, false], val); -constraint int_eq(idx, 2); -solve satisfy; -"#; - - assert_solves(input, "array_bool_element constraint"); -} - -#[test] -fn test_element_with_1based_to_0based_conversion() { - // Verify that 1-based FlatZinc indices are converted to 0-based - let input = r#" -var 1..3: idx; -var 100..300: val; -constraint array_int_element(idx, [100, 200, 300], val); -constraint int_eq(idx, 1); -constraint int_eq(val, 100); -solve satisfy; -"#; - - assert_solves(input, "Element constraint with 1-based to 0-based conversion"); -} - -// ============================================================================ -// Domain Size Validation Tests -// ============================================================================ - -#[test] -#[ignore] // Large domains are now capped with warnings instead of failing -fn test_domain_size_limit_enforcement() { - // Test that domains exceeding MAX_SPARSE_SET_DOMAIN_SIZE are rejected - // MAX_SPARSE_SET_DOMAIN_SIZE = 10,000,000 - let input = r#" -var 0..20000000: x; -solve satisfy; -"#; - - assert_fails(input, "exceeds maximum", "Domain exceeding limit"); -} - -#[test] -#[ignore] // Large domains are now capped with warnings, test expectations outdated -fn test_domain_size_just_under_limit() { - // Test that domains just under the limit work - let input = r#" -var 0..9999999: x; -constraint int_eq(x, 5000000); -solve satisfy; -"#; - - assert_solves(input, "Domain just under limit"); -} - -#[test] -fn test_domain_size_small() { - // Test that normal small domains work fine - let input = r#" -var 1..100: x; -var -50..50: y; -constraint int_eq(x, 42); -solve satisfy; -"#; - - assert_solves(input, "Small domains"); -} - -// ============================================================================ -// Integration Tests (Multiple Features) -// ============================================================================ - -// Note: send_more_money_pattern test removed - features work but full problem is slow to solve -// Variable initialization and array access are tested separately in simpler tests - -#[test] -fn test_coloring_pattern() { - // Test the graph coloring pattern with array access in constraints - let input = r#" -array [1..3] of var 1..3: color; -constraint int_ne(color[1], color[2]); -constraint int_ne(color[2], color[3]); -constraint fzn_all_different_int([color[1], color[2], color[3]]); -solve satisfy; -"#; - - assert_solves(input, "Graph coloring pattern"); -} - -#[test] -fn test_scheduling_pattern() { - // Test scheduling pattern: array access in linear inequalities - let input = r#" -array [1..4] of var 0..20: start; -array [1..4] of int: duration = [2, 3, 4, 5]; -constraint int_lin_le([1, -1], [start[1], start[2]], -2); -constraint int_lin_le([1, -1], [start[3], start[4]], -4); -solve satisfy; -"#; - - assert_solves(input, "Scheduling pattern"); -} - -#[test] -fn test_mixed_array_and_scalar_constraints() { - // Test that we can mix array-based and scalar constraints - let input = r#" -var 1..10: x; -var 1..10: y; -array [1..2] of var 1..10: arr = [x, y]; -constraint int_le(x, y); -constraint int_eq(arr[1], 3); -constraint int_eq(arr[2], 7); -solve satisfy; -"#; - - assert_solves(input, "Mixed array and scalar constraints"); -} - -#[test] -fn test_int_abs_constraint() { - // Test the int_abs constraint that was added - let input = r#" -var -10..10: x; -var 0..10: y; -constraint int_abs(x, y); -constraint int_eq(x, -5); -solve satisfy; -"#; - - assert_solves(input, "int_abs constraint"); -} - -// Note: array_element_with_constants test removed - constraint works but finding solution is slow -// The feature is tested indirectly through element_with_1based_to_0based_conversion test - -#[test] -fn test_complex_array_access_in_all_different() { - // Test more complex array access patterns - let input = r#" -array [1..5] of var 1..9: x; -array [1..3] of var 1..9: subset; -constraint int_eq(subset[1], x[1]); -constraint int_eq(subset[2], x[3]); -constraint int_eq(subset[3], x[5]); -constraint fzn_all_different_int(subset); -solve satisfy; -"#; - - assert_solves(input, "Complex array access with all_different"); -} - -#[test] -fn test_queens_pattern_with_array_access() { - // Test N-Queens pattern with array access - let input = r#" -array [1..4] of var 1..4: q; -constraint fzn_all_different_int(q); -constraint fzn_all_different_int([q[1], q[2], q[3], q[4]]); -constraint int_ne(q[1], q[2]); -constraint int_ne(q[2], q[3]); -constraint int_ne(q[3], q[4]); -solve satisfy; -"#; - - assert_solves(input, "N-Queens pattern with array access"); -}