Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

perf: reintroduce binary encoding of forbid clauses #91

Merged
merged 5 commits into from
Jan 2, 2025
Merged

perf: reintroduce binary encoding of forbid clauses #91

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
2c20a6c
refactor: remove refcell usage
baszalmstra Dec 28, 2024
9627cb5
refactor: introduce binary encoding of at most one constraints
baszalmstra Dec 31, 2024
401772c
Merge branch 'main' into refactor/variable_map
baszalmstra Jan 1, 2025
ac092e0
Merge remote-tracking branch 'upstream/main' into refactor/variable_map
baszalmstra Jan 2, 2025
a5e4e3e
add brackets
baszalmstra Jan 2, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
104 changes: 72 additions & 32 deletions src/conflict.rs
View file
Open in desktop
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
Loading