Skip to content

Commit

Permalink
add the conditional clauses to the DependencyProvider
Browse files Browse the repository at this point in the history
  • Loading branch information
@prsabahrami
prsabahrami committed Jan 22, 2025
1 parent eb4d253 commit 451536e
Showing 1 changed file with 216 additions and 47 deletions.
263 changes: 216 additions & 47 deletions src/solver/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -927,6 +927,154 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
}
}

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,
Expand Down Expand Up @@ -1869,59 +2017,80 @@ async fn add_clauses_for_solvables<D: DependencyProvider>(
);
}

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 {
Expand Down

0 comments on commit 451536e

Please sign in to comment.