From b448d76ab30c4213353841cc6f6b742eb0a9e065 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Adolfo=20Ochagav=C3=ADa?= Date: Thu, 25 Jan 2024 09:50:20 +0100 Subject: [PATCH] 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 | 53 +++------------------------------- src/solver/mod.rs | 23 ++++++--------- 2 files changed, 13 insertions(+), 63 deletions(-) diff --git a/src/solver/decision_tracker.rs b/src/solver/decision_tracker.rs index 3e6734a..d654834 100644 --- a/src/solver/decision_tracker.rs +++ b/src/solver/decision_tracker.rs @@ -10,11 +10,6 @@ pub(crate) struct DecisionTracker { map: DecisionMap, stack: Vec, propagate_index: usize, - - // Fixed assignments are decisions that are true regardless of previous decisions. These - // assignments are not cleared after backtracked. - fixed_assignments: Vec, - fixed_assignment_index: usize, } impl DecisionTracker { @@ -23,8 +18,6 @@ impl DecisionTracker { map: DecisionMap::new(), stack: Vec::new(), propagate_index: 0, - fixed_assignment_index: 0, - fixed_assignments: Vec::new(), } } @@ -32,15 +25,6 @@ impl DecisionTracker { 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 + 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 { - 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 { - 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) } } diff --git a/src/solver/mod.rs b/src/solver/mod.rs index 66e9cbe..16b3a75 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -293,9 +293,8 @@ impl> 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> 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> 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);