Skip to content

Commit

Permalink
perf: reintroduce binary encoding of forbid multiple clauses (#91)
Browse files Browse the repository at this point in the history
  • Loading branch information
@baszalmstra
baszalmstra authored Jan 2, 2025
1 parent f6537fc commit f5b1b73
Show file tree
Hide file tree
Showing 19 changed files with 1,335 additions and 809 deletions.
104 changes: 72 additions & 32 deletions src/conflict.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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},
Expand Down Expand Up @@ -48,19 +49,24 @@ impl Conflict {
solver: &Solver<D, RT>,
) -> ConflictGraph {
let mut graph = DiGraph::<ConflictNode, ConflictEdge>::default();
let mut nodes: HashMap<InternalSolvableId, NodeIndex> = HashMap::default();
let mut nodes: HashMap<SolvableOrRootId, NodeIndex> = HashMap::default();
let mut excluded_nodes: HashMap<StringId, NodeIndex> = 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)));
Expand All @@ -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(...)`")
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -154,8 +191,8 @@ impl Conflict {

fn add_node(
graph: &mut DiGraph<ConflictNode, ConflictEdge>,
nodes: &mut HashMap<InternalSolvableId, NodeIndex>,
solvable_id: InternalSolvableId,
nodes: &mut HashMap<SolvableOrRootId, NodeIndex>,
solvable_id: SolvableOrRootId,
) -> NodeIndex {
*nodes
.entry(solvable_id)
Expand All @@ -176,15 +213,15 @@ 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
Excluded(StringId),
}

impl ConflictNode {
fn solvable_id(self) -> InternalSolvableId {
fn solvable_or_root(self) -> SolvableOrRootId {
match self {
ConflictNode::Solvable(solvable_id) => solvable_id,
ConflictNode::UnresolvedDependency => {
Expand All @@ -195,6 +232,10 @@ impl ConflictNode {
}
}
}

fn solvable(self) -> Option<SolvableId> {
self.solvable_or_root().solvable()
}
}

/// An edge in the graph representation of a [`Conflict`]
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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();

Expand Down Expand Up @@ -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;
};
Expand Down Expand Up @@ -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<InternalSolvableId> = HashSet::new();
let mut reported: HashSet<SolvableOrRootId> = HashSet::new();

// Note: we are only interested in requires edges here
let indenter = Indenter::new(top_level_indent);
Expand Down Expand Up @@ -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;
};

Expand Down Expand Up @@ -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);
Expand All @@ -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()
Expand Down Expand Up @@ -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,
Expand Down
Loading

0 comments on commit f5b1b73

Please sign in to comment.