Skip to content

Commit

Permalink
switch from version set id to variable id in in conditional clauses t…
Browse files Browse the repository at this point in the history 
…o have multiple clauses per version
  • Loading branch information
@prsabahrami
prsabahrami committed Jan 28, 2025
1 parent 8cd35a9 commit 997ae4d
Show file tree
Hide file tree
Showing 4 changed files with 128 additions and 185 deletions.
62 changes: 31 additions & 31 deletions src/conflict.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,10 +14,14 @@ use petgraph::{
use crate::{
internal::{
arena::ArenaId,
id::{ClauseId, SolvableId, SolvableOrRootId, StringId, VersionSetId},
id::{ClauseId, SolvableId, SolvableOrRootId, StringId, VariableId, VersionSetId},

Check failure on line 17 in src/conflict.rs

View workflow job for this annotation

GitHub Actions / Format and Lint 

unused imports: `VariableId`, `VariableMap`
},
runtime::AsyncRuntime,
solver::{clause::Clause, variable_map::VariableOrigin, Solver},
solver::{
clause::Clause,
variable_map::{VariableMap, VariableOrigin},
Solver,
},
DependencyProvider, Interner, Requirement,
};

Expand Down Expand Up @@ -159,7 +163,12 @@ impl Conflict {
ConflictEdge::Conflict(ConflictCause::Constrains(version_set_id)),
);
}
&Clause::Conditional(package_id, condition, requirement) => {
&Clause::Conditional(
package_id,
condition_variable,
condition_version_set_id,
requirement,
) => {
let solvable = package_id
.as_solvable_or_root(&solver.variable_map)
.expect("only solvables can be excluded");
Expand All @@ -176,43 +185,34 @@ impl Conflict {
)
});

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 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),
ConflictEdge::ConditionalRequires(
condition_version_set_id,
requirement,
),
);
} else if conditional_candidates.is_empty() {
} else {
tracing::trace!(
"{package_id:?} conditionally requires {requirement:?}, but the condition has no candidates"
"{package_id:?} conditionally requires {requirement:?} if {condition_variable:?}"
);
graph.add_edge(
package_node,
unresolved_node,
ConflictEdge::ConditionalRequires(condition, requirement),
);
} else {
for &candidate_id in conditional_candidates {
tracing::trace!(
"{package_id:?} conditionally requires {requirement:?} if {candidate_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),
);
}
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_version_set_id,
requirement,
),
);
}
}
}
Expand Down Expand Up @@ -415,10 +415,10 @@ impl ConflictGraph {
ConflictEdge::Requires(requirement) => {
requirement.display(interner).to_string()
}
ConflictEdge::ConditionalRequires(version_set_id, requirement) => {
ConflictEdge::ConditionalRequires(condition_version_set_id, requirement) => {
format!(
"if {} then {}",
interner.display_version_set(*version_set_id),
interner.display_version_set(*condition_version_set_id),
requirement.display(interner)
)
}
Expand Down
110 changes: 40 additions & 70 deletions src/solver/clause.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,9 @@ 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, VersionSetId, Requirement),
/// We need to store the version set id because in the conflict graph, the version set id
/// is used to identify the condition variable.
Conditional(VariableId, 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,
Expand Down Expand Up @@ -237,49 +239,38 @@ impl Clause {
fn conditional(
parent_id: VariableId,
requirement: Requirement,
condition: VersionSetId,
condition_variable: VariableId,
condition_version_set_id: VersionSetId,
decision_tracker: &DecisionTracker,
requirement_candidates: impl IntoIterator<Item = VariableId>,
condition_candidates: impl IntoIterator<Item = VariableId>,
) -> (Self, Option<[Literal; 2]>, bool) {
assert_ne!(decision_tracker.assigned_value(parent_id), Some(false));
let mut condition_candidates = condition_candidates.into_iter();
let requirement_candidates = requirement_candidates.into_iter();

// Check if we have any condition candidates
let first_condition = condition_candidates
.next()
.expect("no condition candidates");

// Map condition candidates to negative literals and requirement candidates to positive literals
let mut iter = condition_candidates
.map(|id| (id, id.negative()))
.chain(requirement_candidates.map(|id| (id, id.positive())))
.peekable();

let condition_literal = if iter.peek().is_some() {
iter.find(|&(id, _)| {
let value = decision_tracker.assigned_value(id);
value.is_none() || value == Some(true)
})
.map(|(_, literal)| literal)
} else {
None
};
match condition_literal {
// Found a valid literal - use it
Some(literal) => (
Clause::Conditional(parent_id, condition, requirement),
Some([parent_id.negative(), literal]),
false,
),
// No valid literals found - conflict case
None => (
Clause::Conditional(parent_id, condition, requirement),
Some([parent_id.negative(), first_condition.negative()]),
true,
let mut requirement_candidates = requirement_candidates.into_iter();

let requirement_literal =
if decision_tracker.assigned_value(condition_variable) == Some(true) {
// then ~condition is false
requirement_candidates
.find(|&id| decision_tracker.assigned_value(id) != Some(false))
.map(|id| id.positive())
} else {
None
};

(
Clause::Conditional(
parent_id,
condition_variable,
condition_version_set_id,
requirement,
),
}
Some([
parent_id.negative(),
requirement_literal.unwrap_or(condition_variable.negative()),
]),
requirement_literal.is_none()
&& decision_tracker.assigned_value(condition_variable) == Some(true),
)
}

/// Tries to fold over all the literals in the clause.
Expand All @@ -294,11 +285,6 @@ 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 @@ -329,14 +315,9 @@ impl Clause {
Clause::Lock(_, s) => [s.negative(), VariableId::root().negative()]
.into_iter()
.try_fold(init, visit),
Clause::Conditional(package_id, condition, requirement) => {
Clause::Conditional(package_id, condition_variable, _, requirement) => {
iter::once(package_id.negative())
.chain(
version_set_to_variables[&condition]
.iter()
.flatten()
.map(|&s| s.negative()),
)
.chain(iter::once(condition_variable.negative()))
.chain(
requirements_to_sorted_candidates[&requirement]
.iter()
Expand All @@ -359,17 +340,11 @@ 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 @@ -506,18 +481,18 @@ impl WatchedLiterals {
pub fn conditional(
package_id: VariableId,
requirement: Requirement,
condition: VersionSetId,
condition_variable: VariableId,
condition_version_set_id: VersionSetId,
decision_tracker: &DecisionTracker,
requirement_candidates: impl IntoIterator<Item = VariableId>,
condition_candidates: impl IntoIterator<Item = VariableId>,
) -> (Option<Self>, bool, Clause) {
let (kind, watched_literals, conflict) = Clause::conditional(
package_id,
requirement,
condition,
condition_variable,
condition_version_set_id,
decision_tracker,
requirement_candidates,
condition_candidates,
);

(
Expand Down Expand Up @@ -545,11 +520,6 @@ 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 @@ -566,7 +536,6 @@ 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 Expand Up @@ -725,13 +694,14 @@ impl<'i, I: Interner> Display for ClauseDisplay<'i, I> {
other,
)
}
Clause::Conditional(package_id, condition, requirement) => {
Clause::Conditional(package_id, condition_variable, _, requirement) => {
write!(
f,
"Conditional({}({:?}), {}, {})",
"Conditional({}({:?}), {}({:?}), {})",
package_id.display(self.variable_map, self.interner),
package_id,
self.interner.display_version_set(condition),
condition_variable.display(self.variable_map, self.interner),
condition_variable,
requirement.display(self.interner),
)
}
Expand Down
Loading

0 comments on commit 997ae4d

Please sign in to comment.