Skip to content

Commit 755a528

Browse files
committed
modulo for both var parameters
1 parent 6029b08 commit 755a528

12 files changed

Lines changed: 1250 additions & 72 deletions

File tree

CHANGELOG.md

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,9 @@
22

33
All notable changes to this project will be documented in this file.
44

5+
## [0.14.1] - 2025-10-17
6+
- Fix modulo to accept two variables
7+
58
## [0.14.0] - 2025-10-16
69
- count(var, var) now uses Vies-s and can work with both const and vars
710
- Boolean XOR implemented

Cargo.lock

Lines changed: 1 addition & 1 deletion
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

Cargo.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
[package]
22
name = "selen"
3-
version = "0.14.0"
3+
version = "0.14.1"
44
edition = "2024"
55
description = "Constraint Satisfaction Problem (CSP) solver"
66
rust-version = "1.88"

debug_backup/test_modulo_debug.rs

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
// Debug test for modulo constraint
2+
use selen::prelude::*;
3+
4+
fn main() {
5+
println!("=== Debug Modulo Constraint ===\n");
6+
7+
// Simplest possible test
8+
let mut m = Model::default();
9+
10+
let x = m.int(47, 47); // Fixed x = 47
11+
let y = m.int(10, 10); // Fixed y = 10
12+
let result = m.int(0, 9); // Result in [0..9]
13+
14+
println!("Variables created:");
15+
println!(" x: {:?}", x);
16+
println!(" y: {:?}", y);
17+
println!(" result: {:?}", result);
18+
19+
// Add modulo constraint
20+
println!("\nAdding modulo constraint: result = x mod y");
21+
let mod_id = m.modulo(x, y);
22+
println!(" Modulo created variable: {:?}", mod_id);
23+
24+
// Constrain result to equal mod_id
25+
m.new(result.eq(mod_id));
26+
27+
println!("\nSolving...");
28+
match m.solve() {
29+
Ok(solution) => {
30+
let x_val = solution.get_int(x);
31+
let y_val = solution.get_int(y);
32+
let result_val = solution.get_int(result);
33+
let mod_val = solution.get_int(mod_id);
34+
35+
println!("✓ Solution found!");
36+
println!(" x = {}", x_val);
37+
println!(" y = {}", y_val);
38+
println!(" result = {} (should be 7)", result_val);
39+
println!(" mod_id = {} (the direct modulo result)", mod_val);
40+
}
41+
Err(e) => {
42+
println!("✗ Failed: {:?}", e);
43+
}
44+
}
45+
}
Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
// Debug: trace what happens with deferred modulo
2+
use selen::prelude::*;
3+
4+
fn main() {
5+
let mut m = Model::default();
6+
7+
let number = m.int(10, 100);
8+
let divisor = m.int(10, 10);
9+
let remainder = m.int(0, 9);
10+
11+
println!("After creating variables:");
12+
println!(" number domain: [10..100]");
13+
println!(" divisor domain: [10..10]");
14+
println!(" remainder domain: [0..9]");
15+
16+
println!("\nCalling m.new(number.eq(47))...");
17+
m.new(number.eq(47));
18+
println!(" (constraint deferred)");
19+
20+
println!("\nCalling m.modulo(number, divisor)...");
21+
let mod_result = m.modulo(number, divisor);
22+
println!(" mod_result variable created: {:?}", mod_result);
23+
24+
println!("\nCalling m.new(remainder.eq(mod_result))...");
25+
m.new(remainder.eq(mod_result));
26+
println!(" (constraint deferred)");
27+
28+
println!("\nCalling m.solve()...");
29+
match m.solve() {
30+
Ok(sol) => {
31+
println!("✓ SOLUTION FOUND!");
32+
println!(" number = {}", sol.get_int(number));
33+
println!(" divisor = {}", sol.get_int(divisor));
34+
println!(" remainder = {}", sol.get_int(remainder));
35+
println!(" mod_result = {}", sol.get_int(mod_result));
36+
}
37+
Err(e) => {
38+
println!("✗ NO SOLUTION: {:?}", e);
39+
}
40+
}
41+
}

src/constraints/api/arithmetic.rs

Lines changed: 41 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -167,8 +167,14 @@ impl Model {
167167
let y_min = y.min_raw(&self.vars);
168168
let y_max = y.max_raw(&self.vars);
169169

170-
// Calculate bounds for modulo result
171-
// This is conservative - the actual bounds depend on the signs of x and y
170+
// IMPORTANT: We must create the result variable with bounds that account for
171+
// potential pending deferred constraints. Since we can't know what those are,
172+
// we use CONSERVATIVE bounds that encompass all possible modulo results.
173+
174+
// For modulo, the result is always in range [0, |divisor|-1] when divisor > 0
175+
// So we need to find the range that could result from ANY x in its range
176+
// and ANY y in its range that isn't zero.
177+
172178
let mut min = Val::ValI(i32::MAX);
173179
let mut max = Val::ValI(i32::MIN);
174180

@@ -207,6 +213,39 @@ impl Model {
207213
Val::ValF(f) => Val::ValF(-f),
208214
};
209215
max = y_abs_max;
216+
} else {
217+
// CRITICAL FIX: Even with sampled bounds, we need to be MORE conservative
218+
// to handle deferred constraints that might widen the operand domains.
219+
// Expand the bounds to cover all possible modulo results.
220+
match (min, max) {
221+
(Val::ValI(_min_i), Val::ValI(_max_i)) => {
222+
// For integers, check what the worst-case modulo result could be
223+
// given the range of divisors
224+
if let (Val::ValI(y_min_i), Val::ValI(y_max_i)) = (y_min, y_max) {
225+
// The maximum modulo result magnitude is (max(|y|) - 1)
226+
let y_abs_max = if y_min_i.abs() > y_max_i.abs() {
227+
y_min_i.abs()
228+
} else {
229+
y_max_i.abs()
230+
};
231+
232+
if y_abs_max > 0 {
233+
// Result can be [-(y_abs_max-1), y_abs_max-1]
234+
// Only expand if needed to encompass computed range
235+
let new_min = Val::ValI(-(y_abs_max - 1));
236+
let new_max = Val::ValI(y_abs_max - 1);
237+
238+
if new_min < min {
239+
min = new_min;
240+
}
241+
if new_max > max {
242+
max = new_max;
243+
}
244+
}
245+
}
246+
}
247+
_ => {} // For floats, keep as-is
248+
}
210249
}
211250

212251
let s = self.new_var_unchecked(min, max);

src/constraints/props/modulo.rs

Lines changed: 89 additions & 68 deletions
Original file line numberDiff line numberDiff line change
@@ -22,20 +22,59 @@ impl<U: View, V: View> Prune for Modulo<U, V> {
2222
let x_max = self.x.max(ctx);
2323
let y_min = self.y.min(ctx);
2424
let y_max = self.y.max(ctx);
25+
let s_min = self.s.min(ctx);
26+
let s_max = self.s.max(ctx);
2527

2628
// If y contains zero or values too close to zero, we can't safely compute modulo
2729
if Val::range_contains_unsafe_divisor(y_min, y_max) {
2830
// We can still try to propagate some constraints if parts of the domain are safe
2931
return Some(());
3032
}
3133

32-
// Calculate possible modulo results
33-
let mut s_candidates = Vec::new();
34-
35-
// For modulo, the result is always in range [0, |y|-1] for positive y
36-
// and [-|y|+1, 0] for negative y, but we need to be more careful with mixed signs
34+
// CASE 1: Both x and y are fixed → exact computation
35+
if x_min == x_max && y_min == y_max {
36+
if let Some(exact_result) = x_min.safe_mod(y_min) {
37+
// Set s to this exact value
38+
self.s.try_set_min(exact_result, ctx)?;
39+
self.s.try_set_max(exact_result, ctx)?;
40+
return Some(());
41+
}
42+
}
43+
44+
// CASE 2: y is fixed (and non-zero) → compute s bounds based on x range
45+
if y_min == y_max {
46+
if let Val::ValI(y_val) = y_min {
47+
if y_val != 0 {
48+
// For modulo: s is in range [0, |y|-1] when y > 0
49+
// or [-(|y|-1), 0] when y < 0
50+
if y_val > 0 {
51+
let s_theoretical_min = Val::ValI(0);
52+
let s_theoretical_max = Val::ValI(y_val - 1);
53+
54+
let new_s_min = if s_theoretical_min > s_min { s_theoretical_min } else { s_min };
55+
let new_s_max = if s_theoretical_max < s_max { s_theoretical_max } else { s_max };
56+
57+
self.s.try_set_min(new_s_min, ctx)?;
58+
self.s.try_set_max(new_s_max, ctx)?;
59+
} else {
60+
// y_val < 0
61+
let s_theoretical_min = Val::ValI(y_val + 1);
62+
let s_theoretical_max = Val::ValI(0);
63+
64+
let new_s_min = if s_theoretical_min > s_min { s_theoretical_min } else { s_min };
65+
let new_s_max = if s_theoretical_max < s_max { s_theoretical_max } else { s_max };
66+
67+
self.s.try_set_min(new_s_min, ctx)?;
68+
self.s.try_set_max(new_s_max, ctx)?;
69+
}
70+
}
71+
}
72+
}
73+
74+
// CASE 3: Both x and y are in bounded ranges → compute s bounds
75+
let mut s_candidates = Vec::with_capacity(4);
3776

38-
// Sample points at domain boundaries and some intermediate values
77+
// Sample points at domain boundaries
3978
let x_samples = if x_min == x_max {
4079
vec![x_min]
4180
} else {
@@ -52,7 +91,7 @@ impl<U: View, V: View> Prune for Modulo<U, V> {
5291
for &x_val in &x_samples {
5392
for &y_val in &y_samples {
5493
if let Some(mod_result) = x_val.safe_mod(y_val) {
55-
// Check if the result is not NaN or infinite
94+
// Check if the result is valid
5695
match mod_result {
5796
Val::ValF(f) if f.is_finite() => s_candidates.push(mod_result),
5897
Val::ValI(_) => s_candidates.push(mod_result),
@@ -64,70 +103,52 @@ impl<U: View, V: View> Prune for Modulo<U, V> {
64103

65104
if !s_candidates.is_empty() {
66105
// Find bounds for s based on modulo properties
67-
let s_min = s_candidates.iter().fold(s_candidates[0], |acc, &x| if x < acc { x } else { acc });
68-
let s_max = s_candidates.iter().fold(s_candidates[0], |acc, &x| if x > acc { x } else { acc });
69-
70-
// For modulo, we know more about the bounds:
71-
// If y > 0: 0 <= s < y
72-
// If y < 0: y < s <= 0
73-
// We can use this to tighten bounds further
74-
let y_abs_min = match (y_min, y_max) {
75-
(Val::ValI(min_i), Val::ValI(max_i)) => {
76-
if min_i > 0 { Some(Val::ValI(0)) }
77-
else if max_i < 0 { Some(Val::ValI(max_i + 1)) }
78-
else { None }
79-
},
80-
(Val::ValF(min_f), Val::ValF(max_f)) => {
81-
if min_f > 0.0 { Some(Val::ValF(0.0)) }
82-
else if max_f < 0.0 { Some(Val::ValF(max_f + 1.0)) }
83-
else { None }
84-
},
85-
_ => None,
86-
};
106+
let s_computed_min = s_candidates.iter().fold(s_candidates[0], |acc, &x| if x < acc { x } else { acc });
107+
let s_computed_max = s_candidates.iter().fold(s_candidates[0], |acc, &x| if x > acc { x } else { acc });
87108

88-
let y_abs_max = match (y_min, y_max) {
89-
(Val::ValI(min_i), Val::ValI(max_i)) => {
90-
if min_i > 0 { Some(Val::ValI(max_i - 1)) }
91-
else if max_i < 0 { Some(Val::ValI(0)) }
92-
else { None }
93-
},
94-
(Val::ValF(min_f), Val::ValF(max_f)) => {
95-
if min_f > 0.0 { Some(Val::ValF(max_f - f64::EPSILON)) }
96-
else if max_f < 0.0 { Some(Val::ValF(0.0)) }
97-
else { None }
98-
},
99-
_ => None,
100-
};
101-
102-
// Use the tighter bounds if available
103-
let final_s_min = if let Some(theoretical_min) = y_abs_min {
104-
if theoretical_min > s_min { theoretical_min } else { s_min }
105-
} else { s_min };
106-
107-
let final_s_max = if let Some(theoretical_max) = y_abs_max {
108-
if theoretical_max < s_max { theoretical_max } else { s_max }
109-
} else { s_max };
110-
111-
// Propagate bounds to s
112-
let _min = self.s.try_set_min(final_s_min, ctx)?;
113-
let _max = self.s.try_set_max(final_s_max, ctx)?;
109+
// CRITICAL FIX: Allow expansion if current domain is too narrow
110+
// This can happen when result variable was created before deferred constraints applied
111+
// and those deferred constraints now require larger modulo values.
112+
// We must try to set the bounds, and if it fails, return None (fail the space)
113+
self.s.try_set_min(s_computed_min, ctx)?;
114+
self.s.try_set_max(s_computed_max, ctx)?;
114115
}
115-
116-
// Back-propagation is complex for modulo, so we do limited propagation
117-
// We can at least ensure that if s is known and y is known, we can constrain x
118-
let s_min = self.s.min(ctx);
119-
let s_max = self.s.max(ctx);
120-
121-
// If y and s are both fixed, we can derive some constraints on x
116+
117+
// CASE 4: Back-propagation from s to x (when y and s are fixed)
122118
if y_min == y_max && s_min == s_max {
123-
// x = k * y + s for some integer k
124-
// We need to find valid values of k such that x is in its domain
125-
let y_val = y_min;
126-
let s_val = s_min;
127-
128-
if let (Some(_), Some(_)) = (y_val.safe_div(Val::ValI(1)), s_val.safe_div(Val::ValI(1))) {
129-
// For now, we don't do complex back-propagation for modulo
130-
// This would require more sophisticated interval arithmetic
119+
if let (Val::ValI(y_val), Val::ValI(s_val)) = (y_min, s_min) {
120+
if y_val != 0 && s_val >= 0 && s_val < y_val.abs() {
121+
// x = k * y + s for some integer k
122+
// We need to find the range of k such that x remains in bounds
123+
let x_current_min = x_min;
124+
let x_current_max = x_max;
125+
126+
// Find the minimum and maximum k
127+
let mut valid_x_values = Vec::with_capacity(8);
128+
129+
if let (Val::ValI(x_curr_min), Val::ValI(x_curr_max)) = (x_current_min, x_current_max) {
130+
// Try k values that produce x in the valid range
131+
let k_min_theoretical = (x_curr_min - s_val) / y_val;
132+
let k_max_theoretical = (x_curr_max - s_val) / y_val;
133+
134+
// Try a range around these theoretical k values
135+
for k in (k_min_theoretical - 1)..=(k_max_theoretical + 1) {
136+
let candidate_x = k * y_val + s_val;
137+
if candidate_x >= x_curr_min && candidate_x <= x_curr_max {
138+
valid_x_values.push(Val::ValI(candidate_x));
139+
}
140+
}
141+
142+
if !valid_x_values.is_empty() {
143+
let new_x_min = valid_x_values.iter().fold(valid_x_values[0], |acc, &x| if x < acc { x } else { acc });
144+
let new_x_max = valid_x_values.iter().fold(valid_x_values[0], |acc, &x| if x > acc { x } else { acc });
145+
146+
// Try to tighten x bounds
147+
self.x.try_set_min(new_x_min, ctx)?;
148+
self.x.try_set_max(new_x_max, ctx)?;
149+
}
150+
}
151+
}
131152
}
132153
}
133154

0 commit comments

Comments
 (0)