fix: give reason to root-level propagation in nogood propagator (#124)

When preprocessing a nogood, if it becomes a unit nogood, the propagator
would assign the negation of the predicate with an empty reason.
However, from the perspective of the proof log, that is invalid as the
input to the propagator was a non-unit nogood.

Author: maartenflippo

pumpkin-solver/src/propagators/nogoods/nogood_propagator.rs

@@ -10,7 +10,6 @@ use crate::basic_types::moving_averages::MovingAverage;
 use crate::basic_types::ConstraintOperationError;
 use crate::basic_types::Inconsistency;
 use crate::basic_types::PropositionalConjunction;
-use crate::conjunction;
 use crate::containers::KeyedVec;
 use crate::engine::conflict_analysis::Mode;
 use crate::engine::nogoods::Lbd;
@@ -1001,6 +1000,11 @@ impl NogoodPropagator {
             return Ok(());
         }
 
+        // After preprocessing the nogood may propagate. If that happens, there is no reason for
+        // the propagation which breaks the proof logging. Therefore, we keep the original nogood
+        // here so we can construct a reason for the propagation later.
+        let mut input_nogood = nogood.clone();
+
         // Then we pre-process the nogood such that (among others) it does not contain duplicates
         Self::preprocess_nogood(&mut nogood, context);
 
@@ -1015,8 +1019,12 @@ impl NogoodPropagator {
                 // return success
                 Ok(())
             } else {
+                // Get the reason for the propagation.
+                input_nogood.retain(|&p| p != nogood[0]);
+
                 // Post the negated predicate at the root to respect the nogood.
-                let result = context.post_predicate(!nogood[0], conjunction!());
+                let result = context
+                    .post_predicate(!nogood[0], PropositionalConjunction::from(input_nogood));
                 match result {
                     Ok(_) => Ok(()),
                     Err(_) => {