fix logging more root level unit thingies

Author: maartenflippo

pumpkin-solver/src/engine/conflict_analysis/conflict_analysis_context.rs

@@ -27,10 +27,10 @@ use crate::variables::DomainId;
 /// Used during conflict analysis to provide the necessary information.
 ///
 /// All fields are made public for the time being for simplicity. In the future that may change.
-pub(crate) struct ConflictAnalysisContext<'a> {
+pub(crate) struct ConflictAnalysisContext<'a, 'reasons> {
     pub(crate) assignments: &'a mut Assignments,
     pub(crate) solver_state: &'a mut CSPSolverState,
-    pub(crate) reason_store: &'a mut ReasonStore,
+    pub(crate) reason_store: &'reasons mut ReasonStore,
     pub(crate) brancher: &'a mut dyn Brancher,
     pub(crate) propagators: &'a mut PropagatorStore,
     pub(crate) semantic_minimiser: &'a mut SemanticMinimiser,
@@ -50,13 +50,13 @@ pub(crate) struct ConflictAnalysisContext<'a> {
     pub(crate) unit_nogood_step_ids: &'a HashMap<Predicate, StepId>,
 }
 
-impl Debug for ConflictAnalysisContext<'_> {
+impl Debug for ConflictAnalysisContext<'_, '_> {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         f.debug_struct(std::any::type_name::<Self>()).finish()
     }
 }
 
-impl<'a> ConflictAnalysisContext<'a> {
+impl<'reasons> ConflictAnalysisContext<'_, 'reasons> {
     /// Returns the last decision which was made by the solver.
     pub(crate) fn find_last_decision(&mut self) -> Option<Predicate> {
         self.assignments.find_last_decision()
@@ -133,11 +133,11 @@ impl<'a> ConflictAnalysisContext<'a> {
         predicate: Predicate,
         assignments: &Assignments,
         current_nogood: CurrentNogood<'_>,
-        reason_store: &'a mut ReasonStore,
-        propagators: &'a mut PropagatorStore,
-        proof_log: &'a mut ProofLog,
+        reason_store: &'reasons mut ReasonStore,
+        propagators: &'reasons mut PropagatorStore,
+        proof_log: &mut ProofLog,
         unit_nogood_step_ids: &HashMap<Predicate, StepId>,
-    ) -> &'a [Predicate] {
+    ) -> &'reasons [Predicate] {
         // TODO: this function could be put into the reason store
 
         // Note that this function can only be called with propagations, and never decision

pumpkin-solver/src/engine/conflict_analysis/resolvers/resolution_resolver.rs

@@ -1,5 +1,8 @@
+use std::num::NonZero;
+
 use super::ConflictResolver;
 use crate::basic_types::moving_averages::MovingAverage;
+use crate::basic_types::HashMap;
 use crate::basic_types::PredicateId;
 use crate::basic_types::PredicateIdGenerator;
 use crate::branching::Brancher;
@@ -12,6 +15,7 @@ use crate::engine::conflict_analysis::LearnedNogood;
 use crate::engine::propagation::CurrentNogood;
 use crate::engine::Assignments;
 use crate::predicates::Predicate;
+use crate::proof::ProofLog;
 use crate::pumpkin_assert_advanced;
 use crate::pumpkin_assert_moderate;
 use crate::pumpkin_assert_simple;
@@ -75,6 +79,8 @@ impl ConflictResolver for ResolutionResolver {
             self.add_predicate_to_conflict_nogood(
                 *predicate,
                 context.assignments,
+                context.proof_log,
+                context.unit_nogood_step_ids,
                 context.brancher,
                 self.mode,
                 context.is_completing_proof,
@@ -244,6 +250,8 @@ impl ConflictResolver for ResolutionResolver {
                 self.add_predicate_to_conflict_nogood(
                     *predicate,
                     context.assignments,
+                    context.proof_log,
+                    context.unit_nogood_step_ids,
                     context.brancher,
                     self.mode,
                     context.is_completing_proof,
@@ -273,13 +281,19 @@ impl ResolutionResolver {
         self.to_process_heap.clear();
     }
 
+    #[allow(
+        clippy::too_many_arguments,
+        reason = "borrow checker complains if passing through the context"
+    )]
     fn add_predicate_to_conflict_nogood(
         &mut self,
         predicate: Predicate,
         assignments: &Assignments,
+        proof_log: &mut ProofLog,
+        unit_nogood_step_ids: &HashMap<Predicate, NonZero<u64>>,
         brancher: &mut dyn Brancher,
         mode: AnalysisMode,
-        is_logging_complete_proof: bool,
+        is_completing_proof: bool,
     ) {
         let dec_level = assignments
             .get_decision_level_for_predicate(&predicate)
@@ -290,18 +304,34 @@ impl ResolutionResolver {
                     assignments.get_upper_bound(predicate.get_domain()),
                 )
             });
-        // Ignore root level predicates.
-        if !is_logging_complete_proof && dec_level == 0 {
-            // do nothing
+
+        // Log all non-initial bounds to the proof.
+        if dec_level == 0 && !is_completing_proof {
+            if !assignments.is_initial_bound(predicate) {
+                let trail_index = assignments
+                    .get_trail_position(&predicate)
+                    .expect("all predicates in reason are true");
+                let trail_entry = assignments.get_trail_entry(trail_index);
+
+                // We do indicate their usage in the proof.
+                let step_id = unit_nogood_step_ids
+                    .get(&trail_entry.predicate)
+                    .copied()
+                    .unwrap();
+                proof_log.add_propagation(step_id);
+            }
+
+            return;
         }
+
         // 1UIP
         // If the variables are from the current decision level then we want to potentially add
         // them to the heap, otherwise we add it to the predicates from lower-decision levels
         //
         // All-decision Learning
         // If the variables are not decisions then we want to potentially add them to the heap,
         // otherwise we add it to the decision predicates which have been discovered previously
-        else if match mode {
+        if match mode {
             AnalysisMode::OneUIP => dec_level == assignments.get_decision_level(),
             AnalysisMode::AllDecision => !assignments.is_decision_predicate(&predicate),
         } {

pumpkin-solver/src/engine/constraint_satisfaction_solver.rs

@@ -386,7 +386,8 @@ impl ConstraintSatisfactionSolver {
                 .iter()
                 .copied()
                 .all(Predicate::is_trivially_true),
-            "At the root, conflict analysis should result in a trivial conflict"
+            "At the root, conflict analysis should result in a trivial conflict: {:?}",
+            result.predicates,
         );
 
         let _ = self