chore: use negative assertions instead of fixed assignments

In previous commits we replaced some usages of fixed assignments. The
only remaining usage was for excluded packages, but since excluded
packages are basically negative assertions, we can reuse the (IMO
simpler) negative assertion system. As a bonus, we get a reduction in
LOC.

Author: aochagavia

src/solver/decision_tracker.rs

@@ -10,11 +10,6 @@ pub(crate) struct DecisionTracker {
     map: DecisionMap,
     stack: Vec<Decision>,
     propagate_index: usize,
-
-    // Fixed assignments are decisions that are true regardless of previous decisions. These
-    // assignments are not cleared after backtracked.
-    fixed_assignments: Vec<Decision>,
-    fixed_assignment_index: usize,
 }
 
 impl DecisionTracker {
@@ -23,24 +18,13 @@ impl DecisionTracker {
             map: DecisionMap::new(),
             stack: Vec::new(),
             propagate_index: 0,
-            fixed_assignment_index: 0,
-            fixed_assignments: Vec::new(),
         }
     }
 
     pub(crate) fn clear(&mut self) {
         self.map = DecisionMap::new();
         self.stack = Vec::new();
         self.propagate_index = 0;
-
-        // The fixed assignment decisions are kept but the propagation index is. This assures that
-        // during the next propagation all fixed assignment decisions are repropagated.
-        self.fixed_assignment_index = 0;
-
-        // Re-apply all the fixed decisions
-        for decision in self.fixed_assignments.iter() {
-            self.map.set(decision.solvable_id, decision.value, 1);
-        }
     }
 
     pub(crate) fn is_empty(&self) -> bool {
@@ -56,10 +40,7 @@ impl DecisionTracker {
     }
 
     pub(crate) fn stack(&self) -> impl Iterator<Item = Decision> + DoubleEndedIterator + '_ {
-        self.fixed_assignments
-            .iter()
-            .copied()
-            .chain(self.stack.iter().copied())
+        self.stack.iter().copied()
     }
 
     pub(crate) fn level(&self, solvable_id: SolvableId) -> u32 {
@@ -92,26 +73,6 @@ impl DecisionTracker {
         }
     }
 
-    /// Attempts to add a fixed assignment decision. A fixed assignment is different from a regular
-    /// decision in that its value is persistent and cannot be reverted by backtracking. This is
-    /// useful for assertion clauses.
-    ///
-    /// Returns true if the solvable was undecided, false if it was already decided to the same
-    /// value.
-    ///
-    /// Returns an error if the solvable was decided to a different value (which means there is a conflict)
-    pub(crate) fn try_add_fixed_assignment(&mut self, decision: Decision) -> Result<bool, ()> {
-        match self.map.value(decision.solvable_id) {
-            None => {
-                self.map.set(decision.solvable_id, decision.value, 1);
-                self.fixed_assignments.push(decision);
-                Ok(true)
-            }
-            Some(value) if value == decision.value => Ok(false),
-            _ => Err(()),
-        }
-    }
-
     pub(crate) fn undo_until(&mut self, level: u32) {
         while let Some(decision) = self.stack.last() {
             if self.level(decision.solvable_id) <= level {
@@ -136,14 +97,8 @@ impl DecisionTracker {
     ///
     /// Side-effect: the decision will be marked as propagated
     pub(crate) fn next_unpropagated(&mut self) -> Option<Decision> {
-        if self.fixed_assignment_index < self.fixed_assignments.len() {
-            let &decision = &self.fixed_assignments[self.fixed_assignment_index];
-            self.fixed_assignment_index += 1;
-            Some(decision)
-        } else {
-            let &decision = self.stack[self.propagate_index..].iter().next()?;
-            self.propagate_index += 1;
-            Some(decision)
-        }
+        let &decision = self.stack[self.propagate_index..].iter().next()?;
+        self.propagate_index += 1;
+        Some(decision)
     }
 }

src/solver/mod.rs

@@ -293,9 +293,8 @@ impl<VS: VersionSet, N: PackageName + Display, D: DependencyProvider<VS, N>> Sol
                     .alloc(ClauseState::forbid_multiple(candidate, other_candidate));
 
                 let clause = &mut self.clauses[clause_id];
-                if clause.has_watches() {
-                    self.watches.start_watching(clause, clause_id);
-                }
+                debug_assert!(clause.has_watches());
+                self.watches.start_watching(clause, clause_id);
             }
         }
 
@@ -308,9 +307,9 @@ impl<VS: VersionSet, N: PackageName + Display, D: DependencyProvider<VS, N>> Sol
                         .alloc(ClauseState::lock(locked_solvable_id, other_candidate));
 
                     let clause = &mut self.clauses[clause_id];
-                    if clause.has_watches() {
-                        self.watches.start_watching(clause, clause_id);
-                    }
+
+                    debug_assert!(clause.has_watches());
+                    self.watches.start_watching(clause, clause_id);
                 }
             }
         }
@@ -319,15 +318,11 @@ impl<VS: VersionSet, N: PackageName + Display, D: DependencyProvider<VS, N>> Sol
         for (solvable, reason) in package_candidates.excluded.iter().copied() {
             let clause_id = self.clauses.alloc(ClauseState::exclude(solvable, reason));
 
-            // Immediately add the decision to unselect this solvable. This should be fine because
-            // no other decision should have been made about this solvable in the first place.
-            let exclude_descision = Decision::new(solvable, false, clause_id);
-            self.decision_tracker
-                .try_add_fixed_assignment(exclude_descision)
-                .expect("already decided about a solvable that wasn't properly added yet.");
+            // Exclusions are negative assertions, tracked outside of the watcher system
+            self.negative_assertions.push((solvable, clause_id));
 
-            // No need to add watches for this clause because the clause is an assertion on which
-            // we already decided.
+            // Conflicts should be impossible here
+            debug_assert!(self.decision_tracker.assigned_value(solvable) != Some(true));
         }
 
         self.clauses_added_for_package.insert(package_name);