From a6b855c5fe0a25bcd23163d5d4d5ee4b7c8be64c Mon Sep 17 00:00:00 2001 From: Bas Zalmstra Date: Mon, 25 Sep 2023 14:12:21 +0200 Subject: [PATCH] refactor: hybrid incremental solver and performance improvements (#349) This is a big PR that does two things: **Incremental solver** The solver is now incremental by default. This means that the solver will only request information from the `DependencyProvider` when it is relatively sure that that information is needed to come up with a solution. Previously the solver would greedily request all information about the problem space up front. This made the solver very unsuitable for cases where requesting information about packages is expensive. Optionally a `DependencyProvider` has the ability to hint to the solver that it already has dependency information available for some candidates. The solver will use this information to increase its knowledge of the problem space without requiring network operations. The latter is used for the conda solver. In general, it's better to have all the information available upfront because if the solver has "all" the information available it is able to reach a solution quicker because it doesn't have to guess about information it doesn't know. **Performance improvements** This PR also implements a performance improvement by being more thoughtful about making decisions about the next steps to take in the algorithm. Instead of picking the first available decision it can make it checks all possible choices to make and picks the decision that involves the least amount of versions to pick. This is similar to what pubgrub does: https://github.com/dart-lang/pub/blob/master/doc/solver.md#decision-making In the future, we might take a look at different heuristics but this implementation is good enough for now. Some results: | | libsolv | libsolv-rs 0.7.0 | libsolv-rs (this) | |------------------------------------|---------|------------|--------------| | python=3.9 | 7.03ms | **3.47ms** | 3.57ms | | xtensor, xsimd | 5.28ms | **2.00ms** | 2.22ms | | tensorflow | 773.27ms | 407.98ms | **152.94ms** | | quetz | 1380.8ms | 1684.7ms | **301.53ms** | | tensorboard=2.1.1, grpc-cpp=1.39.1 | 515.25ms | 122.48ms | **89.41ms** | Note that for "simple" cases this PR is slower but just slightly and for "complex" cases this PR is _much_ faster. --------- Co-authored-by: Tim de Jager --- Cargo.toml | 1 + src/internal/arena.rs | 2 + src/lib.rs | 24 +- src/problem.rs | 2 +- src/solver/cache.rs | 227 +++++ src/solver/clause.rs | 5 +- src/solver/decision_map.rs | 35 + src/solver/decision_tracker.rs | 69 +- src/solver/mod.rs | 940 ++++++++++-------- ...v_rs__solver__test__incremental_crash.snap | 8 + ...olv_rs__solver__test__no_backtracking.snap | 3 +- ...__solver__test__resolve_with_conflict.snap | 5 +- 12 files changed, 865 insertions(+), 456 deletions(-) create mode 100644 src/solver/cache.rs create mode 100644 src/solver/snapshots/rattler_libsolv_rs__solver__test__incremental_crash.snap diff --git a/Cargo.toml b/Cargo.toml index 2d4e53c..12f4c54 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -15,6 +15,7 @@ itertools = "0.11.0" petgraph = "0.6.4" tracing = "0.1.37" elsa = "1.9.0" +bitvec = "1.0.1" serde = { version = "1.0", features = ["derive"], optional = true } [dev-dependencies] diff --git a/src/internal/arena.rs b/src/internal/arena.rs index c1b4f2a..b19f87f 100644 --- a/src/internal/arena.rs +++ b/src/internal/arena.rs @@ -1,3 +1,5 @@ +#![allow(unused)] + use std::cell::{Cell, UnsafeCell}; use std::cmp; use std::marker::PhantomData; diff --git a/src/lib.rs b/src/lib.rs index b9af7d4..6d1131a 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -17,16 +17,19 @@ mod solvable; mod solver; use itertools::Itertools; + +pub use internal::{ + id::{NameId, SolvableId, VersionSetId}, + mapping::Mapping, +}; +pub use pool::Pool; +pub use solvable::Solvable; +pub use solver::{Solver, SolverCache}; use std::{ fmt::{Debug, Display}, hash::Hash, }; -pub use internal::id::{NameId, SolvableId, VersionSetId}; -pub use pool::Pool; -pub use solvable::Solvable; -pub use solver::Solver; - /// The solver is based around the fact that for for every package name we are trying to find a /// single variant. Variants are grouped by their respective package name. A package name is /// anything that we can compare and hash for uniqueness checks. @@ -60,7 +63,7 @@ pub trait DependencyProvider: Sized { /// Sort the specified solvables based on which solvable to try first. The solver will /// iteratively try to select the highest version. If a conflict is found with the highest /// version the next version is tried. This continues until a solution is found. - fn sort_candidates(&self, solver: &Solver, solvables: &mut [SolvableId]); + fn sort_candidates(&self, solver: &SolverCache, solvables: &mut [SolvableId]); /// Returns a list of solvables that should be considered when a package with the given name is /// requested. @@ -92,6 +95,15 @@ pub struct Candidates { /// also be possible to simply return a single candidate using this field provides better error /// messages to the user. pub locked: Option, + + /// A hint to the solver that the dependencies of some of the solvables are also directly + /// available. This allows the solver to request the dependencies of these solvables + /// immediately. Having the dependency information available might make the solver much faster + /// because it has more information available up-front which provides the solver with a more + /// complete picture of the entire problem space. However, it might also be the case that the + /// solver doesnt actually need this information to form a solution. In general though, if the + /// dependencies can easily be provided one should provide them up-front. + pub hint_dependencies_available: Vec, } /// Holds information about the dependencies of a package. diff --git a/src/problem.rs b/src/problem.rs index 7fa568c..f7c3acc 100644 --- a/src/problem.rs +++ b/src/problem.rs @@ -58,7 +58,7 @@ impl Problem { &Clause::Requires(package_id, version_set_id) => { let package_node = Self::add_node(&mut graph, &mut nodes, package_id); - let candidates = solver.get_or_cache_sorted_candidates(version_set_id); + let candidates = solver.cache.get_or_cache_sorted_candidates(version_set_id); if candidates.is_empty() { tracing::info!( "{package_id:?} requires {version_set_id:?}, which has no candidates" diff --git a/src/solver/cache.rs b/src/solver/cache.rs new file mode 100644 index 0000000..721c341 --- /dev/null +++ b/src/solver/cache.rs @@ -0,0 +1,227 @@ +use crate::internal::arena::ArenaId; +use crate::{ + internal::{ + arena::Arena, + frozen_copy_map::FrozenCopyMap, + id::{CandidatesId, DependenciesId}, + }, + Candidates, Dependencies, DependencyProvider, NameId, PackageName, Pool, SolvableId, + VersionSet, VersionSetId, +}; +use bitvec::vec::BitVec; +use elsa::FrozenMap; +use std::cell::RefCell; +use std::marker::PhantomData; + +/// Keeps a cache of previously computed and/or requested information about solvables and version +/// sets. +pub struct SolverCache> { + provider: D, + + /// A mapping from package name to a list of candidates. + candidates: Arena, + package_name_to_candidates: FrozenCopyMap, + + /// A mapping of `VersionSetId` to the candidates that match that set. + version_set_candidates: FrozenMap>, + + /// A mapping of `VersionSetId` to the candidates that do not match that set (only candidates + /// of the package indicated by the version set are included). + version_set_inverse_candidates: FrozenMap>, + + /// A mapping of `VersionSetId` to a sorted list of candidates that match that set. + pub(crate) version_set_to_sorted_candidates: FrozenMap>, + + /// A mapping from a solvable to a list of dependencies + solvable_dependencies: Arena, + solvable_to_dependencies: FrozenCopyMap, + + /// A mapping that indicates that the dependencies for a particular solvable can cheaply be + /// retrieved from the dependency provider. This information is provided by the + /// DependencyProvider when the candidates for a package are requested. + hint_dependencies_available: RefCell, + + _data: PhantomData<(VS, N)>, +} + +impl> SolverCache { + /// Constructs a new instance from a provider. + pub fn new(provider: D) -> Self { + Self { + provider, + + candidates: Default::default(), + package_name_to_candidates: Default::default(), + version_set_candidates: Default::default(), + version_set_inverse_candidates: Default::default(), + version_set_to_sorted_candidates: Default::default(), + solvable_dependencies: Default::default(), + solvable_to_dependencies: Default::default(), + hint_dependencies_available: Default::default(), + + _data: Default::default(), + } + } + + /// Returns a reference to the pool used by the solver + pub fn pool(&self) -> &Pool { + self.provider.pool() + } + + /// Returns the candidates for the package with the given name. This will either ask the + /// [`DependencyProvider`] for the entries or a cached value. + pub fn get_or_cache_candidates(&self, package_name: NameId) -> &Candidates { + // If we already have the candidates for this package cached we can simply return + let candidates_id = match self.package_name_to_candidates.get_copy(&package_name) { + Some(id) => id, + None => { + // Otherwise we have to get them from the DependencyProvider + let candidates = self + .provider + .get_candidates(package_name) + .unwrap_or_default(); + + // Store information about which solvables dependency information is easy to + // retrieve. + { + let mut hint_dependencies_available = + self.hint_dependencies_available.borrow_mut(); + for hint_candidate in candidates.hint_dependencies_available.iter() { + let idx = hint_candidate.to_usize(); + if hint_dependencies_available.len() <= idx { + hint_dependencies_available.resize(idx + 1, false); + } + hint_dependencies_available.set(idx, true) + } + } + + // Allocate an ID so we can refer to the candidates from everywhere + let candidates_id = self.candidates.alloc(candidates); + self.package_name_to_candidates + .insert_copy(package_name, candidates_id); + + candidates_id + } + }; + + // Returns a reference from the arena + &self.candidates[candidates_id] + } + + /// Returns the candidates of a package that match the specified version set. + pub fn get_or_cache_matching_candidates(&self, version_set_id: VersionSetId) -> &[SolvableId] { + match self.version_set_candidates.get(&version_set_id) { + Some(candidates) => candidates, + None => { + let package_name = self.pool().resolve_version_set_package_name(version_set_id); + let version_set = self.pool().resolve_version_set(version_set_id); + let candidates = self.get_or_cache_candidates(package_name); + + let matching_candidates = candidates + .candidates + .iter() + .copied() + .filter(|&p| { + let version = self.pool().resolve_internal_solvable(p).solvable().inner(); + version_set.contains(version) + }) + .collect(); + + self.version_set_candidates + .insert(version_set_id, matching_candidates) + } + } + } + + /// Returns the candidates that do *not* match the specified requirement. + pub fn get_or_cache_non_matching_candidates( + &self, + version_set_id: VersionSetId, + ) -> &[SolvableId] { + match self.version_set_inverse_candidates.get(&version_set_id) { + Some(candidates) => candidates, + None => { + let package_name = self.pool().resolve_version_set_package_name(version_set_id); + let version_set = self.pool().resolve_version_set(version_set_id); + let candidates = self.get_or_cache_candidates(package_name); + + let matching_candidates = candidates + .candidates + .iter() + .copied() + .filter(|&p| { + let version = self.pool().resolve_internal_solvable(p).solvable().inner(); + !version_set.contains(version) + }) + .collect(); + + self.version_set_inverse_candidates + .insert(version_set_id, matching_candidates) + } + } + } + + /// Returns the candidates for the package with the given name similar to + /// [`Self::get_or_cache_candidates`] sorted from highest to lowest. + pub fn get_or_cache_sorted_candidates(&self, version_set_id: VersionSetId) -> &[SolvableId] { + match self.version_set_to_sorted_candidates.get(&version_set_id) { + Some(canidates) => canidates, + None => { + let package_name = self.pool().resolve_version_set_package_name(version_set_id); + let matching_candidates = self.get_or_cache_matching_candidates(version_set_id); + let candidates = self.get_or_cache_candidates(package_name); + + // Sort all the candidates in order in which they should betried by the solver. + let mut sorted_candidates = Vec::new(); + sorted_candidates.extend_from_slice(matching_candidates); + self.provider.sort_candidates(self, &mut sorted_candidates); + + // If we have a solvable that we favor, we sort that to the front. This ensures + // that the version that is favored is picked first. + if let Some(favored_id) = candidates.favored { + if let Some(pos) = sorted_candidates.iter().position(|&s| s == favored_id) { + // Move the element at `pos` to the front of the array + sorted_candidates[0..=pos].rotate_right(1); + } + } + + self.version_set_to_sorted_candidates + .insert(version_set_id, sorted_candidates) + } + } + } + + /// Returns the dependencies of a solvable. Requests the solvables from the + /// [`DependencyProvider`] if they are not known yet. + pub fn get_or_cache_dependencies(&self, solvable_id: SolvableId) -> &Dependencies { + let dependencies_id = match self.solvable_to_dependencies.get_copy(&solvable_id) { + Some(id) => id, + None => { + let dependencies = self.provider.get_dependencies(solvable_id); + let dependencies_id = self.solvable_dependencies.alloc(dependencies); + self.solvable_to_dependencies + .insert_copy(solvable_id, dependencies_id); + dependencies_id + } + }; + + &self.solvable_dependencies[dependencies_id] + } + + /// Returns true if the dependencies for the given solvable are "cheaply" available. This means + /// either the dependency provider indicated that the dependencies for a solvable are available + /// or the dependencies have already been requested. + pub fn are_dependencies_available_for(&self, solvable: SolvableId) -> bool { + if self.solvable_to_dependencies.get_copy(&solvable).is_some() { + true + } else { + let solvable_idx = solvable.to_usize(); + let hint_dependencies_available = self.hint_dependencies_available.borrow(); + let value = hint_dependencies_available + .get(solvable_idx) + .as_deref() + .copied(); + value.unwrap_or(false) + } + } +} diff --git a/src/solver/clause.rs b/src/solver/clause.rs index 2569f1e..f39a232 100644 --- a/src/solver/clause.rs +++ b/src/solver/clause.rs @@ -491,8 +491,11 @@ impl Debug for ClauseDebug<'_, VS, N> let match_spec = self.pool.resolve_version_set(match_spec_id).to_string(); write!( f, - "{} requires {match_spec}", + "{} requires {} {match_spec}", solvable_id.display(self.pool), + self.pool + .resolve_version_set_package_name(match_spec_id) + .display(self.pool) ) } Clause::Constrains(s1, s2, vset_id) => { diff --git a/src/solver/decision_map.rs b/src/solver/decision_map.rs index 6b97006..dc3eb22 100644 --- a/src/solver/decision_map.rs +++ b/src/solver/decision_map.rs @@ -1,5 +1,7 @@ use crate::internal::{arena::ArenaId, id::SolvableId}; +use crate::{PackageName, Pool, VersionSet}; use std::cmp::Ordering; +use std::fmt::{Display, Formatter}; /// Represents a decision (i.e. an assignment to a solvable) and the level at which it was made /// @@ -75,4 +77,37 @@ impl DecisionMap { pub fn value(&self, solvable_id: SolvableId) -> Option { self.map.get(solvable_id.to_usize()).and_then(|d| d.value()) } + + /// Returns an object that can be used to display the contents of the decision map in a human readable fashion. + #[allow(unused)] + pub fn display<'a, VS: VersionSet, N: PackageName + Display>( + &'a self, + pool: &'a Pool, + ) -> DecisionMapDisplay<'a, VS, N> { + DecisionMapDisplay { map: self, pool } + } +} + +pub struct DecisionMapDisplay<'a, VS: VersionSet, N: PackageName + Display> { + map: &'a DecisionMap, + pool: &'a Pool, +} + +impl<'a, VS: VersionSet, N: PackageName + Display> Display for DecisionMapDisplay<'a, VS, N> { + fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { + for (id, solvable) in self.pool.solvables.iter() { + write!(f, "{} := ", solvable.display(self.pool))?; + if let Some(value) = self.map.value(id) { + writeln!( + f, + "{} (level: {})", + if value { "true " } else { "false" }, + self.map.level(id) + )?; + } else { + writeln!(f, "")?; + } + } + Ok(()) + } } diff --git a/src/solver/decision_tracker.rs b/src/solver/decision_tracker.rs index 729009e..3e6734a 100644 --- a/src/solver/decision_tracker.rs +++ b/src/solver/decision_tracker.rs @@ -1,3 +1,4 @@ +use crate::internal::id::ClauseId; use crate::{ internal::id::SolvableId, solver::{decision::Decision, decision_map::DecisionMap}, @@ -9,6 +10,11 @@ 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 { @@ -17,11 +23,24 @@ 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 = Self::new(); + 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 { @@ -36,14 +55,26 @@ impl DecisionTracker { &self.map } - pub(crate) fn stack(&self) -> &[Decision] { - &self.stack + pub(crate) fn stack(&self) -> impl Iterator + DoubleEndedIterator + '_ { + self.fixed_assignments + .iter() + .copied() + .chain(self.stack.iter().copied()) } pub(crate) fn level(&self, solvable_id: SolvableId) -> u32 { self.map.level(solvable_id) } + // Find the clause that caused the assignment of the specified solvable. If no assignment has + // been made to the solvable than `None` is returned. + pub(crate) fn find_clause_for_assignment(&self, solvable_id: SolvableId) -> Option { + self.stack + .iter() + .find(|d| d.solvable_id == solvable_id) + .map(|d| d.derived_from) + } + /// Attempts to add a decision /// /// Returns true if the solvable was undecided, false if it was already decided to the same value @@ -61,6 +92,26 @@ 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 { @@ -85,8 +136,14 @@ impl DecisionTracker { /// /// Side-effect: the decision will be marked as propagated pub(crate) fn next_unpropagated(&mut self) -> Option { - let &decision = self.stack[self.propagate_index..].iter().next()?; - self.propagate_index += 1; - Some(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) + } } } diff --git a/src/solver/mod.rs b/src/solver/mod.rs index e4338c0..3950679 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -1,24 +1,27 @@ use crate::{ internal::{ - arena::{Arena, ArenaId}, - frozen_copy_map::FrozenCopyMap, - id::{CandidatesId, ClauseId, DependenciesId, LearntClauseId, NameId, SolvableId}, + arena::Arena, + id::{ClauseId, LearntClauseId, NameId, SolvableId}, mapping::Mapping, }, pool::Pool, problem::Problem, solvable::SolvableInner, - Candidates, Dependencies, DependencyProvider, PackageName, VersionSet, VersionSetId, + DependencyProvider, PackageName, VersionSet, VersionSetId, }; +use std::collections::HashSet; +use std::fmt::Display; +use std::ops::ControlFlow; -use elsa::{FrozenMap, FrozenVec}; -use std::{collections::HashSet, fmt::Display, marker::PhantomData}; +use itertools::Itertools; +pub use cache::SolverCache; use clause::{Clause, ClauseState, Literal}; use decision::Decision; use decision_tracker::DecisionTracker; use watch_map::WatchMap; +mod cache; pub(crate) mod clause; mod decision; mod decision_map; @@ -27,202 +30,48 @@ mod watch_map; /// Drives the SAT solving process pub struct Solver> { - provider: D, + pub(crate) cache: SolverCache, pub(crate) clauses: Arena, + requires_clauses: Vec<(SolvableId, VersionSetId, ClauseId)>, watches: WatchMap, learnt_clauses: Arena>, learnt_why: Mapping>, learnt_clause_ids: Vec, - /// A mapping from a solvable to a list of dependencies - solvable_dependencies: Arena, - solvable_to_dependencies: FrozenCopyMap, - - /// A mapping from package name to a list of candidates. - candidates: Arena, - package_name_to_candidates: FrozenCopyMap, - - // HACK: Since we are not allowed to iterate over the `package_name_to_candidates` field, we - // store the keys in a seperate vec. - package_names: FrozenVec, - - /// A mapping of `VersionSetId` to the candidates that match that set. - version_set_candidates: FrozenMap>, - - /// A mapping of `VersionSetId` to the candidates that do not match that set. - version_set_inverse_candidates: FrozenMap>, - - /// A mapping of `VersionSetId` to a sorted list of canidates that match that set. - version_set_to_sorted_candidates: FrozenMap>, + clauses_added_for_package: HashSet, + clauses_added_for_solvable: HashSet, decision_tracker: DecisionTracker, /// The version sets that must be installed as part of the solution. root_requirements: Vec, - - _data: PhantomData<(VS, N)>, } -impl> Solver { +impl> Solver { /// Create a solver, using the provided pool pub fn new(provider: D) -> Self { Self { - provider, + cache: SolverCache::new(provider), clauses: Arena::new(), + requires_clauses: Default::default(), watches: WatchMap::new(), learnt_clauses: Arena::new(), learnt_why: Mapping::new(), learnt_clause_ids: Vec::new(), decision_tracker: DecisionTracker::new(), - candidates: Arena::new(), - solvable_dependencies: Default::default(), - solvable_to_dependencies: Default::default(), - package_name_to_candidates: Default::default(), - package_names: Default::default(), root_requirements: Default::default(), - version_set_candidates: Default::default(), - version_set_inverse_candidates: Default::default(), - version_set_to_sorted_candidates: Default::default(), - _data: Default::default(), + clauses_added_for_package: Default::default(), + clauses_added_for_solvable: Default::default(), } } /// Returns a reference to the pool used by the solver pub fn pool(&self) -> &Pool { - self.provider.pool() - } - - /// Returns the candidates for the package with the given name. This will either ask the - /// [`DependencyProvider`] for the entries or a cached value. - pub fn get_or_cache_candidates(&self, package_name: NameId) -> &Candidates { - // If we already have the candidates for this package cached we can simply return - let candidates_id = match self.package_name_to_candidates.get_copy(&package_name) { - Some(id) => id, - None => { - // Otherwise we have to get them from the DependencyProvider - let candidates = self - .provider - .get_candidates(package_name) - .unwrap_or_default(); - - // Allocate an ID so we can refer to the candidates from everywhere - let candidates_id = self.candidates.alloc(candidates); - self.package_name_to_candidates - .insert_copy(package_name, candidates_id); - self.package_names.push(package_name); - - candidates_id - } - }; - - // Returns a reference from the arena - &self.candidates[candidates_id] - } - - /// Returns the candidates of a package that match the specified version set. - pub fn get_or_cache_matching_candidates(&self, version_set_id: VersionSetId) -> &[SolvableId] { - match self.version_set_candidates.get(&version_set_id) { - Some(candidates) => candidates, - None => { - let package_name = self.pool().resolve_version_set_package_name(version_set_id); - let version_set = self.pool().resolve_version_set(version_set_id); - let candidates = self.get_or_cache_candidates(package_name); - - let matching_candidates = candidates - .candidates - .iter() - .copied() - .filter(|&p| { - let version = self.pool().resolve_internal_solvable(p).solvable().inner(); - version_set.contains(version) - }) - .collect(); - - self.version_set_candidates - .insert(version_set_id, matching_candidates) - } - } - } - - /// Returns the candidates that do *not* match the specified requirement. - pub fn get_or_cache_non_matching_candidates( - &self, - version_set_id: VersionSetId, - ) -> &[SolvableId] { - match self.version_set_inverse_candidates.get(&version_set_id) { - Some(candidates) => candidates, - None => { - let package_name = self.pool().resolve_version_set_package_name(version_set_id); - let version_set = self.pool().resolve_version_set(version_set_id); - let candidates = self.get_or_cache_candidates(package_name); - - let matching_candidates = candidates - .candidates - .iter() - .copied() - .filter(|&p| { - let version = self.pool().resolve_internal_solvable(p).solvable().inner(); - !version_set.contains(version) - }) - .collect(); - - self.version_set_inverse_candidates - .insert(version_set_id, matching_candidates) - } - } - } - - /// Returns the candidates for the package with the given name similar to - /// [`Self::get_or_cache_candidates`] sorted from highest to lowest. - pub fn get_or_cache_sorted_candidates(&self, version_set_id: VersionSetId) -> &[SolvableId] { - match self.version_set_to_sorted_candidates.get(&version_set_id) { - Some(canidates) => canidates, - None => { - let package_name = self.pool().resolve_version_set_package_name(version_set_id); - let matching_candidates = self.get_or_cache_matching_candidates(version_set_id); - let candidates = self.get_or_cache_candidates(package_name); - - // Sort all the candidates in order in which they should betried by the solver. - let mut sorted_candidates = Vec::new(); - sorted_candidates.extend_from_slice(matching_candidates); - self.provider.sort_candidates(self, &mut sorted_candidates); - - // If we have a solvable that we favor, we sort that to the front. This ensures - // that the version that is favored is picked first. - if let Some(favored_id) = candidates.favored { - if let Some(pos) = sorted_candidates.iter().position(|&s| s == favored_id) { - // Move the element at `pos` to the front of the array - sorted_candidates[0..=pos].rotate_right(1); - } - } - - self.version_set_to_sorted_candidates - .insert(version_set_id, sorted_candidates) - } - } + self.cache.pool() } - /// Returns the dependencies of a solvable. Requests the solvables from the - /// [`DependencyProvider`] if they are not known yet. - pub fn get_or_cache_dependencies(&self, solvable_id: SolvableId) -> &Dependencies { - let dependencies_id = match self.solvable_to_dependencies.get_copy(&solvable_id) { - Some(id) => id, - None => { - let dependencies = self.provider.get_dependencies(solvable_id); - let dependencies_id = self.solvable_dependencies.alloc(dependencies); - self.solvable_to_dependencies - .insert_copy(solvable_id, dependencies_id); - dependencies_id - } - }; - - &self.solvable_dependencies[dependencies_id] - } -} - -impl> Solver { /// Solves the provided `jobs` and returns a transaction from the found solution /// /// Returns a [`Problem`] if no solution was found, which provides ways to inspect the causes @@ -243,60 +92,12 @@ impl> Sol let root_clause = self.clauses.alloc(ClauseState::root()); assert_eq!(root_clause, ClauseId::install_root()); - // Create clauses for root's dependencies, and their dependencies, and so forth - self.add_clauses_for_root_deps(); - - // Add clauses ensuring only a single candidate per package name is installed - // TODO: (BasZ) Im pretty sure there is a better way to formulate this. Maybe take a look - // at pubgrub? - // TODO: Can we move this to where a package is added? - for package_name in - (0..self.package_names.len()).map(|idx| self.package_names.get_copy(idx).unwrap()) - { - let candidates_id = self - .package_name_to_candidates - .get_copy(&package_name) - .unwrap(); - let candidates = &self.candidates[candidates_id].candidates; - // Each candidate gets a clause with each other candidate - for (i, &candidate) in candidates.iter().enumerate() { - for &other_candidate in &candidates[i + 1..] { - self.clauses - .alloc(ClauseState::forbid_multiple(candidate, other_candidate)); - } - } - } - - // Add clauses for the locked solvable - // TODO: Can we somehow move this to where a package is added? - for package_name in - (0..self.package_names.len()).map(|idx| self.package_names.get_copy(idx).unwrap()) - { - let candidates_id = self - .package_name_to_candidates - .get_copy(&package_name) - .unwrap(); - let candidates = &self.candidates[candidates_id]; - let Some(locked_solvable_id) = candidates.locked else { continue }; - // For each locked solvable, forbid other solvables with the same name - for &other_candidate in &candidates.candidates { - if other_candidate != locked_solvable_id { - self.clauses - .alloc(ClauseState::lock(locked_solvable_id, other_candidate)); - } - } - } - - // Create watches chains - self.make_watches(); - // Run SAT self.run_sat()?; let steps = self .decision_tracker .stack() - .iter() .flat_map(|d| { if d.value && d.solvable_id != SolvableId::root() { Some(d.solvable_id) @@ -310,80 +111,179 @@ impl> Sol Ok(steps) } - /// Adds clauses for root's dependencies, their dependencies, and so forth - /// - /// This function makes sure we only generate clauses for the solvables involved in the problem, - /// traversing the graph of requirements and ignoring unrelated packages. The graph is - /// traversed depth-first. - /// - /// A side effect of this function is that candidates for all involved match specs (in the - /// dependencies or constrains part of the package record) are fetched and cached for future - /// use. The `favored_map` parameter influences the order in which the candidates for a - /// dependency are sorted, giving preference to the favored package (i.e. placing it at the - /// front). - fn add_clauses_for_root_deps(&mut self) { - let mut visited = HashSet::new(); - let mut stack = Vec::new(); + /// Adds a clause to the solver and immediately starts watching its literals. + fn add_and_watch_clause(&mut self, clause: ClauseState) -> ClauseId { + let clause_id = self.clauses.alloc(clause); + let clause = &self.clauses[clause_id]; + + // Add in requires clause lookup + if let &Clause::Requires(solvable_id, version_set_id) = &clause.kind { + self.requires_clauses + .push((solvable_id, version_set_id, clause_id)); + } + + // Start watching the literals of the clause + let clause = &mut self.clauses[clause_id]; + if clause.has_watches() { + self.watches.start_watching(clause, clause_id); + } - stack.push(SolvableId::root()); + clause_id + } - let mut seen_requires = HashSet::new(); - let empty_version_set_id_vec: Vec = Vec::new(); + /// Adds clauses for a solvable. These clauses include requirements and constrains on other + /// solvables. + fn add_clauses_for_solvable(&mut self, solvable_id: SolvableId) -> Vec { + if self.clauses_added_for_solvable.contains(&solvable_id) { + return Vec::new(); + } + + let mut new_clauses = Vec::new(); + let mut queue = vec![solvable_id]; + let mut seen = HashSet::new(); + seen.insert(solvable_id); - while let Some(solvable_id) = stack.pop() { + while let Some(solvable_id) = queue.pop() { let solvable = self.pool().resolve_internal_solvable(solvable_id); + tracing::info!( + "┝━ adding clauses for dependencies of {}", + solvable.display(self.pool()) + ); // Determine the dependencies of the current solvable. There are two cases here: // 1. The solvable is the root solvable which only provides required dependencies. // 2. The solvable is a package candidate in which case we request the corresponding // dependencies from the `DependencyProvider`. let (requirements, constrains) = match solvable.inner { - SolvableInner::Root => (&self.root_requirements, &empty_version_set_id_vec), + SolvableInner::Root => (self.root_requirements.clone(), Vec::new()), SolvableInner::Package(_) => { - let deps = self.get_or_cache_dependencies(solvable_id); - (&deps.requirements, &deps.constrains) + let deps = self.cache.get_or_cache_dependencies(solvable_id); + (deps.requirements.clone(), deps.constrains.clone()) } }; - // Iterate over all the requirements and create clauses. - for &version_set_id in requirements { - // Get the sorted candidates that can fulfill this requirement - let candidates = self.get_or_cache_sorted_candidates(version_set_id); - - // Add any of the candidates to the stack of solvables that we need to visit. Only - // do this if we didnt visit the requirement before. Multiple solvables can share - // the same [`VersionSetId`] if they specify the exact same requirement. - if seen_requires.insert(version_set_id) { - for &candidate in candidates.iter() { - if visited.insert(candidate) { - stack.push(candidate); - } + // Add clauses for the requirements + for version_set_id in requirements { + //self.add_clauses_for_requirement(solvable_id, requirement); + let dependency_name = self.pool().resolve_version_set_package_name(version_set_id); + self.add_clauses_for_package(dependency_name); + + // Find all the solvables that match for the given version set + let candidates = self.cache.get_or_cache_sorted_candidates(version_set_id); + + // Queue requesting the dependencies of the candidates as well if they are cheaply + // available from the dependency provider. + for &candidate in candidates { + if seen.insert(candidate) + && self.cache.are_dependencies_available_for(candidate) + && !self.clauses_added_for_solvable.contains(&candidate) + { + queue.push(candidate); } } - self.clauses.alloc(ClauseState::requires( + // Add the requires clause + let clause_id = self.add_and_watch_clause(ClauseState::requires( solvable_id, version_set_id, candidates, )); + + new_clauses.push(clause_id); } - // Iterate over all constrains and add clauses - for &version_set_id in constrains.as_slice() { - // Get the candidates that do-not match the specified requirement. - let non_candidates = self - .get_or_cache_non_matching_candidates(version_set_id) - .iter() - .copied(); + // Add clauses for the constraints + for version_set_id in constrains { + let dependency_name = self.pool().resolve_version_set_package_name(version_set_id); + self.add_clauses_for_package(dependency_name); + + // Find all the solvables that match for the given version set + let constrained_candidates = self + .cache + .get_or_cache_non_matching_candidates(version_set_id); // Add forbidden clauses for the candidates - for forbidden_candidate in non_candidates { + for forbidden_candidate in constrained_candidates.iter().copied().collect_vec() { let clause = ClauseState::constrains(solvable_id, forbidden_candidate, version_set_id); - self.clauses.alloc(clause); + let clause_id = self.add_and_watch_clause(clause); + new_clauses.push(clause_id) + } + } + + // Start by stating the clauses have been added. + self.clauses_added_for_solvable.insert(solvable_id); + } + + new_clauses + } + + /// Adds all clauses for a specific package name. + /// + /// These clauses include: + /// + /// 1. making sure that only a single candidate for the package is selected (forbid multiple) + /// 2. if there is a locked candidate then that candidate is the only selectable candidate. + /// + /// If this function is called with the same package name twice, the clauses will only be added + /// once. + /// + /// There is no need to propagate after adding these clauses because none of the clauses are + /// assertions (only a single literal) and we assume that no decision has been made about any + /// of the solvables involved. This assumption is checked when debug_assertions are enabled. + fn add_clauses_for_package(&mut self, package_name: NameId) { + if self.clauses_added_for_package.contains(&package_name) { + return; + } + + tracing::info!( + "┝━ adding clauses for package '{}'", + self.pool().resolve_package_name(package_name) + ); + + let package_candidates = self.cache.get_or_cache_candidates(package_name); + let locked_solvable_id = package_candidates.locked; + let candidates = &package_candidates.candidates; + + // Check the assumption that no decision has been made about any of the solvables. + for &candidate in candidates { + debug_assert!( + self.decision_tracker.assigned_value(candidate).is_none(), + "a decision has been made about a candidate of a package that was not properly added yet." + ); + } + + // Each candidate gets a clause to disallow other candidates. + for (i, &candidate) in candidates.iter().enumerate() { + for &other_candidate in &candidates[i + 1..] { + let clause_id = self + .clauses + .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); + } + } + } + + // If there is a locked solvable, forbid other solvables. + if let Some(locked_solvable_id) = locked_solvable_id { + for &other_candidate in candidates { + if other_candidate != locked_solvable_id { + let clause_id = self + .clauses + .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); + } } } } + + self.clauses_added_for_package.insert(package_name); } /// Run the CDCL algorithm to solve the SAT problem @@ -409,55 +309,184 @@ impl> Sol /// The solver loop can be found in [`Solver::resolve_dependencies`]. fn run_sat(&mut self) -> Result<(), Problem> { assert!(self.decision_tracker.is_empty()); + let mut level = 0; - // Assign `true` to the root solvable - let level = 1; - self.decision_tracker - .try_add_decision( - Decision::new(SolvableId::root(), true, ClauseId::install_root()), - 1, - ) - .expect("bug: solvable was already decided!"); + let mut new_clauses = Vec::new(); + loop { + // If the decision loop has been completely reset we want to + if level == 0 { + level = 1; + // Assign `true` to the root solvable. This must be installed to satisfy the solution. + // The root solvable contains the dependencies that were injected when calling + // `Solver::solve`. If we can find a solution were the root is installable we found a + // solution that satisfies the user requirements. + tracing::info!( + "╤══ install {} at level {level}", + SolvableId::root().display(self.pool()) + ); + self.decision_tracker + .try_add_decision( + Decision::new(SolvableId::root(), true, ClauseId::install_root()), + level, + ) + .expect("already decided"); + + // Add the clauses for the root solvable. + new_clauses.append(&mut self.add_clauses_for_solvable(SolvableId::root())); + } - // Forbid packages that rely on dependencies without candidates - self.decide_requires_without_candidates(level) - .map_err(|cause| self.analyze_unsolvable(cause))?; + // Add decisions for Require clauses that form unit clauses. E.g. require clauses that + // have no matching candidates. + self.decide_requires_without_candidates(&std::mem::take(&mut new_clauses)) + .map_err(|clause_id| self.analyze_unsolvable(clause_id))?; - // Propagate after the assignments above - self.propagate(level) - .map_err(|(_, _, cause)| self.analyze_unsolvable(cause))?; + // Propagate any decisions from assignments above. + self.propagate(level) + .map_err(|(_, _, clause_id)| self.analyze_unsolvable(clause_id))?; - // Enter the solver loop - self.resolve_dependencies(level)?; + // Enter the solver loop, return immediately if no new assignments have been made. + level = self.resolve_dependencies(level)?; - Ok(()) + // We have a partial solution. E.g. there is a solution that satisfies all the clauses + // that have been added so far. + + // Determine which solvables are part of the solution for which we did not yet get any + // dependencies. If we find any such solvable it means we did not arrive at the full + // solution yet. + let new_solvables: Vec<_> = self + .decision_tracker + .stack() + // Filter only decisions that led to a positive assignment + .filter(|d| d.value) + // Select solvables for which we do not yet have dependencies + .filter(|d| !self.clauses_added_for_solvable.contains(&d.solvable_id)) + .map(|d| (d.solvable_id, d.derived_from)) + .collect(); + + if new_solvables.is_empty() { + // If no new literals were selected this solution is complete and we can return. + return Ok(()); + } + + tracing::info!( + "====\n==Found newly selected solvables\n- {}\n====", + new_solvables + .iter() + .copied() + .format_with("\n- ", |(id, derived_from), f| f(&format_args!( + "{} (derived from {:?})", + id.display(self.pool()), + self.clauses[derived_from].debug(self.pool()), + ))) + ); + + for (solvable, _) in new_solvables { + // Add the clauses for this particular solvable. + let mut clauses_for_solvable = self.add_clauses_for_solvable(solvable); + + // Immediately assign unit clauses. If clause is found that is a unit clause we + // permanently fix that assignment to false and an error is returned. + for clause_id in clauses_for_solvable.iter().copied() { + let clause = &self.clauses[clause_id]; + + match clause.kind { + Clause::Requires(dependent, requirement) => { + let solvable_is_assigned = + self.decision_tracker.assigned_value(dependent) == Some(true); + if solvable_is_assigned { + let candidates = + self.cache.get_or_cache_matching_candidates(requirement); + let all_candidates_assigned_false = candidates.iter().all(|&s| { + self.decision_tracker.assigned_value(s) == Some(false) + }); + let is_empty = candidates.is_empty(); + + // If none of the candidates is selectable this clause will cause a + // conflict. We have to backtrack to the point where we made the + // decision to select + if all_candidates_assigned_false { + tracing::info!( + "├─ there are no selectable candidates for {clause:?}", + clause = self.clauses[clause_id].debug(self.pool()) + ); + + self.decision_tracker.clear(); + level = 0; + + break; + } else if is_empty { + tracing::info!("├─ added clause {clause:?} has no candidates which invalidates the partial solution", + clause=self.clauses[clause_id].debug(self.pool())); + + self.decision_tracker.clear(); + level = 0; + break; + } + } + } + Clause::Constrains(dependent, forbidden, _) => { + if self.decision_tracker.assigned_value(forbidden) == Some(true) + && self.decision_tracker.assigned_value(dependent) == Some(true) + { + tracing::info!( + "├─ {clause:?} which was already set to true", + clause = self.clauses[clause_id].debug(self.pool()) + ); + self.decision_tracker.clear(); + level = 0; + break; + } + } + _ => unreachable!(), + } + } + + new_clauses.append(&mut clauses_for_solvable); + } + } } /// Forbid packages that rely on dependencies without candidates /// /// Since a requires clause is represented as (¬A ∨ candidate_1 ∨ ... ∨ candidate_n), /// a dependency without candidates becomes (¬A), which means that A should always be false. - fn decide_requires_without_candidates(&mut self, level: u32) -> Result<(), ClauseId> { + fn decide_requires_without_candidates( + &mut self, + clauses: &[ClauseId], + ) -> Result { tracing::info!("=== Deciding assertions for requires without candidates"); - for (clause_id, clause) in self.clauses.iter() { + let mut conflicting_clause = None; + let mut made_a_decision = false; + for &clause_id in clauses.iter() { + let clause = &self.clauses[clause_id]; if let Clause::Requires(solvable_id, _) = clause.kind { if !clause.has_watches() { // A requires clause without watches means it has a single literal (i.e. // there are no candidates) - let decided = self + let decided = match self .decision_tracker - .try_add_decision(Decision::new(solvable_id, false, clause_id), level) - .map_err(|_| clause_id)?; + .try_add_fixed_assignment(Decision::new(solvable_id, false, clause_id)) + { + Ok(decided) => decided, + Err(_) => { + conflicting_clause = Some(clause_id); + true + } + }; if decided { tracing::info!("Set {} = false", solvable_id.display(self.pool())); + made_a_decision = true; } } } } - Ok(()) + match conflicting_clause { + None => Ok(made_a_decision), + Some(clause_id) => Err(clause_id), + } } /// Resolves all dependencies @@ -470,59 +499,71 @@ impl> Sol /// package has been picked yet. Then we pick the highest possible version for that package, or /// the favored version if it was provided by the user, and set its value to true. fn resolve_dependencies(&mut self, mut level: u32) -> Result { - let mut i = 0; loop { - if i >= self.clauses.len() { - break; - } - - let clause_id = ClauseId::from_usize(i); - - let (required_by, candidate) = { - let clause = &self.clauses[clause_id]; - i += 1; - - // We are only interested in requires clauses - let Clause::Requires(solvable_id, deps) = clause.kind else { - continue; - }; + // Make a decision. If no decision could be made it means the problem is satisfyable. + let Some((candidate, required_by, clause_id)) = self.decide() else {break}; - // Consider only clauses in which we have decided to install the solvable - if self.decision_tracker.assigned_value(solvable_id) != Some(true) { - continue; - } + // Propagate the decision + level = self.set_propagate_learn(level, candidate, required_by, clause_id)?; + } - // Consider only clauses in which no candidates have been installed - let candidates = &self.version_set_to_sorted_candidates[&deps]; - if candidates - .iter() - .any(|&c| self.decision_tracker.assigned_value(c) == Some(true)) - { - continue; - } + // We just went through all clauses and there are no choices left to be made + Ok(level) + } - // Get the first candidate that is undecided and should be installed - // - // This assumes that the packages have been provided in the right order when the solvables were created - // (most recent packages first) - ( - solvable_id, - candidates - .iter() - .cloned() - .find(|&c| self.decision_tracker.assigned_value(c).is_none()) - .unwrap(), - ) - }; + /// Pick a solvable that we are going to assign true. This function uses a heuristic to + /// determine to best decision to make. The function selects the requirement that has the least + /// amount of working available candidates and selects the best candidate from that list. This + /// ensures that if there are conflicts they are delt with as early as possible. + fn decide(&mut self) -> Option<(SolvableId, SolvableId, ClauseId)> { + let mut best_decision = None; + for &(solvable_id, deps, clause_id) in self.requires_clauses.iter() { + // Consider only clauses in which we have decided to install the solvable + if self.decision_tracker.assigned_value(solvable_id) != Some(true) { + continue; + } - level = self.set_propagate_learn(level, candidate, required_by, clause_id)?; + // Consider only clauses in which no candidates have been installed + let candidates = &self.cache.version_set_to_sorted_candidates[&deps]; + + // Either find the first assignable candidate or determine that one of the candidates is + // already assigned in which case the clause has already been satisfied. + let candidate = candidates.iter().try_fold( + (None, 0), + |(first_selectable_candidate, selectable_candidates), &candidate| { + let assigned_value = self.decision_tracker.assigned_value(candidate); + match assigned_value { + Some(true) => ControlFlow::Break(()), + Some(false) => ControlFlow::Continue(( + first_selectable_candidate, + selectable_candidates, + )), + None => ControlFlow::Continue(( + first_selectable_candidate.or(Some(candidate)), + selectable_candidates + 1, + )), + } + }, + ); - // We have made progress, and should look at all clauses in the next iteration - i = 0; + match candidate { + ControlFlow::Continue((Some(candidate), count)) => { + let possible_decision = (candidate, solvable_id, clause_id); + best_decision = Some(match best_decision { + None => (count, possible_decision), + Some((best_count, _)) if count < best_count => { + (count, possible_decision) + }, + Some(best_decision) => best_decision, + }) + }, + ControlFlow::Break(_) => continue, + ControlFlow::Continue((None, _)) => unreachable!("when we get here it means that all candidates have been assigned false. This should not be able to happen at this point because during propagation the solvable should have been assigned false as well."), + } } - // We just went through all clauses and there are no choices left to be made - Ok(level) + // Could not find a requirement that needs satisfying. + best_decision.map(|d| d.1) } /// Executes one iteration of the CDCL loop @@ -551,10 +592,15 @@ impl> Sol required_by.display(self.pool()), ); + // Add the decision to the tracker self.decision_tracker .try_add_decision(Decision::new(solvable, true, clause_id), level) .expect("bug: solvable was already decided!"); + self.propagate_and_learn(level) + } + + fn propagate_and_learn(&mut self, mut level: u32) -> Result { loop { let r = self.propagate(level); let Err((conflicting_solvable, attempted_value, conflicting_clause)) = r else { @@ -563,71 +609,85 @@ impl> Sol break; }; - { - tracing::info!( - "├─ Propagation conflicted: could not set {solvable} to {attempted_value}", - solvable = solvable.display(self.pool()) - ); - tracing::info!( - "│ During unit propagation for clause: {:?}", - self.clauses[conflicting_clause].debug(self.pool()) - ); + level = self.learn_from_conflict( + level, + conflicting_solvable, + attempted_value, + conflicting_clause, + )?; + } - tracing::info!( - "│ Previously decided value: {}. Derived from: {:?}", - !attempted_value, - self.clauses[self - .decision_tracker - .stack() - .iter() - .find(|d| d.solvable_id == conflicting_solvable) - .unwrap() - .derived_from] - .debug(self.pool()), - ); - } + Ok(level) + } - if level == 1 { - tracing::info!("╘══ UNSOLVABLE"); - for decision in self.decision_tracker.stack() { - let clause = &self.clauses[decision.derived_from]; - let level = self.decision_tracker.level(decision.solvable_id); - let action = if decision.value { "install" } else { "forbid" }; + fn learn_from_conflict( + &mut self, + mut level: u32, + conflicting_solvable: SolvableId, + attempted_value: bool, + conflicting_clause: ClauseId, + ) -> Result { + { + tracing::info!( + "├─ Propagation conflicted: could not set {solvable} to {attempted_value}", + solvable = conflicting_solvable.display(self.pool()) + ); + tracing::info!( + "│ During unit propagation for clause: {:?}", + self.clauses[conflicting_clause].debug(self.pool()) + ); - if let Clause::ForbidMultipleInstances(..) = clause.kind { - // Skip forbids clauses, to reduce noise - continue; - } + tracing::info!( + "│ Previously decided value: {}. Derived from: {:?}", + !attempted_value, + self.clauses[self + .decision_tracker + .find_clause_for_assignment(conflicting_solvable) + .unwrap()] + .debug(self.pool()), + ); + } + + if level == 1 { + tracing::info!("╘══ UNSOLVABLE"); + for decision in self.decision_tracker.stack() { + let clause = &self.clauses[decision.derived_from]; + let level = self.decision_tracker.level(decision.solvable_id); + let action = if decision.value { "install" } else { "forbid" }; - tracing::info!( - "* ({level}) {action} {}. Reason: {:?}", - decision.solvable_id.display(self.pool()), - clause.debug(self.pool()), - ); + if let Clause::ForbidMultipleInstances(..) = clause.kind { + // Skip forbids clauses, to reduce noise + continue; } - return Err(self.analyze_unsolvable(conflicting_clause)); + tracing::info!( + "* ({level}) {action} {}. Reason: {:?}", + decision.solvable_id.display(self.pool()), + clause.debug(self.pool()), + ); } - let (new_level, learned_clause_id, literal) = - self.analyze(level, conflicting_solvable, conflicting_clause); - level = new_level; + return Err(self.analyze_unsolvable(conflicting_clause)); + } - tracing::info!("├─ Backtracked to level {level}"); + let (new_level, learned_clause_id, literal) = + self.analyze(level, conflicting_solvable, conflicting_clause); + level = new_level; - // Optimization: propagate right now, since we know that the clause is a unit clause - let decision = literal.satisfying_value(); - self.decision_tracker - .try_add_decision( - Decision::new(literal.solvable_id, decision, learned_clause_id), - level, - ) - .expect("bug: solvable was already decided!"); - tracing::info!( - "├─ Propagate after learn: {} = {decision}", - literal.solvable_id.display(self.pool()) - ); - } + tracing::info!("├─ Backtracked to level {level}"); + + // Optimization: propagate right now, since we know that the clause is a unit clause + let decision = literal.satisfying_value(); + self.decision_tracker + .try_add_decision( + Decision::new(literal.solvable_id, decision, learned_clause_id), + level, + ) + .expect("bug: solvable was already decided!"); + tracing::info!( + "├─ Propagate after learn: {} = {decision}", + literal.solvable_id.display(self.pool()) + ); Ok(level) } @@ -642,7 +702,8 @@ impl> Sol fn propagate(&mut self, level: u32) -> Result<(), (SolvableId, bool, ClauseId)> { // Learnt assertions (assertions are clauses that consist of a single literal, and therefore // do not have watches) - for &clause_id in self.learnt_clause_ids.iter() { + for learn_clause_idx in 0..self.learnt_clause_ids.len() { + let clause_id = self.learnt_clause_ids[learn_clause_idx]; let clause = &self.clauses[clause_id]; let Clause::Learnt(learnt_index) = clause.kind else { unreachable!(); @@ -714,7 +775,7 @@ impl> Sol // One of the watched literals is now false if let Some(variable) = clause.next_unwatched_variable( &self.learnt_clauses, - &self.version_set_to_sorted_candidates, + &self.cache.version_set_to_sorted_candidates, self.decision_tracker.map(), ) { debug_assert!(!clause.watched_literals.contains(&variable)); @@ -761,9 +822,9 @@ impl> Sol _ => { tracing::info!( "├─ Propagate {} = {}. {:?}", - remaining_watch.solvable_id.display(self.provider.pool()), + remaining_watch.solvable_id.display(self.cache.pool()), remaining_watch.satisfying_value(), - clause.debug(self.provider.pool()), + clause.debug(self.cache.pool()), ); } } @@ -818,7 +879,7 @@ impl> Sol let mut involved = HashSet::new(); self.clauses[clause_id].kind.visit_literals( &self.learnt_clauses, - &self.version_set_to_sorted_candidates, + &self.cache.version_set_to_sorted_candidates, |literal| { involved.insert(literal.solvable_id); }, @@ -833,9 +894,9 @@ impl> Sol &mut seen, ); - for decision in self.decision_tracker.stack()[1..].iter().rev() { + for decision in self.decision_tracker.stack().rev() { if decision.solvable_id == SolvableId::root() { - panic!("unexpected root solvable") + continue; } let why = decision.derived_from; @@ -856,7 +917,7 @@ impl> Sol self.clauses[why].kind.visit_literals( &self.learnt_clauses, - &self.version_set_to_sorted_candidates, + &self.cache.version_set_to_sorted_candidates, |literal| { if literal.eval(self.decision_tracker.map()) == Some(true) { assert_eq!(literal.solvable_id, decision.solvable_id); @@ -900,7 +961,7 @@ impl> Sol self.clauses[clause_id].kind.visit_literals( &self.learnt_clauses, - &self.version_set_to_sorted_candidates, + &self.cache.version_set_to_sorted_candidates, |literal| { if !first_iteration && literal.solvable_id == conflicting_solvable { // We are only interested in the causes of the conflict, so we ignore the @@ -990,19 +1051,6 @@ impl> Sol (target_level, clause_id, last_literal) } - - fn make_watches(&mut self) { - // Watches are already initialized in the clauses themselves, here we build a linked list for - // each package (a clause will be linked to other clauses that are watching the same package) - for (clause_id, clause) in self.clauses.iter_mut() { - if !clause.has_watches() { - // Skip clauses without watches - continue; - } - - self.watches.start_watching(clause, clause_id); - } - } } #[cfg(test)] @@ -1016,6 +1064,7 @@ mod test { fmt::{Debug, Display, Formatter}, str::FromStr, }; + use tracing_test::traced_test; // Let's define our own packaging version system and dependency specification. // This is a very simple version system, where a package is identified by a name and a version @@ -1193,7 +1242,7 @@ mod test { fn sort_candidates( &self, - _solver: &Solver, String, Self>, + _solver: &SolverCache, String, Self>, solvables: &mut [SolvableId], ) { solvables.sort_by(|a, b| { @@ -1261,8 +1310,13 @@ mod test { ) -> String { use std::fmt::Write; let mut buf = String::new(); - for &solvable_id in solvables { - writeln!(buf, "{}", solvable_id.display(pool)).unwrap(); + for solvable in solvables + .iter() + .copied() + .map(|s| s.display(pool).to_string()) + .sorted() + { + writeln!(buf, "{solvable}").unwrap(); } buf @@ -1280,6 +1334,18 @@ mod test { } } + /// Solve the problem and returns either a solution represented as a string or an error string. + fn solve_snapshot(provider: BundleBoxProvider, specs: &[&str]) -> String { + let requirements = provider.requirements(specs); + let mut solver = Solver::new(provider); + match solver.solve(requirements) { + Ok(solvables) => transaction_to_string(solver.pool(), &solvables), + Err(problem) => problem + .display_user_friendly(&solver, &DefaultSolvableDisplay) + .to_string(), + } + } + /// Test whether we can select a version, this is the most basic operation #[test] fn test_unit_propagation_1() { @@ -1376,29 +1442,18 @@ mod test { let mut solver = Solver::new(provider); let solved = solver.solve(requirements); let solved = match solved { - Ok(solved) => solved, + Ok(solved) => transaction_to_string(solver.pool(), &solved), Err(p) => panic!( "{}", p.display_user_friendly(&solver, &DefaultSolvableDisplay) ), }; - - use std::fmt::Write; - let mut display_result = String::new(); - for &solvable_id in &solved { - writeln!( - display_result, - "{solvable}", - solvable = solvable_id.display(solver.pool()) - ) - .unwrap(); - } - - insta::assert_snapshot!(display_result); + insta::assert_snapshot!(solved); } /// The non-existing package should not be selected #[test] + #[traced_test] fn test_resolve_with_nonexisting() { let provider = BundleBoxProvider::from_packages(&[ ("asdf", 4, vec!["b"]), @@ -1498,8 +1553,8 @@ mod test { let result = transaction_to_string(&solver.pool(), &solved); insta::assert_snapshot!(result, @r###" - b=2 a=1 + b=2 "###); } // @@ -1531,9 +1586,9 @@ mod test { let result = transaction_to_string(&solver.pool(), &solved); insta::assert_snapshot!(result, @r###" + a=2 b=2 c=2 - a=2 "###); } @@ -1567,6 +1622,7 @@ mod test { } #[test] + #[tracing_test::traced_test] fn test_unsat_no_candidates_for_child_1() { let provider = BundleBoxProvider::from_packages(&[("asdf", 1, vec!["c 2"]), ("c", 1, vec![])]); @@ -1597,6 +1653,7 @@ mod test { } #[test] + #[tracing_test::traced_test] fn test_unsat_after_backtracking() { let provider = BundleBoxProvider::from_packages(&[ ("b", 7, vec!["d 1"]), @@ -1714,15 +1771,7 @@ mod test { fn test_missing_dep() { let provider = BundleBoxProvider::from_packages(&[("a", 2, vec!["missing"]), ("a", 1, vec![])]); - let requirements = provider.requirements(&["a"]); - let mut solver = Solver::new(provider); - let result = match solver.solve(requirements) { - Ok(result) => transaction_to_string(solver.pool(), &result), - Err(problem) => problem - .display_user_friendly(&solver, &DefaultSolvableDisplay) - .to_string(), - }; - insta::assert_snapshot!(result); + insta::assert_snapshot!(solve_snapshot(provider, &["a"])); } #[test] @@ -1746,9 +1795,22 @@ mod test { ("pydantic", 13, vec![]), ("pydantic", 14, vec![]), ]); - let requirements = provider.requirements(&["quetz-server", "pydantic 0..10"]); - let mut solver = Solver::new(provider); - let solved = solver.solve(requirements).unwrap(); - insta::assert_snapshot!(transaction_to_string(solver.pool(), &solved)); + insta::assert_snapshot!(solve_snapshot( + provider, + &["quetz-server", "pydantic 0..10"] + )); + } + + #[test] + #[tracing_test::traced_test] + fn test_incremental_crash() { + let provider = BundleBoxProvider::from_packages(&[ + ("a", 3, vec!["missing"]), + ("a", 2, vec!["missing"]), + ("a", 1, vec!["b"]), + ("b", 2, vec!["a 2..4"]), + ("b", 1, vec![]), + ]); + insta::assert_snapshot!(solve_snapshot(provider, &["a"])); } } diff --git a/src/solver/snapshots/rattler_libsolv_rs__solver__test__incremental_crash.snap b/src/solver/snapshots/rattler_libsolv_rs__solver__test__incremental_crash.snap new file mode 100644 index 0000000..6061259 --- /dev/null +++ b/src/solver/snapshots/rattler_libsolv_rs__solver__test__incremental_crash.snap @@ -0,0 +1,8 @@ +--- +source: crates/rattler_libsolv_rs/src/solver/mod.rs +assertion_line: 1810 +expression: "solve_snapshot(provider, &[\"a\"])" +--- +a=1 +b=1 + diff --git a/src/solver/snapshots/rattler_libsolv_rs__solver__test__no_backtracking.snap b/src/solver/snapshots/rattler_libsolv_rs__solver__test__no_backtracking.snap index 73fc6f2..895c3c4 100644 --- a/src/solver/snapshots/rattler_libsolv_rs__solver__test__no_backtracking.snap +++ b/src/solver/snapshots/rattler_libsolv_rs__solver__test__no_backtracking.snap @@ -1,7 +1,8 @@ --- source: crates/rattler_libsolv_rs/src/solver/mod.rs +assertion_line: 1798 expression: "transaction_to_string(solver.pool(), &solved)" --- -quetz-server=1 pydantic=9 +quetz-server=1 diff --git a/src/solver/snapshots/rattler_libsolv_rs__solver__test__resolve_with_conflict.snap b/src/solver/snapshots/rattler_libsolv_rs__solver__test__resolve_with_conflict.snap index e15535f..41b6753 100644 --- a/src/solver/snapshots/rattler_libsolv_rs__solver__test__resolve_with_conflict.snap +++ b/src/solver/snapshots/rattler_libsolv_rs__solver__test__resolve_with_conflict.snap @@ -1,8 +1,9 @@ --- source: crates/rattler_libsolv_rs/src/solver/mod.rs -expression: display_result +assertion_line: 1442 +expression: solved --- -conflicting=0 asdf=3 +conflicting=0 efgh=7