From 0586e742e6b94e76af1a7415054591a6050a15e4 Mon Sep 17 00:00:00 2001
From: prsabahrami
Date: Fri, 17 Jan 2025 15:12:31 -0500
Subject: [PATCH 01/41] initial commit for conditional dependencies support
---
cpp/include/resolvo.h | 9 ++++
cpp/src/lib.rs | 20 +++++++++
src/conflict.rs | 89 ++++++++++++++++++++++++++++++++++---
src/requirement.rs | 30 ++++++++++---
src/snapshot.rs | 8 ++++
src/solver/cache.rs | 5 +++
src/solver/clause.rs | 100 +++++++++++++++++++++++++++++++++++++++---
src/solver/mod.rs | 2 +-
8 files changed, 244 insertions(+), 19 deletions(-)
diff --git a/cpp/include/resolvo.h b/cpp/include/resolvo.h
index 97d00f5..c824df4 100644
--- a/cpp/include/resolvo.h
+++ b/cpp/include/resolvo.h
@@ -24,6 +24,15 @@ inline Requirement requirement_union(VersionSetUnionId id) {
return cbindgen_private::resolvo_requirement_union(id);
}
+/**
+ * Specifies a conditional requirement, where the requirement is only active when the condition is met.
+ * @param condition The version set that must be satisfied for the requirement to be active.
+ * @param requirement The version set that must be satisfied when the condition is met.
+ */
+inline Requirement requirement_conditional(VersionSetId condition, VersionSetId requirement) {
+ return cbindgen_private::resolvo_requirement_conditional(condition, requirement);
+}
+
/**
* Called to solve a package problem.
*
diff --git a/cpp/src/lib.rs b/cpp/src/lib.rs
index 781e365..8267d9e 100644
--- a/cpp/src/lib.rs
+++ b/cpp/src/lib.rs
@@ -48,6 +48,11 @@ pub enum Requirement {
/// cbindgen:derive-eq
/// cbindgen:derive-neq
Union(VersionSetUnionId),
+ /// Specifies a conditional requirement, where the requirement is only active when the condition is met.
+ /// First VersionSetId is the condition, second is the requirement.
+ /// cbindgen:derive-eq
+ /// cbindgen:derive-neq
+ ConditionalRequires(VersionSetId, VersionSetId),
}
impl From for crate::Requirement {
@@ -55,6 +60,9 @@ impl From for crate::Requirement {
match value {
resolvo::Requirement::Single(id) => Requirement::Single(id.into()),
resolvo::Requirement::Union(id) => Requirement::Union(id.into()),
+ resolvo::Requirement::ConditionalRequires(condition, requirement) => {
+ Requirement::ConditionalRequires(condition.into(), requirement.into())
+ }
}
}
}
@@ -64,6 +72,9 @@ impl From for resolvo::Requirement {
match value {
Requirement::Single(id) => resolvo::Requirement::Single(id.into()),
Requirement::Union(id) => resolvo::Requirement::Union(id.into()),
+ Requirement::ConditionalRequires(condition, requirement) => {
+ resolvo::Requirement::ConditionalRequires(condition.into(), requirement.into())
+ }
}
}
}
@@ -539,6 +550,15 @@ pub extern "C" fn resolvo_requirement_union(
Requirement::Union(version_set_union_id)
}
+#[no_mangle]
+#[allow(unused)]
+pub extern "C" fn resolvo_requirement_conditional(
+ condition: VersionSetId,
+ requirement: VersionSetId,
+) -> Requirement {
+ Requirement::ConditionalRequires(condition, requirement)
+}
+
#[cfg(test)]
mod tests {
use super::*;
diff --git a/src/conflict.rs b/src/conflict.rs
index 3d121b6..48bc77a 100644
--- a/src/conflict.rs
+++ b/src/conflict.rs
@@ -11,14 +11,17 @@ use petgraph::{
Direction,
};
-use crate::solver::variable_map::VariableOrigin;
use crate::{
internal::{
arena::ArenaId,
- id::{ClauseId, SolvableId, SolvableOrRootId, StringId, VersionSetId},
+ id::{ClauseId, SolvableId, SolvableOrRootId, StringId, VariableId, VersionSetId},
},
runtime::AsyncRuntime,
- solver::{clause::Clause, Solver},
+ solver::{
+ clause::Clause,
+ variable_map::{VariableMap, VariableOrigin},
+ Solver,
+ },
DependencyProvider, Interner, Requirement,
};
@@ -160,6 +163,49 @@ impl Conflict {
ConflictEdge::Conflict(ConflictCause::Constrains(version_set_id)),
);
}
+ &Clause::Conditional(package_id, condition, then_version_set_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(then_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(...)`")
+ });
+
+ if candidates.is_empty() {
+ tracing::trace!(
+ "{package_id:?} conditionally requires {then_version_set_id:?}, which has no candidates"
+ );
+ graph.add_edge(
+ package_node,
+ unresolved_node,
+ ConflictEdge::ConditionalRequires(then_version_set_id, condition),
+ );
+ } else {
+ for &candidate_id in candidates {
+ tracing::trace!("{package_id:?} conditionally requires {candidate_id:?}");
+
+ let candidate_node =
+ Self::add_node(&mut graph, &mut nodes, candidate_id.into());
+ graph.add_edge(
+ package_node,
+ candidate_node,
+ ConflictEdge::ConditionalRequires(then_version_set_id, condition),
+ );
+ }
+ }
+
+ // Add an edge for the unsatisfied condition if it exists
+ if let Some(condition_solvable) = condition.as_solvable(&solver.variable_map) {
+ let condition_node = Self::add_node(&mut graph, &mut nodes, condition_solvable.into());
+ graph.add_edge(
+ package_node,
+ condition_node,
+ ConflictEdge::Conflict(ConflictCause::UnsatisfiedCondition(condition)),
+ );
+ }
+ }
}
}
@@ -205,7 +251,7 @@ impl Conflict {
solver: &'a Solver,
) -> DisplayUnsat<'a, D> {
let graph = self.graph(solver);
- DisplayUnsat::new(graph, solver.provider())
+ DisplayUnsat::new(graph, solver.provider(), &solver.variable_map)
}
}
@@ -239,13 +285,15 @@ impl ConflictNode {
}
/// An edge in the graph representation of a [`Conflict`]
-#[derive(Copy, Clone, Hash, Eq, PartialEq, Ord, PartialOrd)]
+#[derive(Clone, Copy, Hash, Eq, PartialEq, Ord, PartialOrd)]
pub(crate) enum ConflictEdge {
/// The target node is a candidate for the dependency specified by the
/// [`Requirement`]
Requires(Requirement),
/// The target node is involved in a conflict, caused by `ConflictCause`
Conflict(ConflictCause),
+ /// The target node is a candidate for a conditional dependency
+ ConditionalRequires(Requirement, VariableId),
}
impl ConflictEdge {
@@ -253,12 +301,14 @@ impl ConflictEdge {
match self {
ConflictEdge::Requires(match_spec_id) => Some(match_spec_id),
ConflictEdge::Conflict(_) => None,
+ ConflictEdge::ConditionalRequires(match_spec_id, _) => Some(match_spec_id),
}
}
fn requires(self) -> Requirement {
match self {
ConflictEdge::Requires(match_spec_id) => match_spec_id,
+ ConflictEdge::ConditionalRequires(match_spec_id, _) => match_spec_id,
ConflictEdge::Conflict(_) => panic!("expected requires edge, found conflict"),
}
}
@@ -275,6 +325,8 @@ pub(crate) enum ConflictCause {
ForbidMultipleInstances,
/// The node was excluded
Excluded,
+ /// The condition for a conditional dependency was not satisfied
+ UnsatisfiedCondition(VariableId),
}
/// Represents a node that has been merged with others
@@ -307,6 +359,7 @@ impl ConflictGraph {
&self,
f: &mut impl std::io::Write,
interner: &impl Interner,
+ variable_map: &VariableMap,
simplify: bool,
) -> Result<(), std::io::Error> {
let graph = &self.graph;
@@ -356,6 +409,16 @@ impl ConflictGraph {
"already installed".to_string()
}
ConflictEdge::Conflict(ConflictCause::Excluded) => "excluded".to_string(),
+ ConflictEdge::Conflict(ConflictCause::UnsatisfiedCondition(condition)) => {
+ let condition_solvable = condition.as_solvable(variable_map)
+ .expect("condition must be a solvable");
+ format!("unsatisfied condition: {}", condition_solvable.display(interner))
+ }
+ ConflictEdge::ConditionalRequires(requirement, condition) => {
+ let condition_solvable = condition.as_solvable(variable_map)
+ .expect("condition must be a solvable");
+ format!("if {} then {}", condition_solvable.display(interner), requirement.display(interner))
+ }
};
let target = match target {
@@ -494,6 +557,7 @@ impl ConflictGraph {
.edges_directed(nx, Direction::Outgoing)
.map(|e| match e.weight() {
ConflictEdge::Requires(version_set_id) => (version_set_id, e.target()),
+ ConflictEdge::ConditionalRequires(version_set_id, _) => (version_set_id, e.target()),
ConflictEdge::Conflict(_) => unreachable!(),
})
.chunk_by(|(&version_set_id, _)| version_set_id);
@@ -540,6 +604,7 @@ impl ConflictGraph {
.edges_directed(nx, Direction::Outgoing)
.map(|e| match e.weight() {
ConflictEdge::Requires(version_set_id) => (version_set_id, e.target()),
+ ConflictEdge::ConditionalRequires(version_set_id, _) => (version_set_id, e.target()),
ConflictEdge::Conflict(_) => unreachable!(),
})
.chunk_by(|(&version_set_id, _)| version_set_id);
@@ -673,10 +738,11 @@ pub struct DisplayUnsat<'i, I: Interner> {
installable_set: HashSet,
missing_set: HashSet,
interner: &'i I,
+ variable_map: &'i VariableMap,
}
impl<'i, I: Interner> DisplayUnsat<'i, I> {
- pub(crate) fn new(graph: ConflictGraph, interner: &'i I) -> Self {
+ pub(crate) fn new(graph: ConflictGraph, interner: &'i I, variable_map: &'i VariableMap) -> Self {
let merged_candidates = graph.simplify(interner);
let installable_set = graph.get_installable_set();
let missing_set = graph.get_missing_set();
@@ -687,6 +753,7 @@ impl<'i, I: Interner> DisplayUnsat<'i, I> {
installable_set,
missing_set,
interner,
+ variable_map,
}
}
@@ -1020,6 +1087,7 @@ impl<'i, I: Interner> fmt::Display for DisplayUnsat<'i, I> {
let conflict = match e.weight() {
ConflictEdge::Requires(_) => continue,
ConflictEdge::Conflict(conflict) => conflict,
+ ConflictEdge::ConditionalRequires(_, _) => continue,
};
// The only possible conflict at the root level is a Locked conflict
@@ -1045,6 +1113,15 @@ impl<'i, I: Interner> fmt::Display for DisplayUnsat<'i, I> {
)?;
}
ConflictCause::Excluded => continue,
+ &ConflictCause::UnsatisfiedCondition(condition) => {
+ let condition_solvable = condition.as_solvable(self.variable_map)
+ .expect("condition must be a solvable");
+ writeln!(
+ f,
+ "{indent}condition {} is not satisfied",
+ condition_solvable.display(self.interner),
+ )?;
+ }
};
}
}
diff --git a/src/requirement.rs b/src/requirement.rs
index 244ec48..c8e876f 100644
--- a/src/requirement.rs
+++ b/src/requirement.rs
@@ -13,6 +13,9 @@ pub enum Requirement {
/// This variant is typically used for requirements that can be satisfied by two or more
/// version sets belonging to _different_ packages.
Union(VersionSetUnionId),
+ /// Specifies a conditional requirement, where the requirement is only active when the condition is met.
+ /// First VersionSetId is the condition, second is the requirement.
+ ConditionalRequires(VersionSetId, VersionSetId),
}
impl Default for Requirement {
@@ -46,12 +49,15 @@ impl Requirement {
&'i self,
interner: &'i impl Interner,
) -> impl Iterator- + 'i {
- match *self {
+ match self {
Requirement::Single(version_set) => {
- itertools::Either::Left(std::iter::once(version_set))
+ itertools::Either::Left(itertools::Either::Left(std::iter::once(*version_set)))
}
Requirement::Union(version_set_union) => {
- itertools::Either::Right(interner.version_sets_in_union(version_set_union))
+ itertools::Either::Left(itertools::Either::Right(interner.version_sets_in_union(*version_set_union)))
+ }
+ Requirement::ConditionalRequires(condition, requirement) => {
+ itertools::Either::Right(std::iter::once(*condition).chain(std::iter::once(*requirement)))
}
}
}
@@ -64,18 +70,18 @@ pub(crate) struct DisplayRequirement<'i, I: Interner> {
impl<'i, I: Interner> Display for DisplayRequirement<'i, I> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
- match *self.requirement {
+ match self.requirement {
Requirement::Single(version_set) => write!(
f,
"{} {}",
self.interner
- .display_name(self.interner.version_set_name(version_set)),
- self.interner.display_version_set(version_set)
+ .display_name(self.interner.version_set_name(*version_set)),
+ self.interner.display_version_set(*version_set)
),
Requirement::Union(version_set_union) => {
let formatted_version_sets = self
.interner
- .version_sets_in_union(version_set_union)
+ .version_sets_in_union(*version_set_union)
.format_with(" | ", |version_set, f| {
f(&format_args!(
"{} {}",
@@ -87,6 +93,16 @@ impl<'i, I: Interner> Display for DisplayRequirement<'i, I> {
write!(f, "{}", formatted_version_sets)
}
+ Requirement::ConditionalRequires(condition, requirement) => {
+ write!(
+ f,
+ "if {} then {} {}",
+ self.interner.display_version_set(*condition),
+ self.interner
+ .display_name(self.interner.version_set_name(*requirement)),
+ self.interner.display_version_set(*requirement)
+ )
+ }
}
}
}
diff --git a/src/snapshot.rs b/src/snapshot.rs
index 0b8b6d2..0c4a986 100644
--- a/src/snapshot.rs
+++ b/src/snapshot.rs
@@ -243,6 +243,14 @@ impl DependencySnapshot {
.version_set_unions
.insert(version_set_union_id, version_sets);
}
+ Requirement::ConditionalRequires(condition, requirement) => {
+ if seen.insert(Element::VersionSet(condition)) {
+ queue.push_back(Element::VersionSet(condition));
+ }
+ if seen.insert(Element::VersionSet(requirement)) {
+ queue.push_back(Element::VersionSet(requirement));
+ }
+ }
}
}
}
diff --git a/src/solver/cache.rs b/src/solver/cache.rs
index cf6c6cc..00c8c92 100644
--- a/src/solver/cache.rs
+++ b/src/solver/cache.rs
@@ -280,6 +280,11 @@ impl SolverCache {
}
}
}
+ Requirement::ConditionalRequires(condition, requirement) => {
+ let candidates = self.get_or_cache_sorted_candidates_for_version_set(condition).await?;
+ let sorted_candidates = self.get_or_cache_sorted_candidates_for_version_set(requirement).await?;
+ Ok(sorted_candidates)
+ }
}
}
diff --git a/src/solver/clause.rs b/src/solver/clause.rs
index f034130..4e41c0e 100644
--- a/src/solver/clause.rs
+++ b/src/solver/clause.rs
@@ -11,12 +11,10 @@ use crate::{
internal::{
arena::{Arena, ArenaId},
id::{ClauseId, LearntClauseId, StringId, VersionSetId},
- },
- solver::{
+ }, solver::{
decision_map::DecisionMap, decision_tracker::DecisionTracker, variable_map::VariableMap,
VariableId,
- },
- Interner, NameId, Requirement,
+ }, DependencyProvider, Interner, NameId, Requirement
};
/// Represents a single clause in the SAT problem
@@ -46,7 +44,7 @@ use crate::{
/// limited set of clauses. There are thousands of clauses for a particular
/// dependency resolution problem, and we try to keep the [`Clause`] enum small.
/// A naive implementation would store a `Vec`.
-#[derive(Copy, Clone, Debug)]
+#[derive(Clone, Copy, Debug)]
pub(crate) enum Clause {
/// An assertion that the root solvable must be installed
///
@@ -77,6 +75,10 @@ pub(crate) enum Clause {
///
/// In SAT terms: (¬A ∨ ¬B)
Constrains(VariableId, VariableId, VersionSetId),
+ /// In SAT terms: (¬A ∨ ¬C ∨ B1 ∨ B2 ∨ ... ∨ B99), where A is the solvable,
+ /// C is the condition, and B1 to B99 represent the possible candidates for
+ /// the provided [`Requirement`].
+ Conditional(VariableId, VariableId, Requirement),
/// Forbids the package on the right-hand side
///
/// Note that the package on the left-hand side is not part of the clause,
@@ -230,6 +232,45 @@ impl Clause {
)
}
+ fn conditional_impl(
+ package_id: VariableId,
+ condition: VariableId,
+ then: Requirement,
+ candidates: impl IntoIterator
- ,
+ decision_tracker: &DecisionTracker,
+ ) -> (Self, Option<[Literal; 2]>, bool) {
+ // It only makes sense to introduce a conditional clause when the package is undecided or going to be installed
+ assert_ne!(decision_tracker.assigned_value(package_id), Some(false));
+ assert_ne!(decision_tracker.assigned_value(condition), Some(false));
+
+ let kind = Clause::Conditional(package_id, condition, then);
+ 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,
+ Some([package_id.negative(), watched_candidate.positive()]),
+ false,
+ ),
+
+ // All candidates are assigned to false! Therefore, the clause conflicts with the
+ // current decisions. There are no valid watches for it at the moment, but we will
+ // assign default ones nevertheless, because they will become valid after the solver
+ // restarts.
+ None => (
+ kind,
+ Some([package_id.negative(), first_candidate.positive()]),
+ true,
+ ),
+ }
+ } else {
+ // If there are no candidates there is no need to watch anything.
+ (kind, None, false)
+ }
+ }
+
/// Tries to fold over all the literals in the clause.
///
/// This function is useful to iterate, find, or filter the literals in a
@@ -272,6 +313,17 @@ impl Clause {
Clause::Lock(_, s) => [s.negative(), VariableId::root().negative()]
.into_iter()
.try_fold(init, visit),
+ Clause::Conditional(package_id, condition, then) => {
+ [package_id.negative(), condition.negative()]
+ .into_iter()
+ .chain(
+ requirements_to_sorted_candidates[&then]
+ .iter()
+ .flatten()
+ .map(|&s| s.positive()),
+ )
+ .try_fold(init, visit)
+ }
}
}
@@ -419,6 +471,33 @@ impl WatchedLiterals {
(Self::from_kind_and_initial_watches(watched_literals), kind)
}
+ /// Shorthand method to construct a [Clause::Conditional] without requiring
+ /// complicated arguments.
+ ///
+ /// The returned boolean value is true when adding the clause resulted in a
+ /// conflict.
+ pub fn conditional(
+ package_id: VariableId,
+ condition: VariableId,
+ then: Requirement,
+ candidates: impl IntoIterator
- ,
+ decision_tracker: &DecisionTracker,
+ ) -> (Option, bool, Clause) {
+ let (kind, watched_literals, conflict) = Clause::conditional_impl(
+ package_id,
+ condition,
+ then,
+ candidates,
+ decision_tracker,
+ );
+
+ (
+ WatchedLiterals::from_kind_and_initial_watches(watched_literals),
+ conflict,
+ kind,
+ )
+ }
+
fn from_kind_and_initial_watches(watched_literals: Option<[Literal; 2]>) -> Option {
let watched_literals = watched_literals?;
debug_assert!(watched_literals[0] != watched_literals[1]);
@@ -611,6 +690,17 @@ impl<'i, I: Interner> Display for ClauseDisplay<'i, I> {
other,
)
}
+ Clause::Conditional(package_id, condition, then) => {
+ write!(
+ f,
+ "Conditional({}({:?}), {}({:?}), {})",
+ package_id.display(self.variable_map, self.interner),
+ package_id,
+ condition.display(self.variable_map, self.interner),
+ condition,
+ then.display(self.interner)
+ )
+ }
}
}
}
diff --git a/src/solver/mod.rs b/src/solver/mod.rs
index 8c0e026..cf3adf0 100644
--- a/src/solver/mod.rs
+++ b/src/solver/mod.rs
@@ -695,7 +695,7 @@ impl Solver {
fn resolve_dependencies(&mut self, mut level: u32) -> Result {
loop {
// Make a decision. If no decision could be made it means the problem is
- // satisfyable.
+ // satisfiable.
let Some((candidate, required_by, clause_id)) = self.decide() else {
break;
};
From 0383bfc5a4efa7b1ff4bca49fe6e536d18edcaad Mon Sep 17 00:00:00 2001
From: prsabahrami
Date: Tue, 21 Jan 2025 11:19:10 -0500
Subject: [PATCH 02/41] Add the watched literals for conditional requirements
---
src/conflict.rs | 75 ++++++++++---------
src/requirement.rs | 35 +++++----
src/solver/cache.rs | 8 +-
src/solver/clause.rs | 114 +++++++++++++++--------------
src/solver/mod.rs | 171 +++++++++++++++++++++++++++++++++++++------
5 files changed, 277 insertions(+), 126 deletions(-)
diff --git a/src/conflict.rs b/src/conflict.rs
index 48bc77a..e17ec73 100644
--- a/src/conflict.rs
+++ b/src/conflict.rs
@@ -163,7 +163,7 @@ impl Conflict {
ConflictEdge::Conflict(ConflictCause::Constrains(version_set_id)),
);
}
- &Clause::Conditional(package_id, condition, then_version_set_id) => {
+ &Clause::Conditional(package_id, condition) => {
let solvable = package_id
.as_solvable_or_root(&solver.variable_map)
.expect("only solvables can be excluded");
@@ -172,33 +172,36 @@ impl Conflict {
let candidates = solver.async_runtime.block_on(solver.cache.get_or_cache_sorted_candidates(then_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(...)`")
});
-
+
if candidates.is_empty() {
tracing::trace!(
- "{package_id:?} conditionally requires {then_version_set_id:?}, which has no candidates"
+ "{package_id:?} conditionally requires {condition:?}, which has no candidates"
);
graph.add_edge(
package_node,
unresolved_node,
- ConflictEdge::ConditionalRequires(then_version_set_id, condition),
+ ConflictEdge::ConditionalRequires(condition),
);
} else {
for &candidate_id in candidates {
- tracing::trace!("{package_id:?} conditionally requires {candidate_id:?}");
+ tracing::trace!(
+ "{package_id:?} conditionally requires {candidate_id:?}"
+ );
let candidate_node =
Self::add_node(&mut graph, &mut nodes, candidate_id.into());
graph.add_edge(
package_node,
candidate_node,
- ConflictEdge::ConditionalRequires(then_version_set_id, condition),
+ ConflictEdge::ConditionalRequires(condition),
);
}
}
-
+
// Add an edge for the unsatisfied condition if it exists
if let Some(condition_solvable) = condition.as_solvable(&solver.variable_map) {
- let condition_node = Self::add_node(&mut graph, &mut nodes, condition_solvable.into());
+ let condition_node =
+ Self::add_node(&mut graph, &mut nodes, condition_solvable.into());
graph.add_edge(
package_node,
condition_node,
@@ -251,7 +254,7 @@ impl Conflict {
solver: &'a Solver,
) -> DisplayUnsat<'a, D> {
let graph = self.graph(solver);
- DisplayUnsat::new(graph, solver.provider(), &solver.variable_map)
+ DisplayUnsat::new(graph, solver.provider())
}
}
@@ -293,22 +296,22 @@ pub(crate) enum ConflictEdge {
/// The target node is involved in a conflict, caused by `ConflictCause`
Conflict(ConflictCause),
/// The target node is a candidate for a conditional dependency
- ConditionalRequires(Requirement, VariableId),
+ ConditionalRequires(Requirement),
}
impl ConflictEdge {
fn try_requires(self) -> Option {
match self {
- ConflictEdge::Requires(match_spec_id) => Some(match_spec_id),
+ ConflictEdge::Requires(match_spec_id)
+ | ConflictEdge::ConditionalRequires(match_spec_id) => Some(match_spec_id),
ConflictEdge::Conflict(_) => None,
- ConflictEdge::ConditionalRequires(match_spec_id, _) => Some(match_spec_id),
}
}
fn requires(self) -> Requirement {
match self {
- ConflictEdge::Requires(match_spec_id) => match_spec_id,
- ConflictEdge::ConditionalRequires(match_spec_id, _) => match_spec_id,
+ ConflictEdge::Requires(match_spec_id)
+ | ConflictEdge::ConditionalRequires(match_spec_id) => match_spec_id,
ConflictEdge::Conflict(_) => panic!("expected requires edge, found conflict"),
}
}
@@ -326,7 +329,7 @@ pub(crate) enum ConflictCause {
/// The node was excluded
Excluded,
/// The condition for a conditional dependency was not satisfied
- UnsatisfiedCondition(VariableId),
+ UnsatisfiedCondition(Requirement),
}
/// Represents a node that has been merged with others
@@ -359,7 +362,6 @@ impl ConflictGraph {
&self,
f: &mut impl std::io::Write,
interner: &impl Interner,
- variable_map: &VariableMap,
simplify: bool,
) -> Result<(), std::io::Error> {
let graph = &self.graph;
@@ -410,14 +412,16 @@ impl ConflictGraph {
}
ConflictEdge::Conflict(ConflictCause::Excluded) => "excluded".to_string(),
ConflictEdge::Conflict(ConflictCause::UnsatisfiedCondition(condition)) => {
- let condition_solvable = condition.as_solvable(variable_map)
- .expect("condition must be a solvable");
- format!("unsatisfied condition: {}", condition_solvable.display(interner))
+ // let condition_solvable = condition.as_solvable(&solver.variable_map)
+ // .expect("condition must be a solvable");
+ // format!("unsatisfied condition: {}", condition_solvable.display(interner))
+ todo!()
}
ConflictEdge::ConditionalRequires(requirement, condition) => {
- let condition_solvable = condition.as_solvable(variable_map)
- .expect("condition must be a solvable");
- format!("if {} then {}", condition_solvable.display(interner), requirement.display(interner))
+ // let condition_solvable = condition.as_solvable(&solver.variable_map)
+ // .expect("condition must be a solvable");
+ // format!("if {} then {}", condition_solvable.display(interner), requirement.display(interner))
+ todo!()
}
};
@@ -557,7 +561,9 @@ impl ConflictGraph {
.edges_directed(nx, Direction::Outgoing)
.map(|e| match e.weight() {
ConflictEdge::Requires(version_set_id) => (version_set_id, e.target()),
- ConflictEdge::ConditionalRequires(version_set_id, _) => (version_set_id, e.target()),
+ ConflictEdge::ConditionalRequires(version_set_id, _) => {
+ (version_set_id, e.target())
+ }
ConflictEdge::Conflict(_) => unreachable!(),
})
.chunk_by(|(&version_set_id, _)| version_set_id);
@@ -604,7 +610,9 @@ impl ConflictGraph {
.edges_directed(nx, Direction::Outgoing)
.map(|e| match e.weight() {
ConflictEdge::Requires(version_set_id) => (version_set_id, e.target()),
- ConflictEdge::ConditionalRequires(version_set_id, _) => (version_set_id, e.target()),
+ ConflictEdge::ConditionalRequires(version_set_id, _) => {
+ (version_set_id, e.target())
+ }
ConflictEdge::Conflict(_) => unreachable!(),
})
.chunk_by(|(&version_set_id, _)| version_set_id);
@@ -738,11 +746,10 @@ pub struct DisplayUnsat<'i, I: Interner> {
installable_set: HashSet,
missing_set: HashSet,
interner: &'i I,
- variable_map: &'i VariableMap,
}
impl<'i, I: Interner> DisplayUnsat<'i, I> {
- pub(crate) fn new(graph: ConflictGraph, interner: &'i I, variable_map: &'i VariableMap) -> Self {
+ pub(crate) fn new(graph: ConflictGraph, interner: &'i I) -> Self {
let merged_candidates = graph.simplify(interner);
let installable_set = graph.get_installable_set();
let missing_set = graph.get_missing_set();
@@ -753,7 +760,6 @@ impl<'i, I: Interner> DisplayUnsat<'i, I> {
installable_set,
missing_set,
interner,
- variable_map,
}
}
@@ -1114,13 +1120,14 @@ impl<'i, I: Interner> fmt::Display for DisplayUnsat<'i, I> {
}
ConflictCause::Excluded => continue,
&ConflictCause::UnsatisfiedCondition(condition) => {
- let condition_solvable = condition.as_solvable(self.variable_map)
- .expect("condition must be a solvable");
- writeln!(
- f,
- "{indent}condition {} is not satisfied",
- condition_solvable.display(self.interner),
- )?;
+ // let condition_solvable = condition.as_solvable(self.variable_map)
+ // .expect("condition must be a solvable");
+ // writeln!(
+ // f,
+ // "{indent}condition {} is not satisfied",
+ // condition_solvable.display(self.interner),
+ // )?;
+ todo!()
}
};
}
diff --git a/src/requirement.rs b/src/requirement.rs
index c8e876f..62589f3 100644
--- a/src/requirement.rs
+++ b/src/requirement.rs
@@ -48,17 +48,22 @@ impl Requirement {
pub(crate) fn version_sets<'i>(
&'i self,
interner: &'i impl Interner,
- ) -> impl Iterator
- + 'i {
+ ) -> (
+ impl Iterator
- + 'i,
+ Option,
+ ) {
match self {
Requirement::Single(version_set) => {
- itertools::Either::Left(itertools::Either::Left(std::iter::once(*version_set)))
- }
- Requirement::Union(version_set_union) => {
- itertools::Either::Left(itertools::Either::Right(interner.version_sets_in_union(*version_set_union)))
- }
- Requirement::ConditionalRequires(condition, requirement) => {
- itertools::Either::Right(std::iter::once(*condition).chain(std::iter::once(*requirement)))
+ (itertools::Either::Left(std::iter::once(*version_set)), None)
}
+ Requirement::Union(version_set_union) => (
+ itertools::Either::Right(interner.version_sets_in_union(*version_set_union)),
+ None,
+ ),
+ Requirement::ConditionalRequires(condition, requirement) => (
+ itertools::Either::Left(std::iter::once(*requirement)),
+ Some(*condition),
+ ),
}
}
}
@@ -70,18 +75,18 @@ pub(crate) struct DisplayRequirement<'i, I: Interner> {
impl<'i, I: Interner> Display for DisplayRequirement<'i, I> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
- match self.requirement {
+ match *self.requirement {
Requirement::Single(version_set) => write!(
f,
"{} {}",
self.interner
- .display_name(self.interner.version_set_name(*version_set)),
- self.interner.display_version_set(*version_set)
+ .display_name(self.interner.version_set_name(version_set)),
+ self.interner.display_version_set(version_set)
),
Requirement::Union(version_set_union) => {
let formatted_version_sets = self
.interner
- .version_sets_in_union(*version_set_union)
+ .version_sets_in_union(version_set_union)
.format_with(" | ", |version_set, f| {
f(&format_args!(
"{} {}",
@@ -97,10 +102,10 @@ impl<'i, I: Interner> Display for DisplayRequirement<'i, I> {
write!(
f,
"if {} then {} {}",
- self.interner.display_version_set(*condition),
+ self.interner.display_version_set(condition),
self.interner
- .display_name(self.interner.version_set_name(*requirement)),
- self.interner.display_version_set(*requirement)
+ .display_name(self.interner.version_set_name(requirement)),
+ self.interner.display_version_set(requirement)
)
}
}
diff --git a/src/solver/cache.rs b/src/solver/cache.rs
index 00c8c92..952c8cb 100644
--- a/src/solver/cache.rs
+++ b/src/solver/cache.rs
@@ -281,8 +281,12 @@ impl SolverCache {
}
}
Requirement::ConditionalRequires(condition, requirement) => {
- let candidates = self.get_or_cache_sorted_candidates_for_version_set(condition).await?;
- let sorted_candidates = self.get_or_cache_sorted_candidates_for_version_set(requirement).await?;
+ let candidates = self
+ .get_or_cache_sorted_candidates_for_version_set(condition)
+ .await?;
+ let sorted_candidates = self
+ .get_or_cache_sorted_candidates_for_version_set(requirement)
+ .await?;
Ok(sorted_candidates)
}
}
diff --git a/src/solver/clause.rs b/src/solver/clause.rs
index 4e41c0e..15f9d44 100644
--- a/src/solver/clause.rs
+++ b/src/solver/clause.rs
@@ -11,10 +11,12 @@ use crate::{
internal::{
arena::{Arena, ArenaId},
id::{ClauseId, LearntClauseId, StringId, VersionSetId},
- }, solver::{
+ },
+ solver::{
decision_map::DecisionMap, decision_tracker::DecisionTracker, variable_map::VariableMap,
VariableId,
- }, DependencyProvider, Interner, NameId, Requirement
+ },
+ Interner, NameId, Requirement,
};
/// Represents a single clause in the SAT problem
@@ -78,7 +80,7 @@ pub(crate) enum Clause {
/// In SAT terms: (¬A ∨ ¬C ∨ B1 ∨ B2 ∨ ... ∨ B99), where A is the solvable,
/// C is the condition, and B1 to B99 represent the possible candidates for
/// the provided [`Requirement`].
- Conditional(VariableId, VariableId, Requirement),
+ Conditional(VariableId, Requirement),
/// Forbids the package on the right-hand side
///
/// Note that the package on the left-hand side is not part of the clause,
@@ -232,42 +234,53 @@ impl Clause {
)
}
- fn conditional_impl(
- package_id: VariableId,
- condition: VariableId,
- then: Requirement,
- candidates: impl IntoIterator
- ,
+ fn conditional(
+ parent_id: VariableId,
+ requirement: Requirement,
decision_tracker: &DecisionTracker,
+ requirement_candidates: impl IntoIterator
- ,
+ condition_candidates: impl IntoIterator
- ,
) -> (Self, Option<[Literal; 2]>, bool) {
- // It only makes sense to introduce a conditional clause when the package is undecided or going to be installed
- assert_ne!(decision_tracker.assigned_value(package_id), Some(false));
- assert_ne!(decision_tracker.assigned_value(condition), Some(false));
+ assert_ne!(decision_tracker.assigned_value(parent_id), Some(false));
- let kind = Clause::Conditional(package_id, condition, then);
- let mut candidates = candidates.into_iter().peekable();
+ let mut candidates = condition_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,
- Some([package_id.negative(), watched_candidate.positive()]),
- false,
- ),
-
- // All candidates are assigned to false! Therefore, the clause conflicts with the
- // current decisions. There are no valid watches for it at the moment, but we will
- // assign default ones nevertheless, because they will become valid after the solver
- // restarts.
- None => (
- kind,
- Some([package_id.negative(), first_candidate.positive()]),
- true,
+ match condition_candidates
+ .into_iter()
+ .find(|&condition_id| decision_tracker.assigned_value(condition_id) == Some(true))
+ {
+ Some(_) => Clause::requires(
+ parent_id,
+ requirement,
+ requirement_candidates,
+ decision_tracker,
),
+ None => {
+ if let Some(first_unset_candidate) = candidates.find(|&condition_id| {
+ decision_tracker.assigned_value(condition_id) != Some(false)
+ }) {
+ (
+ Clause::Conditional(parent_id, requirement),
+ Some([parent_id.negative(), first_unset_candidate.negative()]),
+ false,
+ )
+ } else {
+ // All condition candidates are assigned to false! Therefore, the clause conflicts with the
+ // current decisions. There are no valid watches for it at the moment, but we will
+ // assign default ones nevertheless, because they will become valid after the solver
+ // restarts.
+ (
+ Clause::Conditional(parent_id, requirement),
+ Some([parent_id.negative(), first_candidate.negative()]),
+ true,
+ )
+ }
+ }
}
} else {
- // If there are no candidates there is no need to watch anything.
- (kind, None, false)
+ // No condition candidates, so no need to watch anything
+ (Clause::Conditional(parent_id, requirement), None, false)
}
}
@@ -313,17 +326,14 @@ impl Clause {
Clause::Lock(_, s) => [s.negative(), VariableId::root().negative()]
.into_iter()
.try_fold(init, visit),
- Clause::Conditional(package_id, condition, then) => {
- [package_id.negative(), condition.negative()]
- .into_iter()
- .chain(
- requirements_to_sorted_candidates[&then]
- .iter()
- .flatten()
- .map(|&s| s.positive()),
- )
- .try_fold(init, visit)
- }
+ Clause::Conditional(package_id, condition) => iter::once(package_id.negative())
+ .chain(
+ requirements_to_sorted_candidates[&condition]
+ .iter()
+ .flatten()
+ .map(|&s| s.positive()),
+ )
+ .try_fold(init, visit),
}
}
@@ -478,17 +488,17 @@ impl WatchedLiterals {
/// conflict.
pub fn conditional(
package_id: VariableId,
- condition: VariableId,
- then: Requirement,
- candidates: impl IntoIterator
- ,
+ condition: Requirement,
decision_tracker: &DecisionTracker,
+ requirement_candidates: impl IntoIterator
- ,
+ condition_candidates: impl IntoIterator
- ,
) -> (Option, bool, Clause) {
- let (kind, watched_literals, conflict) = Clause::conditional_impl(
+ let (kind, watched_literals, conflict) = Clause::conditional(
package_id,
condition,
- then,
- candidates,
decision_tracker,
+ requirement_candidates,
+ condition_candidates,
);
(
@@ -690,15 +700,13 @@ impl<'i, I: Interner> Display for ClauseDisplay<'i, I> {
other,
)
}
- Clause::Conditional(package_id, condition, then) => {
+ Clause::Conditional(package_id, condition) => {
write!(
f,
- "Conditional({}({:?}), {}({:?}), {})",
+ "Conditional({}({:?}), {})",
package_id.display(self.variable_map, self.interner),
package_id,
- condition.display(self.variable_map, self.interner),
- condition,
- then.display(self.interner)
+ condition.display(self.interner),
)
}
}
diff --git a/src/solver/mod.rs b/src/solver/mod.rs
index cf3adf0..5dfea63 100644
--- a/src/solver/mod.rs
+++ b/src/solver/mod.rs
@@ -788,6 +788,8 @@ impl Solver {
// Get the candidates for the individual version sets.
let version_set_candidates = &self.requirement_to_sorted_candidates[deps];
+ let (version_sets, condition) = deps.version_sets(self.provider());
+
// 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.
@@ -795,10 +797,7 @@ impl Solver {
// 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)
- {
+ for (version_set, candidates) in version_sets.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(
@@ -1536,6 +1535,12 @@ async fn add_clauses_for_solvables(
requirement: Requirement,
candidates: Vec<&'i [SolvableId]>,
},
+ ConditionalSortedCandidates {
+ solvable_id: SolvableOrRootId,
+ requirement: Requirement,
+ requirement_candidates: Vec<&'i [SolvableId]>,
+ condition_candidates: &'i [SolvableId],
+ },
NonMatchingCandidates {
solvable_id: SolvableOrRootId,
version_set_id: VersionSetId,
@@ -1637,10 +1642,13 @@ async fn add_clauses_for_solvables(
}
};
- for version_set_id in requirements
+ for (version_set_id, condition) in requirements
.iter()
- .flat_map(|requirement| requirement.version_sets(cache.provider()))
- .chain(constrains.iter().copied())
+ .flat_map(|requirement| {
+ let (version_sets, condition) = requirement.version_sets(cache.provider());
+ version_sets.map(move |vs| (vs, condition))
+ })
+ .chain(constrains.iter().map(|&vs| (vs, None)))
{
let dependency_name = cache.provider().version_set_name(version_set_id);
if clauses_added_for_package.insert(dependency_name) {
@@ -1661,28 +1669,56 @@ async fn add_clauses_for_solvables(
.boxed_local(),
);
}
+
+ if let Some(condition) = condition {
+ let condition_name = cache.provider().version_set_name(condition);
+ if clauses_added_for_package.insert(condition_name) {
+ pending_futures.push(
+ async move {
+ let condition_candidates =
+ cache.get_or_cache_candidates(condition_name).await?;
+ Ok(TaskResult::Candidates {
+ name_id: condition_name,
+ package_candidates: &condition_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?;
+ let (version_sets, condition) =
+ requirement.version_sets(cache.provider());
+ let candidates =
+ futures::future::try_join_all(version_sets.map(|version_set| {
+ cache
+ .get_or_cache_sorted_candidates_for_version_set(version_set)
+ }))
+ .await?;
- Ok(TaskResult::SortedCandidates {
- solvable_id,
- requirement,
- candidates,
- })
+ if let Some(condition) = condition {
+ let condition_candidates = cache
+ .get_or_cache_sorted_candidates_for_version_set(condition)
+ .await?;
+
+ Ok(TaskResult::ConditionalSortedCandidates {
+ solvable_id,
+ requirement,
+ requirement_candidates: candidates,
+ condition_candidates,
+ })
+ } else {
+ Ok(TaskResult::SortedCandidates {
+ solvable_id,
+ requirement,
+ candidates,
+ })
+ }
}
.boxed_local(),
);
@@ -1846,6 +1882,97 @@ async fn add_clauses_for_solvables(
output.negative_assertions.push((variable, clause_id));
}
}
+ TaskResult::ConditionalSortedCandidates {
+ solvable_id,
+ requirement,
+ requirement_candidates,
+ condition_candidates,
+ } => {
+ tracing::trace!(
+ "conditional candidates 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(),
+ };
+
+ // Cache the candidates for this requirement
+ let version_set_variables: Vec<_> = requirement_candidates
+ .iter()
+ .map(|candidates| {
+ candidates
+ .iter()
+ .map(|&candidate| variable_map.intern_solvable(candidate))
+ .collect::>()
+ })
+ .collect();
+
+ requirement_to_sorted_candidates
+ .insert(requirement.clone(), version_set_variables.clone());
+
+ // Add forbidden clauses for the candidates
+ for candidates in requirement_candidates.iter() {
+ for &candidate in *candidates {
+ let candidate_var = variable_map.intern_solvable(candidate);
+ 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 (watched_literals, kind) = WatchedLiterals::forbid_multiple(
+ a,
+ if positive { b.positive() } else { b.negative() },
+ name_id,
+ );
+ let clause_id = clauses.alloc(watched_literals, kind);
+ debug_assert!(
+ clauses.watched_literals[clause_id.to_usize()].is_some()
+ );
+ output.clauses_to_watch.push(clause_id);
+ },
+ || variable_map.alloc_forbid_multiple_variable(name_id),
+ );
+ }
+ }
+
+ // Add the requirements clause
+ let no_candidates = requirement_candidates
+ .iter()
+ .all(|candidates| candidates.is_empty());
+ let condition_variables = condition_candidates
+ .iter()
+ .map(|&candidate| variable_map.intern_solvable(candidate))
+ .collect::>();
+
+ let (watched_literals, conflict, kind) = WatchedLiterals::conditional(
+ variable,
+ requirement,
+ decision_tracker,
+ version_set_variables.iter().flatten().copied(),
+ condition_variables.iter().copied(),
+ );
+
+ let has_watches = watched_literals.is_some();
+ let clause_id = clauses.alloc(watched_literals, 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,
From 2e6d57b9823ec2d974105eb8f8ce989bc3a37441 Mon Sep 17 00:00:00 2001
From: prsabahrami
Date: Tue, 21 Jan 2025 16:24:02 -0500
Subject: [PATCH 03/41] move conditional requirements to a separate struct
---
cpp/src/lib.rs | 57 ++++----
src/conflict.rs | 63 ++++-----
src/lib.rs | 4 +-
src/requirement.rs | 84 ++++++++----
src/snapshot.rs | 12 +-
src/solver/cache.rs | 9 --
src/solver/clause.rs | 120 ++++++++++-------
src/solver/mod.rs | 219 +++++++++++--------------------
tools/solve-snapshot/src/main.rs | 3 +-
9 files changed, 279 insertions(+), 292 deletions(-)
diff --git a/cpp/src/lib.rs b/cpp/src/lib.rs
index 8267d9e..04d05c0 100644
--- a/cpp/src/lib.rs
+++ b/cpp/src/lib.rs
@@ -31,6 +31,17 @@ impl From for resolvo::SolvableId {
}
}
+/// Specifies a conditional requirement, where the requirement is only active when the condition is met.
+/// First VersionSetId is the condition, second is the requirement.
+/// cbindgen:derive-eq
+/// cbindgen:derive-neq
+#[repr(C)]
+#[derive(Copy, Clone)]
+pub struct ConditionalRequirement {
+ pub condition: Option,
+ pub requirement: Requirement,
+}
+
/// Specifies the dependency of a solvable on a set of version sets.
/// cbindgen:derive-eq
/// cbindgen:derive-neq
@@ -48,11 +59,6 @@ pub enum Requirement {
/// cbindgen:derive-eq
/// cbindgen:derive-neq
Union(VersionSetUnionId),
- /// Specifies a conditional requirement, where the requirement is only active when the condition is met.
- /// First VersionSetId is the condition, second is the requirement.
- /// cbindgen:derive-eq
- /// cbindgen:derive-neq
- ConditionalRequires(VersionSetId, VersionSetId),
}
impl From for crate::Requirement {
@@ -60,9 +66,6 @@ impl From for crate::Requirement {
match value {
resolvo::Requirement::Single(id) => Requirement::Single(id.into()),
resolvo::Requirement::Union(id) => Requirement::Union(id.into()),
- resolvo::Requirement::ConditionalRequires(condition, requirement) => {
- Requirement::ConditionalRequires(condition.into(), requirement.into())
- }
}
}
}
@@ -72,9 +75,24 @@ impl From for resolvo::Requirement {
match value {
Requirement::Single(id) => resolvo::Requirement::Single(id.into()),
Requirement::Union(id) => resolvo::Requirement::Union(id.into()),
- Requirement::ConditionalRequires(condition, requirement) => {
- resolvo::Requirement::ConditionalRequires(condition.into(), requirement.into())
- }
+ }
+ }
+}
+
+impl From for ConditionalRequirement {
+ fn from(value: resolvo::ConditionalRequirement) -> Self {
+ Self {
+ condition: value.condition.map(|id| id.into()),
+ requirement: value.requirement.into(),
+ }
+ }
+}
+
+impl From for resolvo::ConditionalRequirement {
+ fn from(value: ConditionalRequirement) -> Self {
+ Self {
+ condition: value.condition.map(|id| id.into()),
+ requirement: value.requirement.into(),
}
}
}
@@ -173,7 +191,7 @@ pub struct Dependencies {
/// A pointer to the first element of a list of requirements. Requirements
/// defines which packages should be installed alongside the depending
/// package and the constraints applied to the package.
- pub requirements: Vector,
+ pub conditional_requirements: Vector,
/// Defines additional constraints on packages that may or may not be part
/// of the solution. Different from `requirements`, packages in this set
@@ -470,8 +488,8 @@ impl<'d> resolvo::DependencyProvider for &'d DependencyProvider {
};
resolvo::Dependencies::Known(KnownDependencies {
- requirements: dependencies
- .requirements
+ conditional_requirements: dependencies
+ .conditional_requirements
.into_iter()
.map(Into::into)
.collect(),
@@ -486,7 +504,7 @@ impl<'d> resolvo::DependencyProvider for &'d DependencyProvider {
#[repr(C)]
pub struct Problem<'a> {
- pub requirements: Slice<'a, Requirement>,
+ pub requirements: Slice<'a, ConditionalRequirement>,
pub constraints: Slice<'a, VersionSetId>,
pub soft_requirements: Slice<'a, SolvableId>,
}
@@ -550,15 +568,6 @@ pub extern "C" fn resolvo_requirement_union(
Requirement::Union(version_set_union_id)
}
-#[no_mangle]
-#[allow(unused)]
-pub extern "C" fn resolvo_requirement_conditional(
- condition: VersionSetId,
- requirement: VersionSetId,
-) -> Requirement {
- Requirement::ConditionalRequires(condition, requirement)
-}
-
#[cfg(test)]
mod tests {
use super::*;
diff --git a/src/conflict.rs b/src/conflict.rs
index e17ec73..6c1ace8 100644
--- a/src/conflict.rs
+++ b/src/conflict.rs
@@ -14,14 +14,10 @@ use petgraph::{
use crate::{
internal::{
arena::ArenaId,
- id::{ClauseId, SolvableId, SolvableOrRootId, StringId, VariableId, VersionSetId},
+ id::{ClauseId, SolvableId, SolvableOrRootId, StringId, VersionSetId},
},
runtime::AsyncRuntime,
- solver::{
- clause::Clause,
- variable_map::{VariableMap, VariableOrigin},
- Solver,
- },
+ solver::{clause::Clause, variable_map::VariableOrigin, Solver},
DependencyProvider, Interner, Requirement,
};
@@ -163,24 +159,24 @@ impl Conflict {
ConflictEdge::Conflict(ConflictCause::Constrains(version_set_id)),
);
}
- &Clause::Conditional(package_id, condition) => {
+ &Clause::Conditional(package_id, condition, version_set_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(then_version_set_id)).unwrap_or_else(|_| {
+ 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(...)`")
});
if candidates.is_empty() {
tracing::trace!(
- "{package_id:?} conditionally requires {condition:?}, which has no candidates"
+ "{package_id:?} conditionally requires {version_set_id:?}, which has no candidates"
);
graph.add_edge(
package_node,
unresolved_node,
- ConflictEdge::ConditionalRequires(condition),
+ ConflictEdge::ConditionalRequires(condition, version_set_id),
);
} else {
for &candidate_id in candidates {
@@ -193,21 +189,22 @@ impl Conflict {
graph.add_edge(
package_node,
candidate_node,
- ConflictEdge::ConditionalRequires(condition),
+ ConflictEdge::ConditionalRequires(condition, version_set_id),
);
}
}
- // Add an edge for the unsatisfied condition if it exists
- if let Some(condition_solvable) = condition.as_solvable(&solver.variable_map) {
- let condition_node =
- Self::add_node(&mut graph, &mut nodes, condition_solvable.into());
- graph.add_edge(
- package_node,
- condition_node,
- ConflictEdge::Conflict(ConflictCause::UnsatisfiedCondition(condition)),
- );
- }
+ // TODO: Add an edge for the unsatisfied condition if it exists
+ // // Add an edge for the unsatisfied condition if it exists
+ // if let Some(condition_solvable) = condition.as_solvable(&solver.variable_map) {
+ // let condition_node =
+ // Self::add_node(&mut graph, &mut nodes, condition_solvable.into());
+ // graph.add_edge(
+ // package_node,
+ // condition_node,
+ // ConflictEdge::Conflict(ConflictCause::UnsatisfiedCondition(condition.into())),
+ // );
+ // }
}
}
}
@@ -296,22 +293,24 @@ pub(crate) enum ConflictEdge {
/// The target node is involved in a conflict, caused by `ConflictCause`
Conflict(ConflictCause),
/// The target node is a candidate for a conditional dependency
- ConditionalRequires(Requirement),
+ ConditionalRequires(VersionSetId, Requirement),
}
impl ConflictEdge {
fn try_requires(self) -> Option {
match self {
- ConflictEdge::Requires(match_spec_id)
- | ConflictEdge::ConditionalRequires(match_spec_id) => Some(match_spec_id),
+ ConflictEdge::Requires(match_spec_id) => Some(match_spec_id),
+ ConflictEdge::ConditionalRequires(_, _) => None,
ConflictEdge::Conflict(_) => None,
}
}
fn requires(self) -> Requirement {
match self {
- ConflictEdge::Requires(match_spec_id)
- | ConflictEdge::ConditionalRequires(match_spec_id) => match_spec_id,
+ ConflictEdge::Requires(match_spec_id) => match_spec_id,
+ ConflictEdge::ConditionalRequires(_, _) => {
+ panic!("expected requires edge, found conditional requires")
+ }
ConflictEdge::Conflict(_) => panic!("expected requires edge, found conflict"),
}
}
@@ -560,12 +559,12 @@ impl ConflictGraph {
.graph
.edges_directed(nx, Direction::Outgoing)
.map(|e| match e.weight() {
- ConflictEdge::Requires(version_set_id) => (version_set_id, e.target()),
- ConflictEdge::ConditionalRequires(version_set_id, _) => {
- (version_set_id, e.target())
- }
+ ConflictEdge::Requires(req) => (req, e.target()),
+ ConflictEdge::ConditionalRequires(_, req) => (req, e.target()),
ConflictEdge::Conflict(_) => unreachable!(),
})
+ .collect::>()
+ .into_iter()
.chunk_by(|(&version_set_id, _)| version_set_id);
for (_, mut deps) in &dependencies {
@@ -610,11 +609,13 @@ impl ConflictGraph {
.edges_directed(nx, Direction::Outgoing)
.map(|e| match e.weight() {
ConflictEdge::Requires(version_set_id) => (version_set_id, e.target()),
- ConflictEdge::ConditionalRequires(version_set_id, _) => {
+ ConflictEdge::ConditionalRequires(_, version_set_id) => {
(version_set_id, e.target())
}
ConflictEdge::Conflict(_) => unreachable!(),
})
+ .collect::>()
+ .into_iter()
.chunk_by(|(&version_set_id, _)| version_set_id);
// Missing if at least one dependency is missing
diff --git a/src/lib.rs b/src/lib.rs
index 575c678..cdaec9e 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -28,7 +28,7 @@ pub use internal::{
mapping::Mapping,
};
use itertools::Itertools;
-pub use requirement::Requirement;
+pub use requirement::{ConditionalRequirement, Requirement};
pub use solver::{Problem, Solver, SolverCache, UnsolvableOrCancelled};
/// An object that is used by the solver to query certain properties of
@@ -206,7 +206,7 @@ pub struct KnownDependencies {
feature = "serde",
serde(default, skip_serializing_if = "Vec::is_empty")
)]
- pub requirements: Vec,
+ pub conditional_requirements: Vec,
/// Defines additional constraints on packages that may or may not be part
/// of the solution. Different from `requirements`, packages in this set
diff --git a/src/requirement.rs b/src/requirement.rs
index 62589f3..18b6ce8 100644
--- a/src/requirement.rs
+++ b/src/requirement.rs
@@ -2,6 +2,57 @@ use crate::{Interner, VersionSetId, VersionSetUnionId};
use itertools::Itertools;
use std::fmt::Display;
+/// Specifies a conditional requirement, where the requirement is only active when the condition is met.
+#[derive(Clone, Copy, Debug, Hash, Eq, PartialEq, Ord, PartialOrd)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+pub struct ConditionalRequirement {
+ /// The condition that must be met for the requirement to be active.
+ pub condition: Option,
+ /// The requirement that is only active when the condition is met.
+ pub requirement: Requirement,
+}
+
+impl ConditionalRequirement {
+ /// Creates a new conditional requirement.
+ pub fn new(condition: VersionSetId, requirement: Requirement) -> Self {
+ Self {
+ condition: Some(condition),
+ requirement,
+ }
+ }
+ /// Returns the version sets that satisfy the requirement.
+ pub fn requirement_version_sets<'i>(
+ &'i self,
+ interner: &'i impl Interner,
+ ) -> impl Iterator
- + 'i {
+ self.requirement.version_sets(interner)
+ }
+
+ /// Returns the version sets that satisfy the requirement, along with the condition that must be met.
+ pub fn version_sets_with_condition<'i>(
+ &'i self,
+ interner: &'i impl Interner,
+ ) -> impl Iterator
- )> + 'i {
+ self.requirement
+ .version_sets(interner)
+ .map(move |vs| (vs, self.condition))
+ }
+
+ /// Returns the condition and requirement.
+ pub fn into_condition_and_requirement(self) -> (Option, Requirement) {
+ (self.condition, self.requirement)
+ }
+}
+
+impl From for ConditionalRequirement {
+ fn from(value: Requirement) -> Self {
+ Self {
+ condition: None,
+ requirement: value,
+ }
+ }
+}
+
/// Specifies the dependency of a solvable on a set of version sets.
#[derive(Clone, Copy, Debug, Hash, Eq, PartialEq, Ord, PartialOrd)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
@@ -13,9 +64,6 @@ pub enum Requirement {
/// This variant is typically used for requirements that can be satisfied by two or more
/// version sets belonging to _different_ packages.
Union(VersionSetUnionId),
- /// Specifies a conditional requirement, where the requirement is only active when the condition is met.
- /// First VersionSetId is the condition, second is the requirement.
- ConditionalRequires(VersionSetId, VersionSetId),
}
impl Default for Requirement {
@@ -48,22 +96,14 @@ impl Requirement {
pub(crate) fn version_sets<'i>(
&'i self,
interner: &'i impl Interner,
- ) -> (
- impl Iterator
- + 'i,
- Option,
- ) {
- match self {
+ ) -> impl Iterator
- + 'i {
+ match *self {
Requirement::Single(version_set) => {
- (itertools::Either::Left(std::iter::once(*version_set)), None)
+ itertools::Either::Left(std::iter::once(version_set))
+ }
+ Requirement::Union(version_set_union) => {
+ itertools::Either::Right(interner.version_sets_in_union(version_set_union))
}
- Requirement::Union(version_set_union) => (
- itertools::Either::Right(interner.version_sets_in_union(*version_set_union)),
- None,
- ),
- Requirement::ConditionalRequires(condition, requirement) => (
- itertools::Either::Left(std::iter::once(*requirement)),
- Some(*condition),
- ),
}
}
}
@@ -98,16 +138,6 @@ impl<'i, I: Interner> Display for DisplayRequirement<'i, I> {
write!(f, "{}", formatted_version_sets)
}
- Requirement::ConditionalRequires(condition, requirement) => {
- write!(
- f,
- "if {} then {} {}",
- self.interner.display_version_set(condition),
- self.interner
- .display_name(self.interner.version_set_name(requirement)),
- self.interner.display_version_set(requirement)
- )
- }
}
}
}
diff --git a/src/snapshot.rs b/src/snapshot.rs
index 0c4a986..1d2e458 100644
--- a/src/snapshot.rs
+++ b/src/snapshot.rs
@@ -220,7 +220,9 @@ impl DependencySnapshot {
}
}
- for &requirement in deps.requirements.iter() {
+ for &req in deps.conditional_requirements.iter() {
+ let (_, requirement) = req.into_condition_and_requirement(); // TODO: condition
+
match requirement {
Requirement::Single(version_set) => {
if seen.insert(Element::VersionSet(version_set)) {
@@ -243,14 +245,6 @@ impl DependencySnapshot {
.version_set_unions
.insert(version_set_union_id, version_sets);
}
- Requirement::ConditionalRequires(condition, requirement) => {
- if seen.insert(Element::VersionSet(condition)) {
- queue.push_back(Element::VersionSet(condition));
- }
- if seen.insert(Element::VersionSet(requirement)) {
- queue.push_back(Element::VersionSet(requirement));
- }
- }
}
}
}
diff --git a/src/solver/cache.rs b/src/solver/cache.rs
index 952c8cb..cf6c6cc 100644
--- a/src/solver/cache.rs
+++ b/src/solver/cache.rs
@@ -280,15 +280,6 @@ impl SolverCache {
}
}
}
- Requirement::ConditionalRequires(condition, requirement) => {
- let candidates = self
- .get_or_cache_sorted_candidates_for_version_set(condition)
- .await?;
- let sorted_candidates = self
- .get_or_cache_sorted_candidates_for_version_set(requirement)
- .await?;
- Ok(sorted_candidates)
- }
}
}
diff --git a/src/solver/clause.rs b/src/solver/clause.rs
index 15f9d44..2369ebf 100644
--- a/src/solver/clause.rs
+++ b/src/solver/clause.rs
@@ -80,7 +80,7 @@ pub(crate) enum Clause {
/// In SAT terms: (¬A ∨ ¬C ∨ B1 ∨ B2 ∨ ... ∨ B99), where A is the solvable,
/// C is the condition, and B1 to B99 represent the possible candidates for
/// the provided [`Requirement`].
- Conditional(VariableId, Requirement),
+ Conditional(VariableId, VersionSetId, Requirement),
/// Forbids the package on the right-hand side
///
/// Note that the package on the left-hand side is not part of the clause,
@@ -237,50 +237,61 @@ impl Clause {
fn conditional(
parent_id: VariableId,
requirement: Requirement,
+ condition: VersionSetId,
decision_tracker: &DecisionTracker,
requirement_candidates: impl IntoIterator
- ,
condition_candidates: impl IntoIterator
- ,
) -> (Self, Option<[Literal; 2]>, bool) {
assert_ne!(decision_tracker.assigned_value(parent_id), Some(false));
- let mut candidates = condition_candidates.into_iter().peekable();
- let first_candidate = candidates.peek().copied();
- if let Some(first_candidate) = first_candidate {
- match condition_candidates
- .into_iter()
- .find(|&condition_id| decision_tracker.assigned_value(condition_id) == Some(true))
- {
- Some(_) => Clause::requires(
- parent_id,
- requirement,
- requirement_candidates,
- decision_tracker,
- ),
- None => {
- if let Some(first_unset_candidate) = candidates.find(|&condition_id| {
- decision_tracker.assigned_value(condition_id) != Some(false)
- }) {
- (
- Clause::Conditional(parent_id, requirement),
- Some([parent_id.negative(), first_unset_candidate.negative()]),
- false,
- )
- } else {
- // All condition candidates are assigned to false! Therefore, the clause conflicts with the
- // current decisions. There are no valid watches for it at the moment, but we will
- // assign default ones nevertheless, because they will become valid after the solver
- // restarts.
- (
- Clause::Conditional(parent_id, requirement),
- Some([parent_id.negative(), first_candidate.negative()]),
- true,
- )
- }
+ let mut condition_candidates = condition_candidates.into_iter().peekable();
+ let condition_first_candidate = condition_candidates
+ .peek()
+ .copied()
+ .expect("no condition candidates");
+ let mut requirement_candidates = requirement_candidates.into_iter().peekable();
+
+ match condition_candidates
+ .find(|&condition_id| decision_tracker.assigned_value(condition_id) == Some(true))
+ {
+ Some(_) => {
+ // Condition is true, find first requirement candidate not set to false
+ if let Some(req_candidate) = requirement_candidates
+ .find(|&req_id| decision_tracker.assigned_value(req_id) != Some(false))
+ {
+ (
+ Clause::Conditional(parent_id, condition, requirement),
+ Some([parent_id.negative(), req_candidate.positive()]),
+ false,
+ )
+ } else {
+ // No valid requirement candidate, use first condition candidate and mark conflict
+ (
+ Clause::Conditional(parent_id, condition, requirement),
+ Some([parent_id.negative(), condition_first_candidate.positive()]),
+ true,
+ )
+ }
+ }
+ None => {
+ // No true condition, look for unset condition
+ if let Some(unset_condition) = condition_candidates.find(|&condition_id| {
+ decision_tracker.assigned_value(condition_id) != Some(false)
+ }) {
+ (
+ Clause::Conditional(parent_id, condition, requirement),
+ Some([parent_id.negative(), unset_condition.negative()]),
+ false,
+ )
+ } else {
+ // All conditions false
+ (
+ Clause::Conditional(parent_id, condition, requirement),
+ None,
+ false,
+ )
}
}
- } else {
- // No condition candidates, so no need to watch anything
- (Clause::Conditional(parent_id, requirement), None, false)
}
}
@@ -326,14 +337,22 @@ impl Clause {
Clause::Lock(_, s) => [s.negative(), VariableId::root().negative()]
.into_iter()
.try_fold(init, visit),
- Clause::Conditional(package_id, condition) => iter::once(package_id.negative())
- .chain(
- requirements_to_sorted_candidates[&condition]
- .iter()
- .flatten()
- .map(|&s| s.positive()),
- )
- .try_fold(init, visit),
+ Clause::Conditional(package_id, condition, requirement) => {
+ iter::once(package_id.negative())
+ .chain(
+ requirements_to_sorted_candidates[&condition.into()]
+ .iter()
+ .flatten()
+ .map(|&s| s.negative()),
+ )
+ .chain(
+ requirements_to_sorted_candidates[&requirement]
+ .iter()
+ .flatten()
+ .map(|&s| s.positive()),
+ )
+ .try_fold(init, visit)
+ }
}
}
@@ -488,13 +507,15 @@ impl WatchedLiterals {
/// conflict.
pub fn conditional(
package_id: VariableId,
- condition: Requirement,
+ requirement: Requirement,
+ condition: VersionSetId,
decision_tracker: &DecisionTracker,
requirement_candidates: impl IntoIterator
- ,
condition_candidates: impl IntoIterator
- ,
) -> (Option, bool, Clause) {
let (kind, watched_literals, conflict) = Clause::conditional(
package_id,
+ requirement,
condition,
decision_tracker,
requirement_candidates,
@@ -700,13 +721,14 @@ impl<'i, I: Interner> Display for ClauseDisplay<'i, I> {
other,
)
}
- Clause::Conditional(package_id, condition) => {
+ Clause::Conditional(package_id, condition, requirement) => {
write!(
f,
- "Conditional({}({:?}), {})",
+ "Conditional({}({:?}), {}, {})",
package_id.display(self.variable_map, self.interner),
package_id,
- condition.display(self.interner),
+ self.interner.display_version_set(condition),
+ requirement.display(self.interner),
)
}
}
diff --git a/src/solver/mod.rs b/src/solver/mod.rs
index 5dfea63..a64628c 100644
--- a/src/solver/mod.rs
+++ b/src/solver/mod.rs
@@ -19,6 +19,7 @@ use crate::{
id::{ClauseId, LearntClauseId, NameId, SolvableId, SolvableOrRootId, VariableId},
mapping::Mapping,
},
+ requirement::ConditionalRequirement,
runtime::{AsyncRuntime, NowOrNeverRuntime},
solver::binary_encoding::AtMostOnceTracker,
Candidates, Dependencies, DependencyProvider, KnownDependencies, Requirement, VersionSetId,
@@ -51,7 +52,7 @@ struct AddClauseOutput {
/// This struct follows the builder pattern and can have its fields set by one
/// of the available setter methods.
pub struct Problem
{
- requirements: Vec,
+ requirements: Vec,
constraints: Vec,
soft_requirements: S,
}
@@ -80,7 +81,7 @@ impl> Problem {
///
/// Returns the [`Problem`] for further mutation or to pass to
/// [`Solver::solve`].
- pub fn requirements(self, requirements: Vec) -> Self {
+ pub fn requirements(self, requirements: Vec) -> Self {
Self {
requirements,
..self
@@ -172,7 +173,7 @@ pub struct Solver {
decision_tracker: DecisionTracker,
/// The [`Requirement`]s that must be installed as part of the solution.
- root_requirements: Vec,
+ root_requirements: Vec,
/// Additional constraints imposed by the root.
root_constraints: Vec,
@@ -788,7 +789,7 @@ impl Solver {
// Get the candidates for the individual version sets.
let version_set_candidates = &self.requirement_to_sorted_candidates[deps];
- let (version_sets, condition) = deps.version_sets(self.provider());
+ let version_sets = deps.version_sets(self.provider());
// 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
@@ -1518,7 +1519,7 @@ async fn add_clauses_for_solvables(
RequirementCandidateVariables,
ahash::RandomState,
>,
- root_requirements: &[Requirement],
+ root_requirements: &[ConditionalRequirement],
root_constraints: &[VersionSetId],
) -> Result> {
let mut output = AddClauseOutput::default();
@@ -1533,14 +1534,9 @@ async fn add_clauses_for_solvables(
SortedCandidates {
solvable_id: SolvableOrRootId,
requirement: Requirement,
+ condition: Option<(VersionSetId, Vec<&'i [SolvableId]>)>,
candidates: Vec<&'i [SolvableId]>,
},
- ConditionalSortedCandidates {
- solvable_id: SolvableOrRootId,
- requirement: Requirement,
- requirement_candidates: Vec<&'i [SolvableId]>,
- condition_candidates: &'i [SolvableId],
- },
NonMatchingCandidates {
solvable_id: SolvableOrRootId,
version_set_id: VersionSetId,
@@ -1588,7 +1584,7 @@ async fn add_clauses_for_solvables(
ready(Ok(TaskResult::Dependencies {
solvable_id: solvable_or_root,
dependencies: Dependencies::Known(KnownDependencies {
- requirements: root_requirements.to_vec(),
+ conditional_requirements: root_requirements.to_vec(),
constrains: root_constraints.to_vec(),
}),
}))
@@ -1620,8 +1616,8 @@ async fn add_clauses_for_solvables(
None => variable_map.root(),
};
- let (requirements, constrains) = match dependencies {
- Dependencies::Known(deps) => (deps.requirements, deps.constrains),
+ let (conditional_requirements, constrains) = match dependencies {
+ Dependencies::Known(deps) => (deps.conditional_requirements, deps.constrains),
Dependencies::Unknown(reason) => {
// There is no information about the solvable's dependencies, so we add
// an exclusion clause for it
@@ -1642,11 +1638,10 @@ async fn add_clauses_for_solvables(
}
};
- for (version_set_id, condition) in requirements
+ for (version_set_id, condition) in conditional_requirements
.iter()
- .flat_map(|requirement| {
- let (version_sets, condition) = requirement.version_sets(cache.provider());
- version_sets.map(move |vs| (vs, condition))
+ .flat_map(|conditional_requirement| {
+ conditional_requirement.version_sets_with_condition(cache.provider())
})
.chain(constrains.iter().map(|&vs| (vs, None)))
{
@@ -1668,32 +1663,32 @@ async fn add_clauses_for_solvables(
}
.boxed_local(),
);
- }
- if let Some(condition) = condition {
- let condition_name = cache.provider().version_set_name(condition);
- if clauses_added_for_package.insert(condition_name) {
- pending_futures.push(
- async move {
- let condition_candidates =
- cache.get_or_cache_candidates(condition_name).await?;
- Ok(TaskResult::Candidates {
- name_id: condition_name,
- package_candidates: &condition_candidates,
- })
- }
- .boxed_local(),
- );
+ if let Some(condition) = condition {
+ let condition_name = cache.provider().version_set_name(condition);
+ if clauses_added_for_package.insert(condition_name) {
+ pending_futures.push(
+ async move {
+ let condition_candidates =
+ cache.get_or_cache_candidates(condition_name).await?;
+ Ok(TaskResult::Candidates {
+ name_id: condition_name,
+ package_candidates: &condition_candidates,
+ })
+ }
+ .boxed_local(),
+ );
+ }
}
}
}
- for requirement in requirements {
+ for conditional_requirement in conditional_requirements {
// Find all the solvable that match for the given version set
pending_futures.push(
async move {
- let (version_sets, condition) =
- requirement.version_sets(cache.provider());
+ let version_sets =
+ conditional_requirement.requirement_version_sets(cache.provider());
let candidates =
futures::future::try_join_all(version_sets.map(|version_set| {
cache
@@ -1701,21 +1696,26 @@ async fn add_clauses_for_solvables(
}))
.await?;
- if let Some(condition) = condition {
- let condition_candidates = cache
- .get_or_cache_sorted_candidates_for_version_set(condition)
- .await?;
+ // condition is `VersionSetId` right now but it will become a `Requirement`
+ // in the future
+ if let Some(condition) = conditional_requirement.condition {
+ let condition_candidates = vec![
+ cache
+ .get_or_cache_sorted_candidates_for_version_set(condition)
+ .await?,
+ ];
- Ok(TaskResult::ConditionalSortedCandidates {
+ Ok(TaskResult::SortedCandidates {
solvable_id,
- requirement,
- requirement_candidates: candidates,
- condition_candidates,
+ requirement: conditional_requirement.requirement,
+ condition: Some((condition, condition_candidates)),
+ candidates,
})
} else {
Ok(TaskResult::SortedCandidates {
solvable_id,
- requirement,
+ requirement: conditional_requirement.requirement,
+ condition: None,
candidates,
})
}
@@ -1787,6 +1787,7 @@ async fn add_clauses_for_solvables(
TaskResult::SortedCandidates {
solvable_id,
requirement,
+ condition,
candidates,
} => {
tracing::trace!(
@@ -1856,104 +1857,42 @@ async fn add_clauses_for_solvables(
);
}
- // Add the requirements clause
- let no_candidates = candidates.iter().all(|candidates| candidates.is_empty());
- let (watched_literals, conflict, kind) = WatchedLiterals::requires(
- variable,
- requirement,
- version_set_variables.iter().flatten().copied(),
- decision_tracker,
- );
- let has_watches = watched_literals.is_some();
- let clause_id = clauses.alloc(watched_literals, 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::ConditionalSortedCandidates {
- solvable_id,
- requirement,
- requirement_candidates,
- condition_candidates,
- } => {
- tracing::trace!(
- "conditional candidates 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(),
- };
-
- // Cache the candidates for this requirement
- let version_set_variables: Vec<_> = requirement_candidates
- .iter()
- .map(|candidates| {
- candidates
- .iter()
- .map(|&candidate| variable_map.intern_solvable(candidate))
- .collect::>()
- })
- .collect();
-
- requirement_to_sorted_candidates
- .insert(requirement.clone(), version_set_variables.clone());
+ let (watched_literals, conflict, kind) =
+ if let Some((condition, condition_candidates)) = condition {
+ let condition_version_set_variables = requirement_to_sorted_candidates
+ .insert(
+ condition.into(),
+ condition_candidates
+ .iter()
+ .map(|&candidates| {
+ candidates
+ .iter()
+ .map(|&var| variable_map.intern_solvable(var))
+ .collect()
+ })
+ .collect(),
+ );
- // Add forbidden clauses for the candidates
- for candidates in requirement_candidates.iter() {
- for &candidate in *candidates {
- let candidate_var = variable_map.intern_solvable(candidate);
- 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 (watched_literals, kind) = WatchedLiterals::forbid_multiple(
- a,
- if positive { b.positive() } else { b.negative() },
- name_id,
- );
- let clause_id = clauses.alloc(watched_literals, kind);
- debug_assert!(
- clauses.watched_literals[clause_id.to_usize()].is_some()
- );
- output.clauses_to_watch.push(clause_id);
- },
- || variable_map.alloc_forbid_multiple_variable(name_id),
- );
- }
- }
+ // Add a condition clause
+ WatchedLiterals::conditional(
+ variable,
+ requirement,
+ condition,
+ decision_tracker,
+ version_set_variables.iter().flatten().copied(),
+ condition_version_set_variables.iter().flatten().copied(),
+ )
+ } else {
+ WatchedLiterals::requires(
+ variable,
+ requirement,
+ version_set_variables.iter().flatten().copied(),
+ decision_tracker,
+ )
+ };
// Add the requirements clause
- let no_candidates = requirement_candidates
- .iter()
- .all(|candidates| candidates.is_empty());
- let condition_variables = condition_candidates
- .iter()
- .map(|&candidate| variable_map.intern_solvable(candidate))
- .collect::>();
-
- let (watched_literals, conflict, kind) = WatchedLiterals::conditional(
- variable,
- requirement,
- decision_tracker,
- version_set_variables.iter().flatten().copied(),
- condition_variables.iter().copied(),
- );
+ let no_candidates = candidates.iter().all(|candidates| candidates.is_empty());
let has_watches = watched_literals.is_some();
let clause_id = clauses.alloc(watched_literals, kind);
diff --git a/tools/solve-snapshot/src/main.rs b/tools/solve-snapshot/src/main.rs
index 901996c..3629eaf 100644
--- a/tools/solve-snapshot/src/main.rs
+++ b/tools/solve-snapshot/src/main.rs
@@ -128,7 +128,8 @@ fn main() {
let start = Instant::now();
- let problem = Problem::default().requirements(requirements);
+ let problem =
+ Problem::default().requirements(requirements.into_iter().map(Into::into).collect());
let mut solver = Solver::new(provider);
let mut records = None;
let mut error = None;
From 995a2c398d43ecc9f9440ab368e355b1a40b30aa Mon Sep 17 00:00:00 2001
From: prsabahrami
Date: Tue, 21 Jan 2025 16:24:24 -0500
Subject: [PATCH 04/41] minor fix
---
src/solver/mod.rs | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/solver/mod.rs b/src/solver/mod.rs
index a64628c..d1d2ba1 100644
--- a/src/solver/mod.rs
+++ b/src/solver/mod.rs
@@ -1673,7 +1673,7 @@ async fn add_clauses_for_solvables(
cache.get_or_cache_candidates(condition_name).await?;
Ok(TaskResult::Candidates {
name_id: condition_name,
- package_candidates: &condition_candidates,
+ package_candidates: condition_candidates,
})
}
.boxed_local(),
From dd636d293f033f40e1ed65a062ac5b045c634753 Mon Sep 17 00:00:00 2001
From: prsabahrami
Date: Tue, 21 Jan 2025 16:26:22 -0500
Subject: [PATCH 05/41] remove deprecated conditional requirement function from
resolvo.h
---
cpp/include/resolvo.h | 9 ---------
1 file changed, 9 deletions(-)
diff --git a/cpp/include/resolvo.h b/cpp/include/resolvo.h
index c824df4..97d00f5 100644
--- a/cpp/include/resolvo.h
+++ b/cpp/include/resolvo.h
@@ -24,15 +24,6 @@ inline Requirement requirement_union(VersionSetUnionId id) {
return cbindgen_private::resolvo_requirement_union(id);
}
-/**
- * Specifies a conditional requirement, where the requirement is only active when the condition is met.
- * @param condition The version set that must be satisfied for the requirement to be active.
- * @param requirement The version set that must be satisfied when the condition is met.
- */
-inline Requirement requirement_conditional(VersionSetId condition, VersionSetId requirement) {
- return cbindgen_private::resolvo_requirement_conditional(condition, requirement);
-}
-
/**
* Called to solve a package problem.
*
From eb4d253084c4da3aedcafe163a146ba598c9d0ce Mon Sep 17 00:00:00 2001
From: prsabahrami
Date: Wed, 22 Jan 2025 00:18:48 -0500
Subject: [PATCH 06/41] add a map of conditional clauses to the
DependencyProvider struct
---
src/solver/mod.rs | 12 ++++++++++++
1 file changed, 12 insertions(+)
diff --git a/src/solver/mod.rs b/src/solver/mod.rs
index d1d2ba1..1814603 100644
--- a/src/solver/mod.rs
+++ b/src/solver/mod.rs
@@ -37,6 +37,7 @@ mod watch_map;
#[derive(Default)]
struct AddClauseOutput {
new_requires_clauses: Vec<(VariableId, Requirement, ClauseId)>,
+ new_conditional_clauses: Vec<(VariableId, VersionSetId, Requirement, ClauseId)>,
conflicting_clauses: Vec,
negative_assertions: Vec<(VariableId, ClauseId)>,
clauses_to_watch: Vec,
@@ -151,6 +152,7 @@ pub struct Solver {
pub(crate) clauses: Clauses,
requires_clauses: IndexMap, ahash::RandomState>,
+ conditional_clauses: IndexMap, ahash::RandomState>,
watches: WatchMap,
/// A mapping from requirements to the variables that represent the
@@ -201,6 +203,7 @@ impl Solver {
clauses: Clauses::default(),
variable_map: VariableMap::default(),
requires_clauses: Default::default(),
+ conditional_clauses: Default::default(),
requirement_to_sorted_candidates: FrozenMap::default(),
watches: WatchMap::new(),
negative_assertions: Default::default(),
@@ -281,6 +284,7 @@ impl Solver {
clauses: self.clauses,
variable_map: self.variable_map,
requires_clauses: self.requires_clauses,
+ conditional_clauses: self.conditional_clauses,
requirement_to_sorted_candidates: self.requirement_to_sorted_candidates,
watches: self.watches,
negative_assertions: self.negative_assertions,
@@ -661,6 +665,14 @@ impl Solver {
.or_default()
.push((requirement, clause_id));
}
+
+ for (solvable_id, condition, requirement, clause_id) in output.new_conditional_clauses {
+ self.conditional_clauses
+ .entry(solvable_id)
+ .or_default()
+ .push((condition, requirement, clause_id));
+ }
+
self.negative_assertions
.append(&mut output.negative_assertions);
From 451536e0eacef451cbaa505ed72055d4246a323f Mon Sep 17 00:00:00 2001
From: prsabahrami
Date: Wed, 22 Jan 2025 00:18:49 -0500
Subject: [PATCH 07/41] add the conditional clauses to the DependencyProvider
---
src/solver/mod.rs | 263 +++++++++++++++++++++++++++++++++++++---------
1 file changed, 216 insertions(+), 47 deletions(-)
diff --git a/src/solver/mod.rs b/src/solver/mod.rs
index 1814603..ece8f77 100644
--- a/src/solver/mod.rs
+++ b/src/solver/mod.rs
@@ -927,6 +927,154 @@ impl Solver {
}
}
+ for (&solvable_id, conditional_clauses) in self.conditional_clauses.iter() {
+ 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.
+ if best_decision.is_explicit_requirement && !is_explicit_requirement {
+ continue;
+ }
+ }
+
+ // Consider only clauses in which we have decided to install the solvable
+ if self.decision_tracker.assigned_value(solvable_id) != Some(true) {
+ continue;
+ }
+
+ for (condition, requirement, clause_id) in conditional_clauses.iter() {
+ let mut candidate = ControlFlow::Break(());
+
+ // Get the candidates for the individual version sets.
+ let version_set_candidates = &self.requirement_to_sorted_candidates[condition];
+
+ let version_sets = condition.version_sets(self.provider());
+
+ // 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.
+ //
+ // 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 version_sets.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(
+ match candidate {
+ ControlFlow::Continue(x) => x,
+ _ => None,
+ },
+ |first_candidate, &candidate| {
+ 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
+ // already true. Skip it.
+ return ControlFlow::Break(());
+ }
+ Some(false) => {
+ // This candidate has already been assigned false, continue the
+ // search.
+ first_candidate
+ }
+ None => match first_candidate {
+ Some((
+ first_candidate,
+ candidate_version_set,
+ mut candidate_count,
+ package_activity,
+ )) => {
+ // We found a candidate that has not been assigned yet, but
+ // it is not the first candidate.
+ if candidate_version_set == version_set {
+ // Increment the candidate count if this is a candidate
+ // in the same version set.
+ candidate_count += 1u32;
+ }
+ Some((
+ first_candidate,
+ candidate_version_set,
+ candidate_count,
+ package_activity,
+ ))
+ }
+ None => {
+ // We found the first candidate that has not been assigned
+ // yet.
+ let package_activity = self.name_activity[self
+ .provider()
+ .version_set_name(version_set)
+ .to_usize()];
+ Some((candidate, version_set, 1, package_activity))
+ }
+ },
+ })
+ },
+ );
+
+ // Stop searching if we found a candidate that makes the clause true.
+ if candidate.is_break() {
+ break;
+ }
+ }
+
+ match candidate {
+ ControlFlow::Break(_) => {
+ // A candidate has been assigned true which means the clause is already
+ // true, and we can skip it.
+ continue;
+ }
+ ControlFlow::Continue(None) => {
+ unreachable!("when we get here it means that all candidates have been assigned false. This should not be able to happen at this point because during propagation the solvable should have been assigned false as well.")
+ }
+ ControlFlow::Continue(Some((
+ candidate,
+ _version_set_id,
+ candidate_count,
+ package_activity,
+ ))) => {
+ let decision = (candidate, solvable_id, *clause_id);
+ best_decision = Some(match &best_decision {
+ None => PossibleDecision {
+ is_explicit_requirement,
+ package_activity,
+ candidate_count,
+ decision,
+ },
+ Some(best_decision) => {
+ // Prefer decisions on explicit requirements over non-explicit
+ // requirements. This optimizes direct dependencies over transitive
+ // dependencies.
+ if best_decision.is_explicit_requirement && !is_explicit_requirement
+ {
+ continue;
+ }
+
+ // Prefer decisions with a higher package activity score to root out
+ // conflicts faster.
+ if best_decision.package_activity >= package_activity {
+ continue;
+ }
+
+ if best_decision.candidate_count <= candidate_count {
+ continue;
+ }
+
+ PossibleDecision {
+ is_explicit_requirement,
+ package_activity,
+ candidate_count,
+ decision,
+ }
+ }
+ })
+ }
+ }
+ }
+
+ }
+
if let Some(PossibleDecision {
candidate_count,
package_activity,
@@ -1869,59 +2017,80 @@ async fn add_clauses_for_solvables(
);
}
- let (watched_literals, conflict, kind) =
- if let Some((condition, condition_candidates)) = condition {
- let condition_version_set_variables = requirement_to_sorted_candidates
- .insert(
- condition.into(),
- condition_candidates
- .iter()
- .map(|&candidates| {
- candidates
- .iter()
- .map(|&var| variable_map.intern_solvable(var))
- .collect()
- })
- .collect(),
- );
+ if let Some((condition, condition_candidates)) = condition {
+ let condition_version_set_variables = requirement_to_sorted_candidates
+ .insert(
+ condition.into(),
+ condition_candidates
+ .iter()
+ .map(|&candidates| {
+ candidates
+ .iter()
+ .map(|&var| variable_map.intern_solvable(var))
+ .collect()
+ })
+ .collect(),
+ );
- // Add a condition clause
- WatchedLiterals::conditional(
- variable,
- requirement,
- condition,
- decision_tracker,
- version_set_variables.iter().flatten().copied(),
- condition_version_set_variables.iter().flatten().copied(),
- )
- } else {
- WatchedLiterals::requires(
- variable,
- requirement,
- version_set_variables.iter().flatten().copied(),
- decision_tracker,
- )
- };
+ // Add a condition clause
+ let (watched_literals, conflict, kind) = WatchedLiterals::conditional(
+ variable,
+ requirement,
+ condition,
+ decision_tracker,
+ version_set_variables.iter().flatten().copied(),
+ condition_version_set_variables.iter().flatten().copied(),
+ );
+
+ // Add the conditional clause
+ let no_candidates = candidates.iter().all(|candidates| candidates.is_empty());
+
+ let has_watches = watched_literals.is_some();
+ let clause_id = clauses.alloc(watched_literals, kind);
- // Add the requirements clause
- let no_candidates = candidates.iter().all(|candidates| candidates.is_empty());
+ if has_watches {
+ output.clauses_to_watch.push(clause_id);
+ }
- let has_watches = watched_literals.is_some();
- let clause_id = clauses.alloc(watched_literals, kind);
+ output
+ .new_conditional_clauses
+ .push((variable, condition, requirement, clause_id));
- if has_watches {
- output.clauses_to_watch.push(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));
+ }
+
+ } else {
+ let (watched_literals, conflict, kind) = WatchedLiterals::requires(
+ variable,
+ requirement,
+ version_set_variables.iter().flatten().copied(),
+ decision_tracker,
+ );
+
+ // Add the requirements clause
+ let no_candidates = candidates.iter().all(|candidates| candidates.is_empty());
- output
- .new_requires_clauses
- .push((variable, requirement, clause_id));
+ let has_watches = watched_literals.is_some();
+ let clause_id = clauses.alloc(watched_literals, kind);
+
+ if has_watches {
+ output.clauses_to_watch.push(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));
+ 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 {
From a9fdad27c07b0758e4cf45d001931df4d9be012a Mon Sep 17 00:00:00 2001
From: prsabahrami
Date: Wed, 22 Jan 2025 11:00:46 -0500
Subject: [PATCH 08/41] update decide function to iterate over the conditional
clauses.
---
src/solver/mod.rs | 240 ++++++++++++++--------------------------------
1 file changed, 70 insertions(+), 170 deletions(-)
diff --git a/src/solver/mod.rs b/src/solver/mod.rs
index ece8f77..7700f96 100644
--- a/src/solver/mod.rs
+++ b/src/solver/mod.rs
@@ -152,7 +152,8 @@ pub struct Solver {
pub(crate) clauses: Clauses,
requires_clauses: IndexMap, ahash::RandomState>,
- conditional_clauses: IndexMap, ahash::RandomState>,
+ conditional_clauses:
+ IndexMap<(VariableId, VersionSetId), Vec<(Requirement, ClauseId)>, ahash::RandomState>,
watches: WatchMap,
/// A mapping from requirements to the variables that represent the
@@ -668,9 +669,9 @@ impl Solver {
for (solvable_id, condition, requirement, clause_id) in output.new_conditional_clauses {
self.conditional_clauses
- .entry(solvable_id)
+ .entry((solvable_id, condition))
.or_default()
- .push((condition, requirement, clause_id));
+ .push((requirement, clause_id));
}
self.negative_assertions
@@ -780,8 +781,39 @@ impl Solver {
}
let mut best_decision: Option = None;
- for (&solvable_id, requirements) in self.requires_clauses.iter() {
- let is_explicit_requirement = solvable_id == VariableId::root();
+
+ // Chain together the requires_clauses and conditional_clauses iterations
+ let requires_iter = self
+ .requires_clauses
+ .iter()
+ .map(|(&solvable_id, requirements)| {
+ (
+ solvable_id,
+ None,
+ requirements
+ .iter()
+ .map(|(r, c)| (*r, *c))
+ .collect::>(),
+ )
+ });
+
+ let conditional_iter =
+ self.conditional_clauses
+ .iter()
+ .map(|((solvable_id, condition), clauses)| {
+ (
+ *solvable_id,
+ Some(*condition),
+ clauses.iter().map(|(r, c)| (*r, *c)).collect::>(),
+ )
+ });
+
+ for (solvable_id, condition, requirements) in requires_iter.chain(conditional_iter) {
+ let is_explicit_requirement = match condition {
+ None => solvable_id == VariableId::root(),
+ Some(_) => 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.
@@ -795,160 +827,28 @@ impl Solver {
continue;
}
- 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];
+ // For conditional clauses, check that at least one conditional variable is true
+ if let Some(condition) = condition {
+ let condition_requirement: Requirement = condition.into();
+ let conditional_candidates =
+ &self.requirement_to_sorted_candidates[&condition_requirement];
- let version_sets = deps.version_sets(self.provider());
-
- // 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.
- //
- // 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 version_sets.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(
- match candidate {
- ControlFlow::Continue(x) => x,
- _ => None,
- },
- |first_candidate, &candidate| {
- 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
- // already true. Skip it.
- return ControlFlow::Break(());
- }
- Some(false) => {
- // This candidate has already been assigned false, continue the
- // search.
- first_candidate
- }
- None => match first_candidate {
- Some((
- first_candidate,
- candidate_version_set,
- mut candidate_count,
- package_activity,
- )) => {
- // We found a candidate that has not been assigned yet, but
- // it is not the first candidate.
- if candidate_version_set == version_set {
- // Increment the candidate count if this is a candidate
- // in the same version set.
- candidate_count += 1u32;
- }
- Some((
- first_candidate,
- candidate_version_set,
- candidate_count,
- package_activity,
- ))
- }
- None => {
- // We found the first candidate that has not been assigned
- // yet.
- let package_activity = self.name_activity[self
- .provider()
- .version_set_name(version_set)
- .to_usize()];
- Some((candidate, version_set, 1, package_activity))
- }
- },
- })
- },
- );
-
- // Stop searching if we found a candidate that makes the clause true.
- if candidate.is_break() {
- break;
- }
- }
-
- match candidate {
- ControlFlow::Break(_) => {
- // A candidate has been assigned true which means the clause is already
- // true, and we can skip it.
- continue;
- }
- ControlFlow::Continue(None) => {
- unreachable!("when we get here it means that all candidates have been assigned false. This should not be able to happen at this point because during propagation the solvable should have been assigned false as well.")
- }
- ControlFlow::Continue(Some((
- candidate,
- _version_set_id,
- candidate_count,
- package_activity,
- ))) => {
- let decision = (candidate, solvable_id, *clause_id);
- best_decision = Some(match &best_decision {
- None => PossibleDecision {
- is_explicit_requirement,
- package_activity,
- candidate_count,
- decision,
- },
- Some(best_decision) => {
- // Prefer decisions on explicit requirements over non-explicit
- // requirements. This optimizes direct dependencies over transitive
- // dependencies.
- if best_decision.is_explicit_requirement && !is_explicit_requirement
- {
- continue;
- }
-
- // Prefer decisions with a higher package activity score to root out
- // conflicts faster.
- if best_decision.package_activity >= package_activity {
- continue;
- }
-
- if best_decision.candidate_count <= candidate_count {
- continue;
- }
-
- PossibleDecision {
- is_explicit_requirement,
- package_activity,
- candidate_count,
- decision,
- }
- }
- })
- }
- }
- }
- }
-
- for (&solvable_id, conditional_clauses) in self.conditional_clauses.iter() {
- 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.
- if best_decision.is_explicit_requirement && !is_explicit_requirement {
+ if !conditional_candidates.iter().any(|candidates| {
+ candidates.iter().any(|&candidate| {
+ self.decision_tracker.assigned_value(candidate) == Some(true)
+ })
+ }) {
continue;
}
}
- // Consider only clauses in which we have decided to install the solvable
- if self.decision_tracker.assigned_value(solvable_id) != Some(true) {
- continue;
- }
-
- for (condition, requirement, clause_id) in conditional_clauses.iter() {
+ for (requirement, clause_id) in requirements {
let mut candidate = ControlFlow::Break(());
// Get the candidates for the individual version sets.
- let version_set_candidates = &self.requirement_to_sorted_candidates[condition];
+ let version_set_candidates = &self.requirement_to_sorted_candidates[&requirement];
- let version_sets = condition.version_sets(self.provider());
+ let version_sets = requirement.version_sets(self.provider());
// 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
@@ -1034,7 +934,7 @@ impl Solver {
candidate_count,
package_activity,
))) => {
- let decision = (candidate, solvable_id, *clause_id);
+ let decision = (candidate, solvable_id, clause_id);
best_decision = Some(match &best_decision {
None => PossibleDecision {
is_explicit_requirement,
@@ -1072,7 +972,6 @@ impl Solver {
}
}
}
-
}
if let Some(PossibleDecision {
@@ -2018,19 +1917,18 @@ async fn add_clauses_for_solvables(
}
if let Some((condition, condition_candidates)) = condition {
- let condition_version_set_variables = requirement_to_sorted_candidates
- .insert(
- condition.into(),
- condition_candidates
- .iter()
- .map(|&candidates| {
- candidates
- .iter()
- .map(|&var| variable_map.intern_solvable(var))
- .collect()
- })
- .collect(),
- );
+ let condition_version_set_variables = requirement_to_sorted_candidates.insert(
+ condition.into(),
+ condition_candidates
+ .iter()
+ .map(|&candidates| {
+ candidates
+ .iter()
+ .map(|&var| variable_map.intern_solvable(var))
+ .collect()
+ })
+ .collect(),
+ );
// Add a condition clause
let (watched_literals, conflict, kind) = WatchedLiterals::conditional(
@@ -2041,7 +1939,7 @@ async fn add_clauses_for_solvables(
version_set_variables.iter().flatten().copied(),
condition_version_set_variables.iter().flatten().copied(),
);
-
+
// Add the conditional clause
let no_candidates = candidates.iter().all(|candidates| candidates.is_empty());
@@ -2052,9 +1950,12 @@ async fn add_clauses_for_solvables(
output.clauses_to_watch.push(clause_id);
}
- output
- .new_conditional_clauses
- .push((variable, condition, requirement, clause_id));
+ output.new_conditional_clauses.push((
+ variable,
+ condition,
+ requirement,
+ clause_id,
+ ));
if conflict {
output.conflicting_clauses.push(clause_id);
@@ -2062,7 +1963,6 @@ async fn add_clauses_for_solvables(
// Add assertions for unit clauses (i.e. those with no matching candidates)
output.negative_assertions.push((variable, clause_id));
}
-
} else {
let (watched_literals, conflict, kind) = WatchedLiterals::requires(
variable,
From e62b91c91dff530072dd3acb4734f0a29bc02a57 Mon Sep 17 00:00:00 2001
From: prsabahrami
Date: Wed, 22 Jan 2025 11:39:13 -0500
Subject: [PATCH 09/41] add new node types and labels for conditional edges int
he conflict graph
---
src/conflict.rs | 100 ++++++++++++++++++++++++------------------------
1 file changed, 49 insertions(+), 51 deletions(-)
diff --git a/src/conflict.rs b/src/conflict.rs
index 6c1ace8..a597301 100644
--- a/src/conflict.rs
+++ b/src/conflict.rs
@@ -159,52 +159,62 @@ impl Conflict {
ConflictEdge::Conflict(ConflictCause::Constrains(version_set_id)),
);
}
- &Clause::Conditional(package_id, condition, version_set_id) => {
+ &Clause::Conditional(package_id, condition, requirement) => {
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(...)`")
+ let requirement_candidates = solver
+ .async_runtime
+ .block_on(solver.cache.get_or_cache_sorted_candidates(
+ requirement,
+ ))
+ .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(...)`"
+ )
+ });
+
+ let conditional_candidates = solver.async_runtime.block_on(solver.cache.get_or_cache_sorted_candidates(condition.into())).unwrap_or_else(|_| {
+ unreachable!("The condition's version set was used in the solver, so it must have been cached. Therefore cancellation is impossible here and we cannot get an `Err(...)`")
});
- if candidates.is_empty() {
+ if requirement_candidates.is_empty() {
+ tracing::trace!(
+ "{package_id:?} conditionally requires {requirement:?}, which has no candidates"
+ );
+ graph.add_edge(
+ package_node,
+ unresolved_node,
+ ConflictEdge::ConditionalRequires(condition, requirement),
+ );
+ } else if conditional_candidates.is_empty() {
tracing::trace!(
- "{package_id:?} conditionally requires {version_set_id:?}, which has no candidates"
+ "{package_id:?} conditionally requires {requirement:?}, but the condition has no candidates"
);
graph.add_edge(
package_node,
unresolved_node,
- ConflictEdge::ConditionalRequires(condition, version_set_id),
+ ConflictEdge::ConditionalRequires(condition, requirement),
);
} else {
- for &candidate_id in candidates {
+ for &candidate_id in conditional_candidates {
tracing::trace!(
- "{package_id:?} conditionally requires {candidate_id:?}"
+ "{package_id:?} conditionally requires {requirement:?} if {candidate_id:?}"
);
- let candidate_node =
- Self::add_node(&mut graph, &mut nodes, candidate_id.into());
- graph.add_edge(
- package_node,
- candidate_node,
- ConflictEdge::ConditionalRequires(condition, version_set_id),
- );
+ for &candidate_id in requirement_candidates {
+ let candidate_node =
+ Self::add_node(&mut graph, &mut nodes, candidate_id.into());
+ graph.add_edge(
+ package_node,
+ candidate_node,
+ ConflictEdge::ConditionalRequires(condition, requirement),
+ );
+ }
}
}
-
- // TODO: Add an edge for the unsatisfied condition if it exists
- // // Add an edge for the unsatisfied condition if it exists
- // if let Some(condition_solvable) = condition.as_solvable(&solver.variable_map) {
- // let condition_node =
- // Self::add_node(&mut graph, &mut nodes, condition_solvable.into());
- // graph.add_edge(
- // package_node,
- // condition_node,
- // ConflictEdge::Conflict(ConflictCause::UnsatisfiedCondition(condition.into())),
- // );
- // }
}
}
}
@@ -327,8 +337,6 @@ pub(crate) enum ConflictCause {
ForbidMultipleInstances,
/// The node was excluded
Excluded,
- /// The condition for a conditional dependency was not satisfied
- UnsatisfiedCondition(Requirement),
}
/// Represents a node that has been merged with others
@@ -395,6 +403,11 @@ impl ConflictGraph {
ConflictEdge::Requires(_) if target != ConflictNode::UnresolvedDependency => {
"black"
}
+ ConflictEdge::ConditionalRequires(_, _)
+ if target != ConflictNode::UnresolvedDependency =>
+ {
+ "blue"
+ }
_ => "red",
};
@@ -402,6 +415,13 @@ impl ConflictGraph {
ConflictEdge::Requires(requirement) => {
requirement.display(interner).to_string()
}
+ ConflictEdge::ConditionalRequires(version_set_id, requirement) => {
+ format!(
+ "if {} then {}",
+ interner.display_version_set(*version_set_id),
+ requirement.display(interner)
+ )
+ }
ConflictEdge::Conflict(ConflictCause::Constrains(version_set_id)) => {
interner.display_version_set(*version_set_id).to_string()
}
@@ -410,18 +430,6 @@ impl ConflictGraph {
"already installed".to_string()
}
ConflictEdge::Conflict(ConflictCause::Excluded) => "excluded".to_string(),
- ConflictEdge::Conflict(ConflictCause::UnsatisfiedCondition(condition)) => {
- // let condition_solvable = condition.as_solvable(&solver.variable_map)
- // .expect("condition must be a solvable");
- // format!("unsatisfied condition: {}", condition_solvable.display(interner))
- todo!()
- }
- ConflictEdge::ConditionalRequires(requirement, condition) => {
- // let condition_solvable = condition.as_solvable(&solver.variable_map)
- // .expect("condition must be a solvable");
- // format!("if {} then {}", condition_solvable.display(interner), requirement.display(interner))
- todo!()
- }
};
let target = match target {
@@ -1120,16 +1128,6 @@ impl<'i, I: Interner> fmt::Display for DisplayUnsat<'i, I> {
)?;
}
ConflictCause::Excluded => continue,
- &ConflictCause::UnsatisfiedCondition(condition) => {
- // let condition_solvable = condition.as_solvable(self.variable_map)
- // .expect("condition must be a solvable");
- // writeln!(
- // f,
- // "{indent}condition {} is not satisfied",
- // condition_solvable.display(self.interner),
- // )?;
- todo!()
- }
};
}
}
From db7ac8bae89dec5720d10f80685edb24933834d4 Mon Sep 17 00:00:00 2001
From: prsabahrami
Date: Wed, 22 Jan 2025 11:43:00 -0500
Subject: [PATCH 10/41] Fix the issues with current tests
---
src/requirement.rs | 9 +++++++++
tests/solver.rs | 25 ++++++++++++++-----------
2 files changed, 23 insertions(+), 11 deletions(-)
diff --git a/src/requirement.rs b/src/requirement.rs
index 18b6ce8..b498027 100644
--- a/src/requirement.rs
+++ b/src/requirement.rs
@@ -53,6 +53,15 @@ impl From for ConditionalRequirement {
}
}
+impl From for ConditionalRequirement {
+ fn from(value: VersionSetId) -> Self {
+ Self {
+ condition: None,
+ requirement: value.into(),
+ }
+ }
+}
+
/// Specifies the dependency of a solvable on a set of version sets.
#[derive(Clone, Copy, Debug, Hash, Eq, PartialEq, Ord, PartialOrd)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
diff --git a/tests/solver.rs b/tests/solver.rs
index de15d8a..1376528 100644
--- a/tests/solver.rs
+++ b/tests/solver.rs
@@ -22,9 +22,9 @@ use itertools::Itertools;
use resolvo::{
snapshot::{DependencySnapshot, SnapshotProvider},
utils::Pool,
- Candidates, Dependencies, DependencyProvider, Interner, KnownDependencies, NameId, Problem,
- Requirement, SolvableId, Solver, SolverCache, StringId, UnsolvableOrCancelled, VersionSetId,
- VersionSetUnionId,
+ Candidates, ConditionalRequirement, Dependencies, DependencyProvider, Interner,
+ KnownDependencies, NameId, Problem, Requirement, SolvableId, Solver, SolverCache, StringId,
+ UnsolvableOrCancelled, VersionSetId, VersionSetUnionId,
};
use tracing_test::traced_test;
use version_ranges::Ranges;
@@ -123,9 +123,7 @@ impl Spec {
pub fn parse_union(
spec: &str,
) -> impl Iterator- ::Err>> + '_ {
- spec.split('|')
- .map(str::trim)
- .map(|dep| Spec::from_str(dep))
+ spec.split('|').map(str::trim).map(Spec::from_str)
}
}
@@ -386,7 +384,7 @@ impl DependencyProvider for BundleBoxProvider {
candidates
.iter()
.copied()
- .filter(|s| range.contains(&self.pool.resolve_solvable(*s).record) == !inverse)
+ .filter(|s| range.contains(&self.pool.resolve_solvable(*s).record) != inverse)
.collect()
}
@@ -486,7 +484,7 @@ impl DependencyProvider for BundleBoxProvider {
};
let mut result = KnownDependencies {
- requirements: Vec::with_capacity(deps.dependencies.len()),
+ conditional_requirements: Vec::with_capacity(deps.dependencies.len()),
constrains: Vec::with_capacity(deps.constrains.len()),
};
for req in &deps.dependencies {
@@ -516,7 +514,12 @@ impl DependencyProvider for BundleBoxProvider {
.into()
};
- result.requirements.push(requirement);
+ result
+ .conditional_requirements
+ .push(ConditionalRequirement {
+ requirement,
+ condition: None,
+ });
}
for req in &deps.constrains {
@@ -538,7 +541,7 @@ impl DependencyProvider for BundleBoxProvider {
}
/// Create a string from a [`Transaction`]
-fn transaction_to_string(interner: &impl Interner, solvables: &Vec) -> String {
+fn transaction_to_string(interner: &impl Interner, solvables: &[SolvableId]) -> String {
use std::fmt::Write;
let mut buf = String::new();
for solvable in solvables
@@ -590,7 +593,7 @@ fn solve_snapshot(mut provider: BundleBoxProvider, specs: &[&str]) -> String {
let requirements = provider.parse_requirements(specs);
let mut solver = Solver::new(provider).with_runtime(runtime);
- let problem = Problem::new().requirements(requirements);
+ let problem = Problem::new().requirements(requirements.into_iter().map(|r| r.into()).collect());
match solver.solve(problem) {
Ok(solvables) => transaction_to_string(solver.provider(), &solvables),
Err(UnsolvableOrCancelled::Unsolvable(conflict)) => {
From 766a1a611f3d97b417901d5620c3f376cd43a0af Mon Sep 17 00:00:00 2001
From: prsabahrami
Date: Wed, 22 Jan 2025 14:32:38 -0500
Subject: [PATCH 11/41] fix cpp bindings and tests
---
cpp/_deps/corrosion-src | 1 +
cpp/include/resolvo.h | 18 +++++
cpp/src/lib.rs | 120 ++++++++++++++++++++++++++++------
cpp/tests/solve.cpp | 16 +++--
src/solver/clause.rs | 16 ++---
tests/.solver.rs.pending-snap | 10 +++
tests/solver.rs | 71 ++++++++++++++++++++
7 files changed, 215 insertions(+), 37 deletions(-)
create mode 160000 cpp/_deps/corrosion-src
create mode 100644 tests/.solver.rs.pending-snap
diff --git a/cpp/_deps/corrosion-src b/cpp/_deps/corrosion-src
new file mode 160000
index 0000000..ff5a236
--- /dev/null
+++ b/cpp/_deps/corrosion-src
@@ -0,0 +1 @@
+Subproject commit ff5a236550afc591f034e6cc5134ca9e5371bd98
diff --git a/cpp/include/resolvo.h b/cpp/include/resolvo.h
index 97d00f5..5343ac7 100644
--- a/cpp/include/resolvo.h
+++ b/cpp/include/resolvo.h
@@ -4,6 +4,7 @@
#include "resolvo_internal.h"
namespace resolvo {
+using cbindgen_private::ConditionalRequirement;
using cbindgen_private::Problem;
using cbindgen_private::Requirement;
@@ -24,6 +25,23 @@ inline Requirement requirement_union(VersionSetUnionId id) {
return cbindgen_private::resolvo_requirement_union(id);
}
+/**
+ * Specifies a conditional requirement (dependency) of a single version set.
+ * A solvable belonging to the version set satisfies the requirement if the condition is true.
+ */
+inline ConditionalRequirement conditional_requirement_single(VersionSetId id) {
+ return cbindgen_private::resolvo_conditional_requirement_single(id);
+}
+
+/**
+ * Specifies a conditional requirement (dependency) of the union (logical OR) of multiple version
+ * sets. A solvable belonging to any of the version sets contained in the union satisfies the
+ * requirement if the condition is true.
+ */
+inline ConditionalRequirement conditional_requirement_union(VersionSetUnionId id) {
+ return cbindgen_private::resolvo_conditional_requirement_union(id);
+}
+
/**
* Called to solve a package problem.
*
diff --git a/cpp/src/lib.rs b/cpp/src/lib.rs
index 04d05c0..6a1bda2 100644
--- a/cpp/src/lib.rs
+++ b/cpp/src/lib.rs
@@ -31,6 +31,66 @@ impl From for resolvo::SolvableId {
}
}
+/// A wrapper around an optional version set id.
+/// cbindgen:derive-eq
+/// cbindgen:derive-neq
+#[repr(C)]
+#[derive(Copy, Clone)]
+pub struct FfiOptionVersionSetId {
+ pub is_some: bool,
+ pub value: VersionSetId,
+}
+
+impl From