Skip to content

Commit

Permalink
Merge remote-tracking branch 'upstream/main' into feat/decide_explici…
Browse files Browse the repository at this point in the history
…t_first
  • Loading branch information
baszalmstra committed Aug 13, 2024
2 parents 51e0cc6 + 2700ea0 commit db73dec
Show file tree
Hide file tree
Showing 8 changed files with 231 additions and 105 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
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -25,3 +25,4 @@ output/

# Any resolvo snapshots in the root
snapshot-*.json
snapshot_*.json
48 changes: 26 additions & 22 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 @@ -490,26 +490,30 @@ pub extern "C" fn resolvo_solve(
) -> bool {
let mut solver = resolvo::Solver::new(provider);

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(),
};
let problem = resolvo::Problem::new()
.requirements(
problem
.requirements
.iter()
.copied()
.map(Into::into)
.collect(),
)
.constraints(
problem
.constraints
.iter()
.copied()
.map(Into::into)

Check warning on line 507 in cpp/src/lib.rs

View workflow job for this annotation

GitHub Actions / Format and Lint

Diff in /home/runner/work/resolvo/resolvo/cpp/src/lib.rs
.collect(),
)
.soft_requirements(
problem
.soft_requirements
.iter()
.copied()
.map(Into::into),
);

match solver.solve(problem) {
Ok(solution) => {
Expand Down
85 changes: 74 additions & 11 deletions src/solver/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -37,17 +37,63 @@ struct AddClauseOutput {
}

/// 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>,
///
/// 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.
pub struct Problem<S> {
requirements: Vec<Requirement>,
constraints: Vec<VersionSetId>,
soft_requirements: S,
}

impl Default for Problem<std::iter::Empty<SolvableId>> {
fn default() -> Self {
Self::new()
}
}

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.
pub fn new() -> Self {
Self {
requirements: Default::default(),
constraints: Default::default(),
soft_requirements: Default::default(),
}
}
}

impl<S: IntoIterator<Item = SolvableId>> Problem<S> {
/// 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`].
pub fn requirements(self, requirements: Vec<Requirement>) -> Self {
Self {
requirements,
..self
}
}

/// Additional constraints imposed on individual packages that the solvable
/// (if any) chosen for that package _must_ adhere to.
pub constraints: Vec<VersionSetId>,
/// 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`].
pub fn constraints(self, constraints: Vec<VersionSetId>) -> Self {
Self {
constraints,
..self
}
}

/// A set of additional requirements that the solver should _try_ and
/// 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
Expand All @@ -57,7 +103,21 @@ pub struct Problem {
/// 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>,
///
/// # Returns
///
/// Returns the [`Problem`] for further mutation or to pass to
/// [`Solver::solve`].
pub fn soft_requirements<I: IntoIterator<Item = SolvableId>>(
self,
soft_requirements: I,
) -> Problem<I> {
Problem {
requirements: self.requirements,
constraints: self.constraints,
soft_requirements,
}
}
}

/// Drives the SAT solving process.
Expand Down Expand Up @@ -209,7 +269,10 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
/// 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> {
pub fn solve(
&mut self,
problem: Problem<impl IntoIterator<Item = SolvableId>>,
) -> Result<Vec<SolvableId>, UnsolvableOrCancelled> {
self.decision_tracker.clear();
self.negative_assertions.clear();
self.learnt_clauses.clear();
Expand Down
Loading

0 comments on commit db73dec

Please sign in to comment.