Crate resolvo 

Implements a SAT solver for dependency resolution based on the CDCL algorithm (conflict-driven clause learning)

The CDCL algorithm is masterly explained in An Extensible SAT-solver. Regarding the data structures used, we mostly follow the approach taken by libsolv. The code of libsolv is, however, very low level C, so if you are looking for an introduction to CDCL, you are encouraged to look at the paper instead or to keep reading through this codebase and its comments.

Re-exports

pub use id::ConditionId;

pub use id::DenseIndex;

pub use id::NameId;

pub use id::NameTag;

pub use id::SolvableId;

pub use id::SolvableTag;

pub use id::StringId;

pub use id::VariableId;

pub use id::VersionSetId;

pub use id::VersionSetUnionId;

pub use solver_id::DenseId;

pub use solver_id::IdMap;

pub use solver_id::IdSet;

pub use solver_id::SolverId;

pub use solver_id::SparseId;

pub use utils::IndexedSet;

pub use utils::Mapping;

pub use utils::MappingIter;

Modules

conflict

Types to examine why a problem was unsatisfiable, and to report the causes to the user.

id

Public ID types used by dependency providers, snapshots, and diagnostics.

runtime

Solving in resolvo is a compute heavy operation. However, while computing the solver will request additional information from the crate::DependencyProvider and a dependency provider might want to perform multiple requests concurrently. To that end the crate::DependencyProviders methods are async. The implementer can implement the async operations in any way they choose including with any runtime they choose. However, the solver itself is completely single threaded, but it still has to await the calls to the dependency provider. Using the AsyncRuntime allows the caller of the solver to choose how to await the futures.

snapshot

Provides DependencySnapshot, an object that can capture a snapshot of a dependency provider. This can be very useful to abstract over all the ecosystem specific code and provide a serializable object that can later be reused to solve dependencies.

solver_id

ID-keyed storage primitives used by the solver.

utils

Defines several helper functions and structs that make it easier to implement a custom dependency provider.

Structs

Candidates

A list of candidate solvables for a specific package. This is returned from DependencyProvider::get_candidates.

ConditionalRequirement

A ConditionalRequirement is a requirement that is only enforced when a certain condition holds.

EmptySolvables

Empty soft-requirements iterator for a Problem parameterized by an ID type.

KnownDependencies

Holds information about the dependencies of a package when they are known.

Problem

Describes the problem that is to be solved by the solver.

Solver

Drives the SAT solving process.

SolverCache

Keeps a cache of previously computed and/or requested information about solvables and version sets.

Enums

Condition

A condition defines a boolean expression that evaluates to true or false based on whether one or more other requirements are true or false.

Dependencies

Holds information about the dependencies of a package.

HintDependenciesAvailable

Defines for which candidates dependencies are available without the DependencyProvider having to perform extra work, e.g. it’s cheap to request them.

LogicalOperator

A LogicalOperator defines how multiple conditions are compared to each other.

Requirement

Specifies the dependency of a solvable on a set of version sets.

UnsolvableOrCancelled

The root cause of a solver error.

Traits

DependencyProvider

Defines implementation specific behavior for the solver and a way for the solver to access the packages that are available in the system.

Interner

An object that is used by the solver to query certain properties of different internalized objects.