Skip to content

Commit

Permalink
Add the version_sets_to_variables map
Browse files Browse the repository at this point in the history
  • Loading branch information
@prsabahrami
prsabahrami committed Jan 24, 2025
1 parent 7e0e1c6 commit 3ddb16c
Show file tree
Hide file tree
Showing 2 changed files with 41 additions and 12 deletions.
19 changes: 18 additions & 1 deletion src/solver/clause.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -303,6 +303,11 @@ impl Clause {
Vec<Vec<VariableId>>,
ahash::RandomState,
>,
version_set_to_variables: &FrozenMap<
VersionSetId,
Vec<Vec<VariableId>>,
ahash::RandomState,
>,
init: C,
mut visit: F,
) -> ControlFlow<B, C>
Expand Down Expand Up @@ -336,7 +341,7 @@ impl Clause {
Clause::Conditional(package_id, condition, requirement) => {
iter::once(package_id.negative())
.chain(
requirements_to_sorted_candidates[&condition.into()]
version_set_to_variables[&condition]
.iter()
.flatten()
.map(|&s| s.negative()),
Expand All @@ -363,11 +368,17 @@ impl Clause {
Vec<Vec<VariableId>>,
ahash::RandomState,
>,
version_set_to_variables: &FrozenMap<
VersionSetId,
Vec<Vec<VariableId>>,
ahash::RandomState,
>,
mut visit: impl FnMut(Literal),
) {
self.try_fold_literals(
learnt_clauses,
requirements_to_sorted_candidates,
version_set_to_variables,
(),
|_, lit| {
visit(lit);
Expand Down Expand Up @@ -543,6 +554,11 @@ impl WatchedLiterals {
Vec<Vec<VariableId>>,
ahash::RandomState,
>,
version_set_to_variables: &FrozenMap<
VersionSetId,
Vec<Vec<VariableId>>,
ahash::RandomState,
>,
decision_map: &DecisionMap,
for_watch_index: usize,
) -> Option<Literal> {
Expand All @@ -559,6 +575,7 @@ impl WatchedLiterals {
let next = clause.try_fold_literals(
learnt_clauses,
requirement_to_sorted_candidates,
version_set_to_variables,
(),
|_, lit| {
// The next unwatched variable (if available), is a variable that is:
Expand Down
34 changes: 23 additions & 11 deletions src/solver/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -161,6 +161,10 @@ pub struct Solver<D: DependencyProvider, RT: AsyncRuntime = NowOrNeverRuntime> {
requirement_to_sorted_candidates:
FrozenMap<Requirement, RequirementCandidateVariables, ahash::RandomState>,

/// A mapping from version sets to the variables that represent the
/// candidates.
version_set_to_variables: FrozenMap<VersionSetId, Vec<Vec<VariableId>>, ahash::RandomState>,

pub(crate) variable_map: VariableMap,

negative_assertions: Vec<(VariableId, ClauseId)>,
Expand Down Expand Up @@ -206,6 +210,7 @@ impl<D: DependencyProvider> Solver<D, NowOrNeverRuntime> {
requires_clauses: Default::default(),
conditional_clauses: Default::default(),
requirement_to_sorted_candidates: FrozenMap::default(),
version_set_to_variables: FrozenMap::default(),
watches: WatchMap::new(),
negative_assertions: Default::default(),
learnt_clauses: Arena::new(),
Expand All @@ -218,7 +223,6 @@ impl<D: DependencyProvider> Solver<D, NowOrNeverRuntime> {
clauses_added_for_solvable: Default::default(),
forbidden_clauses_added: Default::default(),
name_activity: Default::default(),

activity_add: 1.0,
activity_decay: 0.95,
}
Expand Down Expand Up @@ -287,6 +291,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
requires_clauses: self.requires_clauses,
conditional_clauses: self.conditional_clauses,
requirement_to_sorted_candidates: self.requirement_to_sorted_candidates,
version_set_to_variables: self.version_set_to_variables,
watches: self.watches,
negative_assertions: self.negative_assertions,
learnt_clauses: self.learnt_clauses,
Expand Down Expand Up @@ -484,6 +489,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
&mut self.clauses_added_for_package,
&mut self.forbidden_clauses_added,
&mut self.requirement_to_sorted_candidates,
&self.version_set_to_variables,
&self.root_requirements,
&self.root_constraints,
))?;
Expand Down Expand Up @@ -600,6 +606,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
&mut self.clauses_added_for_package,
&mut self.forbidden_clauses_added,
&mut self.requirement_to_sorted_candidates,
&self.version_set_to_variables,
&self.root_requirements,
&self.root_constraints,
))?;
Expand Down Expand Up @@ -1200,6 +1207,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
clause,
&self.learnt_clauses,
&self.requirement_to_sorted_candidates,
&self.version_set_to_variables,
self.decision_tracker.map(),
watch_index,
) {
Expand Down Expand Up @@ -1359,6 +1367,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
self.clauses.kinds[clause_id.to_usize()].visit_literals(
&self.learnt_clauses,
&self.requirement_to_sorted_candidates,
&self.version_set_to_variables,
|literal| {
involved.insert(literal.variable());
},
Expand Down Expand Up @@ -1397,6 +1406,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
self.clauses.kinds[why.to_usize()].visit_literals(
&self.learnt_clauses,
&self.requirement_to_sorted_candidates,
&self.version_set_to_variables,
|literal| {
if literal.eval(self.decision_tracker.map()) == Some(true) {
assert_eq!(literal.variable(), decision.variable);
Expand Down Expand Up @@ -1444,6 +1454,7 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
clause_kinds[clause_id.to_usize()].visit_literals(
&self.learnt_clauses,
&self.requirement_to_sorted_candidates,
&self.version_set_to_variables,
|literal| {
if !first_iteration && literal.variable() == conflicting_solvable {
// We are only interested in the causes of the conflict, so we ignore the
Expand Down Expand Up @@ -1578,6 +1589,7 @@ async fn add_clauses_for_solvables<D: DependencyProvider>(
RequirementCandidateVariables,
ahash::RandomState,
>,
version_set_to_variables: &FrozenMap<VersionSetId, Vec<Vec<VariableId>>, ahash::RandomState>,
root_requirements: &[ConditionalRequirement],
root_constraints: &[VersionSetId],
) -> Result<AddClauseOutput, Box<dyn Any>> {
Expand Down Expand Up @@ -1766,18 +1778,15 @@ async fn add_clauses_for_solvables<D: DependencyProvider>(
.await?;

// condition is `VersionSetId` right now but it will become a `Requirement`
// in the future
// in the next versions of resolvo
if let Some(condition) = conditional_requirement.condition {
let condition_candidates = vec![
cache
.get_or_cache_sorted_candidates_for_version_set(condition)
.await?,
];
let condition_candidates =
cache.get_or_cache_matching_candidates(condition).await?;

Ok(TaskResult::SortedCandidates {
solvable_id,
requirement: conditional_requirement.requirement,
condition: Some((condition, condition_candidates)),
condition: Some((condition, vec![condition_candidates])),
candidates,
})
} else {
Expand Down Expand Up @@ -1934,15 +1943,18 @@ async fn add_clauses_for_solvables<D: DependencyProvider>(
.display(cache.provider()),
);

let condition_version_set_variables: Vec<_> = condition_candidates
let condition_version_set_variables = version_set_to_variables.insert(
condition,
condition_candidates
.iter()
.map(|&candidates| {
candidates
.iter()
.map(|&var| variable_map.intern_solvable(var))
.collect::<Vec<_>>()
.collect()
})
.collect();
.collect(),
);

// Add a condition clause
let (watched_literals, conflict, kind) = WatchedLiterals::conditional(
Expand Down

0 comments on commit 3ddb16c

Please sign in to comment.