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
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
use crate::{constraints::props::{Propagate, Prune}, variables::{VarId, Val}, variables::views::{Context, View}};
/// Boolean AND constraint: `result = a AND b AND c AND ...`.
/// This constraint enforces that the result variable equals the logical AND of all input variables.
/// All variables are treated as boolean: 0 = false, non-zero = true.
#[derive(Clone, Debug)]
#[doc(hidden)]
pub struct BoolAnd {
operands: Vec<VarId>,
result: VarId,
}
impl BoolAnd {
pub fn new(operands: Vec<VarId>, result: VarId) -> Self {
Self { operands, result }
}
}
impl Prune for BoolAnd {
fn prune(&self, ctx: &mut Context) -> Option<()> {
if self.operands.is_empty() {
// Empty AND is typically true
let _r = self.result.try_set_min(Val::ValI(1), ctx)?;
let _r = self.result.try_set_max(Val::ValI(1), ctx)?;
return Some(());
}
// For boolean AND:
// 1. If result = 1, then all operands must be 1 (non-zero)
// 2. If any operand = 0, then result must be 0
// 3. If result = 0, then at least one operand must be 0
let result_min = self.result.min(ctx);
let result_max = self.result.max(ctx);
// Check if result is fixed to true (1)
if result_min >= Val::ValI(1) {
// All operands must be true (>= 1)
for &operand in &self.operands {
let _min = operand.try_set_min(Val::ValI(1), ctx)?;
}
}
// Check if result is fixed to false (0)
if result_max <= Val::ValI(0) {
// At least one operand must be false (0)
// If all but one operands are already true, force the remaining one to be false
let mut false_operands = 0;
let mut undetermined_operands = Vec::new();
for &operand in &self.operands {
let op_min = operand.min(ctx);
let op_max = operand.max(ctx);
if op_max <= Val::ValI(0) {
false_operands += 1;
} else if op_min <= Val::ValI(0) && op_max >= Val::ValI(1) {
undetermined_operands.push(operand);
}
// If op_min >= 1, the operand is definitely true
}
// If no operands are false and only one is undetermined, it must be false
if false_operands == 0 && undetermined_operands.len() == 1 {
let _max = undetermined_operands[0].try_set_max(Val::ValI(0), ctx)?;
}
}
// Now propagate from operands to result
let mut all_true = true;
let mut any_false = false;
for &operand in &self.operands {
let op_min = operand.min(ctx);
let op_max = operand.max(ctx);
if op_max <= Val::ValI(0) {
// This operand is definitely false
any_false = true;
break;
} else if op_min <= Val::ValI(0) {
// This operand could be false
all_true = false;
}
// If op_min >= 1, this operand is definitely true
}
if any_false {
// At least one operand is false, so result must be false
let _max = self.result.try_set_max(Val::ValI(0), ctx)?;
} else if all_true {
// All operands are definitely true, so result must be true
let _min = self.result.try_set_min(Val::ValI(1), ctx)?;
}
Some(())
}
}
impl Propagate for BoolAnd {
fn list_trigger_vars(&self) -> impl Iterator<Item = VarId> {
core::iter::once(self.result)
.chain(self.operands.iter().copied())
}
}
/// Boolean OR constraint: `result = a OR b OR c OR ...`.
/// This constraint enforces that the result variable equals the logical OR of all input variables.
/// All variables are treated as boolean: 0 = false, non-zero = true.
#[derive(Clone, Debug)]
#[doc(hidden)]
pub struct BoolOr {
operands: Vec<VarId>,
result: VarId,
}
impl BoolOr {
pub fn new(operands: Vec<VarId>, result: VarId) -> Self {
Self { operands, result }
}
}
impl Prune for BoolOr {
fn prune(&self, ctx: &mut Context) -> Option<()> {
if self.operands.is_empty() {
// Empty OR is typically false
let _r = self.result.try_set_min(Val::ValI(0), ctx)?;
let _r = self.result.try_set_max(Val::ValI(0), ctx)?;
return Some(());
}
// For boolean OR:
// 1. If result = 0, then all operands must be 0
// 2. If any operand = 1, then result must be 1
// 3. If result = 1, then at least one operand must be 1
let result_min = self.result.min(ctx);
let result_max = self.result.max(ctx);
// Check if result is fixed to false (0)
if result_max <= Val::ValI(0) {
// All operands must be false (0)
for &operand in &self.operands {
let _max = operand.try_set_max(Val::ValI(0), ctx)?;
}
}
// Check if result is fixed to true (1)
if result_min >= Val::ValI(1) {
// At least one operand must be true (>= 1)
// If all but one operands are already false, force the remaining one to be true
let mut true_operands = 0;
let mut undetermined_operands = Vec::new();
for &operand in &self.operands {
let op_min = operand.min(ctx);
let op_max = operand.max(ctx);
if op_min >= Val::ValI(1) {
true_operands += 1;
} else if op_min <= Val::ValI(0) && op_max >= Val::ValI(1) {
undetermined_operands.push(operand);
}
// If op_max <= 0, the operand is definitely false
}
// If no operands are true and only one is undetermined, it must be true
if true_operands == 0 && undetermined_operands.len() == 1 {
let _min = undetermined_operands[0].try_set_min(Val::ValI(1), ctx)?;
}
}
// Now propagate from operands to result
let mut all_false = true;
let mut any_true = false;
for &operand in &self.operands {
let op_min = operand.min(ctx);
let op_max = operand.max(ctx);
if op_min >= Val::ValI(1) {
// This operand is definitely true
any_true = true;
break;
} else if op_max >= Val::ValI(1) {
// This operand could be true
all_false = false;
}
// If op_max <= 0, this operand is definitely false
}
if any_true {
// At least one operand is true, so result must be true
let _min = self.result.try_set_min(Val::ValI(1), ctx)?;
} else if all_false {
// All operands are definitely false, so result must be false
let _max = self.result.try_set_max(Val::ValI(0), ctx)?;
}
Some(())
}
}
impl Propagate for BoolOr {
fn list_trigger_vars(&self) -> impl Iterator<Item = VarId> {
core::iter::once(self.result)
.chain(self.operands.iter().copied())
}
}
/// Boolean NOT constraint: `result = NOT operand`.
/// This constraint enforces that the result variable equals the logical NOT of the operand.
/// Variables are treated as boolean: 0 = false, non-zero = true.
#[derive(Clone, Debug)]
#[doc(hidden)]
pub struct BoolNot {
operand: VarId,
result: VarId,
}
impl BoolNot {
pub fn new(operand: VarId, result: VarId) -> Self {
Self { operand, result }
}
}
impl Prune for BoolNot {
fn prune(&self, ctx: &mut Context) -> Option<()> {
// For boolean NOT:
// If operand = 0, then result = 1
// If operand != 0, then result = 0
// Conversely:
// If result = 0, then operand != 0 (operand >= 1)
// If result = 1, then operand = 0
let operand_min = self.operand.min(ctx);
let operand_max = self.operand.max(ctx);
let result_min = self.result.min(ctx);
let result_max = self.result.max(ctx);
// Propagate from operand to result
if operand_max <= Val::ValI(0) {
// Operand is definitely false (0), so result must be true (1)
let _min = self.result.try_set_min(Val::ValI(1), ctx)?;
let _max = self.result.try_set_max(Val::ValI(1), ctx)?;
} else if operand_min >= Val::ValI(1) {
// Operand is definitely true (>= 1), so result must be false (0)
let _min = self.result.try_set_min(Val::ValI(0), ctx)?;
let _max = self.result.try_set_max(Val::ValI(0), ctx)?;
}
// Propagate from result to operand
if result_max <= Val::ValI(0) {
// Result is definitely false (0), so operand must be true (>= 1)
let _min = self.operand.try_set_min(Val::ValI(1), ctx)?;
} else if result_min >= Val::ValI(1) {
// Result is definitely true (1), so operand must be false (0)
let _min = self.operand.try_set_min(Val::ValI(0), ctx)?;
let _max = self.operand.try_set_max(Val::ValI(0), ctx)?;
}
Some(())
}
}
impl Propagate for BoolNot {
fn list_trigger_vars(&self) -> impl Iterator<Item = VarId> {
core::iter::once(self.result)
.chain(core::iter::once(self.operand))
}
}
/// Boolean XOR constraint: `result = a XOR b`.
/// This constraint enforces that the result variable equals the logical XOR of two boolean operands.
/// XOR is true (1) when exactly one operand is true (non-zero).
/// Variables are treated as boolean: 0 = false, non-zero = true.
#[derive(Clone, Debug)]
#[doc(hidden)]
pub struct BoolXor {
x: VarId,
y: VarId,
result: VarId,
}
impl BoolXor {
pub fn new(x: VarId, y: VarId, result: VarId) -> Self {
Self { x, y, result }
}
}
impl Prune for BoolXor {
fn prune(&self, ctx: &mut Context) -> Option<()> {
// XOR truth table (treating as boolean: 0 = false, 1 = true):
// x | y | x XOR y
// --+---+--------
// 0 | 0 | 0
// 0 | 1 | 1
// 1 | 0 | 1
// 1 | 1 | 0
//
// So: result = 1 iff (x = 0 and y = 1) or (x = 1 and y = 0)
// result = 0 iff (x = 0 and y = 0) or (x = 1 and y = 1)
let x_min = self.x.min(ctx);
let x_max = self.x.max(ctx);
let y_min = self.y.min(ctx);
let y_max = self.y.max(ctx);
let result_min = self.result.min(ctx);
let result_max = self.result.max(ctx);
// Case 1: result is fixed to 1 (must be true)
if result_min >= Val::ValI(1) {
// x XOR y must be true
// This means: (x=0 AND y=1) OR (x=1 AND y=0)
// If x is definitely 0, then y must be definitely 1
if x_max <= Val::ValI(0) {
let _min = self.y.try_set_min(Val::ValI(1), ctx)?;
}
// If x is definitely 1 (>= 1), then y must be definitely 0
if x_min >= Val::ValI(1) {
let _max = self.y.try_set_max(Val::ValI(0), ctx)?;
}
// Similarly for y
if y_max <= Val::ValI(0) {
let _min = self.x.try_set_min(Val::ValI(1), ctx)?;
}
if y_min >= Val::ValI(1) {
let _max = self.x.try_set_max(Val::ValI(0), ctx)?;
}
}
// Case 2: result is fixed to 0 (must be false)
if result_max <= Val::ValI(0) {
// x XOR y must be false
// This means: (x=0 AND y=0) OR (x=1 AND y=1)
// If x is definitely 0, then y must be definitely 0
if x_max <= Val::ValI(0) {
let _max = self.y.try_set_max(Val::ValI(0), ctx)?;
}
// If x is definitely 1, then y must be definitely 1
if x_min >= Val::ValI(1) {
let _min = self.y.try_set_min(Val::ValI(1), ctx)?;
}
// Similarly for y
if y_max <= Val::ValI(0) {
let _max = self.x.try_set_max(Val::ValI(0), ctx)?;
}
if y_min >= Val::ValI(1) {
let _min = self.x.try_set_min(Val::ValI(1), ctx)?;
}
}
// Case 3: Propagate from fixed x and y to result
// If both x and y are fixed (or determinable)
if x_min == x_max && y_min == y_max {
let x_bool = x_min >= Val::ValI(1);
let y_bool = y_min >= Val::ValI(1);
let xor_result = x_bool != y_bool; // XOR operation
if xor_result {
let _min = self.result.try_set_min(Val::ValI(1), ctx)?;
let _max = self.result.try_set_max(Val::ValI(1), ctx)?;
} else {
let _min = self.result.try_set_min(Val::ValI(0), ctx)?;
let _max = self.result.try_set_max(Val::ValI(0), ctx)?;
}
}
Some(())
}
}
impl Propagate for BoolXor {
fn list_trigger_vars(&self) -> impl Iterator<Item = VarId> {
core::iter::once(self.result)
.chain(core::iter::once(self.x))
.chain(core::iter::once(self.y))
}
}