From f5b1b73d2afdd89a0d5c6ac033b3355c6c50343f Mon Sep 17 00:00:00 2001 From: Bas Zalmstra Date: Thu, 2 Jan 2025 15:20:33 +0100 Subject: [PATCH] perf: reintroduce binary encoding of forbid multiple clauses (#91) --- src/conflict.rs | 104 +- src/internal/id.rs | 170 +-- src/lib.rs | 3 + src/solver/binary_encoding.rs | 167 +++ src/solver/cache.rs | 6 +- src/solver/clause.rs | 285 +++-- src/solver/decision.rs | 8 +- src/solver/decision_map.rs | 35 +- src/solver/decision_tracker.rs | 32 +- src/solver/mod.rs | 1091 +++++++++-------- ..._encoding__test__at_most_once_tracker.snap | 13 + src/solver/variable_map.rs | 163 +++ src/solver/watch_map.rs | 26 +- .../snapshots/solver__merge_installable.snap | 10 +- .../solver__unsat_after_backtracking.snap | 17 +- ...lver__unsat_applies_graph_compression.snap | 3 +- .../solver__unsat_bluesky_conflict.snap | 1 + ..._unsat_incompatible_root_requirements.snap | 9 +- .../solver__unsat_pubgrub_article.snap | 1 + 19 files changed, 1335 insertions(+), 809 deletions(-) create mode 100644 src/solver/binary_encoding.rs create mode 100644 src/solver/snapshots/resolvo__solver__binary_encoding__test__at_most_once_tracker.snap create mode 100644 src/solver/variable_map.rs diff --git a/src/conflict.rs b/src/conflict.rs index edad5e9..3d121b6 100644 --- a/src/conflict.rs +++ b/src/conflict.rs @@ -11,10 +11,11 @@ use petgraph::{ Direction, }; +use crate::solver::variable_map::VariableOrigin; use crate::{ internal::{ arena::ArenaId, - id::{ClauseId, InternalSolvableId, SolvableId, StringId, VersionSetId}, + id::{ClauseId, SolvableId, SolvableOrRootId, StringId, VersionSetId}, }, runtime::AsyncRuntime, solver::{clause::Clause, Solver}, @@ -48,19 +49,24 @@ impl Conflict { solver: &Solver, ) -> ConflictGraph { let mut graph = DiGraph::::default(); - let mut nodes: HashMap = HashMap::default(); + let mut nodes: HashMap = HashMap::default(); let mut excluded_nodes: HashMap = HashMap::default(); - let root_node = Self::add_node(&mut graph, &mut nodes, InternalSolvableId::root()); + let root_node = Self::add_node(&mut graph, &mut nodes, SolvableOrRootId::root()); let unresolved_node = graph.add_node(ConflictNode::UnresolvedDependency); + let mut last_node_by_name = HashMap::default(); for clause_id in &self.clauses { - let clause = &solver.clauses.kinds.borrow()[clause_id.to_usize()]; + let clause = &solver.clauses.kinds[clause_id.to_usize()]; match clause { Clause::InstallRoot => (), Clause::Excluded(solvable, reason) => { tracing::trace!("{solvable:?} is excluded"); - let package_node = Self::add_node(&mut graph, &mut nodes, *solvable); + let solvable = solvable + .as_solvable(&solver.variable_map) + .expect("only solvables can be excluded"); + + let package_node = Self::add_node(&mut graph, &mut nodes, solvable.into()); let excluded_node = excluded_nodes .entry(*reason) .or_insert_with(|| graph.add_node(ConflictNode::Excluded(*reason))); @@ -73,7 +79,10 @@ impl Conflict { } Clause::Learnt(..) => unreachable!(), &Clause::Requires(package_id, version_set_id) => { - let package_node = Self::add_node(&mut graph, &mut nodes, package_id); + let solvable = package_id + .as_solvable_or_root(&solver.variable_map) + .expect("only solvables can be excluded"); + let package_node = Self::add_node(&mut graph, &mut nodes, solvable); let candidates = solver.async_runtime.block_on(solver.cache.get_or_cache_sorted_candidates(version_set_id)).unwrap_or_else(|_| { unreachable!("The version set was used in the solver, so it must have been cached. Therefore cancellation is impossible here and we cannot get an `Err(...)`") @@ -102,20 +111,48 @@ impl Conflict { } } &Clause::Lock(locked, forbidden) => { - let node2_id = Self::add_node(&mut graph, &mut nodes, forbidden); - let conflict = ConflictCause::Locked(locked); + let locked_solvable = locked + .as_solvable(&solver.variable_map) + .expect("only solvables can be excluded"); + let forbidden_solvable = forbidden + .as_solvable(&solver.variable_map) + .expect("only solvables can be excluded"); + let node2_id = + Self::add_node(&mut graph, &mut nodes, forbidden_solvable.into()); + let conflict = ConflictCause::Locked(locked_solvable); graph.add_edge(root_node, node2_id, ConflictEdge::Conflict(conflict)); } &Clause::ForbidMultipleInstances(instance1_id, instance2_id, _) => { - let node1_id = Self::add_node(&mut graph, &mut nodes, instance1_id); - let node2_id = Self::add_node(&mut graph, &mut nodes, instance2_id); + let solvable1 = instance1_id + .as_solvable_or_root(&solver.variable_map) + .expect("only solvables can be excluded"); + let node1_id = Self::add_node(&mut graph, &mut nodes, solvable1); + + let VariableOrigin::ForbidMultiple(name) = + solver.variable_map.origin(instance2_id.variable()) + else { + unreachable!("expected only forbid variables") + }; - let conflict = ConflictCause::ForbidMultipleInstances; - graph.add_edge(node1_id, node2_id, ConflictEdge::Conflict(conflict)); + let previous_node = last_node_by_name.insert(name, node1_id); + if let Some(previous_node) = previous_node { + graph.add_edge( + previous_node, + node1_id, + ConflictEdge::Conflict(ConflictCause::ForbidMultipleInstances), + ); + } } &Clause::Constrains(package_id, dep_id, version_set_id) => { - let package_node = Self::add_node(&mut graph, &mut nodes, package_id); - let dep_node = Self::add_node(&mut graph, &mut nodes, dep_id); + let package_solvable = package_id + .as_solvable_or_root(&solver.variable_map) + .expect("only solvables can be excluded"); + let dependency_solvable = dep_id + .as_solvable_or_root(&solver.variable_map) + .expect("only solvables can be excluded"); + + let package_node = Self::add_node(&mut graph, &mut nodes, package_solvable); + let dep_node = Self::add_node(&mut graph, &mut nodes, dependency_solvable); graph.add_edge( package_node, @@ -154,8 +191,8 @@ impl Conflict { fn add_node( graph: &mut DiGraph, - nodes: &mut HashMap, - solvable_id: InternalSolvableId, + nodes: &mut HashMap, + solvable_id: SolvableOrRootId, ) -> NodeIndex { *nodes .entry(solvable_id) @@ -176,7 +213,7 @@ impl Conflict { #[derive(Copy, Clone, Eq, PartialEq)] pub(crate) enum ConflictNode { /// Node corresponding to a solvable - Solvable(InternalSolvableId), + Solvable(SolvableOrRootId), /// Node representing a dependency without candidates UnresolvedDependency, /// Node representing an exclude reason @@ -184,7 +221,7 @@ pub(crate) enum ConflictNode { } impl ConflictNode { - fn solvable_id(self) -> InternalSolvableId { + fn solvable_or_root(self) -> SolvableOrRootId { match self { ConflictNode::Solvable(solvable_id) => solvable_id, ConflictNode::UnresolvedDependency => { @@ -195,6 +232,10 @@ impl ConflictNode { } } } + + fn solvable(self) -> Option { + self.solvable_or_root().solvable() + } } /// An edge in the graph representation of a [`Conflict`] @@ -227,7 +268,7 @@ impl ConflictEdge { #[derive(Copy, Clone, Hash, Eq, PartialEq, Ord, PartialOrd)] pub(crate) enum ConflictCause { /// The solvable is locked - Locked(InternalSolvableId), + Locked(SolvableId), /// The target node is constrained by the specified version set Constrains(VersionSetId), /// It is forbidden to install multiple instances of the same dependency @@ -284,7 +325,7 @@ impl ConflictGraph { }; // If this is a merged node, skip it unless it is the first one in the group - if let Some(solvable_id) = id.as_solvable() { + if let Some(solvable_id) = id.solvable() { if let Some(merged) = merged_nodes.get(&solvable_id) { if solvable_id != merged.ids[0] { continue; @@ -321,7 +362,7 @@ impl ConflictGraph { ConflictNode::Solvable(mut solvable_2) => { // If the target node has been merged, replace it by the first id in the // group - if let Some(solvable_id) = solvable_2.as_solvable() { + if let Some(solvable_id) = solvable_2.solvable() { if let Some(merged) = merged_nodes.get(&solvable_id) { solvable_2 = merged.ids[0].into(); @@ -381,7 +422,7 @@ impl ConflictGraph { .sorted_unstable() .collect(); - let Some(solvable_id) = candidate.as_solvable() else { + let Some(solvable_id) = candidate.solvable() else { // Root is never merged continue; }; @@ -662,7 +703,7 @@ impl<'i, I: Interner> DisplayUnsat<'i, I> { let graph = &self.graph.graph; let installable_nodes = &self.installable_set; - let mut reported: HashSet = HashSet::new(); + let mut reported: HashSet = HashSet::new(); // Note: we are only interested in requires edges here let indenter = Indenter::new(top_level_indent); @@ -749,8 +790,8 @@ impl<'i, I: Interner> DisplayUnsat<'i, I> { let (DisplayOp::Candidate(child_node), _) = child else { unreachable!() }; - let solvable_id = graph[child_node].solvable_id(); - let Some(solvable_id) = solvable_id.as_solvable() else { + let solvable_id = graph[child_node].solvable_or_root(); + let Some(solvable_id) = solvable_id.solvable() else { continue; }; @@ -799,8 +840,7 @@ impl<'i, I: Interner> DisplayUnsat<'i, I> { let (DisplayOp::Candidate(child_node), _) = child else { unreachable!() }; - let Some(solvable_id) = graph[child_node].solvable_id().as_solvable() - else { + let Some(solvable_id) = graph[child_node].solvable() else { continue; }; let merged = self.merged_candidates.get(&solvable_id); @@ -825,21 +865,21 @@ impl<'i, I: Interner> DisplayUnsat<'i, I> { } } DisplayOp::Candidate(candidate) => { - let solvable_id = graph[candidate].solvable_id(); + let solvable_id = graph[candidate].solvable_or_root(); if reported.contains(&solvable_id) { continue; } let version = if let Some(merged) = solvable_id - .as_solvable() + .solvable() .and_then(|solvable_id| self.merged_candidates.get(&solvable_id)) { - reported.extend(merged.ids.iter().copied().map(InternalSolvableId::from)); + reported.extend(merged.ids.iter().copied().map(SolvableOrRootId::from)); self.interner .display_merged_solvables(&merged.ids) .to_string() - } else if let Some(solvable_id) = solvable_id.as_solvable() { + } else if let Some(solvable_id) = solvable_id.solvable() { self.interner .display_merged_solvables(&[solvable_id]) .to_string() @@ -1001,7 +1041,7 @@ impl<'i, I: Interner> fmt::Display for DisplayUnsat<'i, I> { writeln!( f, "{indent}{} is locked, but another version is required as reported above", - self.interner.display_merged_solvables(&[solvable_id.as_solvable().expect("root is never locked")]), + self.interner.display_merged_solvables(&[solvable_id]), )?; } ConflictCause::Excluded => continue, diff --git a/src/internal/id.rs b/src/internal/id.rs index 6d1d33c..47fe226 100644 --- a/src/internal/id.rs +++ b/src/internal/id.rs @@ -80,76 +80,6 @@ impl ArenaId for VersionSetUnionId { #[cfg_attr(feature = "serde", serde(transparent))] pub struct SolvableId(pub u32); -/// Internally used id for solvables that can also represent the root. -#[repr(transparent)] -#[derive(Copy, Clone, Eq, PartialEq, Hash, Debug, Ord, PartialOrd)] -pub(crate) struct InternalSolvableId(pub u32); -const INTERNAL_SOLVABLE_ROOT: u32 = 0; - -impl InternalSolvableId { - /// Returns the id of the "root" solvable. This is a special solvable that - /// is always present when solving. - pub const fn root() -> Self { - Self(0) - } - - /// Returns if this id represents the root solvable. - pub const fn is_root(self) -> bool { - self.0 == 0 - } - - pub const fn as_solvable(self) -> Option { - match self.0 { - INTERNAL_SOLVABLE_ROOT => None, - x => Some(SolvableId(x - 1)), - } - } - - pub fn display(self, interner: &I) -> impl std::fmt::Display + '_ { - DisplayInternalSolvable { interner, id: self } - } -} - -pub struct DisplayInternalSolvable<'i, I: Interner> { - interner: &'i I, - id: InternalSolvableId, -} - -impl<'i, I: Interner> Display for DisplayInternalSolvable<'i, I> { - fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { - match self.id.0 { - INTERNAL_SOLVABLE_ROOT => write!(f, ""), - x => { - write!(f, "{}", self.interner.display_solvable(SolvableId(x - 1))) - } - } - } -} - -impl From for InternalSolvableId { - fn from(value: SolvableId) -> Self { - Self(value.0 + 1) - } -} - -impl TryFrom for SolvableId { - type Error = (); - - fn try_from(value: InternalSolvableId) -> Result { - value.as_solvable().ok_or(()) - } -} - -impl ArenaId for InternalSolvableId { - fn from_usize(x: usize) -> Self { - Self(x as u32) - } - - fn to_usize(self) -> usize { - self.0 as usize - } -} - impl ArenaId for SolvableId { fn from_usize(x: usize) -> Self { Self(x as u32) @@ -232,6 +162,106 @@ impl ArenaId for DependenciesId { } } +/// A unique identifier for a variable in the solver. +#[repr(transparent)] +#[derive(Copy, Clone, Debug, Eq, PartialEq, Hash, PartialOrd, Ord)] +pub struct VariableId(u32); + +impl VariableId { + pub fn root() -> Self { + Self(0) + } + + pub fn is_root(self) -> bool { + self.0 == 0 + } +} + +impl ArenaId for VariableId { + #[inline] + fn from_usize(x: usize) -> Self { + Self(x.try_into().expect("variable id too big")) + } + + #[inline] + fn to_usize(self) -> usize { + self.0 as usize + } +} + +impl SolvableId { + pub(crate) fn display(self, interner: &I) -> impl Display + '_ { + DisplaySolvableId { + interner, + solvable_id: self, + } + } +} + +pub(crate) struct DisplaySolvableId<'i, I: Interner> { + interner: &'i I, + solvable_id: SolvableId, +} + +impl<'i, I: Interner> Display for DisplaySolvableId<'i, I> { + fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { + write!(f, "{}", self.interner.display_solvable(self.solvable_id)) + } +} + +#[repr(transparent)] +#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] +pub(crate) struct SolvableOrRootId(u32); + +impl SolvableOrRootId { + pub fn root() -> Self { + Self(0) + } + + pub fn is_root(self) -> bool { + self.0 == 0 + } + + pub fn solvable(self) -> Option { + if self.0 == 0 { + None + } else { + Some(SolvableId(self.0 - 1)) + } + } + + pub fn display(self, interner: &I) -> impl Display + '_ { + DisplaySolvableOrRootId { + interner, + solvable_id: self, + } + } +} + +impl From for SolvableOrRootId { + fn from(value: SolvableId) -> Self { + Self( + (value.to_usize() + 1) + .try_into() + .expect("solvable id too big"), + ) + } +} + +pub(crate) struct DisplaySolvableOrRootId<'i, I: Interner> { + interner: &'i I, + solvable_id: SolvableOrRootId, +} + +impl<'i, I: Interner> Display for DisplaySolvableOrRootId<'i, I> { + fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { + match self.solvable_id.solvable() { + Some(solvable_id) => write!(f, "{}", self.interner.display_solvable(solvable_id)), + None => write!(f, "root"), + } + } +} + #[cfg(test)] mod tests { use super::*; diff --git a/src/lib.rs b/src/lib.rs index ece1a5e..575c678 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -91,6 +91,9 @@ pub trait Interner { fn solvable_name(&self, solvable: SolvableId) -> NameId; /// Returns the version sets comprising the given union. + /// + /// The implementor must take care that the order in which the version sets + /// are returned is deterministic. fn version_sets_in_union( &self, version_set_union: VersionSetUnionId, diff --git a/src/solver/binary_encoding.rs b/src/solver/binary_encoding.rs new file mode 100644 index 0000000..144d93c --- /dev/null +++ b/src/solver/binary_encoding.rs @@ -0,0 +1,167 @@ +use std::hash::Hash; + +use indexmap::IndexSet; + +/// An object that is responsible for incrementally building clauses to enforce +/// that at most one of a set of variables can be true. +pub(crate) struct AtMostOnceTracker { + /// The set of variables of which at most one can be assigned true. + variables: IndexSet, + helpers: Vec, +} + +impl Default for AtMostOnceTracker { + fn default() -> Self { + Self { + variables: IndexSet::default(), + helpers: Vec::new(), + } + } +} + +impl AtMostOnceTracker { + /// Add a `variable` to the set of variables of which at most one can be + /// assigned true. + /// + /// `alloc_clause` is a closure that is called to allocate a new clause to + /// enforce (¬A ∨ B?). Where B is either positive or negative based on the + /// value passed to the closure. + pub fn add( + &mut self, + variable: V, + mut alloc_clause: impl FnMut(V, V, bool), + mut alloc_var: impl FnMut() -> V, + ) { + // If the variable is already tracked, we don't need to do anything. + if self.variables.contains(&variable) { + return; + } + + // If there are no variables yet, it means that this is the first variable that + // is added. A single variable can never be in conflict with itself so we don't + // need to add any clauses. + if self.variables.is_empty() { + self.variables.insert(variable.clone()); + return; + } + + // Allocate additional helper variables as needed and create clauses for the + // preexisting variables. + while self.variables.len() > (1 << self.helpers.len()) - 1 { + // Allocate the helper variable + let helper_var = alloc_var(); + let bit_idx = self.helpers.len(); + self.helpers.push(helper_var.clone()); + + // Add a negative clause for all existing variables. + let mask = 1 << bit_idx; + for (idx, var) in self.variables.iter().cloned().enumerate() { + alloc_clause(var, helper_var.clone(), (idx & mask) == mask); + } + } + + let var_idx = self.variables.len(); + self.variables.insert(variable.clone()); + for (bit_idx, helper_var) in self.helpers.iter().enumerate() { + alloc_clause( + variable.clone(), + helper_var.clone(), + ((var_idx >> bit_idx) & 1) == 1, + ); + } + } +} + +#[cfg(test)] +mod test { + use std::fmt::{Display, Formatter}; + + use itertools::Itertools; + + use super::*; + + #[derive(Hash, Eq, PartialEq, Clone)] + enum Variable { + Concrete(usize), + Variable(usize), + } + + impl Display for Variable { + fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { + match self { + Variable::Concrete(id) => write!(f, "x{}", id), + Variable::Variable(id) => write!(f, "v{}", id), + } + } + } + + struct Variables { + next_concrete: usize, + next_variable: usize, + } + + impl Variables { + fn new() -> Self { + Self { + next_concrete: 1, + next_variable: 1, + } + } + + fn concrete(&mut self) -> Variable { + let id = self.next_concrete; + self.next_concrete += 1; + Variable::Concrete(id) + } + + fn variable(&mut self) -> Variable { + let id = self.next_variable; + self.next_variable += 1; + Variable::Variable(id) + } + } + + struct NotBothClause { + a: Variable, + b: Variable, + positive: bool, + } + + impl Display for NotBothClause { + fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { + write!( + f, + "¬{} ∨ {}{}", + self.a, + if self.positive { "" } else { "¬" }, + self.b + ) + } + } + + #[test] + fn test_at_most_once_tracker() { + let mut clauses = Vec::new(); + let mut variables = Variables::new(); + let mut tracker = AtMostOnceTracker::default(); + + let mut add_new_var = || { + let var = variables.concrete(); + tracker.add( + var.clone(), + |a, b, positive| { + clauses.push(NotBothClause { a, b, positive }); + }, + || variables.variable(), + ); + var + }; + + add_new_var(); + add_new_var(); + add_new_var(); + add_new_var(); + + insta::assert_snapshot!(clauses.iter().format("\n")); + } +} diff --git a/src/solver/cache.rs b/src/solver/cache.rs index 0a35b5a..cf6c6cc 100644 --- a/src/solver/cache.rs +++ b/src/solver/cache.rs @@ -34,8 +34,7 @@ pub struct SolverCache { /// A mapping of [`Requirement`] to a sorted list of candidates that fulfill /// that requirement. - pub(crate) requirement_to_sorted_candidates: - FrozenMap, ahash::RandomState>, + requirement_to_sorted_candidates: FrozenMap, ahash::RandomState>, /// A mapping from a solvable to a list of dependencies solvable_dependencies: Arena, @@ -53,7 +52,6 @@ impl SolverCache { pub fn new(provider: D) -> Self { Self { provider, - candidates: Default::default(), package_name_to_candidates: Default::default(), package_name_to_candidates_in_flight: Default::default(), @@ -287,7 +285,7 @@ impl SolverCache { /// Returns the sorted candidates for a singular version set requirement /// (akin to a [`Requirement::Single`]). - async fn get_or_cache_sorted_candidates_for_version_set( + pub(crate) async fn get_or_cache_sorted_candidates_for_version_set( &self, version_set_id: VersionSetId, ) -> Result<&[SolvableId], Box> { diff --git a/src/solver/clause.rs b/src/solver/clause.rs index 7624d6d..4ccc610 100644 --- a/src/solver/clause.rs +++ b/src/solver/clause.rs @@ -9,10 +9,13 @@ use elsa::FrozenMap; use crate::{ internal::{ arena::{Arena, ArenaId}, - id::{ClauseId, InternalSolvableId, LearntClauseId, StringId, VersionSetId}, + id::{ClauseId, LearntClauseId, StringId, VersionSetId}, }, - solver::{decision_map::DecisionMap, decision_tracker::DecisionTracker}, - Interner, NameId, Requirement, SolvableId, + solver::{ + decision_map::DecisionMap, decision_tracker::DecisionTracker, variable_map::VariableMap, + VariableId, + }, + Interner, NameId, Requirement, }; /// Represents a single clause in the SAT problem @@ -30,7 +33,7 @@ use crate::{ /// /// For additional clarity: if `(¬A ∨ ¬B)` is a clause, `¬A` and `¬B` are its /// literals, and `A` and `B` are variables. In our implementation, variables -/// are represented by [`InternalSolvableId`], and assignments are tracked in +/// are represented by [`VariableId`], and assignments are tracked in /// the [`DecisionMap`]. /// /// The solver will attempt to assign values to the variables involved in the @@ -53,7 +56,7 @@ pub(crate) enum Clause { /// /// In SAT terms: (¬A ∨ B1 ∨ B2 ∨ ... ∨ B99), where B1 to B99 represent the /// possible candidates for the provided [`Requirement`]. - Requires(InternalSolvableId, Requirement), + Requires(VariableId, Requirement), /// Ensures only a single version of a package is installed /// /// Usage: generate one [`Clause::ForbidMultipleInstances`] clause for each @@ -61,7 +64,7 @@ pub(crate) enum Clause { /// itself forbids two solvables from being installed at the same time. /// /// In SAT terms: (¬A ∨ ¬B) - ForbidMultipleInstances(InternalSolvableId, InternalSolvableId, NameId), + ForbidMultipleInstances(VariableId, Literal, NameId), /// Forbids packages that do not satisfy a solvable's constrains /// /// Usage: for each constrains relationship in a package, determine all the @@ -72,7 +75,7 @@ pub(crate) enum Clause { /// separate variant for user-friendly error messages. /// /// In SAT terms: (¬A ∨ ¬B) - Constrains(InternalSolvableId, InternalSolvableId, VersionSetId), + Constrains(VariableId, VariableId, VersionSetId), /// Forbids the package on the right-hand side /// /// Note that the package on the left-hand side is not part of the clause, @@ -82,7 +85,7 @@ pub(crate) enum Clause { /// In SAT terms: (¬root ∨ ¬B). Note that we could encode this as an /// assertion (¬B), but that would require additional logic in the /// solver. - Lock(InternalSolvableId, InternalSolvableId), + Lock(VariableId, VariableId), /// A clause learnt during solving /// /// The learnt clause id can be used to retrieve the clause's literals, @@ -92,7 +95,7 @@ pub(crate) enum Clause { /// A clause that forbids a package from being installed for an external /// reason. - Excluded(InternalSolvableId, StringId), + Excluded(VariableId, StringId), } impl Clause { @@ -109,9 +112,9 @@ impl Clause { /// starting the solving process, but can be true for clauses that are /// added dynamically. fn requires( - parent: InternalSolvableId, + parent: VariableId, requirement: Requirement, - candidates: &[SolvableId], + candidates: impl IntoIterator, decision_tracker: &DecisionTracker, ) -> (Self, Option<[Literal; 2]>, bool) { // It only makes sense to introduce a requires clause when the parent solvable @@ -119,16 +122,10 @@ impl Clause { assert_ne!(decision_tracker.assigned_value(parent), Some(false)); let kind = Clause::Requires(parent, requirement); - if candidates.is_empty() { - // If there are no candidates there is no need to watch anything. - (kind, None, false) - } else { - match candidates - .iter() - .copied() - .map(InternalSolvableId::from) - .find(|&c| decision_tracker.assigned_value(c) != Some(false)) - { + let mut candidates = candidates.into_iter().peekable(); + let first_candidate = candidates.peek().copied(); + if let Some(first_candidate) = first_candidate { + match candidates.find(|&c| decision_tracker.assigned_value(c) != Some(false)) { // Watch any candidate that is not assigned to false Some(watched_candidate) => ( kind, @@ -142,13 +139,13 @@ impl Clause { // restarts. None => ( kind, - Some([ - parent.negative(), - InternalSolvableId::from(candidates[0]).positive(), - ]), + Some([parent.negative(), first_candidate.positive()]), true, ), } + } else { + // If there are no candidates there is no need to watch anything. + (kind, None, false) } } @@ -164,8 +161,8 @@ impl Clause { /// starting the solving process, but can be true for clauses that are /// added dynamically. fn constrains( - parent: InternalSolvableId, - forbidden_solvable: InternalSolvableId, + parent: VariableId, + forbidden_solvable: VariableId, via: VersionSetId, decision_tracker: &DecisionTracker, ) -> (Self, Option<[Literal; 2]>, bool) { @@ -188,13 +185,13 @@ impl Clause { /// Returns the ids of the solvables that will be watched as well as the /// clause itself. fn forbid_multiple( - candidate: InternalSolvableId, - constrained_candidate: InternalSolvableId, + candidate: VariableId, + constrained_candidate: Literal, name: NameId, ) -> (Self, Option<[Literal; 2]>) { ( Clause::ForbidMultipleInstances(candidate, constrained_candidate, name), - Some([candidate.negative(), constrained_candidate.negative()]), + Some([candidate.negative(), constrained_candidate]), ) } @@ -202,20 +199,17 @@ impl Clause { (Clause::InstallRoot, None) } - fn exclude(candidate: InternalSolvableId, reason: StringId) -> (Self, Option<[Literal; 2]>) { + fn exclude(candidate: VariableId, reason: StringId) -> (Self, Option<[Literal; 2]>) { (Clause::Excluded(candidate, reason), None) } fn lock( - locked_candidate: InternalSolvableId, - other_candidate: InternalSolvableId, + locked_candidate: VariableId, + other_candidate: VariableId, ) -> (Self, Option<[Literal; 2]>) { ( Clause::Lock(locked_candidate, other_candidate), - Some([ - InternalSolvableId::root().negative(), - other_candidate.negative(), - ]), + Some([VariableId::root().negative(), other_candidate.negative()]), ) } @@ -244,7 +238,7 @@ impl Clause { learnt_clauses: &Arena>, requirements_to_sorted_candidates: &FrozenMap< Requirement, - Vec, + Vec>, ahash::RandomState, >, init: C, @@ -264,15 +258,17 @@ impl Clause { .chain( requirements_to_sorted_candidates[&match_spec_id] .iter() - .map(|&s| InternalSolvableId::from(s).positive()), + .flatten() + .map(|&s| s.positive()), ) .try_fold(init, visit), - Clause::Constrains(s1, s2, _) | Clause::ForbidMultipleInstances(s1, s2, _) => { - [s1.negative(), s2.negative()] - .into_iter() - .try_fold(init, visit) + Clause::Constrains(s1, s2, _) => [s1.negative(), s2.negative()] + .into_iter() + .try_fold(init, visit), + Clause::ForbidMultipleInstances(s1, s2, _) => { + [s1.negative(), s2].into_iter().try_fold(init, visit) } - Clause::Lock(_, s) => [s.negative(), InternalSolvableId::root().negative()] + Clause::Lock(_, s) => [s.negative(), VariableId::root().negative()] .into_iter() .try_fold(init, visit), } @@ -286,7 +282,7 @@ impl Clause { learnt_clauses: &Arena>, requirements_to_sorted_candidates: &FrozenMap< Requirement, - Vec, + Vec>, ahash::RandomState, >, mut visit: impl FnMut(Literal), @@ -303,9 +299,14 @@ impl Clause { } /// Construct a [`ClauseDisplay`] to display the clause. - pub fn display<'i, I: Interner>(&self, interner: &'i I) -> ClauseDisplay<'i, I> { + pub fn display<'i, I: Interner>( + &self, + variable_map: &'i VariableMap, + interner: &'i I, + ) -> ClauseDisplay<'i, I> { ClauseDisplay { kind: *self, + variable_map, interner, } } @@ -321,7 +322,7 @@ impl Clause { /// them all. #[derive(Clone)] pub(crate) struct ClauseState { - // The ids of the solvables this clause is watching + // The ids of the literals this clause is watching pub watched_literals: [Literal; 2], // The ids of the next clause in each linked list that this clause is part of pub(crate) next_watches: [Option; 2], @@ -341,9 +342,9 @@ impl ClauseState { /// The returned boolean value is true when adding the clause resulted in a /// conflict. pub fn requires( - candidate: InternalSolvableId, + candidate: VariableId, requirement: Requirement, - matching_candidates: &[SolvableId], + matching_candidates: impl IntoIterator, decision_tracker: &DecisionTracker, ) -> (Self, bool, Clause) { let (kind, watched_literals, conflict) = Clause::requires( @@ -366,8 +367,8 @@ impl ClauseState { /// The returned boolean value is true when adding the clause resulted in a /// conflict. pub fn constrains( - candidate: InternalSolvableId, - constrained_package: InternalSolvableId, + candidate: VariableId, + constrained_package: VariableId, requirement: VersionSetId, decision_tracker: &DecisionTracker, ) -> (Self, bool, Clause) { @@ -385,17 +386,14 @@ impl ClauseState { ) } - pub fn lock( - locked_candidate: InternalSolvableId, - other_candidate: InternalSolvableId, - ) -> (Self, Clause) { + pub fn lock(locked_candidate: VariableId, other_candidate: VariableId) -> (Self, Clause) { let (kind, watched_literals) = Clause::lock(locked_candidate, other_candidate); (Self::from_kind_and_initial_watches(watched_literals), kind) } pub fn forbid_multiple( - candidate: InternalSolvableId, - other_candidate: InternalSolvableId, + candidate: VariableId, + other_candidate: Literal, name: NameId, ) -> (Self, Clause) { let (kind, watched_literals) = Clause::forbid_multiple(candidate, other_candidate, name); @@ -407,7 +405,7 @@ impl ClauseState { (Self::from_kind_and_initial_watches(watched_literals), kind) } - pub fn exclude(candidate: InternalSolvableId, reason: StringId) -> (Self, Clause) { + pub fn exclude(candidate: VariableId, reason: StringId) -> (Self, Clause) { let (kind, watched_literals) = Clause::exclude(candidate, reason); (Self::from_kind_and_initial_watches(watched_literals), kind) } @@ -425,30 +423,26 @@ impl ClauseState { clause } - pub fn link_to_clause(&mut self, watch_index: usize, linked_clause: Option) { - self.next_watches[watch_index] = linked_clause; - } - pub fn unlink_clause( &mut self, linked_clause: &ClauseState, - watched_solvable: InternalSolvableId, + watched_solvable: VariableId, linked_clause_watch_index: usize, ) { - if self.watched_literals[0].solvable_id() == watched_solvable { + if self.watched_literals[0].variable() == watched_solvable { self.next_watches[0] = linked_clause.next_watches[linked_clause_watch_index]; } else { - debug_assert_eq!(self.watched_literals[1].solvable_id(), watched_solvable); + debug_assert_eq!(self.watched_literals[1].variable(), watched_solvable); self.next_watches[1] = linked_clause.next_watches[linked_clause_watch_index]; } } #[inline] - pub fn next_watched_clause(&self, solvable_id: InternalSolvableId) -> Option { - if solvable_id == self.watched_literals[0].solvable_id() { + pub fn next_watched_clause(&self, solvable_id: VariableId) -> Option { + if solvable_id == self.watched_literals[0].variable() { self.next_watches[0] } else { - debug_assert_eq!(self.watched_literals[1].solvable_id(), solvable_id); + debug_assert_eq!(self.watched_literals[1].variable(), solvable_id); self.next_watches[1] } } @@ -464,7 +458,7 @@ impl ClauseState { learnt_clauses: &Arena>, requirement_to_sorted_candidates: &FrozenMap< Requirement, - Vec, + Vec>, ahash::RandomState, >, decision_map: &DecisionMap, @@ -488,8 +482,7 @@ impl ClauseState { // The next unwatched variable (if available), is a variable that is: // * Not already being watched // * Not yet decided, or decided in such a way that the literal yields true - if self.watched_literals[other_watch_index].solvable_id() - != lit.solvable_id() + if self.watched_literals[other_watch_index].variable() != lit.variable() && lit.eval(decision_map).unwrap_or(true) { ControlFlow::Break(lit) @@ -508,15 +501,17 @@ impl ClauseState { } /// Represents a literal in a SAT clause (i.e. either A or ¬A) +#[repr(transparent)] #[derive(Debug, Copy, Clone, Eq, PartialEq)] pub(crate) struct Literal(u32); impl Literal { - /// Constructs a new [`Literal`] from a [`InternalSolvableId`] and a boolean + /// Constructs a new [`Literal`] from a [`VariableId`] and a boolean /// indicating whether the literal should be negated. - pub fn new(solvable_id: InternalSolvableId, negate: bool) -> Self { - assert!(solvable_id.0 < (u32::MAX >> 1) - 1, "solvable id too big"); - Self(solvable_id.0 << 1 | negate as u32) + pub fn new(variable: VariableId, negate: bool) -> Self { + let variable_idx = variable.to_usize(); + let literal_idx = variable_idx << 1 | negate as usize; + Self(literal_idx.try_into().expect("literal id too big")) } } @@ -552,8 +547,9 @@ impl Literal { /// Returns the value that would make the literal evaluate to true if /// assigned to the literal's solvable - pub(crate) fn solvable_id(self) -> InternalSolvableId { - InternalSolvableId(self.0 >> 1) + #[inline] + pub(crate) fn variable(self) -> VariableId { + VariableId::from_usize((self.0 >> 1) as usize) } /// Evaluates the literal, or returns `None` if no value has been assigned @@ -561,12 +557,12 @@ impl Literal { #[inline(always)] pub(crate) fn eval(self, decision_map: &DecisionMap) -> Option { decision_map - .value(self.solvable_id()) + .value(self.variable()) .map(|value| value != self.negate()) } } -impl InternalSolvableId { +impl VariableId { /// Constructs a [`Literal`] that indicates this solvable should be assigned /// a positive value. pub fn positive(self) -> Literal { @@ -584,50 +580,51 @@ impl InternalSolvableId { pub(crate) struct ClauseDisplay<'i, I: Interner> { kind: Clause, interner: &'i I, + variable_map: &'i VariableMap, } impl<'i, I: Interner> Display for ClauseDisplay<'i, I> { fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { match self.kind { Clause::InstallRoot => write!(f, "InstallRoot"), - Clause::Excluded(solvable_id, reason) => { + Clause::Excluded(variable, reason) => { write!( f, "Excluded({}({:?}), {})", - solvable_id.display(self.interner), - solvable_id, + variable.display(self.variable_map, self.interner), + variable, self.interner.display_string(reason) ) } Clause::Learnt(learnt_id) => write!(f, "Learnt({learnt_id:?})"), - Clause::Requires(solvable_id, requirement) => { + Clause::Requires(variable, requirement) => { write!( f, "Requires({}({:?}), {})", - solvable_id.display(self.interner), - solvable_id, + variable.display(self.variable_map, self.interner), + variable, requirement.display(self.interner), ) } - Clause::Constrains(s1, s2, version_set_id) => { + Clause::Constrains(v1, v2, version_set_id) => { write!( f, "Constrains({}({:?}), {}({:?}), {})", - s1.display(self.interner), - s1, - s2.display(self.interner), - s2, + v1.display(self.variable_map, self.interner), + v1, + v2.display(self.variable_map, self.interner), + v2, self.interner.display_version_set(version_set_id) ) } - Clause::ForbidMultipleInstances(s1, s2, name) => { + Clause::ForbidMultipleInstances(v1, v2, name) => { write!( f, "ForbidMultipleInstances({}({:?}), {}({:?}), {})", - s1.display(self.interner), - s1, - s2.display(self.interner), - s2, + v1.display(self.variable_map, self.interner), + v1, + v2.variable().display(self.variable_map, self.interner), + v2, self.interner.display_name(name) ) } @@ -635,9 +632,9 @@ impl<'i, I: Interner> Display for ClauseDisplay<'i, I> { write!( f, "Lock({}({:?}), {}({:?}))", - locked.display(self.interner), + locked.display(self.variable_map, self.interner), locked, - other.display(self.interner), + other.display(self.variable_map, self.interner), other, ) } @@ -660,10 +657,10 @@ mod test { #[test] #[allow(clippy::bool_assert_comparison)] fn test_literal_satisfying_value() { - let lit = InternalSolvableId::root().negative(); + let lit = VariableId::root().negative(); assert_eq!(lit.satisfying_value(), false); - let lit = InternalSolvableId::root().positive(); + let lit = VariableId::root().positive(); assert_eq!(lit.satisfying_value(), true); } @@ -671,19 +668,19 @@ mod test { fn test_literal_eval() { let mut decision_map = DecisionMap::new(); - let literal = InternalSolvableId::root().positive(); - let negated_literal = InternalSolvableId::root().negative(); + let literal = VariableId::root().positive(); + let negated_literal = VariableId::root().negative(); // Undecided assert_eq!(literal.eval(&decision_map), None); assert_eq!(negated_literal.eval(&decision_map), None); // Decided - decision_map.set(InternalSolvableId::root(), true, 1); + decision_map.set(VariableId::root(), true, 1); assert_eq!(literal.eval(&decision_map), Some(true)); assert_eq!(negated_literal.eval(&decision_map), Some(false)); - decision_map.set(InternalSolvableId::root(), false, 1); + decision_map.set(VariableId::root(), false, 1); assert_eq!(literal.eval(&decision_map), Some(false)); assert_eq!(negated_literal.eval(&decision_map), Some(true)); } @@ -696,34 +693,34 @@ mod test { ClauseId::from_usize(3).into(), ], [ - InternalSolvableId::from_usize(1596).negative(), - InternalSolvableId::from_usize(1211).negative(), + VariableId::from_usize(1596).negative(), + VariableId::from_usize(1211).negative(), ], ); let clause2 = clause( [None, ClauseId::from_usize(3).into()], [ - InternalSolvableId::from_usize(1596).negative(), - InternalSolvableId::from_usize(1208).negative(), + VariableId::from_usize(1596).negative(), + VariableId::from_usize(1208).negative(), ], ); let clause3 = clause( [None, None], [ - InternalSolvableId::from_usize(1211).negative(), - InternalSolvableId::from_usize(42).negative(), + VariableId::from_usize(1211).negative(), + VariableId::from_usize(42).negative(), ], ); // Unlink 0 { let mut clause1 = clause1.clone(); - clause1.unlink_clause(&clause2, InternalSolvableId::from_usize(1596), 0); + clause1.unlink_clause(&clause2, VariableId::from_usize(1596), 0); assert_eq!( clause1.watched_literals, [ - InternalSolvableId::from_usize(1596).negative(), - InternalSolvableId::from_usize(1211).negative() + VariableId::from_usize(1596).negative(), + VariableId::from_usize(1211).negative() ] ); assert_eq!(clause1.next_watches, [None, ClauseId::from_usize(3).into()]) @@ -732,12 +729,12 @@ mod test { // Unlink 1 { let mut clause1 = clause1; - clause1.unlink_clause(&clause3, InternalSolvableId::from_usize(1211), 0); + clause1.unlink_clause(&clause3, VariableId::from_usize(1211), 0); assert_eq!( clause1.watched_literals, [ - InternalSolvableId::from_usize(1596).negative(), - InternalSolvableId::from_usize(1211).negative() + VariableId::from_usize(1596).negative(), + VariableId::from_usize(1211).negative() ] ); assert_eq!(clause1.next_watches, [ClauseId::from_usize(2).into(), None]) @@ -752,27 +749,27 @@ mod test { ClauseId::from_usize(2).into(), ], [ - InternalSolvableId::from_usize(1596).negative(), - InternalSolvableId::from_usize(1211).negative(), + VariableId::from_usize(1596).negative(), + VariableId::from_usize(1211).negative(), ], ); let clause2 = clause( [None, None], [ - InternalSolvableId::from_usize(1596).negative(), - InternalSolvableId::from_usize(1211).negative(), + VariableId::from_usize(1596).negative(), + VariableId::from_usize(1211).negative(), ], ); // Unlink 0 { let mut clause1 = clause1.clone(); - clause1.unlink_clause(&clause2, InternalSolvableId::from_usize(1596), 0); + clause1.unlink_clause(&clause2, VariableId::from_usize(1596), 0); assert_eq!( clause1.watched_literals, [ - InternalSolvableId::from_usize(1596).negative(), - InternalSolvableId::from_usize(1211).negative() + VariableId::from_usize(1596).negative(), + VariableId::from_usize(1211).negative() ] ); assert_eq!(clause1.next_watches, [None, ClauseId::from_usize(2).into()]) @@ -781,12 +778,12 @@ mod test { // Unlink 1 { let mut clause1 = clause1; - clause1.unlink_clause(&clause2, InternalSolvableId::from_usize(1211), 1); + clause1.unlink_clause(&clause2, VariableId::from_usize(1211), 1); assert_eq!( clause1.watched_literals, [ - InternalSolvableId::from_usize(1596).negative(), - InternalSolvableId::from_usize(1211).negative() + VariableId::from_usize(1596).negative(), + VariableId::from_usize(1211).negative() ] ); assert_eq!(clause1.next_watches, [ClauseId::from_usize(2).into(), None]) @@ -797,20 +794,20 @@ mod test { fn test_requires_with_and_without_conflict() { let mut decisions = DecisionTracker::new(); - let parent = InternalSolvableId::from_usize(1); - let candidate1 = SolvableId::from_usize(2); - let candidate2 = SolvableId::from_usize(3); + let parent = VariableId::from_usize(1); + let candidate1 = VariableId::from_usize(2); + let candidate2 = VariableId::from_usize(3); // No conflict, all candidates available let (clause, conflict, _kind) = ClauseState::requires( parent, VersionSetId::from_usize(0).into(), - &[candidate1, candidate2], + [candidate1, candidate2], &decisions, ); assert!(!conflict); - assert_eq!(clause.watched_literals[0].solvable_id(), parent); - assert_eq!(clause.watched_literals[1].solvable_id(), candidate1.into()); + assert_eq!(clause.watched_literals[0].variable(), parent); + assert_eq!(clause.watched_literals[1].variable(), candidate1.into()); // No conflict, still one candidate available decisions @@ -822,12 +819,12 @@ mod test { let (clause, conflict, _kind) = ClauseState::requires( parent, VersionSetId::from_usize(0).into(), - &[candidate1, candidate2], + [candidate1, candidate2], &decisions, ); assert!(!conflict); - assert_eq!(clause.watched_literals[0].solvable_id(), parent); - assert_eq!(clause.watched_literals[1].solvable_id(), candidate2.into()); + assert_eq!(clause.watched_literals[0].variable(), parent); + assert_eq!(clause.watched_literals[1].variable(), candidate2.into()); // Conflict, no candidates available decisions @@ -839,12 +836,12 @@ mod test { let (clause, conflict, _kind) = ClauseState::requires( parent, VersionSetId::from_usize(0).into(), - &[candidate1, candidate2], + [candidate1, candidate2], &decisions, ); assert!(conflict); - assert_eq!(clause.watched_literals[0].solvable_id(), parent); - assert_eq!(clause.watched_literals[1].solvable_id(), candidate1.into()); + assert_eq!(clause.watched_literals[0].variable(), parent); + assert_eq!(clause.watched_literals[1].variable(), candidate1.into()); // Panic decisions @@ -854,7 +851,7 @@ mod test { ClauseState::requires( parent, VersionSetId::from_usize(0).into(), - &[candidate1, candidate2], + [candidate1, candidate2], &decisions, ) }) @@ -866,15 +863,15 @@ mod test { fn test_constrains_with_and_without_conflict() { let mut decisions = DecisionTracker::new(); - let parent = InternalSolvableId::from_usize(1); - let forbidden = InternalSolvableId::from_usize(2); + let parent = VariableId::from_usize(1); + let forbidden = VariableId::from_usize(2); // No conflict, forbidden package not installed let (clause, conflict, _kind) = ClauseState::constrains(parent, forbidden, VersionSetId::from_usize(0), &decisions); assert!(!conflict); - assert_eq!(clause.watched_literals[0].solvable_id(), parent); - assert_eq!(clause.watched_literals[1].solvable_id(), forbidden); + assert_eq!(clause.watched_literals[0].variable(), parent); + assert_eq!(clause.watched_literals[1].variable(), forbidden); // Conflict, forbidden package installed decisions @@ -883,8 +880,8 @@ mod test { let (clause, conflict, _kind) = ClauseState::constrains(parent, forbidden, VersionSetId::from_usize(0), &decisions); assert!(conflict); - assert_eq!(clause.watched_literals[0].solvable_id(), parent); - assert_eq!(clause.watched_literals[1].solvable_id(), forbidden); + assert_eq!(clause.watched_literals[0].variable(), parent); + assert_eq!(clause.watched_literals[1].variable(), forbidden); // Panic decisions diff --git a/src/solver/decision.rs b/src/solver/decision.rs index 2decdbc..afd12e7 100644 --- a/src/solver/decision.rs +++ b/src/solver/decision.rs @@ -1,17 +1,17 @@ -use crate::internal::id::{ClauseId, InternalSolvableId}; +use crate::internal::id::{ClauseId, VariableId}; /// Represents an assignment to a variable #[derive(Copy, Clone, Eq, PartialEq)] pub(crate) struct Decision { - pub(crate) solvable_id: InternalSolvableId, + pub(crate) variable: VariableId, pub(crate) value: bool, pub(crate) derived_from: ClauseId, } impl Decision { - pub(crate) fn new(solvable: InternalSolvableId, value: bool, derived_from: ClauseId) -> Self { + pub(crate) fn new(variable: VariableId, value: bool, derived_from: ClauseId) -> Self { Self { - solvable_id: solvable, + variable, value, derived_from, } diff --git a/src/solver/decision_map.rs b/src/solver/decision_map.rs index 5522e74..7de521b 100644 --- a/src/solver/decision_map.rs +++ b/src/solver/decision_map.rs @@ -1,13 +1,14 @@ use std::cmp::Ordering; -use crate::internal::{arena::ArenaId, id::InternalSolvableId}; +use crate::internal::arena::ArenaId; +use crate::internal::id::VariableId; -/// Represents a decision (i.e. an assignment to a solvable) and the level at +/// Represents a decision (i.e. an assignment to a variable) and the level at /// which it was made /// /// = 0: undecided -/// > 0: level of decision when the solvable is set to true -/// < 0: level of decision when the solvable is set to false +/// > 0: level of decision when the variable is set to true +/// < 0: level of decision when the variable is set to false #[repr(transparent)] #[derive(Copy, Clone)] struct DecisionAndLevel(i32); @@ -47,37 +48,37 @@ impl DecisionMap { } } - pub fn reset(&mut self, solvable_id: InternalSolvableId) { - let solvable_id = solvable_id.to_usize(); - if solvable_id < self.map.len() { + pub fn reset(&mut self, variable_id: VariableId) { + let variable_id = variable_id.to_usize(); + if variable_id < self.map.len() { // SAFE: because we check that the solvable id is within bounds - unsafe { *self.map.get_unchecked_mut(solvable_id) = DecisionAndLevel::undecided() }; + unsafe { *self.map.get_unchecked_mut(variable_id) = DecisionAndLevel::undecided() }; } } - pub fn set(&mut self, solvable_id: InternalSolvableId, value: bool, level: u32) { - let solvable_id = solvable_id.to_usize(); - if solvable_id >= self.map.len() { + pub fn set(&mut self, variable_id: VariableId, value: bool, level: u32) { + let variable_id = variable_id.to_usize(); + if variable_id >= self.map.len() { self.map - .resize_with(solvable_id + 1, DecisionAndLevel::undecided); + .resize_with(variable_id + 1, DecisionAndLevel::undecided); } // SAFE: because we ensured that vec contains at least the correct number of // elements. unsafe { - *self.map.get_unchecked_mut(solvable_id) = + *self.map.get_unchecked_mut(variable_id) = DecisionAndLevel::with_value_and_level(value, level) }; } - pub fn level(&self, solvable_id: InternalSolvableId) -> u32 { + pub fn level(&self, variable_id: VariableId) -> u32 { self.map - .get(solvable_id.to_usize()) + .get(variable_id.to_usize()) .map_or(0, |d| d.level()) } #[inline(always)] - pub fn value(&self, solvable_id: InternalSolvableId) -> Option { - self.map.get(solvable_id.to_usize()).and_then(|d| d.value()) + pub fn value(&self, variable_id: VariableId) -> Option { + self.map.get(variable_id.to_usize()).and_then(|d| d.value()) } } diff --git a/src/solver/decision_tracker.rs b/src/solver/decision_tracker.rs index 23995d3..8fcc8cd 100644 --- a/src/solver/decision_tracker.rs +++ b/src/solver/decision_tracker.rs @@ -1,8 +1,5 @@ -use crate::internal::id::ClauseId; -use crate::{ - internal::id::InternalSolvableId, - solver::{decision::Decision, decision_map::DecisionMap}, -}; +use crate::internal::id::{ClauseId, VariableId}; +use crate::solver::{decision::Decision, decision_map::DecisionMap}; /// Tracks the assignments to solvables, keeping a log that can be used to backtrack, and a map that /// can be used to query the current value assigned @@ -28,8 +25,8 @@ impl DecisionTracker { } #[inline(always)] - pub(crate) fn assigned_value(&self, solvable_id: InternalSolvableId) -> Option { - self.map.value(solvable_id) + pub(crate) fn assigned_value(&self, variable_id: VariableId) -> Option { + self.map.value(variable_id) } pub(crate) fn map(&self) -> &DecisionMap { @@ -40,19 +37,16 @@ impl DecisionTracker { self.stack.iter().copied() } - pub(crate) fn level(&self, solvable_id: InternalSolvableId) -> u32 { - self.map.level(solvable_id) + pub(crate) fn level(&self, variable_id: VariableId) -> u32 { + self.map.level(variable_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: InternalSolvableId, - ) -> Option { + pub(crate) fn find_clause_for_assignment(&self, variable_id: VariableId) -> Option { self.stack .iter() - .find(|d| d.solvable_id == solvable_id) + .find(|d| d.variable == variable_id) .map(|d| d.derived_from) } @@ -62,9 +56,9 @@ impl DecisionTracker { /// /// Returns an error if the solvable was decided to a different value (which means there is a conflict) pub(crate) fn try_add_decision(&mut self, decision: Decision, level: u32) -> Result { - match self.map.value(decision.solvable_id) { + match self.map.value(decision.variable) { None => { - self.map.set(decision.solvable_id, decision.value, level); + self.map.set(decision.variable, decision.value, level); self.stack.push(decision); Ok(true) } @@ -80,7 +74,7 @@ impl DecisionTracker { } while let Some(decision) = self.stack.last() { - if self.level(decision.solvable_id) <= level { + if self.level(decision.variable) <= level { break; } @@ -90,12 +84,12 @@ impl DecisionTracker { pub(crate) fn undo_last(&mut self) -> (Decision, u32) { let decision = self.stack.pop().unwrap(); - self.map.reset(decision.solvable_id); + self.map.reset(decision.variable); self.propagate_index = self.stack.len(); let top_decision = self.stack.last().unwrap(); - (decision, self.map.level(top_decision.solvable_id)) + (decision, self.map.level(top_decision.variable)) } /// Returns the next decision in the log for which unit propagation still needs to run diff --git a/src/solver/mod.rs b/src/solver/mod.rs index 271a5b6..9fca0bf 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -1,38 +1,43 @@ -use std::{any::Any, cell::RefCell, fmt::Display, future::ready, ops::ControlFlow}; +use std::{any::Any, fmt::Display, future::ready, ops::ControlFlow}; use ahash::{HashMap, HashSet}; pub use cache::SolverCache; use clause::{Clause, ClauseState, Literal}; use decision::Decision; use decision_tracker::DecisionTracker; +use elsa::FrozenMap; use futures::{stream::FuturesUnordered, FutureExt, StreamExt}; -use indexmap::{IndexMap, IndexSet}; +use indexmap::IndexMap; use itertools::Itertools; +use variable_map::VariableMap; use watch_map::WatchMap; use crate::{ conflict::Conflict, internal::{ arena::{Arena, ArenaId}, - id::{ClauseId, InternalSolvableId, LearntClauseId, NameId, SolvableId}, + id::{ClauseId, LearntClauseId, NameId, SolvableId, SolvableOrRootId, VariableId}, mapping::Mapping, }, runtime::{AsyncRuntime, NowOrNeverRuntime}, + solver::binary_encoding::AtMostOnceTracker, Candidates, Dependencies, DependencyProvider, KnownDependencies, Requirement, VersionSetId, }; +mod binary_encoding; mod cache; pub(crate) mod clause; mod decision; mod decision_map; mod decision_tracker; +pub(crate) mod variable_map; mod watch_map; #[derive(Default)] struct AddClauseOutput { - new_requires_clauses: Vec<(InternalSolvableId, Requirement, ClauseId)>, + new_requires_clauses: Vec<(VariableId, Requirement, ClauseId)>, conflicting_clauses: Vec, - negative_assertions: Vec<(InternalSolvableId, ClauseId)>, + negative_assertions: Vec<(VariableId, ClauseId)>, clauses_to_watch: Vec, new_names: Vec, } @@ -123,40 +128,46 @@ impl> Problem { #[derive(Default)] pub(crate) struct Clauses { - pub(crate) kinds: RefCell>, - states: RefCell>, + pub(crate) kinds: Vec, + states: Vec, } impl Clauses { - pub fn alloc(&self, state: ClauseState, kind: Clause) -> ClauseId { - let mut kinds = self.kinds.borrow_mut(); - let mut states = self.states.borrow_mut(); - let id = ClauseId::from_usize(kinds.len()); - kinds.push(kind); - states.push(state); + pub fn alloc(&mut self, state: ClauseState, kind: Clause) -> ClauseId { + let id = ClauseId::from_usize(self.kinds.len()); + self.kinds.push(kind); + self.states.push(state); id } } +type RequirementCandidateVariables = Vec>; + /// Drives the SAT solving process. pub struct Solver { pub(crate) async_runtime: RT, pub(crate) cache: SolverCache, pub(crate) clauses: Clauses, - requires_clauses: - IndexMap, ahash::RandomState>, + requires_clauses: IndexMap, ahash::RandomState>, watches: WatchMap, - negative_assertions: Vec<(InternalSolvableId, ClauseId)>, + /// A mapping from requirements to the variables that represent the + /// candidates. + requirement_to_sorted_candidates: + FrozenMap, + + pub(crate) variable_map: VariableMap, + + negative_assertions: Vec<(VariableId, ClauseId)>, learnt_clauses: Arena>, learnt_why: Mapping>, learnt_clause_ids: Vec, - clauses_added_for_package: RefCell>, - clauses_added_for_solvable: RefCell>, - forbidden_clauses_added: RefCell>>, + clauses_added_for_package: HashSet, + clauses_added_for_solvable: HashSet, + forbidden_clauses_added: HashMap>, decision_tracker: DecisionTracker, @@ -187,7 +198,9 @@ impl Solver { cache: SolverCache::new(provider), async_runtime: NowOrNeverRuntime, clauses: Clauses::default(), + variable_map: VariableMap::default(), requires_clauses: Default::default(), + requirement_to_sorted_candidates: FrozenMap::default(), watches: WatchMap::new(), negative_assertions: Default::default(), learnt_clauses: Arena::new(), @@ -231,7 +244,7 @@ impl From> for UnsolvableOrCancelled { /// An error during the propagation step #[derive(Debug)] pub(crate) enum PropagationError { - Conflict(InternalSolvableId, bool, ClauseId), + Conflict(VariableId, bool, ClauseId), Cancelled(Box), } @@ -265,7 +278,9 @@ impl Solver { async_runtime: runtime, cache: self.cache, clauses: self.clauses, + variable_map: self.variable_map, requires_clauses: self.requires_clauses, + requirement_to_sorted_candidates: self.requirement_to_sorted_candidates, watches: self.watches, negative_assertions: self.negative_assertions, learnt_clauses: self.learnt_clauses, @@ -343,16 +358,20 @@ impl Solver { assert_eq!(root_clause, ClauseId::install_root()); assert!( - self.run_sat(InternalSolvableId::root())?, + self.run_sat(SolvableOrRootId::root())?, "bug: Since root is the first requested solvable, \ should have returned Err instead of Ok(false) if root is unsolvable" ); for additional in problem.soft_requirements { - let additional = additional.into(); + let additional_var = self.variable_map.intern_solvable(additional); - if self.decision_tracker.assigned_value(additional).is_none() { - self.run_sat(additional)?; + if self + .decision_tracker + .assigned_value(additional_var) + .is_none() + { + self.run_sat(additional.into())?; } } @@ -364,7 +383,7 @@ impl Solver { fn chosen_solvables(&self) -> impl Iterator + '_ { self.decision_tracker.stack().filter_map(|d| { if d.value { - d.solvable_id.as_solvable() + d.variable.as_solvable(&self.variable_map) } else { // Ignore things that are set to false None @@ -372,359 +391,6 @@ impl Solver { }) } - /// Adds clauses for a solvable. These clauses include requirements and - /// constrains on other solvables. - /// - /// Returns the added clauses, and an additional list with conflicting - /// clauses (if any). - /// - /// If the provider has requested the solving process to be cancelled, the - /// cancellation value will be returned as an `Err(...)`. - async fn add_clauses_for_solvables( - &self, - solvable_ids: impl IntoIterator, - ) -> Result> { - let mut output = AddClauseOutput::default(); - - tracing::trace!("Add clauses for solvables"); - - pub enum TaskResult<'i> { - Dependencies { - solvable_id: InternalSolvableId, - dependencies: Dependencies, - }, - SortedCandidates { - solvable_id: InternalSolvableId, - requirement: Requirement, - candidates: &'i [SolvableId], - }, - NonMatchingCandidates { - solvable_id: InternalSolvableId, - version_set_id: VersionSetId, - non_matching_candidates: &'i [SolvableId], - }, - Candidates { - name_id: NameId, - package_candidates: &'i Candidates, - }, - } - - // Mark the initial seen solvables as seen - let mut pending_solvables = vec![]; - { - let mut clauses_added_for_solvable = self.clauses_added_for_solvable.borrow_mut(); - for solvable_id in solvable_ids { - if clauses_added_for_solvable.insert(solvable_id) { - pending_solvables.push(solvable_id); - } - } - } - - let mut seen = pending_solvables.iter().copied().collect::>(); - let mut pending_futures = FuturesUnordered::new(); - loop { - // Iterate over all pending solvables and request their dependencies. - for internal_solvable_id in pending_solvables.drain(..) { - // Get the solvable information and request its requirements and constraints - tracing::trace!( - "┝━ adding clauses for dependencies of {}", - internal_solvable_id.display(self.provider()), - ); - - // If the solvable is the root solvable, we can skip the dependency provider - // and use the root requirements and constraints directly. - let get_dependencies_fut = - if let Some(solvable_id) = internal_solvable_id.as_solvable() { - async move { - let deps = self.cache.get_or_cache_dependencies(solvable_id).await?; - Ok(TaskResult::Dependencies { - solvable_id: internal_solvable_id, - dependencies: deps.clone(), - }) - } - .left_future() - } else { - ready(Ok(TaskResult::Dependencies { - solvable_id: internal_solvable_id, - dependencies: Dependencies::Known(KnownDependencies { - requirements: self.root_requirements.clone(), - constrains: self.root_constraints.clone(), - }), - })) - .right_future() - }; - - pending_futures.push(get_dependencies_fut.boxed_local()); - } - - let Some(result) = pending_futures.next().await else { - // No more pending results - break; - }; - - let mut clauses_added_for_solvable = self.clauses_added_for_solvable.borrow_mut(); - let mut clauses_added_for_package = self.clauses_added_for_package.borrow_mut(); - - match result? { - TaskResult::Dependencies { - solvable_id, - dependencies, - } => { - // Get the solvable information and request its requirements and constraints - tracing::trace!( - "dependencies available for {}", - solvable_id.display(self.provider()), - ); - - let (requirements, constrains) = match dependencies { - Dependencies::Known(deps) => (deps.requirements, deps.constrains), - Dependencies::Unknown(reason) => { - // There is no information about the solvable's dependencies, so we add - // an exclusion clause for it - - let (state, kind) = ClauseState::exclude(solvable_id, reason); - let clause_id = self.clauses.alloc(state, kind); - - // Exclusions are negative assertions, tracked outside of the watcher - // system - output.negative_assertions.push((solvable_id, clause_id)); - - // There might be a conflict now - if self.decision_tracker.assigned_value(solvable_id) == Some(true) { - output.conflicting_clauses.push(clause_id); - } - - continue; - } - }; - - for version_set_id in requirements - .iter() - .flat_map(|requirement| requirement.version_sets(self.provider())) - .chain(constrains.iter().copied()) - { - let dependency_name = self.provider().version_set_name(version_set_id); - if clauses_added_for_package.insert(dependency_name) { - tracing::trace!( - "┝━ Adding clauses for package '{}'", - self.provider().display_name(dependency_name), - ); - - pending_futures.push( - async move { - let package_candidates = - self.cache.get_or_cache_candidates(dependency_name).await?; - Ok(TaskResult::Candidates { - name_id: dependency_name, - package_candidates, - }) - } - .boxed_local(), - ); - } - } - - for requirement in requirements { - // Find all the solvable that match for the given version set - pending_futures.push( - async move { - let candidates = self - .cache - .get_or_cache_sorted_candidates(requirement) - .await?; - Ok(TaskResult::SortedCandidates { - solvable_id, - requirement, - candidates, - }) - } - .boxed_local(), - ); - } - - for version_set_id in constrains { - // Find all the solvables that match for the given version set - pending_futures.push( - async move { - let non_matching_candidates = self - .cache - .get_or_cache_non_matching_candidates(version_set_id) - .await?; - Ok(TaskResult::NonMatchingCandidates { - solvable_id, - version_set_id, - non_matching_candidates, - }) - } - .boxed_local(), - ) - } - } - TaskResult::Candidates { - name_id, - package_candidates, - } => { - // Get the solvable information and request its requirements and constraints - tracing::trace!( - "Package candidates available for {}", - self.provider().display_name(name_id) - ); - - output.new_names.push(name_id); - - let locked_solvable_id = package_candidates.locked; - let candidates = &package_candidates.candidates; - - // 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 (state, kind) = ClauseState::lock( - locked_solvable_id.into(), - other_candidate.into(), - ); - let clause_id = self.clauses.alloc(state, kind); - - debug_assert!(self.clauses.states.borrow_mut() - [clause_id.to_usize()] - .has_watches()); - output.clauses_to_watch.push(clause_id); - } - } - } - - // Add a clause for solvables that are externally excluded. - for (solvable, reason) in package_candidates.excluded.iter().copied() { - let (state, kind) = ClauseState::exclude(solvable.into(), reason); - let clause_id = self.clauses.alloc(state, kind); - - // Exclusions are negative assertions, tracked outside of the watcher system - output - .negative_assertions - .push((solvable.into(), clause_id)); - - // Conflicts should be impossible here - debug_assert!( - self.decision_tracker.assigned_value(solvable.into()) != Some(true) - ); - } - } - TaskResult::SortedCandidates { - solvable_id, - requirement, - candidates, - } => { - tracing::trace!( - "Sorted candidates available for {}", - requirement.display(self.provider()), - ); - - // 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.into()) { - continue; - } - - // If the dependencies are already available for the - // candidate, queue the candidate for processing. - if self.cache.are_dependencies_available_for(candidate) - && clauses_added_for_solvable.insert(candidate.into()) - { - pending_solvables.push(candidate.into()); - } - - // Add forbid constraints for this solvable on all other - // solvables that have been visited already for the same - // version set name. - let name_id = self.provider().solvable_name(candidate); - let mut forbidden_clauses_added = self.forbidden_clauses_added.borrow_mut(); - let other_solvables = forbidden_clauses_added.entry(name_id).or_default(); - let candidate = InternalSolvableId::from(candidate); - if other_solvables.insert(candidate) { - for &other_candidate in other_solvables.iter() { - if candidate == other_candidate { - continue; - } - - let (state, kind) = ClauseState::forbid_multiple( - candidate, - other_candidate, - name_id, - ); - let clause_id = self.clauses.alloc(state, kind); - - debug_assert!(self.clauses.states.borrow_mut() - [clause_id.to_usize()] - .has_watches()); - output.clauses_to_watch.push(clause_id); - } - } - } - - // Add the requirements clause - let no_candidates = candidates.is_empty(); - let (state, conflict, kind) = ClauseState::requires( - solvable_id, - requirement, - candidates, - &self.decision_tracker, - ); - let has_watches = state.has_watches(); - let clause_id = self.clauses.alloc(state, kind); - - if has_watches { - output.clauses_to_watch.push(clause_id); - } - - output - .new_requires_clauses - .push((solvable_id, requirement, clause_id)); - - if conflict { - output.conflicting_clauses.push(clause_id); - } else if no_candidates { - // Add assertions for unit clauses (i.e. those with no matching candidates) - output.negative_assertions.push((solvable_id, clause_id)); - } - } - TaskResult::NonMatchingCandidates { - solvable_id, - version_set_id, - non_matching_candidates, - } => { - tracing::trace!( - "non matching candidates available for {} {}", - self.provider() - .display_name(self.provider().version_set_name(version_set_id)), - self.provider().display_version_set(version_set_id), - ); - - // Add forbidden clauses for the candidates - for &forbidden_candidate in non_matching_candidates { - let (state, conflict, kind) = ClauseState::constrains( - solvable_id, - forbidden_candidate.into(), - version_set_id, - &self.decision_tracker, - ); - - let clause_id = self.clauses.alloc(state, kind); - output.clauses_to_watch.push(clause_id); - - if conflict { - output.conflicting_clauses.push(clause_id); - } - } - } - } - } - - tracing::trace!("Done adding clauses for solvables"); - - Ok(output) - } - /// Run the CDCL algorithm to solve the SAT problem /// /// The CDCL algorithm's job is to find a valid assignment to the variables @@ -758,12 +424,12 @@ impl Solver { /// If the solution process is cancelled (see /// [`DependencyProvider::should_cancel_with_value`]), /// returns [`UnsolvableOrCancelled::Cancelled`] as an `Err`. - fn run_sat(&mut self, solvable: InternalSolvableId) -> Result { + fn run_sat(&mut self, root_solvable: SolvableOrRootId) -> Result { let starting_level = self .decision_tracker .stack() .next_back() - .map(|decision| self.decision_tracker.level(decision.solvable_id)) + .map(|decision| self.decision_tracker.level(decision.variable)) .unwrap_or(0); let mut level = starting_level; @@ -788,21 +454,39 @@ impl Solver { // solution that satisfies the user requirements. tracing::trace!( "╤══ Install {} at level {level}", - solvable.display(self.provider()) + root_solvable.display(self.provider()) ); self.decision_tracker .try_add_decision( - Decision::new(solvable, true, ClauseId::install_root()), + Decision::new( + self.variable_map.intern_solvable_or_root(root_solvable), + true, + ClauseId::install_root(), + ), level, ) .expect("already decided"); // Add the clauses for the root solvable. - let output = self - .async_runtime - .block_on(self.add_clauses_for_solvables([solvable]))?; + let output = self.async_runtime.block_on(add_clauses_for_solvables( + [root_solvable], + &self.cache, + &mut self.clauses, + &self.decision_tracker, + &mut self.variable_map, + &mut self.clauses_added_for_solvable, + &mut self.clauses_added_for_package, + &mut self.forbidden_clauses_added, + &mut self.requirement_to_sorted_candidates, + &self.root_requirements, + &self.root_constraints, + ))?; if let Err(clause_id) = self.process_add_clause_output(output) { - return self.run_sat_process_unsolvable(solvable, starting_level, clause_id); + return self.run_sat_process_unsolvable( + root_solvable, + starting_level, + clause_id, + ); } } @@ -819,7 +503,7 @@ impl Solver { Err(PropagationError::Conflict(_, _, clause_id)) => { if level == starting_level + 1 { return self.run_sat_process_unsolvable( - solvable, + root_solvable, starting_level, clause_id, ); @@ -827,7 +511,7 @@ impl Solver { // The conflict was caused because new clauses have been added dynamically. // We need to start over. tracing::debug!("├─ added clause {clause} introduces a conflict which invalidates the partial solution", - clause=self.clauses.kinds.borrow()[clause_id.to_usize()].display(self.provider())); + clause=self.clauses.kinds[clause_id.to_usize()].display(&self.variable_map, self.provider())); level = starting_level; self.decision_tracker.undo_until(starting_level); continue; @@ -858,12 +542,13 @@ impl Solver { .filter(|d| d.value) // Select solvables for which we do not yet have dependencies .filter(|d| { - !self - .clauses_added_for_solvable - .borrow() - .contains(&d.solvable_id) + let Some(solvable_or_root) = d.variable.as_solvable_or_root(&self.variable_map) + else { + return false; + }; + !self.clauses_added_for_solvable.contains(&solvable_or_root) }) - .map(|d| (d.solvable_id, d.derived_from)) + .map(|d| (d.variable, d.derived_from)) .collect(); if new_solvables.is_empty() { @@ -883,22 +568,40 @@ impl Solver { .copied() .format_with("\n- ", |(id, derived_from), f| f(&format_args!( "{} (derived from {})", - id.display(self.provider()), - self.clauses.kinds.borrow()[derived_from.to_usize()] - .display(self.provider()), + id.display(&self.variable_map, self.provider()), + self.clauses.kinds[derived_from.to_usize()] + .display(&self.variable_map, self.provider()), ))) ); tracing::debug!("===="); // Concurrently get the solvable's clauses - let output = self.async_runtime.block_on(self.add_clauses_for_solvables( - new_solvables.iter().map(|(solvable_id, _)| *solvable_id), + let output = self.async_runtime.block_on(add_clauses_for_solvables( + new_solvables + .iter() + .filter_map(|(variable, _)| { + self.variable_map + .origin(*variable) + .as_solvable() + .map(Into::into) + }) + .collect::>(), + &self.cache, + &mut self.clauses, + &self.decision_tracker, + &mut self.variable_map, + &mut self.clauses_added_for_solvable, + &mut self.clauses_added_for_package, + &mut self.forbidden_clauses_added, + &mut self.requirement_to_sorted_candidates, + &self.root_requirements, + &self.root_constraints, ))?; // Serially process the outputs, to reduce the need for synchronization for &clause_id in &output.conflicting_clauses { tracing::debug!("├─ Added clause {clause} introduces a conflict which invalidates the partial solution", - clause=self.clauses.kinds.borrow()[clause_id.to_usize()].display(self.provider())); + clause=self.clauses.kinds[clause_id.to_usize()].display(&self.variable_map, self.provider())); } if let Err(_first_conflicting_clause_id) = self.process_add_clause_output(output) { @@ -917,7 +620,7 @@ impl Solver { /// sets it to `false` and returns `Ok(false)`. fn run_sat_process_unsolvable( &mut self, - solvable: InternalSolvableId, + solvable_or_root: SolvableOrRootId, starting_level: u32, clause_id: ClauseId, ) -> Result { @@ -930,7 +633,11 @@ impl Solver { self.decision_tracker.undo_until(starting_level); self.decision_tracker .try_add_decision( - Decision::new(solvable, false, ClauseId::install_root()), + Decision::new( + self.variable_map.intern_solvable_or_root(solvable_or_root), + false, + ClauseId::install_root(), + ), starting_level + 1, ) .expect("bug: already decided - decision should have been undone"); @@ -939,7 +646,7 @@ impl Solver { } fn process_add_clause_output(&mut self, mut output: AddClauseOutput) -> Result<(), ClauseId> { - let mut clauses = self.clauses.states.borrow_mut(); + let clauses = &mut self.clauses.states; for clause_id in output.clauses_to_watch { debug_assert!( clauses[clause_id.to_usize()].has_watches(), @@ -997,8 +704,9 @@ impl Solver { tracing::info!( "╒══ Install {} at level {level} (derived from {})", - candidate.display(self.provider()), - self.clauses.kinds.borrow()[clause_id.to_usize()].display(self.provider()) + candidate.display(&self.variable_map, self.provider()), + self.clauses.kinds[clause_id.to_usize()] + .display(&self.variable_map, self.provider()) ); // Propagate the decision @@ -1043,7 +751,7 @@ impl Solver { /// with the least amount of possible candidates requires less /// backtracking to determine unsatisfiability than a requirement with /// more possible candidates. - fn decide(&mut self) -> Option<(InternalSolvableId, InternalSolvableId, ClauseId)> { + fn decide(&mut self) -> Option<(VariableId, VariableId, ClauseId)> { struct PossibleDecision { /// The activity of the package that is selected package_activity: f32, @@ -1057,12 +765,12 @@ impl Solver { candidate_count: u32, /// The decision to make. - decision: (SolvableId, InternalSolvableId, ClauseId), + decision: (VariableId, VariableId, ClauseId), } let mut best_decision: Option = None; for (&solvable_id, requirements) in self.requires_clauses.iter() { - let is_explicit_requirement = solvable_id == InternalSolvableId::root(); + let is_explicit_requirement = solvable_id == VariableId::root(); if let Some(best_decision) = &best_decision { // If we already have an explicit requirement, there is no need to evaluate // non-explicit requirements. @@ -1079,14 +787,20 @@ impl Solver { for (deps, clause_id) in requirements.iter() { let mut candidate = ControlFlow::Break(()); + // Get the candidates for the individual version sets. + let version_set_candidates = &self.requirement_to_sorted_candidates[deps]; + // Iterate over all version sets in the requirement and find the first version // set that we can act on, or if a single candidate (from any version set) makes // the clause true. - for version_set in deps.version_sets(self.provider()) { - // Consider only clauses in which no candidates have been installed - let candidates = &self.cache.requirement_to_sorted_candidates - [&Requirement::Single(version_set)]; - + // + // NOTE: We zip the version sets from the requirements and the variables that we + // previously cached. This assumes that the order of the version sets is the + // same in both collections. + for (version_set, candidates) in deps + .version_sets(self.provider()) + .zip(version_set_candidates) + { // Find the first candidate that is not yet assigned a value or find the first // value that makes this clause true. candidate = candidates.iter().try_fold( @@ -1095,8 +809,7 @@ impl Solver { _ => None, }, |first_candidate, &candidate| { - let assigned_value = - self.decision_tracker.assigned_value(candidate.into()); + let assigned_value = self.decision_tracker.assigned_value(candidate); ControlFlow::Continue(match assigned_value { Some(true) => { // This candidate has already been assigned so the clause is @@ -1213,8 +926,9 @@ impl Solver { { tracing::trace!( "deciding to assign {}, ({}, {} activity score, {} possible candidates)", - self.provider().display_solvable(*candidate), - self.clauses.kinds.borrow()[clause_id.to_usize()].display(self.provider()), + candidate.display(&self.variable_map, self.provider()), + self.clauses.kinds[clause_id.to_usize()] + .display(&self.variable_map, self.provider()), package_activity, candidate_count, ); @@ -1225,7 +939,7 @@ impl Solver { |PossibleDecision { decision: (candidate, required_by, via), .. - }| { (candidate.into(), required_by, via) }, + }| { (candidate, required_by, via) }, ) } @@ -1246,8 +960,8 @@ impl Solver { fn set_propagate_learn( &mut self, mut level: u32, - solvable: InternalSolvableId, - _required_by: InternalSolvableId, + solvable: VariableId, + _required_by: VariableId, clause_id: ClauseId, ) -> Result { level += 1; @@ -1287,37 +1001,38 @@ impl Solver { fn learn_from_conflict( &mut self, mut level: u32, - conflicting_solvable: InternalSolvableId, + conflicting_solvable: VariableId, attempted_value: bool, conflicting_clause: ClauseId, ) -> Result { { tracing::info!( "├┬ Propagation conflicted: could not set {solvable} to {attempted_value}", - solvable = conflicting_solvable.display(self.provider()), + solvable = conflicting_solvable.display(&self.variable_map, self.provider()), ); tracing::info!( "││ During unit propagation for clause: {}", - self.clauses.kinds.borrow()[conflicting_clause.to_usize()].display(self.provider()) + self.clauses.kinds[conflicting_clause.to_usize()] + .display(&self.variable_map, self.provider()) ); tracing::info!( "││ Previously decided value: {}. Derived from: {}", !attempted_value, - self.clauses.kinds.borrow()[self + self.clauses.kinds[self .decision_tracker .find_clause_for_assignment(conflicting_solvable) .unwrap() .to_usize()] - .display(self.provider()), + .display(&self.variable_map, self.provider()), ); } if level == 1 { for decision in self.decision_tracker.stack() { let clause_id = decision.derived_from; - let clause = self.clauses.kinds.borrow()[clause_id.to_usize()]; - let level = self.decision_tracker.level(decision.solvable_id); + let clause = self.clauses.kinds[clause_id.to_usize()]; + let level = self.decision_tracker.level(decision.variable); let action = if decision.value { "install" } else { "forbid" }; if let Clause::ForbidMultipleInstances(..) = clause { @@ -1327,9 +1042,11 @@ impl Solver { tracing::info!( "* ({level}) {action} {}. Reason: {}", - decision.solvable_id.display(self.provider()), - self.clauses.kinds.borrow()[decision.derived_from.to_usize()] - .display(self.provider()), + decision + .variable + .display(&self.variable_map, self.provider()), + self.clauses.kinds[decision.derived_from.to_usize()] + .display(&self.variable_map, self.provider()), ); } @@ -1346,13 +1063,15 @@ impl Solver { let decision = literal.satisfying_value(); self.decision_tracker .try_add_decision( - Decision::new(literal.solvable_id(), decision, learned_clause_id), + Decision::new(literal.variable(), decision, learned_clause_id), level, ) .expect("bug: solvable was already decided!"); tracing::debug!( "│├ Propagate after learn: {} = {decision}", - literal.solvable_id().display(self.provider()), + literal + .variable() + .display(&self.variable_map, self.provider()), ); tracing::info!("│└ Backtracked from {old_level} -> {level}"); @@ -1386,7 +1105,7 @@ impl Solver { if decided { tracing::trace!( "Negative assertions derived from other rules: Propagate assertion {} = {}", - solvable_id.display(self.provider()), + solvable_id.display(&self.variable_map, self.provider()), value ); } @@ -1395,7 +1114,7 @@ impl Solver { // Assertions derived from learnt rules 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.kinds.borrow()[clause_id.to_usize()]; + let clause = self.clauses.kinds[clause_id.to_usize()]; let Clause::Learnt(learnt_index) = clause else { unreachable!(); }; @@ -1413,27 +1132,28 @@ impl Solver { let decided = self .decision_tracker .try_add_decision( - Decision::new(literal.solvable_id(), decision, clause_id), + Decision::new(literal.variable(), decision, clause_id), level, ) - .map_err(|_| { - PropagationError::Conflict(literal.solvable_id(), decision, clause_id) - })?; + .map_err(|_| PropagationError::Conflict(literal.variable(), decision, clause_id))?; if decided { tracing::trace!( "├─ Propagate assertion {} = {}", - literal.solvable_id().display(self.provider()), + literal + .variable() + .display(&self.variable_map, self.provider()), decision ); } } // Watched solvables - let clauses = self.clauses.kinds.borrow(); - let mut clause_states = self.clauses.states.borrow_mut(); + let clauses = &self.clauses.kinds; + let clause_states = &mut self.clauses.states; + let interner = self.cache.provider(); while let Some(decision) = self.decision_tracker.next_unpropagated() { - let watched_literal = Literal::new(decision.solvable_id, decision.value); + let watched_literal = Literal::new(decision.variable, decision.value); // Propagate, iterating through the linked list of clauses that watch this // solvable @@ -1467,17 +1187,15 @@ impl Solver { predecessor_clause_id = Some(clause_id); // Configure the next clause to visit - next_clause_id = clause_state.next_watched_clause(watched_literal.solvable_id()); + next_clause_id = clause_state.next_watched_clause(watched_literal.variable()); // Determine which watch turned false. - let (watch_index, other_watch_index) = if clause_state.watched_literals[0] - .solvable_id() - == watched_literal.solvable_id() - { - (0, 1) - } else { - (1, 0) - }; + let (watch_index, other_watch_index) = + if clause_state.watched_literals[0].variable() == watched_literal.variable() { + (0, 1) + } else { + (1, 0) + }; debug_assert!( clause_state.watched_literals[watch_index].eval(self.decision_tracker.map()) == Some(false) @@ -1494,7 +1212,7 @@ impl Solver { } else if let Some(variable) = clause_state.next_unwatched_literal( &clauses[clause_id.to_usize()], &self.learnt_clauses, - &self.cache.requirement_to_sorted_candidates, + &self.requirement_to_sorted_candidates, self.decision_tracker.map(), watch_index, ) { @@ -1525,18 +1243,14 @@ impl Solver { .decision_tracker .try_add_decision( Decision::new( - remaining_watch.solvable_id(), + remaining_watch.variable(), remaining_watch.satisfying_value(), clause_id, ), level, ) .map_err(|_| { - PropagationError::Conflict( - remaining_watch.solvable_id(), - true, - clause_id, - ) + PropagationError::Conflict(remaining_watch.variable(), true, clause_id) })?; if decided { @@ -1547,9 +1261,11 @@ impl Solver { _ => { tracing::debug!( "├ Propagate {} = {}. {}", - remaining_watch.solvable_id().display(self.provider()), + remaining_watch + .variable() + .display(&self.variable_map, interner), remaining_watch.satisfying_value(), - clause.display(self.provider()) + clause.display(&self.variable_map, interner) ); } } @@ -1594,7 +1310,7 @@ impl Solver { /// unrecoverable conflict fn analyze_unsolvable(&mut self, clause_id: ClauseId) -> Conflict { let last_decision = self.decision_tracker.stack().last().unwrap(); - let highest_level = self.decision_tracker.level(last_decision.solvable_id); + let highest_level = self.decision_tracker.level(last_decision.variable); debug_assert_eq!(highest_level, 1); let mut conflict = Conflict::default(); @@ -1602,17 +1318,17 @@ impl Solver { tracing::info!("=== ANALYZE UNSOLVABLE"); let mut involved = HashSet::default(); - self.clauses.kinds.borrow()[clause_id.to_usize()].visit_literals( + self.clauses.kinds[clause_id.to_usize()].visit_literals( &self.learnt_clauses, - &self.cache.requirement_to_sorted_candidates, + &self.requirement_to_sorted_candidates, |literal| { - involved.insert(literal.solvable_id()); + involved.insert(literal.variable()); }, ); let mut seen = HashSet::default(); Self::analyze_unsolvable_clause( - &self.clauses.kinds.borrow(), + &self.clauses.kinds, &self.learnt_why, clause_id, &mut conflict, @@ -1620,34 +1336,34 @@ impl Solver { ); for decision in self.decision_tracker.stack().rev() { - if decision.solvable_id.is_root() { + if decision.variable.is_root() { continue; } let why = decision.derived_from; - if !involved.contains(&decision.solvable_id) { + if !involved.contains(&decision.variable) { continue; } assert_ne!(why, ClauseId::install_root()); Self::analyze_unsolvable_clause( - &self.clauses.kinds.borrow(), + &self.clauses.kinds, &self.learnt_why, why, &mut conflict, &mut seen, ); - self.clauses.kinds.borrow()[why.to_usize()].visit_literals( + self.clauses.kinds[why.to_usize()].visit_literals( &self.learnt_clauses, - &self.cache.requirement_to_sorted_candidates, + &self.requirement_to_sorted_candidates, |literal| { if literal.eval(self.decision_tracker.map()) == Some(true) { - assert_eq!(literal.solvable_id(), decision.solvable_id); + assert_eq!(literal.variable(), decision.variable); } else { - involved.insert(literal.solvable_id()); + involved.insert(literal.variable()); } }, ); @@ -1672,7 +1388,7 @@ impl Solver { fn analyze( &mut self, mut current_level: u32, - mut conflicting_solvable: InternalSolvableId, + mut conflicting_solvable: VariableId, mut clause_id: ClauseId, ) -> (u32, ClauseId, Literal) { let mut seen = HashSet::default(); @@ -1683,33 +1399,33 @@ impl Solver { let mut s_value; let mut learnt_why = Vec::new(); let mut first_iteration = true; - let clause_kinds = self.clauses.kinds.borrow(); + let clause_kinds = &self.clauses.kinds; loop { learnt_why.push(clause_id); clause_kinds[clause_id.to_usize()].visit_literals( &self.learnt_clauses, - &self.cache.requirement_to_sorted_candidates, + &self.requirement_to_sorted_candidates, |literal| { - if !first_iteration && literal.solvable_id() == conflicting_solvable { + if !first_iteration && literal.variable() == conflicting_solvable { // We are only interested in the causes of the conflict, so we ignore the // solvable whose value was propagated return; } - if !seen.insert(literal.solvable_id()) { + if !seen.insert(literal.variable()) { // Skip literals we have already seen return; } - let decision_level = self.decision_tracker.level(literal.solvable_id()); + let decision_level = self.decision_tracker.level(literal.variable()); if decision_level == current_level { causes_at_current_level += 1; } else if current_level > 1 { let learnt_literal = Literal::new( - literal.solvable_id(), + literal.variable(), self.decision_tracker - .assigned_value(literal.solvable_id()) + .assigned_value(literal.variable()) .unwrap(), ); learnt.push(learnt_literal); @@ -1726,7 +1442,7 @@ impl Solver { loop { let (last_decision, last_decision_level) = self.decision_tracker.undo_last(); - conflicting_solvable = last_decision.solvable_id; + conflicting_solvable = last_decision.variable; s_value = last_decision.value; clause_id = last_decision.derived_from; @@ -1734,7 +1450,7 @@ impl Solver { // We are interested in the first literal we come across that caused the // conflicting assignment - if seen.contains(&last_decision.solvable_id) { + if seen.contains(&last_decision.variable) { break; } } @@ -1745,17 +1461,14 @@ impl Solver { } } - // No longer need the kinds - drop(clause_kinds); - let last_literal = Literal::new(conflicting_solvable, s_value); learnt.push(last_literal); // Increase the activity of the packages in the learned clause for literal in &learnt { let name_id = literal - .solvable_id() - .as_solvable() + .variable() + .as_solvable(&self.variable_map) .map(|s| self.provider().solvable_name(s)); if let Some(name_id) = name_id { self.name_activity[name_id.to_usize()] += self.activity_add; @@ -1771,10 +1484,8 @@ impl Solver { let clause_id = self.clauses.alloc(state, kind); self.learnt_clause_ids.push(clause_id); if has_watches { - self.watches.start_watching( - &mut self.clauses.states.borrow_mut()[clause_id.to_usize()], - clause_id, - ); + self.watches + .start_watching(&mut self.clauses.states[clause_id.to_usize()], clause_id); } tracing::debug!("│├ Learnt disjunction:",); @@ -1782,7 +1493,7 @@ impl Solver { tracing::debug!( "││ - {}{}", if lit.negate() { "NOT " } else { "" }, - lit.solvable_id().display(self.provider()), + lit.variable().display(&self.variable_map, self.provider()), ); } @@ -1803,3 +1514,401 @@ impl Solver { } } } + +/// Adds clauses for a solvable. These clauses include requirements and +/// constrains on other solvables. +/// +/// Returns the added clauses, and an additional list with conflicting +/// clauses (if any). +/// +/// If the provider has requested the solving process to be cancelled, the +/// cancellation value will be returned as an `Err(...)`. +/// +/// This function is not part of the `Solver` struct because it needs to +/// selectively mutably borrow some of the solver's fields. +#[allow(clippy::too_many_arguments)] +async fn add_clauses_for_solvables( + solvable_ids: impl IntoIterator, + cache: &SolverCache, + clauses: &mut Clauses, + decision_tracker: &DecisionTracker, + variable_map: &mut VariableMap, + clauses_added_for_solvable: &mut HashSet, + clauses_added_for_package: &mut HashSet, + forbidden_clauses_added: &mut HashMap>, + requirement_to_sorted_candidates: &mut FrozenMap< + Requirement, + RequirementCandidateVariables, + ahash::RandomState, + >, + root_requirements: &[Requirement], + root_constraints: &[VersionSetId], +) -> Result> { + let mut output = AddClauseOutput::default(); + + tracing::trace!("Add clauses for solvables"); + + pub enum TaskResult<'i> { + Dependencies { + solvable_id: SolvableOrRootId, + dependencies: Dependencies, + }, + SortedCandidates { + solvable_id: SolvableOrRootId, + requirement: Requirement, + candidates: Vec<&'i [SolvableId]>, + }, + NonMatchingCandidates { + solvable_id: SolvableOrRootId, + version_set_id: VersionSetId, + non_matching_candidates: &'i [SolvableId], + }, + Candidates { + name_id: NameId, + package_candidates: &'i Candidates, + }, + } + + // Mark the initial seen solvables as seen + let mut pending_solvables = vec![]; + { + for solvable_id in solvable_ids { + if clauses_added_for_solvable.insert(solvable_id) { + pending_solvables.push(solvable_id); + } + } + } + + let mut seen = pending_solvables.iter().copied().collect::>(); + let mut pending_futures = FuturesUnordered::new(); + loop { + // Iterate over all pending solvables and request their dependencies. + for solvable_or_root in pending_solvables.drain(..) { + // If the solvable is the root solvable, we can skip the dependency provider + // and use the root requirements and constraints directly. + let get_dependencies_fut = if let Some(solvable_id) = solvable_or_root.solvable() { + // Get the solvable information and request its requirements and constraints + tracing::trace!( + "┝━ adding clauses for dependencies of {}", + solvable_id.display(cache.provider()), + ); + + async move { + let deps = cache.get_or_cache_dependencies(solvable_id).await?; + Ok(TaskResult::Dependencies { + solvable_id: solvable_or_root, + dependencies: deps.clone(), + }) + } + .left_future() + } else { + ready(Ok(TaskResult::Dependencies { + solvable_id: solvable_or_root, + dependencies: Dependencies::Known(KnownDependencies { + requirements: root_requirements.to_vec(), + constrains: root_constraints.to_vec(), + }), + })) + .right_future() + }; + + pending_futures.push(get_dependencies_fut.boxed_local()); + } + + let Some(result) = pending_futures.next().await else { + // No more pending results + break; + }; + + match result? { + TaskResult::Dependencies { + solvable_id, + dependencies, + } => { + // Get the solvable information and request its requirements and constraints + tracing::trace!( + "dependencies available for {}", + solvable_id.display(cache.provider()), + ); + + // Allocate a variable for the solvable + let variable = match solvable_id.solvable() { + Some(solvable_id) => variable_map.intern_solvable(solvable_id), + None => variable_map.root(), + }; + + let (requirements, constrains) = match dependencies { + Dependencies::Known(deps) => (deps.requirements, deps.constrains), + Dependencies::Unknown(reason) => { + // There is no information about the solvable's dependencies, so we add + // an exclusion clause for it + + let (state, kind) = ClauseState::exclude(variable, reason); + let clause_id = clauses.alloc(state, kind); + + // Exclusions are negative assertions, tracked outside the watcher + // system + output.negative_assertions.push((variable, clause_id)); + + // There might be a conflict now + if decision_tracker.assigned_value(variable) == Some(true) { + output.conflicting_clauses.push(clause_id); + } + + continue; + } + }; + + for version_set_id in requirements + .iter() + .flat_map(|requirement| requirement.version_sets(cache.provider())) + .chain(constrains.iter().copied()) + { + let dependency_name = cache.provider().version_set_name(version_set_id); + if clauses_added_for_package.insert(dependency_name) { + tracing::trace!( + "┝━ Adding clauses for package '{}'", + cache.provider().display_name(dependency_name), + ); + + pending_futures.push( + async move { + let package_candidates = + cache.get_or_cache_candidates(dependency_name).await?; + Ok(TaskResult::Candidates { + name_id: dependency_name, + package_candidates, + }) + } + .boxed_local(), + ); + } + } + + for requirement in requirements { + // Find all the solvable that match for the given version set + pending_futures.push( + async move { + let candidates = futures::future::try_join_all( + requirement + .version_sets(cache.provider()) + .map(|version_set| { + cache.get_or_cache_sorted_candidates_for_version_set( + version_set, + ) + }), + ) + .await?; + + Ok(TaskResult::SortedCandidates { + solvable_id, + requirement, + candidates, + }) + } + .boxed_local(), + ); + } + + for version_set_id in constrains { + // Find all the solvables that match for the given version set + pending_futures.push( + async move { + let non_matching_candidates = cache + .get_or_cache_non_matching_candidates(version_set_id) + .await?; + Ok(TaskResult::NonMatchingCandidates { + solvable_id, + version_set_id, + non_matching_candidates, + }) + } + .boxed_local(), + ) + } + } + TaskResult::Candidates { + name_id, + package_candidates, + } => { + // Get the solvable information and request its requirements and constraints + tracing::trace!( + "Package candidates available for {}", + cache.provider().display_name(name_id) + ); + + output.new_names.push(name_id); + + let candidates = &package_candidates.candidates; + + // If there is a locked solvable, forbid other solvables. + if let Some(locked_solvable_id) = package_candidates.locked { + let locked_solvable_var = variable_map.intern_solvable(locked_solvable_id); + for &other_candidate in candidates { + if other_candidate != locked_solvable_id { + let other_candidate_var = variable_map.intern_solvable(other_candidate); + let (state, kind) = + ClauseState::lock(locked_solvable_var, other_candidate_var); + let clause_id = clauses.alloc(state, kind); + + debug_assert!(clauses.states[clause_id.to_usize()].has_watches()); + output.clauses_to_watch.push(clause_id); + } + } + } + + // Add a clause for solvables that are externally excluded. + for (solvable, reason) in package_candidates.excluded.iter().copied() { + let solvable_var = variable_map.intern_solvable(solvable); + let (state, kind) = ClauseState::exclude(solvable_var, reason); + let clause_id = clauses.alloc(state, kind); + + // Exclusions are negative assertions, tracked outside the watcher system + output.negative_assertions.push((solvable_var, clause_id)); + + // Conflicts should be impossible here + debug_assert!(decision_tracker.assigned_value(solvable_var) != Some(true)); + } + } + TaskResult::SortedCandidates { + solvable_id, + requirement, + candidates, + } => { + tracing::trace!( + "Sorted candidates available for {}", + requirement.display(cache.provider()), + ); + + // Allocate a variable for the solvable + let variable = match solvable_id.solvable() { + Some(solvable_id) => variable_map.intern_solvable(solvable_id), + None => variable_map.root(), + }; + + // Intern all the solvables of the candidates. + let version_set_variables = requirement_to_sorted_candidates.insert( + requirement, + candidates + .iter() + .map(|&candidates| { + candidates + .iter() + .map(|&var| variable_map.intern_solvable(var)) + .collect() + }) + .collect(), + ); + + // Queue requesting the dependencies of the candidates as well if they are + // cheaply available from the dependency provider. + for (candidate, candidate_var) in candidates + .iter() + .zip(version_set_variables) + .flat_map(|(&candidates, variable)| { + candidates.iter().copied().zip(variable.iter().copied()) + }) + { + if !seen.insert(candidate.into()) { + continue; + } + + // If the dependencies are already available for the + // candidate, queue the candidate for processing. + if cache.are_dependencies_available_for(candidate) + && clauses_added_for_solvable.insert(candidate.into()) + { + pending_solvables.push(candidate.into()); + } + + // Add forbid constraints for this solvable on all other + // solvables that have been visited already for the same + // version set name. + let name_id = cache.provider().solvable_name(candidate); + let other_solvables = forbidden_clauses_added.entry(name_id).or_default(); + other_solvables.add( + candidate_var, + |a, b, positive| { + let (state, kind) = ClauseState::forbid_multiple( + a, + if positive { b.positive() } else { b.negative() }, + name_id, + ); + let clause_id = clauses.alloc(state, kind); + debug_assert!(clauses.states[clause_id.to_usize()].has_watches()); + output.clauses_to_watch.push(clause_id); + }, + || variable_map.alloc_forbid_multiple_variable(name_id), + ); + } + + // Add the requirements clause + let no_candidates = candidates.iter().all(|candidates| candidates.is_empty()); + let (state, conflict, kind) = ClauseState::requires( + variable, + requirement, + version_set_variables.iter().flatten().copied(), + decision_tracker, + ); + let has_watches = state.has_watches(); + let clause_id = clauses.alloc(state, kind); + + if has_watches { + output.clauses_to_watch.push(clause_id); + } + + output + .new_requires_clauses + .push((variable, requirement, clause_id)); + + if conflict { + output.conflicting_clauses.push(clause_id); + } else if no_candidates { + // Add assertions for unit clauses (i.e. those with no matching candidates) + output.negative_assertions.push((variable, clause_id)); + } + } + TaskResult::NonMatchingCandidates { + solvable_id, + version_set_id, + non_matching_candidates, + } => { + tracing::trace!( + "non matching candidates available for {} {}", + cache + .provider() + .display_name(cache.provider().version_set_name(version_set_id)), + cache.provider().display_version_set(version_set_id), + ); + + // Allocate a variable for the solvable + let variable = match solvable_id.solvable() { + Some(solvable_id) => variable_map.intern_solvable(solvable_id), + None => variable_map.root(), + }; + + // Add forbidden clauses for the candidates + for &forbidden_candidate in non_matching_candidates { + let forbidden_candidate_var = variable_map.intern_solvable(forbidden_candidate); + let (state, conflict, kind) = ClauseState::constrains( + variable, + forbidden_candidate_var, + version_set_id, + decision_tracker, + ); + + let clause_id = clauses.alloc(state, kind); + output.clauses_to_watch.push(clause_id); + + if conflict { + output.conflicting_clauses.push(clause_id); + } + } + } + } + } + + tracing::trace!("Done adding clauses for solvables"); + + Ok(output) +} diff --git a/src/solver/snapshots/resolvo__solver__binary_encoding__test__at_most_once_tracker.snap b/src/solver/snapshots/resolvo__solver__binary_encoding__test__at_most_once_tracker.snap new file mode 100644 index 0000000..e88e556 --- /dev/null +++ b/src/solver/snapshots/resolvo__solver__binary_encoding__test__at_most_once_tracker.snap @@ -0,0 +1,13 @@ +--- +source: src/solver/binary_encoding.rs +expression: "clauses.iter().format(\"\\n\")" +snapshot_kind: text +--- +¬x1 ∨ ¬v1 +¬x2 ∨ v1 +¬x1 ∨ ¬v2 +¬x2 ∨ ¬v2 +¬x3 ∨ ¬v1 +¬x3 ∨ v2 +¬x4 ∨ v1 +¬x4 ∨ v2 diff --git a/src/solver/variable_map.rs b/src/solver/variable_map.rs new file mode 100644 index 0000000..608ed68 --- /dev/null +++ b/src/solver/variable_map.rs @@ -0,0 +1,163 @@ +use std::{collections::hash_map::Entry, fmt::Display}; + +use ahash::HashMap; + +use crate::{ + internal::{ + arena::ArenaId, + id::{SolvableOrRootId, VariableId}, + }, + Interner, NameId, SolvableId, +}; + +/// All variables in the solver are stored in a `VariableMap`. This map is used +/// to keep track of the semantics of a variable, e.g. what a specific variable +/// represents. +/// +/// The `VariableMap` is responsible for assigning unique identifiers to each +/// variable represented by [`VariableId`]. +pub struct VariableMap { + /// The id of the next variable to be allocated. + next_id: usize, + + /// A map from solvable id to variable id. + solvable_to_variable: HashMap, + + /// Records the origins of all variables. + origins: HashMap, +} + +/// Describes the origin of a variable. +#[derive(Clone, Debug)] +pub enum VariableOrigin { + /// The variable is the root of the decision tree. + Root, + + /// The variable represents a specific solvable. + Solvable(SolvableId), + + /// A variable that helps encode an at most one constraint. + ForbidMultiple(NameId), +} + +impl Default for VariableMap { + fn default() -> Self { + let mut origins = HashMap::default(); + origins.insert(VariableId::root(), VariableOrigin::Root); + + Self { + next_id: 1, // The first variable id is 1 because 0 is reserved for the root. + solvable_to_variable: HashMap::default(), + origins, + } + } +} + +impl VariableMap { + /// Allocate a variable for a new variable or reuse an existing one. + pub fn intern_solvable(&mut self, solvable_id: SolvableId) -> VariableId { + match self.solvable_to_variable.entry(solvable_id) { + Entry::Occupied(entry) => *entry.get(), + Entry::Vacant(entry) => { + let id = self.next_id; + self.next_id += 1; + let variable_id = VariableId::from_usize(id); + entry.insert(variable_id); + self.origins + .insert(variable_id, VariableOrigin::Solvable(solvable_id)); + variable_id + } + } + } + + /// Allocate a variable for a solvable or the root. + pub fn intern_solvable_or_root(&mut self, solvable_or_root_id: SolvableOrRootId) -> VariableId { + match solvable_or_root_id.solvable() { + Some(solvable_id) => self.intern_solvable(solvable_id), + None => VariableId::root(), + } + } + + /// Allocate a variable that helps encode an at most one constraint. + pub fn alloc_forbid_multiple_variable(&mut self, name: NameId) -> VariableId { + let id = self.next_id; + self.next_id += 1; + let variable_id = VariableId::from_usize(id); + self.origins + .insert(variable_id, VariableOrigin::ForbidMultiple(name)); + variable_id + } + + /// Returns the origin of a variable. The origin describes the semantics of + /// a variable. + pub fn origin(&self, variable_id: VariableId) -> VariableOrigin { + self.origins[&variable_id].clone() + } + + /// Returns the root variable + pub fn root(&self) -> VariableId { + VariableId::root() + } +} + +impl VariableId { + /// Returns the solvable id associated with the variable if it represents a + /// solvable. + pub fn as_solvable(self, variable_map: &VariableMap) -> Option { + variable_map.origin(self).as_solvable() + } + + pub fn as_solvable_or_root(self, variable_map: &VariableMap) -> Option { + variable_map.origin(self).as_solvable_or_root() + } + + /// Returns an object that can be used to format the variable. + pub fn display<'i, I: Interner>( + self, + variable_map: &'i VariableMap, + interner: &'i I, + ) -> VariableDisplay<'i, I> { + VariableDisplay { + variable: self, + interner, + variable_map, + } + } +} + +pub struct VariableDisplay<'i, I: Interner> { + variable: VariableId, + interner: &'i I, + variable_map: &'i VariableMap, +} + +impl<'i, I: Interner> Display for VariableDisplay<'i, I> { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self.variable_map.origin(self.variable) { + VariableOrigin::Root => write!(f, "root"), + VariableOrigin::Solvable(solvable_id) => { + write!(f, "{}", self.interner.display_solvable(solvable_id)) + } + VariableOrigin::ForbidMultiple(name) => { + write!(f, "forbid-multiple({})", self.interner.display_name(name)) + } + } + } +} + +impl VariableOrigin { + pub fn as_solvable(&self) -> Option { + match self { + VariableOrigin::Solvable(solvable_id) => Some(*solvable_id), + _ => None, + } + } + + pub fn as_solvable_or_root(&self) -> Option { + match self { + VariableOrigin::Solvable(solvable_id) => Some((*solvable_id).into()), + VariableOrigin::Root => Some(SolvableOrRootId::root()), + _ => None, + } + } +} diff --git a/src/solver/watch_map.rs b/src/solver/watch_map.rs index 86fb281..07cce36 100644 --- a/src/solver/watch_map.rs +++ b/src/solver/watch_map.rs @@ -3,10 +3,11 @@ use crate::{ solver::clause::{ClauseState, Literal}, }; -/// A map from solvables to the clauses that are watching them +/// A map from literals to the clauses that are watching them. Each literal +/// forms a linked list of clauses that are all watching that literal. pub(crate) struct WatchMap { - /// Note: the map is to a single clause, but clauses form a linked list, so - /// it is possible to go from one to the next + // Note: the map is to a single clause, but clauses form a linked list, so + // it is possible to go from one to the next map: Mapping, } @@ -17,11 +18,16 @@ impl WatchMap { } } + /// Add the clause to the linked list of the literals that the clause is + /// watching. pub(crate) fn start_watching(&mut self, clause: &mut ClauseState, clause_id: ClauseId) { for (watch_index, watched_literal) in clause.watched_literals.into_iter().enumerate() { - let already_watching = self.first_clause_watching_literal(watched_literal); - clause.link_to_clause(watch_index, already_watching); - self.watch_literal(watched_literal, clause_id); + // Construct a linked list by adding the clause to the start of the linked list + // and setting the previous head of the chain as the next element in the linked + // list. + let current_head = self.map.get(watched_literal).copied(); + clause.next_watches[watch_index] = current_head; + self.map.insert(watched_literal, clause_id); } } @@ -38,7 +44,7 @@ impl WatchMap { // are no longer watching what brought us here if let Some(predecessor_clause) = predecessor_clause { // Unlink the clause - predecessor_clause.unlink_clause(clause, previous_watch.solvable_id(), watch_index); + predecessor_clause.unlink_clause(clause, previous_watch.variable(), watch_index); } else if let Some(next_watch) = clause.next_watches[watch_index] { // This was the first clause in the chain self.map.insert(previous_watch, next_watch); @@ -52,14 +58,12 @@ impl WatchMap { clause.next_watches[watch_index] = previous_clause_id; } + /// Returns the id of the first clause that is watching the specified + /// literal. pub(crate) fn first_clause_watching_literal( &mut self, watched_literal: Literal, ) -> Option { self.map.get(watched_literal).copied() } - - pub(crate) fn watch_literal(&mut self, watched_literal: Literal, id: ClauseId) { - self.map.insert(watched_literal, id); - } } diff --git a/tests/snapshots/solver__merge_installable.snap b/tests/snapshots/solver__merge_installable.snap index a4da2af..e71dae0 100644 --- a/tests/snapshots/solver__merge_installable.snap +++ b/tests/snapshots/solver__merge_installable.snap @@ -1,9 +1,11 @@ --- source: tests/solver.rs expression: "solve_snapshot(provider, &[\"a 0..3\", \"a 3..5\"])" +snapshot_kind: text --- The following packages are incompatible -├─ a >=0, <3 can be installed with any of the following options: -│ └─ a 1 | 2 -└─ a >=3, <5 cannot be installed because there are no viable options: - └─ a 3 | 4, which conflicts with the versions reported above. +├─ a >=3, <5 can be installed with any of the following options: +│ └─ a 3 +└─ a >=0, <3 cannot be installed because there are no viable options: + ├─ a 2, which conflicts with the versions reported above. + └─ a 1, which conflicts with the versions reported above. diff --git a/tests/snapshots/solver__unsat_after_backtracking.snap b/tests/snapshots/solver__unsat_after_backtracking.snap index 1eb0e23..42bed9d 100644 --- a/tests/snapshots/solver__unsat_after_backtracking.snap +++ b/tests/snapshots/solver__unsat_after_backtracking.snap @@ -1,13 +1,14 @@ --- source: tests/solver.rs expression: error +snapshot_kind: text --- The following packages are incompatible -├─ b * can be installed with any of the following options: -│ └─ b 6 | 7 would require -│ └─ d >=1, <2, which can be installed with any of the following options: -│ └─ d 1 -└─ c * cannot be installed because there are no viable options: - └─ c 1 | 2 would require - └─ d >=2, <3, which cannot be installed because there are no viable options: - └─ d 2, which conflicts with the versions reported above. +├─ c * can be installed with any of the following options: +│ └─ c 1 | 2 would require +│ └─ d >=2, <3, which can be installed with any of the following options: +│ └─ d 2 +└─ b * cannot be installed because there are no viable options: + └─ b 6 | 7 would require + └─ d >=1, <2, which cannot be installed because there are no viable options: + └─ d 1, which conflicts with the versions reported above. diff --git a/tests/snapshots/solver__unsat_applies_graph_compression.snap b/tests/snapshots/solver__unsat_applies_graph_compression.snap index ac122eb..c1fb2f3 100644 --- a/tests/snapshots/solver__unsat_applies_graph_compression.snap +++ b/tests/snapshots/solver__unsat_applies_graph_compression.snap @@ -1,10 +1,11 @@ --- source: tests/solver.rs expression: error +snapshot_kind: text --- The following packages are incompatible ├─ c >=101, <104 can be installed with any of the following options: -│ └─ c 101 | 103 +│ └─ c 103 └─ a * cannot be installed because there are no viable options: └─ a 9 | 10 would require └─ b *, which cannot be installed because there are no viable options: diff --git a/tests/snapshots/solver__unsat_bluesky_conflict.snap b/tests/snapshots/solver__unsat_bluesky_conflict.snap index e86b6d7..de63f8b 100644 --- a/tests/snapshots/solver__unsat_bluesky_conflict.snap +++ b/tests/snapshots/solver__unsat_bluesky_conflict.snap @@ -1,6 +1,7 @@ --- source: tests/solver.rs expression: error +snapshot_kind: text --- The following packages are incompatible ├─ suitcase-utils >=54, <100 can be installed with any of the following options: diff --git a/tests/snapshots/solver__unsat_incompatible_root_requirements.snap b/tests/snapshots/solver__unsat_incompatible_root_requirements.snap index 8a7563f..9816018 100644 --- a/tests/snapshots/solver__unsat_incompatible_root_requirements.snap +++ b/tests/snapshots/solver__unsat_incompatible_root_requirements.snap @@ -1,9 +1,10 @@ --- source: tests/solver.rs expression: error +snapshot_kind: text --- The following packages are incompatible -├─ a >=0, <4 can be installed with any of the following options: -│ └─ a 2 -└─ a >=5, <10 cannot be installed because there are no viable options: - └─ a 5, which conflicts with the versions reported above. +├─ a >=5, <10 can be installed with any of the following options: +│ └─ a 5 +└─ a >=0, <4 cannot be installed because there are no viable options: + └─ a 2, which conflicts with the versions reported above. diff --git a/tests/snapshots/solver__unsat_pubgrub_article.snap b/tests/snapshots/solver__unsat_pubgrub_article.snap index 5e2d80a..b40db87 100644 --- a/tests/snapshots/solver__unsat_pubgrub_article.snap +++ b/tests/snapshots/solver__unsat_pubgrub_article.snap @@ -1,6 +1,7 @@ --- source: tests/solver.rs expression: error +snapshot_kind: text --- The following packages are incompatible ├─ icons >=1, <2 can be installed with any of the following options: