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 ¶m_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}