Skip to main content

zelen/
lib.rs

1//! Zelen - Direct MiniZinc Constraint Solver
2//!
3//! Zelen parses a subset of MiniZinc and translates it directly to the [Selen](https://github.com/radevgit/selen) 
4//! constraint solver, bypassing FlatZinc compilation. This allows you to:
5//!
6//! - **Parse MiniZinc** from strings or files
7//! - **Solve directly** using a single function call
8//! - **Access variable information** with variable name to ID mappings
9//! - **Use as a library** in your Rust projects
10//!
11//! # Quick Start
12//!
13//! ## Simple Usage
14//!
15//! ```
16//! use zelen;
17//!
18//! let source = r#"
19//!     var 1..10: x;
20//!     var 1..10: y;
21//!     constraint x + y = 15;
22//!     solve satisfy;
23//! "#;
24//!
25//! // Parse and solve directly
26//! match zelen::solve(source) {
27//!     Ok(Ok(solution)) => { /* Found solution! */ },
28//!     Ok(Err(_)) => { /* No solution exists */ },
29//!     Err(e) => { /* Parse error */ },
30//! }
31//! ```
32//!
33//! ## With Variable Access
34//!
35//! ```
36//! use zelen::Translator;
37//!
38//! let source = "var 1..10: x; solve satisfy;";
39//! let ast = zelen::parse(source).unwrap();
40//! let model_data = Translator::translate_with_vars(&ast).unwrap();
41//!
42//! // Access variables by name
43//! for (name, var_id) in &model_data.int_vars {
44//!     // name is available here
45//!     let _ = (name, var_id);
46//! }
47//! ```
48//!
49//! # Supported Features
50//!
51//! - Integer, boolean, and float variables
52//! - Variable arrays with initialization
53//! - Arithmetic and comparison operators
54//! - Boolean logic operators
55//! - Global constraints: `all_different`, `element`
56//! - Aggregation functions: `min`, `max`, `sum`, `forall`, `exists`
57//! - Nested forall loops
58//! - Satisfy, minimize, and maximize objectives
59
60pub mod ast;
61pub mod error;
62pub mod lexer;
63pub mod parser;
64pub mod translator;
65
66pub use ast::*;
67pub use error::{Error, Result};
68pub use lexer::Lexer;
69pub use parser::Parser;
70pub use translator::{Translator, TranslatedModel, ObjectiveType};
71
72// Re-export commonly used Selen types for convenience
73pub use selen;
74// Re-export specific selen types to avoid conflicts
75pub use selen::prelude::{Model, Solution, VarId};
76
77/// Configuration for the Selen solver backend
78///
79/// Allows customizing solver behavior like timeout, memory limits, and solution enumeration.
80///
81/// # Example
82///
83/// ```
84/// use zelen::SolverConfig;
85///
86/// let config = SolverConfig::default()
87///     .with_time_limit_ms(5000)
88///     .with_memory_limit_mb(1024)
89///     .with_all_solutions(true);
90/// assert_eq!(config.time_limit_ms, Some(5000));
91/// ```
92#[derive(Debug, Clone)]
93pub struct SolverConfig {
94    /// Time limit in milliseconds (None = use Selen default)
95    pub time_limit_ms: Option<u64>,
96    /// Memory limit in MB (None = use Selen default)
97    pub memory_limit_mb: Option<u64>,
98    /// Whether to find all solutions (for satisfaction problems)
99    pub all_solutions: bool,
100    /// Maximum number of solutions to find (None = unlimited)
101    pub max_solutions: Option<usize>,
102}
103
104impl Default for SolverConfig {
105    fn default() -> Self {
106        Self {
107            time_limit_ms: None,
108            memory_limit_mb: None,
109            all_solutions: false,
110            max_solutions: None,
111        }
112    }
113}
114
115impl SolverConfig {
116    /// Set the time limit in milliseconds
117    pub fn with_time_limit_ms(mut self, ms: u64) -> Self {
118        self.time_limit_ms = if ms > 0 { Some(ms) } else { None };
119        self
120    }
121
122    /// Set the memory limit in MB
123    pub fn with_memory_limit_mb(mut self, mb: u64) -> Self {
124        self.memory_limit_mb = if mb > 0 { Some(mb) } else { None };
125        self
126    }
127
128    /// Enable finding all solutions
129    pub fn with_all_solutions(mut self, all: bool) -> Self {
130        self.all_solutions = all;
131        self
132    }
133
134    /// Set the maximum number of solutions to find
135    pub fn with_max_solutions(mut self, n: usize) -> Self {
136        self.max_solutions = if n > 0 { Some(n) } else { None };
137        self
138    }
139
140    /// Convert to Selen's SolverConfig
141    fn to_selen_config(&self) -> selen::utils::config::SolverConfig {
142        let mut config = selen::utils::config::SolverConfig::default();
143        if let Some(ms) = self.time_limit_ms {
144            config.timeout_ms = Some(ms);
145        }
146        if let Some(mb) = self.memory_limit_mb {
147            config.max_memory_mb = Some(mb);
148        }
149        config
150    }
151}
152
153/// Parse a MiniZinc model from source text into an AST
154///
155/// # Arguments
156///
157/// * `source` - MiniZinc source code as a string
158///
159/// # Returns
160///
161/// An AST (Abstract Syntax Tree) representing the model, or a parsing error
162///
163/// # Example
164///
165/// ```
166/// let ast = zelen::parse("var 1..10: x; solve satisfy;");
167/// assert!(ast.is_ok());
168/// ```
169pub fn parse(source: &str) -> Result<ast::Model> {
170    let lexer = Lexer::new(source);
171    let mut parser = Parser::new(lexer).with_source(source.to_string());
172    parser.parse_model()
173}
174
175/// Translate a MiniZinc AST to a Selen model
176///
177/// # Arguments
178///
179/// * `ast` - The MiniZinc AST to translate
180///
181/// # Returns
182///
183/// A Selen Model ready to solve, or a translation error
184///
185/// # Example
186///
187/// ```
188/// let ast = zelen::parse("var 1..10: x; solve satisfy;").unwrap();
189/// let model = zelen::translate(&ast);
190/// assert!(model.is_ok());
191/// ```
192pub fn translate(ast: &ast::Model) -> Result<selen::prelude::Model> {
193    Translator::translate(ast)
194}
195
196/// Parse and translate MiniZinc source directly to a Selen model
197///
198/// This is a convenience function that combines `parse()` and `translate()`.
199///
200/// # Arguments
201///
202/// * `source` - MiniZinc source code as a string
203///
204/// # Returns
205///
206/// A Selen Model ready to solve, or an error (either parsing or translation)
207///
208/// # Example
209///
210/// ```
211/// let model = zelen::build_model(r#"
212///     var 1..10: x;
213///     constraint x > 5;
214///     solve satisfy;
215/// "#);
216/// assert!(model.is_ok());
217/// ```
218pub fn build_model(source: &str) -> Result<selen::prelude::Model> {
219    let ast = parse(source)?;
220    translate(&ast)
221}
222
223/// Parse and translate MiniZinc source directly to a Selen model with custom configuration
224///
225/// This version allows configuring solver parameters like timeouts and memory limits.
226///
227/// # Arguments
228///
229/// * `source` - MiniZinc source code as a string
230/// * `config` - Solver configuration
231///
232/// # Returns
233///
234/// A Selen Model ready to solve, or an error (either parsing or translation)
235///
236/// # Example
237///
238/// ```
239/// let config = zelen::SolverConfig::default()
240///     .with_time_limit_ms(5000)
241///     .with_memory_limit_mb(1024);
242/// 
243/// let model = zelen::build_model_with_config("var 1..10: x; solve satisfy;", config);
244/// assert!(model.is_ok());
245/// ```
246pub fn build_model_with_config(source: &str, config: SolverConfig) -> Result<selen::prelude::Model> {
247    let ast = parse(source)?;
248    let selen_config = config.to_selen_config();
249    Translator::translate_with_config(&ast, selen_config)
250}
251
252/// Solve a MiniZinc model with custom solver configuration and return solutions
253///
254/// This function combines parse, translate with config, and solve/enumerate.
255/// It respects the `all_solutions` and `max_solutions` flags from the config.
256///
257/// # Arguments
258///
259/// * `source` - MiniZinc source code as a string
260/// * `config` - Solver configuration including all_solutions and max_solutions settings
261///
262/// # Returns
263///
264/// A vector of solutions found. If `all_solutions` is false, returns at most one solution.
265/// If `all_solutions` is true, returns multiple solutions up to `max_solutions` limit.
266///
267/// # Example
268///
269/// ```
270/// let config = zelen::SolverConfig::default()
271///     .with_all_solutions(false)
272///     .with_time_limit_ms(5000);
273///
274/// let solutions = zelen::solve_with_config("var 1..10: x; solve satisfy;", config);
275/// assert!(solutions.is_ok());
276/// ```
277pub fn solve_with_config(
278    source: &str,
279    config: SolverConfig,
280) -> Result<Vec<selen::core::Solution>> {
281    let model = build_model_with_config(source, config.clone())?;
282    
283    if config.all_solutions {
284        // Enumerate all solutions up to max_solutions limit
285        let max = config.max_solutions.unwrap_or(usize::MAX);
286        Ok(model.enumerate().take(max).collect())
287    } else {
288        // Single solution
289        match model.solve() {
290            Ok(solution) => Ok(vec![solution]),
291            Err(_) => Ok(Vec::new()),  // No solution found
292        }
293    }
294}
295
296/// Solve a MiniZinc model and return the solution
297///
298/// This is a convenience function that combines parse, translate, and solve.
299///
300/// # Arguments
301///
302/// * `source` - MiniZinc source code as a string
303///
304/// # Returns
305///
306/// Returns a nested Result:
307/// - Outer `Result`: Parsing/translation errors
308/// - Inner `Result`: Solver errors (satisfiability, resource limits, etc.)
309///
310/// # Example
311///
312/// ```
313/// match zelen::solve("var 1..10: x; solve satisfy;") {
314///     Ok(Ok(solution)) => assert!(true), // Solution found
315///     Ok(Err(_)) => assert!(true), // Unsatisfiable
316///     Err(e) => panic!("Parse error: {}", e),
317/// }
318/// ```
319pub fn solve(source: &str) -> Result<std::result::Result<selen::core::Solution, selen::core::SolverError>> {
320    let model = build_model(source)?;
321    Ok(model.solve())
322}
323
324/// Load and parse a MiniZinc data file (.dzn format)
325///
326/// Parses a .dzn file and returns the raw source with parameter declarations added.
327/// This allows separate handling of model and data files while respecting MiniZinc semantics.
328///
329/// # Arguments
330///
331/// * `dzn_source` - Content of a .dzn data file
332/// * `mzn_source` - The model file source (to preserve its structure)
333///
334/// # Returns
335///
336/// Combined MiniZinc source suitable for parsing
337///
338/// # Example
339///
340/// ```
341/// let model = "int: n; array[1..n] of int: costs; var 1..n: x; solve satisfy;";
342/// let data = "n = 5; costs = [1,2,3,4,5];";
343/// let combined = zelen::load_dzn_data(data, model).unwrap();
344/// ```
345pub fn load_dzn_data(dzn_source: &str, mzn_source: &str) -> Result<String> {
346    // Parse .dzn assignments with proper handling of complex syntax
347    // (.dzn files can have sets like {1,2,3} and nested structures)
348    let mut data_params = String::new();
349    let mut current_stmt = String::new();
350    
351    for ch in dzn_source.chars() {
352        current_stmt.push(ch);
353        
354        // Only process complete statements (ending with ';')
355        if ch == ';' {
356            let trimmed = current_stmt.trim();
357            
358            // Skip if just a semicolon or empty
359            if trimmed.len() > 1 {
360                // Remove inline comments first
361                let code = if let Some(pos) = trimmed.find('%') {
362                    &trimmed[..pos]
363                } else {
364                    trimmed
365                };
366                
367                let code = code.trim_end_matches(';').trim();
368                
369                if !code.is_empty() && !code.starts_with('%') {
370                    // Now extract "name = value" (value can have {}, [], nested structures)
371                    if let Some(eq_pos) = code.find('=') {
372                        let name = code[..eq_pos].trim();
373                        let value = code[eq_pos + 1..].trim();
374                        
375                        // Infer type from value
376                        let type_decl = infer_dzn_type(value);
377                        
378                        data_params.push_str(&format!("{}: {} = {};\n", type_decl, name, value));
379                    }
380                }
381            }
382            
383            current_stmt.clear();
384        }
385    }
386    
387    // Merge: prepend data parameters, then add model
388    // But filter out duplicate declarations from model
389    let mut filtered_model = String::new();
390    let mut param_names = std::collections::HashSet::new();
391    
392    // Extract declared parameter names from data
393    for line in data_params.lines() {
394        if let Some(eq_pos) = line.find('=') {
395            let before_eq = &line[..eq_pos];
396            if let Some(last_colon) = before_eq.rfind(':') {
397                let name_part = &before_eq[last_colon+1..].trim();
398                if let Some(name) = name_part.split_whitespace().next() {
399                    param_names.insert(name.to_string());
400                }
401            }
402        }
403    }
404    
405    // Filter model - skip parameter declarations for names we have data for
406    for line in mzn_source.lines() {
407        let code_line = if let Some(pos) = line.find('%') {
408            &line[..pos]
409        } else {
410            line
411        };
412        
413        let trimmed = code_line.trim();
414        
415        // Skip lines that declare parameters we're providing data for
416        let mut skip = false;
417        if !trimmed.starts_with("var ") && !trimmed.starts_with("constraint ") 
418            && !trimmed.starts_with("solve ") && trimmed.contains(':') 
419            && !trimmed.contains('=') && trimmed.ends_with(';') {
420            // This looks like a parameter declaration without initializer
421            for param_name in &param_names {
422                if let Some(last_colon) = trimmed.rfind(':') {
423                    let after_colon = &trimmed[last_colon+1..].trim_end_matches(';');
424                    if after_colon.trim().ends_with(param_name) {
425                        skip = true;
426                        break;
427                    }
428                }
429            }
430        }
431        
432        if !skip {
433            filtered_model.push_str(line);
434            filtered_model.push('\n');
435        }
436    }
437    
438    Ok(format!("{}\n{}", data_params, filtered_model))
439}
440
441/// Infer MiniZinc type from a .dzn value string
442/// Handles simple scalars and complex array/set syntax
443fn infer_dzn_type(value: &str) -> String {
444    let trimmed = value.trim();
445    
446    if trimmed.starts_with('[') {
447        // Array: could be simple [1,2,3] or complex [{...}, {...}]
448        // For complex arrays with sets, default to "array[int] of int"
449        // The type will be overridden or fixed by the MiniZinc semantics anyway
450        
451        if trimmed.contains('{') {
452            // Likely an array of sets - use generic array type
453            // MiniZinc will infer the proper type during parsing
454            "array[int] of int".to_string()
455        } else {
456            // Simple array - count elements
457            let inner = &trimmed[1..trimmed.len().saturating_sub(1)];
458            if inner.is_empty() {
459                "array[int] of int".to_string()
460            } else {
461                let elem_count = count_array_elements(inner);
462                let elem_type = determine_element_type(inner);
463                format!("array[1..{}] of {}", elem_count, elem_type)
464            }
465        }
466    } else if trimmed == "true" || trimmed == "false" {
467        "bool".to_string()
468    } else if trimmed.parse::<f64>().is_ok() && trimmed.contains('.') {
469        "float".to_string()
470    } else if trimmed.parse::<i64>().is_ok() {
471        "int".to_string()
472    } else {
473        // Unknown type - default to int
474        "int".to_string()
475    }
476}
477
478/// Count comma-separated elements in an array value string
479fn count_array_elements(inner: &str) -> usize {
480    if inner.trim().is_empty() {
481        return 0;
482    }
483    
484    let mut depth: i32 = 0;
485    let mut count = 1;
486    
487    for ch in inner.chars() {
488        match ch {
489            '{' | '[' => depth += 1,
490            '}' | ']' => depth = (depth - 1).max(0),
491            ',' if depth == 0 => count += 1,
492            _ => {}
493        }
494    }
495    
496    count
497}
498
499/// Determine the element type of array elements
500fn determine_element_type(inner: &str) -> &'static str {
501    if inner.contains('.') {
502        "float"
503    } else if inner.contains("true") || inner.contains("false") {
504        "bool"
505    } else {
506        "int"
507    }
508}
509
510#[cfg(test)]
511mod tests {
512    use super::*;
513
514    #[test]
515    fn test_parse_simple_model() {
516        let source = r#"
517            int: n = 5;
518            var 1..n: x;
519            constraint x > 2;
520            solve satisfy;
521        "#;
522        
523        let result = parse(source);
524        assert!(result.is_ok(), "Failed to parse: {:?}", result.err());
525        
526        let model = result.unwrap();
527        assert_eq!(model.items.len(), 4);
528    }
529
530    #[test]
531    fn test_parse_nqueens() {
532        let source = r#"
533            int: n = 4;
534            array[1..n] of var 1..n: queens;
535            constraint alldifferent(queens);
536            solve satisfy;
537        "#;
538        
539        let result = parse(source);
540        assert!(result.is_ok(), "Failed to parse: {:?}", result.err());
541        
542        let model = result.unwrap();
543        assert_eq!(model.items.len(), 4);
544    }
545
546    #[test]
547    fn test_parse_with_expressions() {
548        let source = r#"
549            int: n = 10;
550            array[1..n] of var int: x;
551            constraint sum(x) == 100;
552            constraint forall(i in 1..n)(x[i] >= 0);
553            solve minimize sum(i in 1..n)(x[i] * x[i]);
554        "#;
555        
556        let result = parse(source);
557        assert!(result.is_ok(), "Failed to parse: {:?}", result.err());
558    }
559
560    #[test]
561    fn test_error_reporting() {
562        let source = "int n = 5"; // Missing colon
563        
564        let result = parse(source);
565        assert!(result.is_err());
566        
567        if let Err(e) = result {
568            let error_msg = format!("{}", e);
569            assert!(error_msg.contains("line 1"));
570        }
571    }
572}