zelen 0.5.1

Direct MiniZinc to Selen Solver
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90

#![allow(dead_code)]

/// Test forall loops (comprehensions) in constraints
use zelen::{parse, translator::Translator};

fn main() {
    println!("=== Testing Forall Loops ===\n");

    // Test 1: Simple forall with constraint
    println!("Test 1: Simple forall loop\n");
    let source1 = r#"
        int: n = 5;
        array[1..n] of var 1..10: x;
        
        constraint forall(i in 1..n)(x[i] >= i);
        
        solve satisfy;
    "#;

    let ast = parse(source1).unwrap();
    let result = Translator::translate_with_vars(&ast);
    
    match result {
        Ok(model_data) => {
            match model_data.model.solve() {
                Ok(sol) => {
                    println!("✓ SOLVED!");
                    if let Some(arr) = model_data.int_var_arrays.get("x") {
                        println!("  x array values:");
                        for (i, var_id) in arr.iter().enumerate() {
                            let val = sol.get_int(*var_id);
                            println!("    x[{}] = {}", i + 1, val);
                            assert!(val >= (i + 1) as i32, "Constraint violated!");
                        }
                    }
                    println!("  ✓ All constraints satisfied!\n");
                }
                Err(e) => println!("✗ FAILED TO SOLVE: {:?}\n", e),
            }
        }
        Err(e) => println!("✗ TRANSLATION ERROR: {:?}\n", e),
    }

    // Test 2: Forall with multiple generators (nested loops)
    println!("Test 2: Forall with multiple generators\n");
    let source2 = r#"
        int: n = 3;
        array[1..n] of var 1..10: x;
        
        constraint forall(i in 1..n, j in i+1..n)(
            x[i] < x[j]
        );
        
        solve satisfy;
    "#;

    let ast2 = parse(source2);
    match ast2 {
        Ok(parsed_ast) => {
            let result2 = Translator::translate_with_vars(&parsed_ast);
            match result2 {
                Ok(model_data) => {
                    match model_data.model.solve() {
                        Ok(sol) => {
                            println!("✓ SOLVED!");
                            if let Some(arr) = model_data.int_var_arrays.get("x") {
                                println!("  x array values:");
                                for (i, var_id) in arr.iter().enumerate() {
                                    let val = sol.get_int(*var_id);
                                    println!("    x[{}] = {}", i + 1, val);
                                }
                                // Verify multi-generator constraints
                                let vals: Vec<_> = arr.iter().map(|v| sol.get_int(*v)).collect();
                                for i in 0..vals.len() {
                                    for j in (i+1)..vals.len() {
                                        assert!(vals[i] < vals[j], "Constraint x[{}] < x[{}] violated!", i+1, j+1);
                                    }
                                }
                            }
                            println!("  ✓ All constraints satisfied!\n");
                        }
                        Err(e) => println!("✗ FAILED TO SOLVE: {:?}\n", e),
                    }
                }
                Err(e) => println!("✗ TRANSLATION ERROR: {:?}\n", e),
            }
        }
        Err(e) => println!("✗ PARSE ERROR: {:?}\n", e),
    }
}