Remove fixed assignments (#16)

Note for reviewers: this PR assumes that #15 has been merged. Ideally,
I'd take my `fix-nested-deps-issue` branch as a base, but then the PR
would end up being created in my own repository. Fortunately the whole
code is in a single commit, so you can have a look at the last commit's
diff (or wait till #15 is merged).

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);