Skip to content

Commit ec7d6f3

Browse files
committed
Implemented flatzinc
1 parent 227d1b9 commit ec7d6f3

22 files changed

Lines changed: 1895 additions & 85 deletions

.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,3 +24,4 @@ target
2424
# Added by cargo
2525

2626
/target
27+
/zinc

Cargo.lock

Lines changed: 2 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

Cargo.toml

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,7 @@ readme = "README.md"
1717
crate-type = ["lib"]
1818

1919
[dependencies]
20-
# Use local path during development
21-
selen = { version = "0.9", path = "../selen" }
20+
selen = "0.9"
2221

2322
[dev-dependencies]
2423

README.md

Lines changed: 103 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,42 @@ zelen = "0.1"
2727

2828
## Quick Start
2929

30-
### From FlatZinc String
30+
### Recommended API: FlatZincSolver
31+
32+
The easiest way to use Zelen is with the `FlatZincSolver` - it provides automatic FlatZinc-compliant output:
33+
34+
```rust
35+
use zelen::prelude::*;
36+
37+
let fzn = r#"
38+
var 1..10: x;
39+
var 1..10: y;
40+
constraint int_eq(x, 5);
41+
constraint int_plus(x, y, 12);
42+
solve satisfy;
43+
"#;
44+
45+
let mut solver = FlatZincSolver::new();
46+
solver.load_str(fzn)?;
47+
solver.solve()?;
48+
49+
// Automatic FlatZinc-compliant output with statistics
50+
print!("{}", solver.to_flatzinc());
51+
// Outputs:
52+
// x = 5;
53+
// y = 7;
54+
// ----------
55+
// ==========
56+
// %%%mzn-stat: solutions=1
57+
// %%%mzn-stat: nodes=0
58+
// %%%mzn-stat: propagations=0
59+
// %%%mzn-stat: solveTime=0.001
60+
// %%%mzn-stat-end
61+
```
62+
63+
### Low-Level API: Direct Model Integration
64+
65+
For more control, use the Model integration API:
3166

3267
```rust
3368
use zelen::prelude::*;
@@ -103,54 +138,59 @@ if let Ok(solution) = model.solve() {
103138
}
104139
```
105140

106-
### FlatZinc-Compliant Output
141+
### Configurable Output and Statistics
107142

108-
Zelen provides a formatter to output solutions according to the FlatZinc specification:
143+
Control statistics and solution enumeration:
109144

110145
```rust
111146
use zelen::prelude::*;
112-
use zelen::output::format_solution;
113-
use std::collections::HashMap;
114147

115-
let fzn = r#"
116-
var 1..10: x;
117-
var 1..10: y;
118-
constraint int_eq(x, 5);
119-
constraint int_eq(y, 3);
120-
solve satisfy;
121-
"#;
148+
let fzn = "var 1..10: x; solve satisfy;";
122149

123-
let mut model = Model::default();
124-
model.from_flatzinc_str(fzn)?;
150+
// Configure solver options
151+
let mut solver = FlatZincSolver::new();
152+
solver.with_statistics(true); // Enable/disable statistics
153+
solver.max_solutions(3); // Find up to 3 solutions
154+
solver.find_all_solutions(); // Find all solutions
125155

126-
match model.solve() {
127-
Ok(solution) => {
128-
// Get variable names from the parser (you'd track these during parsing)
129-
let var_names = HashMap::from([
130-
(x_var_id, "x".to_string()),
131-
(y_var_id, "y".to_string()),
132-
]);
133-
134-
// Format according to FlatZinc spec
135-
let output = format_solution(&solution, &var_names);
136-
print!("{}", output);
137-
// Outputs:
138-
// x = 5;
139-
// y = 3;
140-
// ----------
141-
}
142-
Err(_) => {
143-
println!("{}", zelen::output::format_no_solution());
144-
// Outputs: =====UNSATISFIABLE=====
145-
}
146-
}
156+
solver.load_str(fzn)?;
157+
solver.solve()?;
158+
159+
// Get formatted output
160+
let output = solver.to_flatzinc(); // Returns String
161+
solver.print_flatzinc(); // Prints directly
162+
163+
// Access solutions programmatically
164+
let count = solver.solution_count();
165+
let solution = solver.get_solution(0);
166+
```
167+
168+
### FlatZinc Specification Compliance
169+
170+
Zelen follows the [FlatZinc specification](https://docs.minizinc.dev/en/stable/fzn-spec.html#output) exactly:
171+
172+
**Output Format:**
173+
- Variable assignments: `varname = value;`
174+
- Solution separator: `----------`
175+
- Search complete: `==========`
176+
- Unsatisfiable: `=====UNSATISFIABLE=====`
177+
178+
**Statistics Format** (optional, configurable):
179+
```
180+
%%%mzn-stat: solutions=1
181+
%%%mzn-stat: nodes=10
182+
%%%mzn-stat: failures=0
183+
%%%mzn-stat: propagations=21
184+
%%%mzn-stat: variables=4
185+
%%%mzn-stat: propagators=1
186+
%%%mzn-stat: solveTime=0.001
187+
%%%mzn-stat: peakMem=1.00
188+
%%%mzn-stat-end
147189
```
148190

149-
The output format follows the [FlatZinc specification](https://docs.minizinc.dev/en/stable/fzn-spec.html#output):
150-
- Each variable assignment on its own line: `varname = value;`
151-
- Separator line `----------` marks the end of a solution
152-
- `=====UNSATISFIABLE=====` when no solution exists
153-
- `=====UNKNOWN=====` when satisfiability cannot be determined
191+
All statistics are automatically extracted from Selen's solver:
192+
- **Standard** (FlatZinc spec): solutions, nodes, failures, solveTime (seconds), peakMem (MB)
193+
- **Extended**: propagations, variables, propagators
154194

155195
## Using with MiniZinc
156196

@@ -219,17 +259,32 @@ Zelen has been tested on 851 real-world FlatZinc files from the OR-Tools test su
219259

220260
## Examples
221261

222-
Check the `examples/` directory for more complete examples:
262+
The repository includes comprehensive examples demonstrating different aspects of the library:
223263

224-
```bash
225-
# Basic FlatZinc parsing and solving
226-
cargo run --example flatzinc_simple
264+
### Basic Usage
265+
- **`simple_usage.rs`** - Basic constraint solving with FlatZincContext API
266+
- **`clean_api.rs`** - High-level FlatZincSolver API with automatic output formatting
267+
- **`solver_demo.rs`** - Demonstrates solving various constraint problem types
268+
269+
### FlatZinc Integration
270+
- **`flatzinc_simple.rs`** - Simple FlatZinc model solving
271+
- **`flatzinc_output.rs`** - FlatZinc-compliant output formatting
227272

228-
# FlatZinc-compliant output formatting
229-
cargo run --example flatzinc_output
273+
### Multiple Solutions & Configuration
274+
- **`multiple_solutions.rs`** - Enumerate multiple solutions with configurable limits
275+
- **`spec_compliance.rs`** - FlatZinc specification compliance demonstration
276+
- **`optimization_test.rs`** - Minimize/maximize with optimal and intermediate solutions
230277

231-
# Complete solver demo with multiple problem types
232-
cargo run --example solver_demo
278+
### Statistics & Monitoring
279+
- **`enhanced_statistics.rs`** - All available solver statistics from Selen
280+
- **`statistics_units.rs`** - Statistics unit verification (seconds, megabytes)
281+
282+
Run any example with:
283+
```bash
284+
cargo run --example <name>
285+
# For instance:
286+
cargo run --example clean_api
287+
cargo run --example multiple_solutions
233288
```
234289

235290
## Testing

docs/FLATZINC.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ This document provides a high-level overview of the FlatZinc integration with Se
1414

1515
MiniZinc can export constraint satisfaction problems to FlatZinc format (*.fzn):
1616
- **Flattening Process**: https://docs.minizinc.dev/en/stable/flattening.html
17-
- **FlatZinc Specification**: https://docs.minizinc.dev/en/latest/fzn-spec.html
17+
- **FlatZinc Specification**: https://docs.minizinc.dev/en/stable/fzn-spec.html
1818
- BNF grammar is at the end of the spec document
1919
- **Latest MiniZinc Release**: 2.9.4
2020

@@ -181,7 +181,7 @@ A: Tokenizer + recursive-descent for statements. Expression parser TBD. See [ZIN
181181

182182
## References
183183

184-
- [FlatZinc 2.8.4 Specification](https://docs.minizinc.dev/en/latest/fzn-spec.html)
184+
- [FlatZinc Specification](https://docs.minizinc.dev/en/stable/fzn-spec.html)
185185
- [MiniZinc Documentation](https://docs.minizinc.dev/)
186186
- [MiniZinc Global Constraints](https://docs.minizinc.dev/en/stable/lib-globals.html)
187187

docs/ZINC.md

Lines changed: 12 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
1-
https://docs.minizinc.dev/en/stable/flattening.html
2-
https://docs.minizinc.dev/en/stable/fzn-spec.html
1+
# FlatZinc Documentation
2+
3+
- Flattening: https://docs.minizinc.dev/en/stable/flattening.html
4+
- FlatZinc Specification: https://docs.minizinc.dev/en/stable/fzn-spec.html
35

46

57

@@ -121,11 +123,11 @@ pub fn import_flatzinc_str(input: &str) -> Result<Model, ZincImportError>;
121123

122124
## 2. MiniZinc and FlatZinc Standards and References
123125

124-
- **MiniZinc Language Reference (2.8.4):**
125-
- [MiniZinc 2.8.4 Language Reference](https://www.minizinc.org/doc-2.8.4/en/index.html)
126+
- **MiniZinc Language Reference:**
127+
- [MiniZinc Language Reference](https://docs.minizinc.dev/en/stable/)
126128
- [MiniZinc Grammar (BNF)](https://github.com/MiniZinc/libminizinc/blob/master/doc/grammar/minizinc.bnf)
127-
- **FlatZinc Specification (2.8.4):**
128-
- [FlatZinc 2.8.4 Specification](https://www.minizinc.org/doc-2.8.4/en/fzn-spec.html)
129+
- **FlatZinc Specification:**
130+
- [FlatZinc Specification](https://docs.minizinc.dev/en/stable/fzn-spec.html)
129131
- **File Types:**
130132
- `.mzn` — Model files (constraints, variables, parameters)
131133
- `.dzn` — Data files (parameter assignments)
@@ -199,11 +201,11 @@ pub fn import_flatzinc_str(input: &str) -> Result<Model, ZincImportError>;
199201

200202
## 5. References and Resources
201203

202-
- [MiniZinc 2.8.4 Language Reference](https://www.minizinc.org/doc-2.8.4/en/index.html)
204+
- [MiniZinc Language Reference](https://docs.minizinc.dev/en/stable/)
203205
- [MiniZinc BNF Grammar](https://github.com/MiniZinc/libminizinc/blob/master/doc/grammar/minizinc.bnf)
204-
- [FlatZinc 2.8.4 Specification](https://www.minizinc.org/doc-2.8.4/en/fzn-spec.html)
205-
- [MiniZinc Example Models](https://www.minizinc.org/examples.html)
206-
- [MiniZinc Standard Library](https://www.minizinc.org/doc-2.8.4/en/lib-globals.html)
206+
- [FlatZinc Specification](https://docs.minizinc.dev/en/stable/fzn-spec.html)
207+
- [MiniZinc Example Models](https://www.minizinc.org/software/)
208+
- [MiniZinc Standard Library](https://docs.minizinc.dev/en/stable/lib-globals.html)
207209

208210
---
209211

examples/clean_api.rs

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
//! Clean API example - the way it should be!
2+
//!
3+
//! Just call the methods: load → solve → to_flatzinc()
4+
5+
use zelen::prelude::*;
6+
7+
fn main() -> Result<(), Box<dyn std::error::Error>> {
8+
println!("=== FlatZinc Solver - Clean API ===\n");
9+
10+
// Example 1: Simple usage
11+
println!("Example 1: Simple Problem");
12+
println!("-------------------------");
13+
{
14+
let fzn = r#"
15+
var 1..10: x;
16+
var 1..10: y;
17+
constraint int_eq(x, 5);
18+
constraint int_plus(x, y, 12);
19+
solve satisfy;
20+
"#;
21+
22+
let mut solver = FlatZincSolver::new();
23+
solver.load_str(fzn)?;
24+
solver.solve().ok();
25+
26+
print!("{}", solver.to_flatzinc());
27+
}
28+
29+
// Example 2: Unsatisfiable problem
30+
println!("\nExample 2: Unsatisfiable");
31+
println!("------------------------");
32+
{
33+
let fzn = r#"
34+
var 1..5: x;
35+
constraint int_eq(x, 3);
36+
constraint int_eq(x, 7);
37+
solve satisfy;
38+
"#;
39+
40+
let mut solver = FlatZincSolver::new();
41+
solver.load_str(fzn)?;
42+
solver.solve().ok();
43+
44+
print!("{}", solver.to_flatzinc());
45+
}
46+
47+
// Example 3: From file
48+
println!("\nExample 3: N-Queens");
49+
println!("-------------------");
50+
{
51+
let fzn = r#"
52+
array[1..4] of var 1..4: q;
53+
constraint all_different(q);
54+
solve satisfy;
55+
"#;
56+
57+
let mut solver = FlatZincSolver::new();
58+
solver.load_str(fzn)?;
59+
60+
if solver.solve().is_ok() {
61+
solver.print_flatzinc();
62+
} else {
63+
println!("No solution found");
64+
}
65+
}
66+
67+
println!("\n=== API Summary ===");
68+
println!("1. FlatZincSolver::new() - create solver");
69+
println!("2. solver.load_str(fzn) - load FlatZinc");
70+
println!("3. solver.solve() - solve (satisfy/minimize/maximize)");
71+
println!("4. solver.to_flatzinc() - get formatted output with statistics");
72+
println!("5. solver.print_flatzinc() - print directly");
73+
println!("\nNo manual formatting, no manual context, no manual anything!");
74+
75+
Ok(())
76+
}

0 commit comments

Comments
 (0)