Skip to content

Commit

Permalink
feat(solver)!: Add Problem struct to describe solver input
Browse files Browse the repository at this point in the history
  • Loading branch information
eviltak committed Aug 6, 2024
1 parent 13830ad commit f3f886d
Show file tree
Hide file tree
Showing 6 changed files with 193 additions and 133 deletions.
7 changes: 4 additions & 3 deletions cpp/include/resolvo.h
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
#include "resolvo_internal.h"

namespace resolvo {
using cbindgen_private::Problem;
using cbindgen_private::Requirement;

/**
Expand All @@ -30,8 +31,8 @@ inline Requirement requirement_union(VersionSetUnionId id) {
* stored in `result`. If the solve was unsuccesfull an error describing the reason is returned and
* the result vector will be empty.
*/
inline String solve(DependencyProvider &provider, Slice<Requirement> requirements,
Slice<VersionSetId> constraints, Vector<SolvableId> &result) {
inline String solve(DependencyProvider &provider, const Problem &problem,
Vector<SolvableId> &result) {
cbindgen_private::DependencyProvider bridge{
static_cast<void *>(&provider),
private_api::bridge_display_solvable,
Expand All @@ -50,7 +51,7 @@ inline String solve(DependencyProvider &provider, Slice<Requirement> requirement
};

String error;
cbindgen_private::resolvo_solve(&bridge, requirements, constraints, &error, &result);
cbindgen_private::resolvo_solve(&bridge, &problem, &error, &result);
return error;
}
} // namespace resolvo
45 changes: 31 additions & 14 deletions cpp/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -473,28 +473,45 @@ impl<'d> resolvo::DependencyProvider for &'d DependencyProvider {
}
}

#[repr(C)]
pub struct Problem<'a> {
pub requirements: Slice<'a, Requirement>,
pub constraints: Slice<'a, VersionSetId>,
pub soft_requirements: Slice<'a, SolvableId>,
}

#[no_mangle]
#[allow(unused)]
pub extern "C" fn resolvo_solve(
provider: &DependencyProvider,
requirements: Slice<Requirement>,
constraints: Slice<VersionSetId>,
problem: &Problem,
error: &mut String,
result: &mut Vector<SolvableId>,
) -> bool {
let requirements = requirements
.into_iter()
.copied()
.map(Into::into)
.collect::<Vec<_>>();
let constraints = constraints
.into_iter()
.copied()
.map(Into::into)
.collect::<Vec<_>>();

let mut solver = resolvo::Solver::new(provider);
match solver.solve(requirements, constraints) {

let problem = resolvo::Problem {
requirements: problem
.requirements
.into_iter()
.copied()
.map(Into::into)
.collect(),
constraints: problem
.constraints
.into_iter()
.copied()
.map(Into::into)
.collect(),
soft_requirements: problem
.soft_requirements
.into_iter()
.copied()
.map(Into::into)
.collect(),
};

match solver.solve(problem) {
Ok(solution) => {
*result = solution.into_iter().map(Into::into).collect();
true
Expand Down
20 changes: 15 additions & 5 deletions cpp/tests/solve.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -216,19 +216,27 @@ SCENARIO("Solve") {

auto c_1 = db.alloc_candidate("c", 1, {});

const auto d_1 = db.alloc_candidate("d", 1, {});

// Construct a problem to be solved by the solver
resolvo::Vector<resolvo::Requirement> requirements = {db.alloc_requirement("a", 1, 3)};
resolvo::Vector<resolvo::VersionSetId> constraints = {db.alloc_version_set("b", 1, 3),
db.alloc_version_set("c", 1, 3)};
resolvo::Vector<resolvo::VersionSetId> constraints = {
db.alloc_version_set("b", 1, 3),
db.alloc_version_set("c", 1, 3),
db.alloc_version_set("d", 2, 2),
};
resolvo::Vector soft_requirements{c_1, d_1};

// Solve the problem
resolvo::Vector<resolvo::SolvableId> result;
resolvo::solve(db, requirements, constraints, result);
resolvo::Problem problem = {requirements, constraints, soft_requirements};
resolvo::solve(db, problem, result);

// Check the result
REQUIRE(result.size() == 2);
REQUIRE(result.size() == 3);
REQUIRE(result[0] == a_2);
REQUIRE(result[1] == b_2);
REQUIRE(result[2] == c_1);
}

SCENARIO("Solve Union") {
Expand Down Expand Up @@ -264,7 +272,9 @@ SCENARIO("Solve Union") {

// Solve the problem
resolvo::Vector<resolvo::SolvableId> result;
resolvo::solve(db, requirements, constraints, result);
resolvo::Problem problem = {requirements, constraints, {}};
resolvo::solve(db, problem, result);
;

// Check the result
REQUIRE(result.size() == 4);
Expand Down
2 changes: 1 addition & 1 deletion src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ pub use internal::{
};
use itertools::Itertools;
pub use requirement::Requirement;
pub use solver::{Solver, SolverCache, UnsolvableOrCancelled};
pub use solver::{Problem, Solver, SolverCache, UnsolvableOrCancelled};

/// An object that is used by the solver to query certain properties of
/// different internalized objects.
Expand Down
141 changes: 59 additions & 82 deletions src/solver/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -34,12 +34,30 @@ struct AddClauseOutput {
clauses_to_watch: Vec<ClauseId>,
}

/// Describes the problem that is to be solved by the solver.
#[derive(Default)]
pub struct Problem {
/// The requirements that _must_ have one candidate solvable be included in the
/// solution.
pub requirements: Vec<Requirement>,

/// Additional constraints imposed on individual packages that the solvable (if any)
/// chosen for that package _must_ adhere to.
pub constraints: Vec<VersionSetId>,

/// A set of 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.
///
/// 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.
pub soft_requirements: Vec<SolvableId>,
}

/// Drives the SAT solving process.
///
/// The solver can solve for multiple solvables in addition to the root requirements
/// (see [`Solver::solve_with_additional`]), with the solution being _cumulative_. That is,
/// each requested solvable is subject to all the clauses introduced and decisions made
/// in previous solvable requests.
pub struct Solver<D: DependencyProvider, RT: AsyncRuntime = NowOrNeverRuntime> {
pub(crate) async_runtime: RT,
pub(crate) cache: SolverCache<D>,
Expand Down Expand Up @@ -160,71 +178,58 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
}
}

/// Solves for the provided `root_requirements` and `root_constraints`. The
/// `root_requirements` are package that will be included in the
/// solution. `root_constraints` are additional constrains which do not
/// necesarily need to be included in the solution.
///
/// Returns a [`Conflict`] if no solution was found, which provides ways to
/// inspect the causes and report them to the user.
pub fn solve(
&mut self,
root_requirements: Vec<Requirement>,
root_constraints: Vec<VersionSetId>,
) -> Result<Vec<SolvableId>, UnsolvableOrCancelled> {
self.solve_for_root(root_requirements, root_constraints)?;

let steps: Vec<_> = self.chosen_solvables().collect();

tracing::trace!("Solvables found:");
for step in &steps {
tracing::trace!(
" - {}",
InternalSolvableId::from(*step).display(self.provider())
);
}

Ok(steps)
}

/// Solves for the provided `root_requirements` and `root_constraints`, along with
/// a set of additional (optional) solvables.
///
/// The `root_requirements` are packages that must be included in the
/// solution. `root_constraints` are additional constraints applicable to
/// individual packages that the solvable (if any) chosen for that package
/// must adhere to.
/// 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 additional solvables as it can.
/// Each additional solvable is subject to all the clauses and decisions introduced
/// 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 additional solvable is _not_ subject to the
/// 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 [`UnsolvableOrCancelled::Unsolvable`] only if the _root_ requirements and
/// constraints could not be solved for; if an additional solvable is unsolvable, it is
/// simply not included in the solution.
pub fn solve_with_additional(
&mut self,
root_requirements: Vec<VersionSetId>,
root_constraints: Vec<VersionSetId>,
additional_solvables: impl IntoIterator<Item = SolvableId>,
) -> Result<impl Iterator<Item = SolvableId> + '_, UnsolvableOrCancelled> {
self.solve_for_root(root_requirements, root_constraints)?;
/// # Returns
///
/// 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 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) -> Result<Vec<SolvableId>, UnsolvableOrCancelled> {
self.decision_tracker.clear();
self.negative_assertions.clear();
self.learnt_clauses.clear();
self.learnt_why = Mapping::new();
self.clauses = Default::default();
self.root_requirements = problem.requirements;
self.root_constraints = problem.constraints;

for additional in additional_solvables.into_iter() {
// The first clause will always be the install root clause. Here we verify that
// this is indeed the case.
let root_clause = self.clauses.borrow_mut().alloc(ClauseState::root());
assert_eq!(root_clause, ClauseId::install_root());

assert!(
self.run_sat(InternalSolvableId::root())?,
"bug: Since root is the first requested solvable, \
should have returned Err instead of Ok(false) if root is unsolvable"
);

for additional in problem.soft_requirements {
let additional = additional.into();

if self.decision_tracker.assigned_value(additional).is_none() {
self.run_sat(additional)?;
}
}

Ok(self.chosen_solvables())
Ok(self.chosen_solvables().collect())
}

/// Returns the solvables that the solver has chosen to include in the solution so far.
Expand All @@ -239,34 +244,6 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
})
}

fn solve_for_root(
&mut self,
root_requirements: Vec<VersionSetId>,
root_constraints: Vec<VersionSetId>,
) -> Result<(), UnsolvableOrCancelled> {
// Clear state
self.decision_tracker.clear();
self.negative_assertions.clear();
self.learnt_clauses.clear();
self.learnt_why = Mapping::new();
self.clauses = Default::default();
self.root_requirements = root_requirements;
self.root_constraints = root_constraints;

// The first clause will always be the install root clause. Here we verify that
// this is indeed the case.
let root_clause = self.clauses.borrow_mut().alloc(ClauseState::root());
assert_eq!(root_clause, ClauseId::install_root());

assert!(
self.run_sat(InternalSolvableId::root())?,
"bug: Since root is the first requested solvable, \
should have returned Err instead of Ok(false) if root is unsolvable"
);

Ok(())
}

/// Adds clauses for a solvable. These clauses include requirements and
/// constrains on other solvables.
///
Expand Down
Loading

0 comments on commit f3f886d

Please sign in to comment.