diff --git a/pumpkin-crates/core/src/api/solver.rs b/pumpkin-crates/core/src/api/solver.rs index b9b4fe57b..95f01a5fe 100644 --- a/pumpkin-crates/core/src/api/solver.rs +++ b/pumpkin-crates/core/src/api/solver.rs @@ -143,8 +143,8 @@ impl Solver { self.satisfaction_solver.get_solution_reference() } - pub(crate) fn is_logging_full_proof(&self) -> bool { - self.satisfaction_solver.is_logging_full_proof() + pub(crate) fn is_logging_proof(&self) -> bool { + self.satisfaction_solver.is_logging_proof() } } diff --git a/pumpkin-crates/core/src/constraints/arithmetic/equality.rs b/pumpkin-crates/core/src/constraints/arithmetic/equality.rs index 9dbe430c1..8ffdddad1 100644 --- a/pumpkin-crates/core/src/constraints/arithmetic/equality.rs +++ b/pumpkin-crates/core/src/constraints/arithmetic/equality.rs @@ -85,7 +85,7 @@ where Var: IntegerVariable + Clone + 'static, { fn post(self, solver: &mut Solver) -> Result<(), ConstraintOperationError> { - if self.terms.len() == 2 && !solver.is_logging_full_proof() { + if self.terms.len() == 2 && !solver.is_logging_proof() { let _ = solver.add_propagator(BinaryEqualsPropagatorArgs { a: self.terms[0].clone(), b: self.terms[1].scaled(-1).offset(self.rhs), @@ -110,7 +110,7 @@ where solver: &mut Solver, reification_literal: Literal, ) -> Result<(), ConstraintOperationError> { - if self.terms.len() == 2 { + if self.terms.len() == 2 && !solver.is_logging_proof() { let _ = solver.add_propagator(ReifiedPropagatorArgs { propagator: BinaryEqualsPropagatorArgs { a: self.terms[0].clone(), diff --git a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs index 5f8c431c1..9d75a5b14 100644 --- a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs +++ b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs @@ -279,8 +279,8 @@ impl ConstraintSatisfactionSolver { finalize_proof(context); } - pub(crate) fn is_logging_full_proof(&self) -> bool { - self.internal_parameters.proof_log.is_logging_inferences() + pub(crate) fn is_logging_proof(&self) -> bool { + self.internal_parameters.proof_log.is_logging_proof() } } diff --git a/pumpkin-crates/core/src/proof/mod.rs b/pumpkin-crates/core/src/proof/mod.rs index 3d9ba7e6f..e0fd40af7 100644 --- a/pumpkin-crates/core/src/proof/mod.rs +++ b/pumpkin-crates/core/src/proof/mod.rs @@ -316,6 +316,10 @@ impl ProofLog { _ => ConstraintTag::create_from_index(0), } } + + pub(crate) fn is_logging_proof(&self) -> bool { + self.internal_proof.is_some() + } } #[derive(Debug)]