selen 0.15.5

Constraint Satisfaction Problem (CSP) 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
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127

use selen::prelude::*;

#[test]
fn test_implies_true_implies_true() {
    let mut m = Model::default();
    let a = m.bool();
    let b = m.bool();
    
    m.implies(a, b);  // a → b
    m.new(a.eq(bool(true)));  // a is true
    
    let solution = m.solve().unwrap();
    // If a is true, b must be true
    assert_eq!(solution.get_bool(a).unwrap(), true);
    assert_eq!(solution.get_bool(b).unwrap(), true);
}

#[test]
fn test_implies_false_allows_anything() {
    let mut m = Model::default();
    let a = m.bool();
    let b = m.bool();
    
    m.implies(a, b);  // a → b
    m.new(a.eq(bool(false)));  // a is false
    
    let solution = m.solve().unwrap();
    // If a is false, b can be either true or false
    assert_eq!(solution.get_bool(a).unwrap(), false);
    // b can be anything, just check we got a solution
    let _ = solution.get_bool(b).unwrap();
}

#[test]
fn test_implies_violation() {
    let mut m = Model::default();
    let a = m.bool();
    let b = m.bool();
    
    m.implies(a, b);  // a → b
    m.new(a.eq(bool(true)));  // a is true
    m.new(b.eq(bool(false))); // b is false - violates implication!
    
    // Should be unsatisfiable: true → false is false
    assert!(m.solve().is_err());
}

#[test]
fn test_implies_chain() {
    let mut m = Model::default();
    let a = m.bool();
    let b = m.bool();
    let c = m.bool();
    
    m.implies(a, b);  // a → b
    m.implies(b, c);  // b → c
    m.new(a.eq(bool(true)));  // a is true
    
    let solution = m.solve().unwrap();
    // Chain: if a then b, if b then c, so if a then c
    assert_eq!(solution.get_bool(a).unwrap(), true);
    assert_eq!(solution.get_bool(b).unwrap(), true);
    assert_eq!(solution.get_bool(c).unwrap(), true);
}

#[test]
fn test_implies_multiple() {
    let mut m = Model::default();
    let a = m.bool();
    let b = m.bool();
    let c = m.bool();
    
    m.implies(a, b);  // if a then b
    m.implies(a, c);  // if a then c
    m.new(a.eq(bool(true)));  // a is true
    
    let solution = m.solve().unwrap();
    // If a is true, both b and c must be true
    assert_eq!(solution.get_bool(a).unwrap(), true);
    assert_eq!(solution.get_bool(b).unwrap(), true);
    assert_eq!(solution.get_bool(c).unwrap(), true);
}

#[test]
fn test_implies_biconditional() {
    let mut m = Model::default();
    let a = m.bool();
    let b = m.bool();
    
    // a ↔ b (biconditional) = (a → b) ∧ (b → a)
    m.implies(a, b);
    m.implies(b, a);
    m.new(a.eq(bool(true)));
    
    let solution = m.solve().unwrap();
    // Both must have the same value
    assert_eq!(solution.get_bool(a).unwrap(), true);
    assert_eq!(solution.get_bool(b).unwrap(), true);
}

#[test]
fn test_implies_with_int_conditions() {
    let mut m = Model::default();
    let x = m.int(1, 10);
    let y = m.int(1, 10);
    let a = m.bool();
    let b = m.bool();
    
    let five = m.int(5, 5);  // constant variable
    
    // Reified: a ↔ (x > 5)
    m.gt_reif(x, five, a);
    // Reified: b ↔ (y > 5)
    m.gt_reif(y, five, b);
    
    // If x > 5, then y > 5
    m.implies(a, b);
    
    m.new(x.eq(int(7)));  // x > 5, so a = true
    
    let solution = m.solve().unwrap();
    assert_eq!(solution.get_int(x), 7);
    assert_eq!(solution.get_bool(a).unwrap(), true);
    assert_eq!(solution.get_bool(b).unwrap(), true);
    // y must be > 5
    assert!(solution.get_int(y) > 5);
}