Crate rattler_libsolv_rs
source ·Expand description
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.
Modules
- Types to examine why a problem was unsatisfiable, and to report the causes to the user.
- Ranges are constraints defining sets of versions. They are a convenience struct that implements
crate::VersionSet
for any version type that implementsOrd
+Clone
.
Structs
- A list of candidate solvables for a specific package. This is returned from
DependencyProvider::get_candidates
. - Display merged candidates on single line with
|
as separator. - Holds information about the dependencies of a package.
- The id associated to a package name
- A pool that stores data related to the available packages.
- A solvable represents a single candidate of a package. This is type is generic on
V
which can be supplied by the user. In most cases this is going to be something like a record that contains the version of the package and other metadata. A solvable is always associated with aNameId
, which is an interned name in thePool
. - The id associated to a solvable
- Drives the SAT solving process
- The id associated with a VersionSet.
Traits
- Defines implementation specific behavior for the solver and a way for the solver to access the packages that are available in the system.
- The solver is based around the fact that for for every package name we are trying to find a single variant. Variants are grouped by their respective package name. A package name is anything that we can compare and hash for uniqueness checks.
- Defines how merged candidates should be displayed.
- A
VersionSet
is describes a set of “versions”. The trait defines whether a given version is part of the set or not.