Skip to content

Commit

Permalink
feat!: decide on explicit requirements first (#61)
Browse files Browse the repository at this point in the history
  • Loading branch information
baszalmstra authored Sep 9, 2024
1 parent a291024 commit 187806c
Show file tree
Hide file tree
Showing 5 changed files with 127 additions and 72 deletions.
4 changes: 2 additions & 2 deletions .github/workflows/rust-compile.yml
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ jobs:
- name: Run rustfmt
uses: actions-rust-lang/rustfmt@v1
- name: Run clippy
run: cargo clippy
run: cargo clippy --workspace

test:
name: Test
Expand All @@ -56,4 +56,4 @@ jobs:
- name: Build
run: cargo build
- name: Run tests
run: cargo test -- --nocapture
run: cargo test --workspace -- --nocapture
16 changes: 5 additions & 11 deletions cpp/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -387,7 +387,7 @@ impl<'d> resolvo::Interner for &'d DependencyProvider {
) -> impl Iterator<Item = resolvo::VersionSetId> {
unsafe { (self.version_sets_in_union)(self.data, version_set_union.into()) }
.as_slice()
.into_iter()
.iter()
.copied()
.map(Into::into)
}
Expand Down Expand Up @@ -435,7 +435,7 @@ impl<'d> resolvo::DependencyProvider for &'d DependencyProvider {
.collect(),
excluded: candidates
.excluded
.into_iter()
.iter()
.map(|excluded| (excluded.solvable.into(), excluded.reason.into()))
.collect(),
})
Expand Down Expand Up @@ -494,26 +494,20 @@ pub extern "C" fn resolvo_solve(
.requirements(
problem
.requirements
.into_iter()
.iter()
.copied()
.map(Into::into)
.collect(),
)
.constraints(
problem
.constraints
.into_iter()
.iter()
.copied()
.map(Into::into)
.collect(),
)
.soft_requirements(
problem
.soft_requirements
.into_iter()
.copied()
.map(Into::into),
);
.soft_requirements(problem.soft_requirements.iter().copied().map(Into::into));

match solver.solve(problem) {
Ok(solution) => {
Expand Down
141 changes: 85 additions & 56 deletions src/solver/mod.rs
Original file line number Diff line number Diff line change
@@ -1,11 +1,13 @@
use std::{
any::Any, cell::RefCell, collections::HashSet, fmt::Display, future::ready, ops::ControlFlow,
};

pub use cache::SolverCache;
use clause::{Clause, ClauseState, Literal};
use decision::Decision;
use decision_tracker::DecisionTracker;
use futures::{stream::FuturesUnordered, FutureExt, StreamExt};
use itertools::Itertools;
use std::fmt::Display;
use std::{any::Any, cell::RefCell, collections::HashSet, future::ready, ops::ControlFlow};
use watch_map::WatchMap;

use crate::{
Expand Down Expand Up @@ -36,11 +38,12 @@ struct AddClauseOutput {

/// Describes the problem that is to be solved by the solver.
///
/// This struct is generic over the type `S` of the collection of soft requirements passed
/// to the solver, typically expected to be a type implementing [`IntoIterator`].
/// This struct is generic over the type `S` of the collection of soft
/// requirements passed to the solver, typically expected to be a type
/// implementing [`IntoIterator`].
///
/// This struct follows the builder pattern and can have its fields set by one of the available
/// setter methods.
/// This struct follows the builder pattern and can have its fields set by one
/// of the available setter methods.
pub struct Problem<S> {
requirements: Vec<Requirement>,
constraints: Vec<VersionSetId>,
Expand All @@ -54,8 +57,8 @@ impl Default for Problem<std::iter::Empty<SolvableId>> {
}

impl Problem<std::iter::Empty<SolvableId>> {
/// Creates a new empty [`Problem`]. Use the setter methods to build the problem
/// before passing it to the solver to be solved.
/// Creates a new empty [`Problem`]. Use the setter methods to build the
/// problem before passing it to the solver to be solved.
pub fn new() -> Self {
Self {
requirements: Default::default(),
Expand All @@ -66,41 +69,45 @@ impl Problem<std::iter::Empty<SolvableId>> {
}

impl<S: IntoIterator<Item = SolvableId>> Problem<S> {
/// Sets the requirements that _must_ have one candidate solvable be included in the
/// solution.
/// Sets the requirements that _must_ have one candidate solvable be
/// included in the solution.
///
/// Returns the [`Problem`] for further mutation or to pass to [`Solver::solve`].
/// Returns the [`Problem`] for further mutation or to pass to
/// [`Solver::solve`].
pub fn requirements(self, requirements: Vec<Requirement>) -> Self {
Self {
requirements,
..self
}
}

/// Sets the additional constraints imposed on individual packages that the solvable (if any)
/// chosen for that package _must_ adhere to.
/// Sets the additional constraints imposed on individual packages that the
/// solvable (if any) chosen for that package _must_ adhere to.
///
/// Returns the [`Problem`] for further mutation or to pass to [`Solver::solve`].
/// Returns the [`Problem`] for further mutation or to pass to
/// [`Solver::solve`].
pub fn constraints(self, constraints: Vec<VersionSetId>) -> Self {
Self {
constraints,
..self
}
}

/// Sets the additional requirements that the solver should _try_ and fulfill once it has
/// found a solution to the main problem.
/// Sets the additional requirements that the solver should _try_ and
/// fulfill once it has found a solution to the main problem.
///
/// An unsatisfiable soft requirement does not cause a conflict; the solver will try
/// and fulfill as many soft requirements as possible and skip the unsatisfiable ones.
/// An unsatisfiable soft requirement does not cause a conflict; the solver
/// will try and fulfill as many soft requirements as possible and skip
/// the unsatisfiable ones.
///
/// Soft requirements are currently only specified as individual solvables to be
/// included in the solution, however in the future they will be able to be specified
/// as version sets.
/// Soft requirements are currently only specified as individual solvables
/// to be included in the solution, however in the future they will be
/// able to be specified as version sets.
///
/// # Returns
///
/// Returns the [`Problem`] for further mutation or to pass to [`Solver::solve`].
/// Returns the [`Problem`] for further mutation or to pass to
/// [`Solver::solve`].
pub fn soft_requirements<I: IntoIterator<Item = SolvableId>>(
self,
soft_requirements: I,
Expand Down Expand Up @@ -236,27 +243,32 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {

/// Solves the given [`Problem`].
///
/// The solver first solves for the root requirements and constraints, and then
/// tries to include in the solution as many of the soft requirements as it can.
/// Each soft requirement is subject to all the clauses and decisions introduced
/// for all the previously decided solvables in the solution.
/// The solver first solves for the root requirements and constraints, and
/// then tries to include in the solution as many of the soft
/// requirements as it can. Each soft requirement is subject to all the
/// clauses and decisions introduced for all the previously decided
/// solvables in the solution.
///
/// Unless the corresponding package has been requested by a version set in another
/// solvable's clauses, each soft requirement is _not_ subject to the
/// package-level clauses introduced in [`DependencyProvider::get_candidates`] since the
/// solvables have been requested specifically (not through a version set) in the solution.
/// Unless the corresponding package has been requested by a version set in
/// another solvable's clauses, each soft requirement is _not_ subject
/// to the package-level clauses introduced in
/// [`DependencyProvider::get_candidates`] since the solvables have been
/// requested specifically (not through a version set) in the solution.
///
/// # Returns
///
/// If a solution was found, returns a [`Vec`] of the solvables included in the solution.
/// If a solution was found, returns a [`Vec`] of the solvables included in
/// the solution.
///
/// If no solution to the _root_ requirements and constraints was found, returns a
/// [`Conflict`] wrapped in a [`UnsolvableOrCancelled::Unsolvable`], which provides ways to
/// inspect the causes and report them to the user. If a soft requirement is unsolvable,
/// it is simply not included in the solution.
/// If no solution to the _root_ requirements and constraints was found,
/// returns a [`Conflict`] wrapped in a
/// [`UnsolvableOrCancelled::Unsolvable`], which provides ways to
/// inspect the causes and report them to the user. If a soft requirement is
/// unsolvable, it is simply not included in the solution.
///
/// If the solution process is cancelled (see [`DependencyProvider::should_cancel_with_value`]),
/// returns an [`UnsolvableOrCancelled::Cancelled`] containing the cancellation value.
/// If the solution process is cancelled (see
/// [`DependencyProvider::should_cancel_with_value`]), returns an
/// [`UnsolvableOrCancelled::Cancelled`] containing the cancellation value.
pub fn solve(
&mut self,
problem: Problem<impl IntoIterator<Item = SolvableId>>,
Expand Down Expand Up @@ -291,7 +303,8 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
Ok(self.chosen_solvables().collect())
}

/// Returns the solvables that the solver has chosen to include in the solution so far.
/// Returns the solvables that the solver has chosen to include in the
/// solution so far.
fn chosen_solvables(&self) -> impl Iterator<Item = SolvableId> + '_ {
self.decision_tracker.stack().filter_map(|d| {
if d.value {
Expand Down Expand Up @@ -668,12 +681,14 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
///
/// The solver loop can be found in [`Solver::resolve_dependencies`].
///
/// Returns `Ok(true)` if a solution was found for `solvable`. If a solution was not
/// found, returns `Ok(false)` if some decisions have already been made by the solver
/// (i.e. the decision tracker stack is not empty). Otherwise, returns
/// [`UnsolvableOrCancelled::Unsolvable`] as an `Err` on no solution.
/// Returns `Ok(true)` if a solution was found for `solvable`. If a solution
/// was not found, returns `Ok(false)` if some decisions have already
/// been made by the solver (i.e. the decision tracker stack is not
/// empty). Otherwise, returns [`UnsolvableOrCancelled::Unsolvable`] as
/// an `Err` on no solution.
///
/// If the solution process is cancelled (see [`DependencyProvider::should_cancel_with_value`]),
/// If the solution process is cancelled (see
/// [`DependencyProvider::should_cancel_with_value`]),
/// returns [`UnsolvableOrCancelled::Cancelled`] as an `Err`.
fn run_sat(&mut self, solvable: InternalSolvableId) -> Result<bool, UnsolvableOrCancelled> {
let starting_level = self
Expand Down Expand Up @@ -824,12 +839,13 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
}
}

/// Decides how to terminate the solver algorithm when the given `solvable` was
/// deemed unsolvable by [`Solver::run_sat`].
/// Decides how to terminate the solver algorithm when the given `solvable`
/// was deemed unsolvable by [`Solver::run_sat`].
///
/// Returns an `Err` value of [`UnsolvableOrCancelled::Unsolvable`] only if `solvable` is
/// the very first solvable we are solving for. Otherwise, undoes all the decisions made
/// when trying to solve for `solvable`, sets it to `false` and returns `Ok(false)`.
/// Returns an `Err` value of [`UnsolvableOrCancelled::Unsolvable`] only if
/// `solvable` is the very first solvable we are solving for. Otherwise,
/// undoes all the decisions made when trying to solve for `solvable`,
/// sets it to `false` and returns `Ok(false)`.
fn run_sat_process_unsolvable(
&mut self,
solvable: InternalSolvableId,
Expand Down Expand Up @@ -912,8 +928,16 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
/// ensures that if there are conflicts they are delt with as early as
/// possible.
fn decide(&mut self) -> Option<(InternalSolvableId, InternalSolvableId, ClauseId)> {
let mut best_decision = None;
let mut best_decision: Option<(bool, i32, (SolvableId, InternalSolvableId, ClauseId))> =
None;
for &(solvable_id, deps, clause_id) in &self.requires_clauses {
let is_explicit_requirement = solvable_id == InternalSolvableId::root();
if !is_explicit_requirement && matches!(best_decision, Some((true, _, _))) {
// If we already have an explicit requirement, there is no need to evaluate
// non-explicit requirements.
continue;
}

// Consider only clauses in which we have decided to install the solvable
if self.decision_tracker.assigned_value(solvable_id) != Some(true) {
continue;
Expand Down Expand Up @@ -947,9 +971,10 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
ControlFlow::Continue((Some(candidate), count)) => {
let possible_decision = (candidate, solvable_id, clause_id);
best_decision = Some(match best_decision {
None => (count, possible_decision),
Some((best_count, _)) if count < best_count => {
(count, possible_decision)
None => (is_explicit_requirement, count, possible_decision),
Some((false, _, _)) if is_explicit_requirement => (is_explicit_requirement, count, possible_decision),
Some((_, best_count, _)) if count < best_count => {
(is_explicit_requirement, count, possible_decision)
}
Some(best_decision) => best_decision,
})
Expand All @@ -959,7 +984,9 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
}
}

if let Some((count, (candidate, _solvable_id, clause_id))) = best_decision {
if let Some((_is_explicit_requirement, count, (candidate, _solvable_id, clause_id))) =
best_decision
{
tracing::trace!(
"deciding to assign {}, ({}, {} possible candidates)",
self.provider().display_solvable(candidate),
Expand All @@ -969,9 +996,11 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
}

// Could not find a requirement that needs satisfying.
best_decision.map(|(_best_count, (candidate, required_by, via))| {
(candidate.into(), required_by, via)
})
best_decision.map(
|(_is_explicit_dependency, _best_count, (candidate, required_by, via))| {
(candidate.into(), required_by, via)
},
)
}

/// Executes one iteration of the CDCL loop
Expand Down
32 changes: 32 additions & 0 deletions tests/solver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1360,6 +1360,38 @@ fn test_snapshot_union_requirements() {
));
}

#[test]
fn test_explicit_root_requirements() {
let provider = BundleBoxProvider::from_packages(&[
// `a` depends transitively on `b`
("a", 1, vec!["b"]),
// `b` depends on `c`, but the highest version of `b` constrains `c` to `<2`.
("b", 1, vec!["c"]),
("b", 2, vec!["c 1..2"]),
// `c` has more versions than `b`, so the heuristic will most likely pick `b` first.
("c", 1, vec![]),
("c", 2, vec![]),
("c", 3, vec![]),
("c", 4, vec![]),
("c", 5, vec![]),
]);

// We require both `a` and `c` explicitly. The expected outcome will be that we
// get the highest versions of `a` and `c` and a lower version of `b`.
let requirements = provider.requirements(&["a", "c"]);

let mut solver = Solver::new(provider);
let problem = Problem::default().requirements(requirements);
let solved = solver.solve(problem).unwrap();

let result = transaction_to_string(solver.provider(), &solved);
assert_snapshot!(result, @r###"
a=1
b=1
c=5
"###);
}

#[cfg(feature = "serde")]
fn serialize_snapshot(snapshot: &DependencySnapshot, destination: impl AsRef<std::path::Path>) {
let file = std::io::BufWriter::new(std::fs::File::create(destination.as_ref()).unwrap());
Expand Down
6 changes: 3 additions & 3 deletions tools/solve-snapshot/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -58,14 +58,14 @@ fn main() {

// Generate a range of problems.
let mut rng = StdRng::seed_from_u64(0);
let requirement_dist = WeightedIndex::new(&[
let requirement_dist = WeightedIndex::new([
10, // 10 times more likely to pick a package
if snapshot.version_sets.len() > 0 {
if !snapshot.version_sets.is_empty() {
1
} else {
0
},
if snapshot.version_set_unions.len() > 0 {
if !snapshot.version_set_unions.is_empty() {
1
} else {
0
Expand Down

0 comments on commit 187806c

Please sign in to comment.