From 31ee9e465c5b765fe1ff2ef2c2d633fbde323005 Mon Sep 17 00:00:00 2001 From: Anton Geraschenko Date: Sun, 14 Dec 2025 15:07:07 -0800 Subject: [PATCH 1/2] Fix sign error in greater_than helper `greater_than(terms, rhs)` is implemented as `greater_than_or_equals(terms, rhs - 1)`, but should be `greater_than_or_equals(terms, rhs - 1)`. This is likely a copy-paste error from the implementation of `less_than`. Note: I've added a unit test saying that "x > 0" is not satisfiable for an integer variable x which is required to be 0. This feels like an odd test to have. I'm happy to remove or change it. --- .../src/constraints/arithmetic/inequality.rs | 2 +- pumpkin-solver/tests/solver_test.rs | 16 ++++++++++++++++ 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/pumpkin-crates/core/src/constraints/arithmetic/inequality.rs b/pumpkin-crates/core/src/constraints/arithmetic/inequality.rs index 1c9212381..cce9471d1 100644 --- a/pumpkin-crates/core/src/constraints/arithmetic/inequality.rs +++ b/pumpkin-crates/core/src/constraints/arithmetic/inequality.rs @@ -40,7 +40,7 @@ pub fn greater_than( rhs: i32, constraint_tag: ConstraintTag, ) -> impl NegatableConstraint { - greater_than_or_equals(terms, rhs - 1, constraint_tag) + greater_than_or_equals(terms, rhs + 1, constraint_tag) } /// Create the [`NegatableConstraint`] `\sum terms_i >= rhs`. diff --git a/pumpkin-solver/tests/solver_test.rs b/pumpkin-solver/tests/solver_test.rs index 60165f584..0814899a3 100644 --- a/pumpkin-solver/tests/solver_test.rs +++ b/pumpkin-solver/tests/solver_test.rs @@ -2,6 +2,7 @@ use std::path::PathBuf; +use pumpkin_solver::ConstraintOperationError; use pumpkin_solver::Solver; use pumpkin_solver::constraints; use pumpkin_solver::options::SolverOptions; @@ -63,3 +64,18 @@ fn proof_with_equality_unit_nogood_step() { let result = solver.satisfy(&mut brancher, &mut Indefinite); assert!(matches!(result, SatisfactionResult::Unsatisfiable(_, _))); } + +#[test] +fn greater_than_bug() { + let mut solver = Solver::default(); + + let constraint_tag = solver.new_constraint_tag(); + let x = solver.new_named_bounded_integer(0, 0, "x"); + let gt = solver.add_constraint(constraints::greater_than([x], 0, constraint_tag)); + + match gt.post() { + Err(ConstraintOperationError::InfeasiblePropagator) => {} + Ok(()) => panic!("expected InfeasiblePropagator when posting x > 0 for x fixed to 0"), + Err(e) => panic!("unexpected error: {e:?}"), + } +} From d34df48e1096f20912c4b8f557cfad75cf2e4eac Mon Sep 17 00:00:00 2001 From: Anton Geraschenko Date: Mon, 15 Dec 2025 10:07:30 -0800 Subject: [PATCH 2/2] Move test to inequality.rs. Add the same test for less_than. --- .../src/constraints/arithmetic/inequality.rs | 35 +++++++++++++++++++ pumpkin-solver/tests/solver_test.rs | 16 --------- 2 files changed, 35 insertions(+), 16 deletions(-) diff --git a/pumpkin-crates/core/src/constraints/arithmetic/inequality.rs b/pumpkin-crates/core/src/constraints/arithmetic/inequality.rs index cce9471d1..0de38aa74 100644 --- a/pumpkin-crates/core/src/constraints/arithmetic/inequality.rs +++ b/pumpkin-crates/core/src/constraints/arithmetic/inequality.rs @@ -140,3 +140,38 @@ impl NegatableConstraint for Inequality { } } } + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn less_than_conflict() { + let mut solver = Solver::default(); + + let constraint_tag = solver.new_constraint_tag(); + let x = solver.new_named_bounded_integer(0, 0, "x"); + + let result = less_than([x], 0, constraint_tag).post(&mut solver); + assert_eq!( + result, + Err(ConstraintOperationError::InfeasiblePropagator), + "Expected {result:?} to be an `InfeasiblePropagator` error" + ); + } + + #[test] + fn greater_than_conflict() { + let mut solver = Solver::default(); + + let constraint_tag = solver.new_constraint_tag(); + let x = solver.new_named_bounded_integer(0, 0, "x"); + + let result = greater_than([x], 0, constraint_tag).post(&mut solver); + assert_eq!( + result, + Err(ConstraintOperationError::InfeasiblePropagator), + "Expected {result:?} to be an `InfeasiblePropagator` error" + ); + } +} diff --git a/pumpkin-solver/tests/solver_test.rs b/pumpkin-solver/tests/solver_test.rs index 0814899a3..60165f584 100644 --- a/pumpkin-solver/tests/solver_test.rs +++ b/pumpkin-solver/tests/solver_test.rs @@ -2,7 +2,6 @@ use std::path::PathBuf; -use pumpkin_solver::ConstraintOperationError; use pumpkin_solver::Solver; use pumpkin_solver::constraints; use pumpkin_solver::options::SolverOptions; @@ -64,18 +63,3 @@ fn proof_with_equality_unit_nogood_step() { let result = solver.satisfy(&mut brancher, &mut Indefinite); assert!(matches!(result, SatisfactionResult::Unsatisfiable(_, _))); } - -#[test] -fn greater_than_bug() { - let mut solver = Solver::default(); - - let constraint_tag = solver.new_constraint_tag(); - let x = solver.new_named_bounded_integer(0, 0, "x"); - let gt = solver.add_constraint(constraints::greater_than([x], 0, constraint_tag)); - - match gt.post() { - Err(ConstraintOperationError::InfeasiblePropagator) => {} - Ok(()) => panic!("expected InfeasiblePropagator when posting x > 0 for x fixed to 0"), - Err(e) => panic!("unexpected error: {e:?}"), - } -}