Add regression test for XOR encoding bug in pindakaas

Resolves #77
Resolves #78

crates/huub/src/model/bool.rs

@@ -443,7 +443,7 @@ mod tests {
 	use expect_test::expect;
 	use itertools::Itertools;
 
-	use crate::{BoolExpr, InitConfig, Model, Solver};
+	use crate::{model::bool::BoolView, BoolExpr, InitConfig, Model, Solver};
 
 	#[test]
 	fn test_bool_and() {
@@ -484,13 +484,13 @@ mod tests {
 		slv.expect_solutions(
 			&vars,
 			expect![[r#"
-    false, false, true
-    false, true, false
-    false, true, true
-    true, false, false
-    true, false, true
-    true, true, false
-    true, true, true"#]],
+		false, false, true
+		false, true, false
+		false, true, true
+		true, false, false
+		true, false, true
+		true, true, false
+		true, true, true"#]],
 		);
 
 		// Simple Unsatisfiable test case
@@ -518,10 +518,33 @@ mod tests {
 		slv.expect_solutions(
 			&vars,
 			expect![[r#"
-    false, false, true
-    false, true, false
-    true, false, false
-    true, true, true"#]],
+				false, false, true
+				false, true, false
+				true, false, false
+				true, true, true"#]],
+		);
+
+		// Regression test case
+		let mut m = Model::default();
+		let b = m.new_bool_vars(2);
+
+		m += BoolExpr::Equiv(vec![
+			BoolExpr::View(b[1].clone()),
+			BoolExpr::Xor(vec![
+				BoolExpr::View(BoolView::Const(true)),
+				BoolExpr::View(b[0].clone()),
+			]),
+		]);
+		let (mut slv, map): (Solver, _) = m.to_solver(&InitConfig::default()).unwrap();
+		let vars: Vec<_> = b
+			.into_iter()
+			.map(|x| map.get(&mut slv, &x.into()))
+			.collect();
+		slv.expect_solutions(
+			&vars,
+			expect![[r#"
+				false, true
+				true, false"#]],
 		);
 
 		// Simple Unsatisfiable test case
@@ -553,10 +576,10 @@ mod tests {
 		slv.expect_solutions(
 			&vars,
 			expect![[r#"
-    false, false, true
-    false, true, false
-    true, false, false
-    true, true, true"#]],
+		false, false, true
+		false, true, false
+		true, false, false
+		true, true, true"#]],
 		);
 	}
 
@@ -578,10 +601,10 @@ mod tests {
 		slv.expect_solutions(
 			&vars,
 			expect![[r#"
-    false, false, false
-    false, false, true
-    false, true, false
-    true, true, true"#]],
+		false, false, false
+		false, false, true
+		false, true, false
+		true, true, true"#]],
 		);
 	}
 
@@ -603,10 +626,10 @@ mod tests {
 		slv.expect_solutions(
 			&vars,
 			expect![[r#"
-    false, false, false
-    true, false, true
-    true, true, false
-    true, true, true"#]],
+		false, false, false
+		true, false, true
+		true, true, false
+		true, true, true"#]],
 		);
 	}
 }

crates/huub/src/model/constraint.rs

@@ -203,7 +203,7 @@ impl Constraint {
 					.collect();
 				// coeffs * vars <= c
 				slv.add_propagator(IntLinearLessEqBounds::prepare(vars.clone(), *c));
-				// coeffs * vars >= c <=>  -coeffs * vars <= -c
+				// coeffs * vars >= c <=> -coeffs * vars <= -c
 				slv.add_propagator(IntLinearLessEqBounds::prepare(
 					vars.into_iter().map(|v| -v),
 					-c,

crates/huub/src/propagator/array_int_minimum.rs

@@ -158,8 +158,8 @@ mod tests {
 		slv.expect_solutions(
 			&vars,
 			expect![[r#"
-    3, 3, 3, 3
-    4, 3, 3, 3"#]],
+		3, 3, 3, 3
+		4, 3, 3, 3"#]],
 		);
 	}
 
@@ -195,12 +195,12 @@ mod tests {
 		slv.expect_solutions(
 			&vars,
 			expect![[r#"
-    1, 3, 2, 3
-    1, 3, 3, 3
-    2, 3, 2, 3
-    2, 3, 3, 3
-    3, 3, 2, 3
-    3, 3, 3, 3"#]],
+		1, 3, 2, 3
+		1, 3, 3, 3
+		2, 3, 2, 3
+		2, 3, 3, 3
+		3, 3, 2, 3
+		3, 3, 3, 3"#]],
 		);
 	}
 

crates/huub/src/propagator/array_var_int_element.rs

@@ -276,22 +276,22 @@ mod tests {
 		slv.expect_solutions(
 			&[idx, y, a, b, c],
 			expect![[r#"
-    0, 3, 3, 2, 4
-    0, 3, 3, 2, 5
-    0, 3, 3, 3, 4
-    0, 3, 3, 3, 5
-    0, 4, 4, 2, 4
-    0, 4, 4, 2, 5
-    0, 4, 4, 3, 4
-    0, 4, 4, 3, 5
-    1, 3, 3, 3, 4
-    1, 3, 3, 3, 5
-    1, 3, 4, 3, 4
-    1, 3, 4, 3, 5
-    2, 4, 3, 2, 4
-    2, 4, 3, 3, 4
-    2, 4, 4, 2, 4
-    2, 4, 4, 3, 4"#]],
+		0, 3, 3, 2, 4
+		0, 3, 3, 2, 5
+		0, 3, 3, 3, 4
+		0, 3, 3, 3, 5
+		0, 4, 4, 2, 4
+		0, 4, 4, 2, 5
+		0, 4, 4, 3, 4
+		0, 4, 4, 3, 5
+		1, 3, 3, 3, 4
+		1, 3, 3, 3, 5
+		1, 3, 4, 3, 4
+		1, 3, 4, 3, 5
+		2, 4, 3, 2, 4
+		2, 4, 3, 3, 4
+		2, 4, 4, 2, 4
+		2, 4, 4, 3, 4"#]],
 		);
 	}
 

crates/huub/src/propagator/disjunctive.rs

@@ -620,16 +620,16 @@ mod tests {
 		slv.expect_solutions(
 			&[a, b, c],
 			expect![[r#"
-    0, 3, 2
-    0, 4, 2
-    0, 4, 3
-    1, 3, 0
-    1, 4, 0
-    1, 4, 3
-    2, 4, 0
-    2, 4, 1
-    4, 0, 3
-    4, 1, 0"#]],
+		0, 3, 2
+		0, 4, 2
+		0, 4, 3
+		1, 3, 0
+		1, 4, 0
+		1, 4, 3
+		2, 4, 0
+		2, 4, 1
+		4, 0, 3
+		4, 1, 0"#]],
 		);
 	}
 }

crates/huub/src/propagator/int_lin_le.rs

@@ -338,17 +338,17 @@ mod tests {
 		slv.expect_solutions(
 			&[r, a, b, c],
 			expect![[r#"
-    false, 1, 1, 1
-    false, 1, 1, 2
-    false, 1, 2, 1
-    false, 1, 2, 2
-    false, 2, 1, 1
-    false, 2, 1, 2
-    false, 2, 2, 1
-    false, 2, 2, 2
-    true, 1, 1, 1
-    true, 1, 1, 2
-    true, 1, 2, 1"#]],
+		false, 1, 1, 1
+		false, 1, 1, 2
+		false, 1, 2, 1
+		false, 1, 2, 2
+		false, 2, 1, 1
+		false, 2, 1, 2
+		false, 2, 2, 1
+		false, 2, 2, 2
+		true, 1, 1, 1
+		true, 1, 1, 2
+		true, 1, 2, 1"#]],
 		);
 	}
 
@@ -378,17 +378,17 @@ mod tests {
 		slv.expect_solutions(
 			&[r, a, b, c],
 			expect![[r#"
-    false, 1, 1, 1
-    false, 1, 1, 2
-    false, 1, 2, 1
-    false, 1, 2, 2
-    false, 2, 1, 1
-    false, 2, 1, 2
-    false, 2, 2, 1
-    false, 2, 2, 2
-    true, 2, 1, 2
-    true, 2, 2, 1
-    true, 2, 2, 2"#]],
+		false, 1, 1, 1
+		false, 1, 1, 2
+		false, 1, 2, 1
+		false, 1, 2, 2
+		false, 2, 1, 1
+		false, 2, 1, 2
+		false, 2, 2, 1
+		false, 2, 2, 2
+		true, 2, 1, 2
+		true, 2, 2, 1
+		true, 2, 2, 2"#]],
 		);
 	}
 }