pubsat 0.1.0

//! Top-level resolver.
//!
//! [`DependencyResolver`] orchestrates the full pipeline:
//! [`DependencyGraph`] → primed [`ConstraintEncoder`] →
//! [`crate::sat::SatProblem`] → [`crate::sat::SatSolver`] →
//! [`Resolution`].
//!
//! ## Version preferences via greedy SAT assumptions
//!
//! A pure SAT model is "some satisfying assignment"; among
//! versions that satisfy a `Dependency` constraint, the solver's
//! pick is arbitrary. The resolver layers a *preference* on top:
//! every non-root package gets a positive-literal assumption
//! pinning its newest available version. The "all preferences at
//! once" solve is the fast path (most graphs solve cleanly that
//! way). On UNSAT, the resolver greedily adds preferences one at
//! a time, keeping each only if the cumulative problem stays SAT
//! — a maximal compatible subset rather than an all-or-nothing
//! fallback.
//!
//! See [`ConstraintEncoder`] module docs for the cache-priming hot
//! path the resolver depends on for performance.

use std::collections::{HashMap, HashSet};
use std::sync::Arc;
use std::time::Duration;

use semver::Version;

use crate::constraint::Constraint;
use crate::encoding::ConstraintEncoder;
use crate::error::{ResolutionError, ResolutionResult};
use crate::graph::{DependencyGraph, DependencyType};
use crate::registry::PackageRegistry;
use crate::sat::{
    Literal, SatProblem, SatSolution, SolverBackend, SolverConfig, create_solver_with_backend,
};

/// Tuning knobs for the resolver. Defaults are reasonable for npm-shaped graphs.
#[derive(Debug, Clone)]
pub struct ResolutionConfig {
    /// Add per-package "pin newest version" SAT assumptions (with
    /// greedy fallback on UNSAT). Disabling this gives faster
    /// resolution but arbitrary version selection.
    pub prefer_newer: bool,
    /// Whether to include `Development` edges from the graph in the
    /// SAT problem.
    pub include_dev: bool,
    /// Whether to include `Optional` edges from the graph in the
    /// SAT problem. Optional deps absent from the graph are
    /// silently skipped regardless.
    pub include_optional: bool,
    /// Per-solve timeout passed through to the SAT backend.
    pub solver_timeout: Duration,
    /// Which SAT backend to use. Defaults to the most-capable
    /// backend whose feature is enabled.
    pub solver_backend: SolverBackend,
}

impl Default for ResolutionConfig {
    fn default() -> Self {
        Self {
            prefer_newer: true,
            include_dev: false,
            include_optional: true,
            solver_timeout: Duration::from_secs(30),
            solver_backend: SolverBackend::default(),
        }
    }
}

/// One package selected by the resolver.
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub struct ResolvedPackage {
    pub name: String,
    pub version: Version,
    /// The kind of dependency edge that brought this package in.
    /// For packages pulled in by multiple edges (e.g., both runtime
    /// and dev), this reports one of them; runtime takes precedence.
    pub dependency_type: DependencyType,
    /// The package that requested this dependency (the source of
    /// the edge in the graph), or `"root"` for top-level requests.
    pub resolved_from: String,
}

/// The output of a successful resolution.
#[derive(Debug, Clone)]
pub struct Resolution {
    /// Selected packages, sorted by name.
    pub packages: Vec<ResolvedPackage>,
    pub resolution_time: Duration,
    pub variables_count: u32,
    pub clauses_count: usize,
}

/// Per-attempt state. Created once per `DependencyResolver::resolve`
/// call; not reused across attempts.
struct ResolutionContext<R: PackageRegistry> {
    graph: DependencyGraph,
    registry: Arc<R>,
    config: ResolutionConfig,
    version_cache: HashMap<String, Vec<Version>>,
}

impl<R: PackageRegistry> ResolutionContext<R> {
    fn new(graph: DependencyGraph, registry: Arc<R>, config: ResolutionConfig) -> Self {
        Self {
            graph,
            registry,
            config,
            version_cache: HashMap::new(),
        }
    }

    async fn resolve(&mut self) -> ResolutionResult<Resolution> {
        let start_time = std::time::Instant::now();

        let packages = self.collect_packages();
        self.populate_version_cache(&packages).await?;
        let problem = self.generate_sat_problem().await?;
        let solution = self.solve_with_preferences(&problem).await?;
        self.extract_resolution(solution, &problem, start_time.elapsed())
    }

    /// Every distinct package name appearing in the graph (subject
    /// to dep-type filtering).
    fn collect_packages(&self) -> HashSet<String> {
        let mut packages = HashSet::new();
        for node_idx in self.graph.all_nodes() {
            let Some(node) = self.graph.node_data(node_idx) else {
                continue;
            };
            packages.insert(node.name.clone());
            for (dep_idx, edge) in self.graph.dependencies(node_idx) {
                let Some(dep_node) = self.graph.node_data(dep_idx) else {
                    continue;
                };
                if self.should_include(edge.dependency_type) {
                    packages.insert(dep_node.name.clone());
                }
            }
        }
        packages
    }

    fn should_include(&self, dep_type: DependencyType) -> bool {
        match dep_type {
            DependencyType::Runtime | DependencyType::Peer => true,
            DependencyType::Development => self.config.include_dev,
            DependencyType::Optional => self.config.include_optional,
        }
    }

    /// Fetch every available version of every involved package and
    /// merge in versions baked into graph nodes themselves (the
    /// synthetic-root case and any caller-pinned nodes).
    async fn populate_version_cache(&mut self, packages: &HashSet<String>) -> ResolutionResult<()> {
        for name in packages {
            if self.version_cache.contains_key(name) {
                continue;
            }
            match self.registry.get_package_versions(name).await {
                Ok(versions) => {
                    self.version_cache.insert(name.clone(), versions);
                }
                Err(_) => {
                    // Insert an empty list so we don't refetch a missing
                    // package on every reference, and so node-attached
                    // versions (below) can extend it.
                    self.version_cache.insert(name.clone(), Vec::new());
                }
            }
        }

        // Merge in versions baked into graph nodes themselves —
        // covers the synthetic root the caller assembled and any
        // local-only or non-registry packages. Without this, the SAT
        // problem can silently drop entire constraint chains
        // originating at a node the registry doesn't know about.
        for node_idx in self.graph.all_nodes() {
            if let Some(node) = self.graph.node_data(node_idx) {
                if let Some(version) = &node.version {
                    let entry = self.version_cache.entry(node.name.clone()).or_default();
                    if !entry.contains(version) {
                        entry.push(version.clone());
                    }
                }
            }
        }

        Ok(())
    }

    async fn generate_sat_problem(&mut self) -> ResolutionResult<SatProblem> {
        let mut encoder = ConstraintEncoder::new(self.registry.clone());
        encoder.set_local_versions(self.version_cache.clone());

        // Pre-allocate variables in sorted order so variable
        // numbering is stable across runs (Varisat's branching
        // depends on it; without sorting, identical inputs resolve
        // differently between runs).
        let mut sorted_names: Vec<&String> = self.version_cache.keys().collect();
        sorted_names.sort();
        for name in sorted_names {
            if let Some(versions) = self.version_cache.get(name) {
                for version in versions {
                    encoder
                        .variables_mut()
                        .get_or_create_variable(name, version);
                }
            }
        }

        self.encode_root_constraints(&mut encoder).await?;
        self.encode_dependency_constraints(&mut encoder).await?;
        self.encode_version_conflicts(&mut encoder).await?;

        Ok(encoder.build_problem())
    }

    /// For every package the graph references, require at least one
    /// of its known versions to be selected. Combined with the
    /// at-most-one constraints, this means "exactly one version".
    async fn encode_root_constraints(
        &self,
        encoder: &mut ConstraintEncoder<R>,
    ) -> ResolutionResult<()> {
        let mut names: Vec<&String> = self.version_cache.keys().collect();
        names.sort();
        for name in names {
            if let Some(versions) = self.version_cache.get(name) {
                if !versions.is_empty() {
                    encoder
                        .encode_constraint(&Constraint::AtLeastOne {
                            package: name.clone(),
                            versions: versions.clone(),
                        })
                        .await
                        .map_err(|e| ResolutionError::simple_conflict(e.to_string()))?;
                }
            }
        }
        Ok(())
    }

    /// For every (parent, dep_edge, dep_target) tuple in the graph,
    /// emit a `Dependency` constraint that says "if any version of
    /// parent is selected, some satisfying version of dep_target
    /// must also be selected". The encoder lowers this into one
    /// clause per parent-version × possible-dep-version pair.
    async fn encode_dependency_constraints(
        &self,
        encoder: &mut ConstraintEncoder<R>,
    ) -> ResolutionResult<()> {
        for node_idx in self.graph.all_nodes() {
            let Some(node) = self.graph.node_data(node_idx) else {
                continue;
            };
            let parent_name = &node.name;
            let Some(parent_versions) = self.version_cache.get(parent_name) else {
                continue;
            };

            for version in parent_versions {
                for (dep_idx, edge) in self.graph.dependencies(node_idx) {
                    if !self.should_include(edge.dependency_type) {
                        continue;
                    }
                    let Some(dep_node) = self.graph.node_data(dep_idx) else {
                        continue;
                    };
                    let constraint = Constraint::Dependency {
                        package: dep_node.name.clone(),
                        version_set: edge.version_set.clone(),
                        dependent: Some(format!("{}@{}", parent_name, version)),
                    };
                    encoder
                        .encode_constraint(&constraint)
                        .await
                        .map_err(|e| ResolutionError::simple_conflict(e.to_string()))?;
                }
            }
        }
        Ok(())
    }

    /// Emit `AtMostOne` for every package with more than one
    /// candidate version. Sorted order so clause ordering is stable
    /// across runs.
    async fn encode_version_conflicts(
        &self,
        encoder: &mut ConstraintEncoder<R>,
    ) -> ResolutionResult<()> {
        let mut sorted: Vec<(&String, &Vec<Version>)> = self.version_cache.iter().collect();
        sorted.sort_by(|a, b| a.0.cmp(b.0));
        for (name, versions) in sorted {
            if versions.len() > 1 {
                encoder
                    .encode_constraint(&Constraint::AtMostOne {
                        package: name.clone(),
                        versions: versions.clone(),
                    })
                    .await
                    .map_err(|e| ResolutionError::simple_conflict(e.to_string()))?;
            }
        }
        Ok(())
    }

    /// Build the per-package "pin newest version" preference
    /// assumptions. Roots (nodes with no incoming edges) are
    /// excluded because they're constraint-providers, not
    /// installables — they're not the subject of preference.
    fn build_newest_version_preferences(
        &self,
        encoder_variables: &crate::encoding::VariableEncoder,
    ) -> Vec<Literal> {
        let root_names: HashSet<String> = self
            .graph
            .all_nodes()
            .iter()
            .filter(|idx| self.graph.dependents(**idx).is_empty())
            .filter_map(|idx| self.graph.node_data(*idx).map(|n| n.name.clone()))
            .collect();

        let mut packages: Vec<&String> = self.version_cache.keys().collect();
        packages.sort();

        let mut prefs = Vec::new();
        for package in packages {
            if root_names.contains(package) {
                continue;
            }
            let versions = match self.version_cache.get(package) {
                Some(v) if !v.is_empty() => v,
                _ => continue,
            };
            // version_cache is sorted newest-first (by the registry).
            let newest = &versions[0];
            if let Some(var) = encoder_variables.get_variable(package, newest) {
                prefs.push(Literal::positive(var));
            }
        }
        prefs
    }

    async fn solve_with_preferences(&self, base: &SatProblem) -> ResolutionResult<SatSolution> {
        if !self.config.prefer_newer {
            return self.solve_sat_problem(base).await;
        }

        // We need the variable encoder to map preferences to literals
        // — re-derive a tiny one from the problem's variable_names map.
        let var_encoder = encoder_variables_from_problem(base);
        let prefs = self.build_newest_version_preferences(&var_encoder);

        // Fast path: all preferences at once.
        let mut all_prefs = base.clone();
        for p in &prefs {
            all_prefs.add_assumption(*p);
        }
        match self.solve_sat_problem(&all_prefs).await {
            Ok(SatSolution::Satisfiable(model)) => {
                return Ok(SatSolution::Satisfiable(model));
            }
            Ok(SatSolution::Unknown) => {
                return Err(ResolutionError::simple_conflict(
                    "SAT solver could not determine satisfiability within time limit".to_string(),
                ));
            }
            // UNSAT or error → greedy.
            _ => {}
        }

        // Greedy: build a maximal compatible subset of preferences.
        let mut accepted: Vec<Literal> = Vec::with_capacity(prefs.len());
        for pref in &prefs {
            let mut candidate = base.clone();
            for a in &accepted {
                candidate.add_assumption(*a);
            }
            candidate.add_assumption(*pref);
            if matches!(
                self.solve_sat_problem(&candidate).await,
                Ok(SatSolution::Satisfiable(_))
            ) {
                accepted.push(*pref);
            }
        }

        let mut final_problem = base.clone();
        for a in &accepted {
            final_problem.add_assumption(*a);
        }
        match self.solve_sat_problem(&final_problem).await? {
            sol @ SatSolution::Satisfiable(_) => Ok(sol),
            // Defensive: the accepted set was just verified satisfiable,
            // so re-solving with it should succeed. If it doesn't, fall
            // back to a no-preferences solve.
            _ => self.solve_sat_problem(base).await,
        }
    }

    async fn solve_sat_problem(&self, problem: &SatProblem) -> ResolutionResult<SatSolution> {
        let mut solver = create_solver_with_backend(
            self.config.solver_backend,
            SolverConfig {
                timeout: self.config.solver_timeout,
                ..Default::default()
            },
        )
        .await
        .map_err(|e| ResolutionError::simple_conflict(e.to_string()))?;

        let solution = solver
            .solve(problem)
            .await
            .map_err(|e| ResolutionError::simple_conflict(e.to_string()))?;

        match &solution {
            SatSolution::Satisfiable(_) => Ok(solution),
            SatSolution::Unsatisfiable => Err(ResolutionError::simple_conflict(
                "No valid package resolution exists — constraints are contradictory".to_string(),
            )),
            SatSolution::Unknown => Err(ResolutionError::simple_conflict(
                "SAT solver could not determine satisfiability within time limit".to_string(),
            )),
        }
    }

    fn extract_resolution(
        &self,
        solution: SatSolution,
        problem: &SatProblem,
        elapsed: Duration,
    ) -> ResolutionResult<Resolution> {
        let SatSolution::Satisfiable(model) = solution else {
            return Err(ResolutionError::simple_conflict(
                "extract_resolution called on non-satisfiable solution".to_string(),
            ));
        };

        // Root packages (no incoming edges) are constraint-providers,
        // not installables — they're in the SAT problem so their own
        // dependency edges get encoded, but they shouldn't appear in
        // the output.
        let root_package_names: HashSet<String> = self
            .graph
            .all_nodes()
            .iter()
            .filter(|idx| self.graph.dependents(**idx).is_empty())
            .filter_map(|idx| self.graph.node_data(*idx).map(|n| n.name.clone()))
            .collect();

        let mut resolved_packages = Vec::new();
        for var in 1..=problem.num_variables {
            if model.get(var) != Some(true) {
                continue;
            }
            let Some(name) = problem.get_variable_name(var) else {
                // Auxiliary variable (no name attached); skip.
                continue;
            };
            // Split on the last '@' so scoped packages (@scope/pkg@1.2.3) work.
            let Some(at_idx) = name.rfind('@') else {
                continue;
            };
            let (pkg, ver_str) = (&name[..at_idx], &name[at_idx + 1..]);
            if root_package_names.contains(pkg) {
                continue;
            }
            let Ok(version) = Version::parse(ver_str) else {
                continue;
            };

            let (dependency_type, resolved_from) = self.determine_package_source(pkg);
            resolved_packages.push(ResolvedPackage {
                name: pkg.to_string(),
                version,
                dependency_type,
                resolved_from,
            });
        }

        resolved_packages.sort_by(|a, b| a.name.cmp(&b.name));
        resolved_packages.dedup_by(|a, b| a.name == b.name && a.version == b.version);

        Ok(Resolution {
            packages: resolved_packages,
            resolution_time: elapsed,
            variables_count: problem.num_variables,
            clauses_count: problem.clauses.len(),
        })
    }

    /// Identify which incoming edge brought a package in. Runtime
    /// edges take precedence over peer / dev / optional if a package
    /// is pulled in via multiple edge types.
    fn determine_package_source(&self, package_name: &str) -> (DependencyType, String) {
        let mut best: Option<(DependencyType, String)> = None;
        for node_idx in self.graph.all_nodes() {
            let Some(node) = self.graph.node_data(node_idx) else {
                continue;
            };
            for (dep_idx, edge) in self.graph.dependencies(node_idx) {
                let Some(dep_node) = self.graph.node_data(dep_idx) else {
                    continue;
                };
                if dep_node.name != package_name {
                    continue;
                }
                let candidate = (edge.dependency_type, node.name.clone());
                best = Some(match best.take() {
                    None => candidate,
                    Some(prev) => prefer_runtime(prev, candidate),
                });
            }
        }
        best.unwrap_or((DependencyType::Runtime, "root".to_string()))
    }
}

/// Pick the more "load-bearing" edge type between two candidates:
/// Runtime > Peer > Optional > Development. Used to surface the
/// most relevant edge when a package is pulled in via several.
fn prefer_runtime(
    a: (DependencyType, String),
    b: (DependencyType, String),
) -> (DependencyType, String) {
    let rank = |t: DependencyType| match t {
        DependencyType::Runtime => 0,
        DependencyType::Peer => 1,
        DependencyType::Optional => 2,
        DependencyType::Development => 3,
    };
    if rank(a.0) <= rank(b.0) { a } else { b }
}

/// Reconstruct a `VariableEncoder`-equivalent lookup table from a
/// finalized `SatProblem`'s variable_names map. Lets the preference
/// builder map `(package, version)` back to a SAT variable without
/// holding on to the original encoder.
fn encoder_variables_from_problem(problem: &SatProblem) -> crate::encoding::VariableEncoder {
    let mut encoder = crate::encoding::VariableEncoder::new();
    let mut entries: Vec<(u32, &String)> = problem
        .metadata
        .variable_names
        .iter()
        .map(|(v, n)| (*v, n))
        .collect();
    entries.sort_by_key(|(v, _)| *v);
    for (_var, name) in entries {
        let Some(at_idx) = name.rfind('@') else {
            continue;
        };
        let (pkg, ver_str) = (&name[..at_idx], &name[at_idx + 1..]);
        if let Ok(version) = Version::parse(ver_str) {
            encoder.get_or_create_variable(pkg, &version);
        }
    }
    encoder
}

/// Public top-level resolver. Holds the registry and config so
/// `resolve` is callable repeatedly against the same registry,
/// each call creating its own per-attempt resolution state.
pub struct DependencyResolver<R: PackageRegistry> {
    registry: Arc<R>,
    config: ResolutionConfig,
}

impl<R: PackageRegistry + 'static> DependencyResolver<R> {
    pub fn new(registry: Arc<R>) -> Self {
        Self {
            registry,
            config: ResolutionConfig::default(),
        }
    }

    pub fn with_config(registry: Arc<R>, config: ResolutionConfig) -> Self {
        Self { registry, config }
    }

    pub fn config(&self) -> &ResolutionConfig {
        &self.config
    }

    /// Resolve a graph into a concrete selection of packages.
    /// Returns `Err` if no satisfying assignment exists or if the
    /// SAT backend errors / times out.
    pub async fn resolve(&self, graph: DependencyGraph) -> ResolutionResult<Resolution> {
        let mut ctx = ResolutionContext::new(graph, self.registry.clone(), self.config.clone());
        ctx.resolve().await
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::builder::DependencyGraphBuilder;
    use crate::registry::{MockRegistry, VersionMetadata};
    use crate::version::VersionSet;

    fn vs(s: &str) -> VersionSet {
        s.parse().unwrap()
    }

    fn root_with_deps<'a>(deps: &[(&'a str, &'a str)]) -> VersionMetadata {
        let mut root = VersionMetadata::new("root", Version::new(1, 0, 0));
        for (name, set) in deps {
            root.dependencies.insert(name.to_string(), vs(set));
        }
        root
    }

    async fn build_and_resolve<R: PackageRegistry + 'static>(
        registry: Arc<R>,
        root: VersionMetadata,
    ) -> ResolutionResult<Resolution> {
        let mut builder = DependencyGraphBuilder::new(registry.clone());
        let graph = builder.build(root).await?;
        DependencyResolver::new(registry).resolve(graph).await
    }

    #[tokio::test]
    async fn resolve_single_dependency_picks_newest_compatible() {
        let registry =
            Arc::new(MockRegistry::new().with_versions("dep", &["1.0.0", "1.5.0", "2.0.0"]));
        let root = root_with_deps(&[("dep", "^1.0.0")]);
        let resolution = build_and_resolve(registry, root).await.unwrap();

        assert_eq!(resolution.packages.len(), 1);
        let pkg = &resolution.packages[0];
        assert_eq!(pkg.name, "dep");
        assert_eq!(
            pkg.version,
            Version::new(1, 5, 0),
            "should pick newest in ^1.0.0 (1.5.0, not 2.0.0)",
        );
    }

    #[tokio::test]
    async fn resolve_handles_diamond_dependency() {
        // root → a → c
        // root → b → c   (both want ^1.0.0; one c@1.5.0 satisfies both)
        let registry = Arc::new(
            MockRegistry::new()
                .with_versions("a", &["1.0.0"])
                .with_versions("b", &["1.0.0"])
                .with_versions("c", &["1.0.0", "1.5.0"])
                .with_dependency("a", "1.0.0", "c", vs("^1.0.0"))
                .with_dependency("b", "1.0.0", "c", vs("^1.0.0")),
        );
        let root = root_with_deps(&[("a", "^1.0.0"), ("b", "^1.0.0")]);
        let resolution = build_and_resolve(registry, root).await.unwrap();

        let by_name: HashMap<_, _> = resolution
            .packages
            .iter()
            .map(|p| (p.name.as_str(), &p.version))
            .collect();
        assert_eq!(by_name.len(), 3);
        assert_eq!(by_name.get("c"), Some(&&Version::new(1, 5, 0)));
    }

    #[tokio::test]
    async fn resolve_falls_back_when_newest_creates_conflict() {
        // root → a@^1, root → b@^1
        // a@1.0.0 needs c@1.0.0 exactly
        // b@1.0.0 needs c@1.0.0 exactly
        // Newest c is 2.0.0; greedy fallback must drop that preference.
        let registry = Arc::new(
            MockRegistry::new()
                .with_versions("a", &["1.0.0"])
                .with_versions("b", &["1.0.0"])
                .with_versions("c", &["1.0.0", "2.0.0"])
                .with_dependency("a", "1.0.0", "c", vs("=1.0.0"))
                .with_dependency("b", "1.0.0", "c", vs("=1.0.0")),
        );
        let root = root_with_deps(&[("a", "^1.0.0"), ("b", "^1.0.0")]);
        let resolution = build_and_resolve(registry, root).await.unwrap();

        let c = resolution
            .packages
            .iter()
            .find(|p| p.name == "c")
            .expect("c should be present");
        assert_eq!(
            c.version,
            Version::new(1, 0, 0),
            "greedy fallback should drop the newest-c preference"
        );
    }

    #[tokio::test]
    async fn resolve_returns_unsatisfiable_for_contradictory_constraints() {
        // root needs a@=1.0.0 AND a@=2.0.0 — impossible.
        let registry = Arc::new(MockRegistry::new().with_versions("a", &["1.0.0", "2.0.0"]));
        let mut root = VersionMetadata::new("root", Version::new(1, 0, 0));
        // Two different dependency edges to the same package with
        // contradictory constraints. We can't actually put both in
        // a BTreeMap (same key), so we go via the graph directly.
        root.dependencies.insert("a".into(), vs("=1.0.0"));

        let mut builder = DependencyGraphBuilder::new(registry.clone());
        let mut graph = builder.build(root).await.unwrap();

        let root_idx = graph.get_node("root").unwrap();
        let a_idx = graph.get_node("a").unwrap();
        graph.add_edge(
            root_idx,
            a_idx,
            crate::graph::DependencyEdge::new(DependencyType::Runtime, vs("=2.0.0")),
        );

        let err = DependencyResolver::new(registry)
            .resolve(graph)
            .await
            .unwrap_err();
        assert!(
            err.to_string().contains("No valid package resolution")
                || err.to_string().contains("contradictory"),
            "expected UNSAT-style error, got {}",
            err,
        );
    }

    #[tokio::test]
    async fn resolve_does_not_include_root_package_in_output() {
        let registry = Arc::new(MockRegistry::new().with_versions("dep", &["1.0.0"]));
        let root = root_with_deps(&[("dep", "^1.0.0")]);
        let resolution = build_and_resolve(registry, root).await.unwrap();
        assert!(
            !resolution.packages.iter().any(|p| p.name == "root"),
            "root package is a constraint provider; it should not appear in the output",
        );
    }
}

#[cfg(test)]
mod proptests {
    //! Property-based tests for [`DependencyResolver`] invariants
    //! on its output.
    //!
    //! Each property generates a small registry + root with deps
    //! engineered to be satisfiable (the constraint always matches
    //! at least one registered version, so resolution succeeds),
    //! resolves it, and asserts an invariant on the output.
    //!
    //! `cases` is dialed down from 256 to 32 — each case runs the
    //! full build + encode + solve pipeline.

    use super::*;
    use crate::builder::DependencyGraphBuilder;
    use crate::registry::{MockRegistry, VersionMetadata};
    use crate::version::VersionSet;
    use proptest::prelude::*;

    /// Generate a "small" version with each axis in 0..5.
    fn small_version() -> impl Strategy<Value = Version> {
        (0u64..5, 0u64..5, 0u64..5).prop_map(|(a, b, c)| Version::new(a, b, c))
    }

    /// A always-satisfiable registry shape:
    ///   - Two packages "dep_a" and "dep_b".
    ///   - Each carries between 1 and 3 versions.
    ///   - At least one version of each is guaranteed in the
    ///     returned `pinned_a` / `pinned_b`, so callers can build a
    ///     root that's guaranteed to resolve.
    fn satisfiable_registry() -> impl Strategy<Value = (Arc<MockRegistry>, Version, Version)> {
        (
            prop::collection::vec(small_version(), 1..=3),
            prop::collection::vec(small_version(), 1..=3),
        )
            .prop_map(|(mut a_versions, mut b_versions)| {
                // Dedupe + sort so we always have at least one of each.
                a_versions.sort();
                a_versions.dedup();
                b_versions.sort();
                b_versions.dedup();

                // Pin the *first* version of each (smallest) as the
                // anchor used to construct satisfiable constraints later.
                let pinned_a = a_versions[0].clone();
                let pinned_b = b_versions[0].clone();

                let a_strs: Vec<String> = a_versions.iter().map(|v| v.to_string()).collect();
                let b_strs: Vec<String> = b_versions.iter().map(|v| v.to_string()).collect();
                let a_refs: Vec<&str> = a_strs.iter().map(|s| s.as_str()).collect();
                let b_refs: Vec<&str> = b_strs.iter().map(|s| s.as_str()).collect();

                let registry = Arc::new(
                    MockRegistry::new()
                        .with_versions("dep_a", &a_refs)
                        .with_versions("dep_b", &b_refs),
                );
                (registry, pinned_a, pinned_b)
            })
    }

    fn block_on<F: std::future::Future<Output = T>, T>(fut: F) -> T {
        tokio::runtime::Builder::new_current_thread()
            .enable_all()
            .build()
            .unwrap()
            .block_on(fut)
    }

    proptest! {
        #![proptest_config(ProptestConfig::with_cases(32))]

        /// The root package is a constraint-provider, not an
        /// installable. It must never appear in
        /// `resolution.packages`.
        #[test]
        fn resolution_excludes_root(
            (registry, pinned_a, pinned_b) in satisfiable_registry(),
        ) {
            // Root depends on both packages with `*` — always satisfiable.
            let root = VersionMetadata::new("my-root", Version::new(1, 0, 0))
                .with_dependency("dep_a", VersionSet::any())
                .with_dependency("dep_b", VersionSet::any());

            let resolution = block_on(async {
                let graph = DependencyGraphBuilder::new(registry.clone())
                    .build(root)
                    .await?;
                DependencyResolver::new(registry).resolve(graph).await
            }).map_err(|e| TestCaseError::fail(format!("resolution failed: {}", e)))?;

            prop_assert!(
                !resolution.packages.iter().any(|p| p.name == "my-root"),
                "root must not appear in resolution; got {:?}",
                resolution.packages,
            );
            // Use pinned anchors to silence unused-variable lints
            // and document that they were generated.
            let _ = (pinned_a, pinned_b);
        }

        /// At most one version per package in the output. This is
        /// the central invariant the SAT encoding enforces via the
        /// per-package `AtMostOne` clauses.
        #[test]
        fn resolution_has_unique_versions_per_package(
            (registry, _pinned_a, _pinned_b) in satisfiable_registry(),
        ) {
            let root = VersionMetadata::new("my-root", Version::new(1, 0, 0))
                .with_dependency("dep_a", VersionSet::any())
                .with_dependency("dep_b", VersionSet::any());

            let resolution = block_on(async {
                let graph = DependencyGraphBuilder::new(registry.clone())
                    .build(root)
                    .await?;
                DependencyResolver::new(registry).resolve(graph).await
            }).map_err(|e| TestCaseError::fail(format!("resolution failed: {}", e)))?;

            let mut names = std::collections::HashMap::<String, Version>::new();
            for pkg in &resolution.packages {
                if let Some(existing) = names.insert(pkg.name.clone(), pkg.version.clone()) {
                    if existing != pkg.version {
                        return Err(TestCaseError::fail(format!(
                            "package {} resolved to both {} and {}",
                            pkg.name, existing, pkg.version,
                        )));
                    }
                }
            }
        }

        /// Every selected `(package, version)` satisfies every
        /// incoming dependency-edge constraint in the original
        /// graph. This is the headline correctness property —
        /// "the resolver respects the constraints it was given."
        #[test]
        fn resolution_satisfies_every_incoming_edge_constraint(
            (registry, pinned_a, pinned_b) in satisfiable_registry(),
        ) {
            // Use `^pinned` for each dep — guaranteed to match
            // pinned itself (and possibly more), so satisfiable.
            let root = VersionMetadata::new("my-root", Version::new(1, 0, 0))
                .with_dependency("dep_a", VersionSet::Caret(pinned_a))
                .with_dependency("dep_b", VersionSet::Caret(pinned_b));

            let (resolution, graph) = block_on(async {
                let graph = DependencyGraphBuilder::new(registry.clone())
                    .build(root)
                    .await?;
                let resolution = DependencyResolver::new(registry)
                    .resolve(graph.clone())
                    .await?;
                Ok::<_, ResolutionError>((resolution, graph))
            }).map_err(|e| TestCaseError::fail(format!("resolution failed: {}", e)))?;

            for pkg in &resolution.packages {
                let Some(node_idx) = graph.get_node(&pkg.name) else {
                    continue;
                };
                // Every edge in the graph pointing AT this package
                // must be satisfied by the selected version.
                for (parent_idx, edge) in graph.dependents(node_idx) {
                    let parent_name = graph
                        .node_data(parent_idx)
                        .map(|n| n.name.clone())
                        .unwrap_or_else(|| "?".into());
                    prop_assert!(
                        edge.version_set.satisfies(&pkg.version),
                        "selected {}@{} fails the edge constraint {} → {} ({})",
                        pkg.name, pkg.version, parent_name, pkg.name, edge.version_set,
                    );
                }
            }
        }

        /// Resolution is deterministic: same registry + root →
        /// same resolution. The encoder sorts HashMap iteration
        /// and the SAT backend is deterministic; this checks the
        /// composition.
        #[test]
        fn resolution_is_deterministic(
            (registry, _pinned_a, _pinned_b) in satisfiable_registry(),
        ) {
            let make_root = || {
                VersionMetadata::new("my-root", Version::new(1, 0, 0))
                    .with_dependency("dep_a", VersionSet::any())
                    .with_dependency("dep_b", VersionSet::any())
            };
            let resolve_once = || {
                block_on(async {
                    let graph = DependencyGraphBuilder::new(registry.clone())
                        .build(make_root())
                        .await?;
                    DependencyResolver::new(registry.clone()).resolve(graph).await
                })
            };
            let first = resolve_once().map_err(|e| {
                TestCaseError::fail(format!("first resolution failed: {}", e))
            })?;
            let second = resolve_once().map_err(|e| {
                TestCaseError::fail(format!("second resolution failed: {}", e))
            })?;

            // Compare the (name, version) pairs as the
            // load-bearing output — resolution_time obviously
            // varies between runs.
            let first_pairs: Vec<(String, Version)> = first
                .packages
                .iter()
                .map(|p| (p.name.clone(), p.version.clone()))
                .collect();
            let second_pairs: Vec<(String, Version)> = second
                .packages
                .iter()
                .map(|p| (p.name.clone(), p.version.clone()))
                .collect();
            prop_assert_eq!(first_pairs, second_pairs);
        }
    }
}