pubsat 0.1.0

//! Lowering [`Constraint`]s to CNF for SAT solving.
//!
//! The encoder maps each `(package, version)` pair to a SAT
//! variable, encodes each [`Constraint`] variant as one or more
//! [`Clause`]s over those variables, and produces a [`SatProblem`]
//! ready for a [`SatSolver`](crate::sat::SatSolver).
//!
//! ## Hot path: prime `local_versions` before encoding
//!
//! Looking up which versions of a package satisfy a
//! [`VersionSet`] is on the encoding hot path. If the encoder has
//! to round-trip to the registry for every `(package, version_set)`
//! pair touched by a `Dependency` or `Implies` constraint, the
//! wall-clock cost dominates everything else: ~7000 redundant
//! fetches on a 68-package transitive closure (~5 minutes), all to
//! ask the registry questions whose answers are already in some
//! other cache somewhere.
//!
//! The fix is to pre-populate a local
//! `package_name -> Vec<Version>` map (typically derived from the
//! resolver's metadata cache) via
//! [`ConstraintEncoder::set_local_versions`] before calling
//! [`ConstraintEncoder::encode_constraint`]. The encoder filters
//! that map in-process and only falls back to the registry when a
//! package is missing — which should be never in the normal
//! resolver flow.

use std::collections::HashMap;
use std::sync::Arc;

use semver::Version;

use crate::constraint::Constraint;
use crate::error::{ResolutionError, ResolutionResult};
use crate::graph::DependencyGraph;
use crate::registry::PackageRegistry;
use crate::sat::{Clause, Literal, SatProblem};
use crate::version::VersionSet;

pub type EncodingResult<T> = ResolutionResult<T>;

/// Parse `"name@version"` (or `"@scope/name@version"`) into its
/// components. Splits on the *last* `@` so scoped packages work.
/// Returns `None` if the input isn't in `name@version` form.
fn parse_pkg_at_version(s: &str) -> Option<(&str, Version)> {
    let idx = s.rfind('@')?;
    if idx == 0 {
        // Pure scoped package without a version, like `@scope/pkg`.
        return None;
    }
    let name = &s[..idx];
    let version = Version::parse(&s[idx + 1..]).ok()?;
    Some((name, version))
}

/// Bookkeeping for the SAT-variable namespace: assigns one variable
/// per `(package, version)` pair, hands out auxiliary variables for
/// the sequential at-most-one encoding, and supports reverse-lookup
/// for human-readable debugging.
#[derive(Debug, Clone, Default)]
pub struct VariableEncoder {
    package_variables: HashMap<(String, Version), u32>,
    variable_packages: HashMap<u32, (String, Version)>,
    package_ranges: HashMap<String, Vec<u32>>,
    next_variable: u32,
}

impl VariableEncoder {
    pub fn new() -> Self {
        Self {
            package_variables: HashMap::new(),
            variable_packages: HashMap::new(),
            package_ranges: HashMap::new(),
            // Variables are 1-indexed per DIMACS convention.
            next_variable: 1,
        }
    }

    /// Return the existing variable for `(package, version)`, or
    /// allocate a fresh one.
    pub fn get_or_create_variable(&mut self, package: &str, version: &Version) -> u32 {
        let key = (package.to_string(), version.clone());
        if let Some(&var) = self.package_variables.get(&key) {
            return var;
        }
        let var = self.next_variable;
        self.next_variable += 1;
        self.package_variables.insert(key.clone(), var);
        self.variable_packages.insert(var, key);
        self.package_ranges
            .entry(package.to_string())
            .or_default()
            .push(var);
        var
    }

    /// Look up the variable for `(package, version)` without
    /// allocating a new one.
    pub fn get_variable(&self, package: &str, version: &Version) -> Option<u32> {
        let key = (package.to_string(), version.clone());
        self.package_variables.get(&key).copied()
    }

    pub fn get_package(&self, variable: u32) -> Option<&(String, Version)> {
        self.variable_packages.get(&variable)
    }

    pub fn get_package_variables(&self, package: &str) -> Vec<u32> {
        self.package_ranges
            .get(package)
            .cloned()
            .unwrap_or_default()
    }

    pub fn num_variables(&self) -> u32 {
        self.next_variable.saturating_sub(1)
    }

    /// Package names that the encoder has seen, in arbitrary order.
    pub fn package_names(&self) -> Vec<String> {
        self.package_ranges.keys().cloned().collect()
    }

    /// Allocate a fresh auxiliary variable that isn't tied to any
    /// `(package, version)` pair. Used by the sequential
    /// at-most-one encoding.
    pub fn allocate_auxiliary(&mut self) -> u32 {
        let var = self.next_variable;
        self.next_variable += 1;
        var
    }
}

/// Encodes [`Constraint`]s as CNF clauses against a
/// [`VariableEncoder`].
///
/// Build with [`ConstraintEncoder::new`], optionally prime the
/// version cache with [`ConstraintEncoder::set_local_versions`],
/// then call [`ConstraintEncoder::encode_constraint`] or
/// [`ConstraintEncoder::encode_from_graph`] to accumulate clauses.
/// [`ConstraintEncoder::build_problem`] consumes the encoder and
/// returns the final [`SatProblem`].
#[derive(Debug)]
pub struct ConstraintEncoder<R> {
    variables: VariableEncoder,
    clauses: Vec<Clause>,
    clause_descriptions: HashMap<usize, String>,
    registry: Arc<R>,
    /// `package_name -> versions` map primed by the caller before
    /// encoding. See the module docs for why.
    local_versions: HashMap<String, Vec<Version>>,
}

impl<R> ConstraintEncoder<R>
where
    R: PackageRegistry,
{
    pub fn new(registry: Arc<R>) -> Self {
        Self {
            variables: VariableEncoder::new(),
            clauses: Vec::new(),
            clause_descriptions: HashMap::new(),
            registry,
            local_versions: HashMap::new(),
        }
    }

    /// Provide a pre-populated `package_name -> versions` map. The
    /// encoder's internal version-resolution path filters this map
    /// in-process rather than calling the registry — see the module
    /// docs for why priming this matters on real graphs.
    pub fn set_local_versions(&mut self, versions: HashMap<String, Vec<Version>>) {
        self.local_versions = versions;
    }

    pub fn variables(&self) -> &VariableEncoder {
        &self.variables
    }

    pub fn variables_mut(&mut self) -> &mut VariableEncoder {
        &mut self.variables
    }

    pub fn clauses(&self) -> &[Clause] {
        &self.clauses
    }

    pub fn clause_descriptions(&self) -> &HashMap<usize, String> {
        &self.clause_descriptions
    }

    /// Encode a single constraint into CNF clauses.
    pub async fn encode_constraint(&mut self, constraint: &Constraint) -> EncodingResult<()> {
        match constraint {
            Constraint::Dependency {
                package,
                version_set,
                dependent,
            } => {
                self.encode_dependency(package, version_set, dependent.as_deref())
                    .await
            }

            Constraint::Conflict {
                package1,
                version1,
                package2,
                version2,
            } => self.encode_conflict(package1, version1, package2, version2),

            Constraint::AtMostOne { package, versions } => {
                self.encode_at_most_one(package, versions)
            }

            Constraint::AtLeastOne { package, versions } => {
                self.encode_at_least_one(package, versions)
            }

            Constraint::Exactly { package, version } => self.encode_exactly(package, version),

            Constraint::Exclude { package, version } => self.encode_exclude(package, version),

            Constraint::Implies {
                premise_package,
                premise_version,
                conclusion_package,
                conclusion_version_set,
            } => {
                self.encode_implies(
                    premise_package,
                    premise_version,
                    conclusion_package,
                    conclusion_version_set,
                )
                .await
            }

            Constraint::OptionalDependency {
                package,
                version_set,
                dependent,
                condition: _,
            } => {
                // Optional dependencies are soft: if no satisfying
                // versions exist, silently emit no clauses (so UNSAT
                // never gets blamed on a missing optional dep).
                self.encode_optional_dependency(package, version_set, dependent.as_deref())
                    .await
            }

            Constraint::ConditionalDependency {
                package,
                version_set,
                dependent,
                condition: _,
            } => {
                // Per the constraint module docs, the caller is
                // responsible for deciding whether a conditional dep
                // is active and emitting (or omitting) the constraint
                // accordingly. By the time we see one, treat it as a
                // regular dependency.
                self.encode_dependency(package, version_set, dependent.as_deref())
                    .await
            }
        }
    }

    /// Encode a batch of constraints, short-circuiting on the first
    /// hard failure.
    pub async fn encode_constraints(&mut self, constraints: &[Constraint]) -> EncodingResult<()> {
        for constraint in constraints {
            self.encode_constraint(constraint).await?;
        }
        Ok(())
    }

    /// Encode a graph: emit a `Dependency` constraint for each edge,
    /// and ensure every node with a known version has a SAT variable
    /// reserved. Optional edges are encoded as
    /// [`Constraint::OptionalDependency`].
    pub async fn encode_from_graph(&mut self, graph: &DependencyGraph) -> EncodingResult<()> {
        use crate::graph::DependencyType;

        // Allocate a variable for each node with a pinned version.
        // Unpinned nodes get their variables allocated lazily when
        // an edge mentioning them is encoded.
        for node_index in graph.all_nodes() {
            if let Some(node) = graph.node_data(node_index) {
                if let Some(version) = &node.version {
                    self.variables.get_or_create_variable(&node.name, version);
                }
            }
        }

        for node_index in graph.all_nodes() {
            let dependent_name = graph.node_data(node_index).map(|n| n.name.clone());

            for (dep_index, edge) in graph.dependencies(node_index) {
                let Some(dep_node) = graph.node_data(dep_index) else {
                    continue;
                };

                let constraint =
                    if edge.optional || edge.dependency_type == DependencyType::Optional {
                        Constraint::OptionalDependency {
                            package: dep_node.name.clone(),
                            version_set: edge.version_set.clone(),
                            dependent: dependent_name.clone(),
                            condition: None,
                        }
                    } else {
                        Constraint::Dependency {
                            package: dep_node.name.clone(),
                            version_set: edge.version_set.clone(),
                            dependent: dependent_name.clone(),
                        }
                    };

                self.encode_constraint(&constraint).await?;
            }
        }

        Ok(())
    }

    /// Consume the encoder and produce a finalized [`SatProblem`].
    ///
    /// Adds per-package "at-most-one" constraints in the process —
    /// every package that has 2+ candidate versions gets a clause
    /// forbidding the solver from picking two of them at once.
    pub fn build_problem(mut self) -> SatProblem {
        // Sort package names so the at-most-one clauses are emitted
        // in a deterministic order — this keeps the SAT variable
        // allocation order stable across runs.
        let mut packages = self.variables.package_names();
        packages.sort();
        for package in packages {
            let vars = self.variables.get_package_variables(&package);
            if vars.len() > 1 {
                let description = format!("at-most-one for {}", package);
                let _ = self.encode_at_most_one_variables(&vars, &description);
            }
        }

        let mut problem = SatProblem::new(self.variables.num_variables());
        problem.add_clauses(self.clauses);

        // Stamp variables with human-readable names so SAT diagnostics
        // and conflict reports can speak in `name@version` rather than
        // numbered literals.
        for (var, (package, version)) in &self.variables.variable_packages {
            problem.set_variable_name(*var, format!("{}@{}", package, version));
        }

        problem.metadata.description = "Dependency resolution SAT problem".to_string();
        problem
    }

    async fn encode_dependency(
        &mut self,
        package: &str,
        version_set: &VersionSet,
        dependent: Option<&str>,
    ) -> EncodingResult<()> {
        let satisfied_versions = self.get_versions_for_set(package, version_set).await?;

        if satisfied_versions.is_empty() {
            return Err(ResolutionError::no_matching_versions(
                package.to_string(),
                version_set.clone(),
            ));
        }

        let literals: Vec<Literal> = satisfied_versions
            .iter()
            .map(|version| {
                Literal::positive(self.variables.get_or_create_variable(package, version))
            })
            .collect();

        if let Some(dep_pkg) = dependent {
            // `dependent` may be either a bare name (emit one clause
            // per version of the dependent) or `"name@version"`
            // (emit one clause for the exact version). The
            // version-specific form is what `encode_from_graph` emits
            // and is what the resolver typically wants.
            let dep_vars = parse_pkg_at_version(dep_pkg)
                .and_then(|(name, version)| {
                    self.variables.get_variable(name, &version).map(|v| vec![v])
                })
                .unwrap_or_else(|| self.variables.get_package_variables(dep_pkg));

            for dep_var in dep_vars {
                let mut clause_literals = vec![Literal::negative(dep_var)];
                clause_literals.extend(literals.iter().copied());

                let clause = Clause::new(clause_literals);
                let description = format!(
                    "{}@{:?} requires {} ({})",
                    dep_pkg,
                    self.variables.get_package(dep_var).map(|(_, v)| v),
                    package,
                    version_set,
                );
                self.add_clause_with_description(clause, description);
            }
        } else {
            // Root dependency: just require at least one satisfying
            // version of `package`.
            let clause = Clause::new(literals);
            let description = format!("require {} ({})", package, version_set);
            self.add_clause_with_description(clause, description);
        }

        Ok(())
    }

    async fn encode_optional_dependency(
        &mut self,
        package: &str,
        version_set: &VersionSet,
        dependent: Option<&str>,
    ) -> EncodingResult<()> {
        // Soft semantics: if no satisfying versions are reachable,
        // silently emit no clauses. UNSAT must not be triggerable by
        // an optional dep.
        let satisfied_versions = match self.get_versions_for_set(package, version_set).await {
            Ok(v) if !v.is_empty() => v,
            _ => return Ok(()),
        };

        let literals: Vec<Literal> = satisfied_versions
            .iter()
            .map(|version| {
                Literal::positive(self.variables.get_or_create_variable(package, version))
            })
            .collect();

        if let Some(dep_pkg) = dependent {
            let dep_vars = parse_pkg_at_version(dep_pkg)
                .and_then(|(name, version)| {
                    self.variables.get_variable(name, &version).map(|v| vec![v])
                })
                .unwrap_or_else(|| self.variables.get_package_variables(dep_pkg));

            for dep_var in dep_vars {
                let mut clause_literals = vec![Literal::negative(dep_var)];
                clause_literals.extend(literals.iter().copied());
                let clause = Clause::new(clause_literals);
                let description = format!(
                    "[optional] {}@{:?} optionally requires {} ({})",
                    dep_pkg,
                    self.variables.get_package(dep_var).map(|(_, v)| v),
                    package,
                    version_set,
                );
                self.add_clause_with_description(clause, description);
            }
        } else {
            // Root-level optional dep: variables get allocated above
            // but we deliberately emit no requiring clause.
        }

        Ok(())
    }

    fn encode_conflict(
        &mut self,
        package1: &str,
        version1: &Version,
        package2: &str,
        version2: &Version,
    ) -> EncodingResult<()> {
        let var1 = self.variables.get_or_create_variable(package1, version1);
        let var2 = self.variables.get_or_create_variable(package2, version2);
        let clause = Clause::binary(Literal::negative(var1), Literal::negative(var2));
        let description = format!(
            "conflict: {}@{} vs {}@{}",
            package1, version1, package2, version2
        );
        self.add_clause_with_description(clause, description);
        Ok(())
    }

    fn encode_at_most_one(&mut self, package: &str, versions: &[Version]) -> EncodingResult<()> {
        let variables: Vec<u32> = versions
            .iter()
            .map(|version| self.variables.get_or_create_variable(package, version))
            .collect();
        let description = format!("at-most-one for {} versions: {:?}", package, versions);
        self.encode_at_most_one_variables(&variables, &description)
    }

    fn encode_at_least_one(&mut self, package: &str, versions: &[Version]) -> EncodingResult<()> {
        let literals: Vec<Literal> = versions
            .iter()
            .map(|version| {
                Literal::positive(self.variables.get_or_create_variable(package, version))
            })
            .collect();
        if literals.is_empty() {
            return Err(ResolutionError::no_matching_versions(
                package.to_string(),
                VersionSet::any(),
            ));
        }
        let clause = Clause::new(literals);
        let description = format!("at-least-one for {} versions: {:?}", package, versions);
        self.add_clause_with_description(clause, description);
        Ok(())
    }

    fn encode_exactly(&mut self, package: &str, version: &Version) -> EncodingResult<()> {
        let var = self.variables.get_or_create_variable(package, version);
        let clause = Clause::unit(Literal::positive(var));
        let description = format!("exactly {}@{}", package, version);
        self.add_clause_with_description(clause, description);
        Ok(())
    }

    fn encode_exclude(&mut self, package: &str, version: &Version) -> EncodingResult<()> {
        let var = self.variables.get_or_create_variable(package, version);
        let clause = Clause::unit(Literal::negative(var));
        let description = format!("exclude {}@{}", package, version);
        self.add_clause_with_description(clause, description);
        Ok(())
    }

    async fn encode_implies(
        &mut self,
        premise_package: &str,
        premise_version: &Version,
        conclusion_package: &str,
        conclusion_version_set: &VersionSet,
    ) -> EncodingResult<()> {
        let premise_var = self
            .variables
            .get_or_create_variable(premise_package, premise_version);
        let conclusion_versions = self
            .get_versions_for_set(conclusion_package, conclusion_version_set)
            .await?;

        if conclusion_versions.is_empty() {
            return Err(ResolutionError::no_matching_versions(
                conclusion_package.to_string(),
                conclusion_version_set.clone(),
            ));
        }

        let mut clause_literals = vec![Literal::negative(premise_var)];
        for version in &conclusion_versions {
            let var = self
                .variables
                .get_or_create_variable(conclusion_package, version);
            clause_literals.push(Literal::positive(var));
        }

        let clause = Clause::new(clause_literals);
        let description = format!(
            "{}@{} implies {} ({})",
            premise_package, premise_version, conclusion_package, conclusion_version_set
        );
        self.add_clause_with_description(clause, description);
        Ok(())
    }

    /// Emit an at-most-one cardinality constraint over the given
    /// variables. Uses pairwise encoding (O(n²) clauses) for small
    /// `n ≤ 4` and sequential/ladder encoding (O(n) clauses with
    /// auxiliary variables) for larger `n`. Pairwise explodes
    /// quadratically — a package with 20 candidate versions would
    /// generate 190 binary clauses pairwise but only ~57 sequentially.
    fn encode_at_most_one_variables(
        &mut self,
        variables: &[u32],
        description: &str,
    ) -> EncodingResult<()> {
        if variables.len() <= 1 {
            return Ok(());
        }

        if variables.len() <= 4 {
            for i in 0..variables.len() {
                for j in (i + 1)..variables.len() {
                    let clause = Clause::binary(
                        Literal::negative(variables[i]),
                        Literal::negative(variables[j]),
                    );
                    self.add_clause_with_description(
                        clause,
                        format!(
                            "{} (pair {} vs {})",
                            description, variables[i], variables[j]
                        ),
                    );
                }
            }
            return Ok(());
        }

        // Sequential/ladder encoding:
        //   aux_i = "at least one of x_1..x_i has been selected"
        // Clauses:
        //   ¬x_1 ∨ aux_1
        //   ¬x_i ∨ aux_i              (i in 1..n-1)
        //   ¬aux_{i-1} ∨ aux_i        (transitivity)
        //   ¬x_i ∨ ¬aux_{i-1}         (x_i excludes any earlier pick)
        //   ¬x_n ∨ ¬aux_{n-2}         (final variable)
        let n = variables.len();
        let mut aux_vars = Vec::with_capacity(n - 1);
        for _ in 0..n - 1 {
            aux_vars.push(self.variables.allocate_auxiliary());
        }

        // First: x_1 → aux_1
        self.add_clause_with_description(
            Clause::binary(
                Literal::negative(variables[0]),
                Literal::positive(aux_vars[0]),
            ),
            format!(
                "{} (seq: {} -> aux_{})",
                description, variables[0], aux_vars[0]
            ),
        );

        for i in 1..n - 1 {
            // x_i → aux_i
            self.add_clause_with_description(
                Clause::binary(
                    Literal::negative(variables[i]),
                    Literal::positive(aux_vars[i]),
                ),
                format!(
                    "{} (seq: {} -> aux_{})",
                    description, variables[i], aux_vars[i]
                ),
            );
            // aux_{i-1} → aux_i
            self.add_clause_with_description(
                Clause::binary(
                    Literal::negative(aux_vars[i - 1]),
                    Literal::positive(aux_vars[i]),
                ),
                format!(
                    "{} (seq: aux_{} -> aux_{})",
                    description,
                    aux_vars[i - 1],
                    aux_vars[i]
                ),
            );
            // x_i ∧ aux_{i-1} forbidden
            self.add_clause_with_description(
                Clause::binary(
                    Literal::negative(variables[i]),
                    Literal::negative(aux_vars[i - 1]),
                ),
                format!(
                    "{} (seq: {} blocks aux_{})",
                    description,
                    variables[i],
                    aux_vars[i - 1]
                ),
            );
        }

        // Last: x_n ∧ aux_{n-2} forbidden
        self.add_clause_with_description(
            Clause::binary(
                Literal::negative(variables[n - 1]),
                Literal::negative(aux_vars[n - 2]),
            ),
            format!(
                "{} (seq: {} blocks aux_{})",
                description,
                variables[n - 1],
                aux_vars[n - 2]
            ),
        );

        Ok(())
    }

    fn add_clause_with_description(&mut self, clause: Clause, description: String) {
        let index = self.clauses.len();
        self.clauses.push(clause);
        self.clause_descriptions.insert(index, description);
    }

    /// Versions of `package` satisfying `version_set`. Filters the
    /// primed `local_versions` map if it has an entry; falls back to
    /// the registry only when the package is missing from the
    /// primed map. See the module docs for why priming matters.
    async fn get_versions_for_set(
        &self,
        package: &str,
        version_set: &VersionSet,
    ) -> EncodingResult<Vec<Version>> {
        if let Some(all) = self.local_versions.get(package) {
            return Ok(all
                .iter()
                .filter(|v| version_set.satisfies(v))
                .cloned()
                .collect());
        }
        self.registry
            .get_satisfying_versions(package, version_set)
            .await
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::registry::MockRegistry;

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

    #[test]
    fn variable_encoder_allocates_and_reuses() {
        let mut encoder = VariableEncoder::new();
        let v1 = encoder.get_or_create_variable("a", &Version::new(1, 0, 0));
        let v2 = encoder.get_or_create_variable("a", &Version::new(2, 0, 0));
        let v3 = encoder.get_or_create_variable("b", &Version::new(1, 0, 0));
        assert_eq!(v1, 1);
        assert_eq!(v2, 2);
        assert_eq!(v3, 3);
        assert_eq!(encoder.num_variables(), 3);
        assert_eq!(
            encoder.get_or_create_variable("a", &Version::new(1, 0, 0)),
            v1
        );
        assert_eq!(encoder.get_package_variables("a"), vec![1, 2]);
        assert_eq!(encoder.get_package_variables("b"), vec![3]);
    }

    #[test]
    fn variable_encoder_auxiliary_variables_have_unique_numbers() {
        let mut encoder = VariableEncoder::new();
        let _ = encoder.get_or_create_variable("a", &Version::new(1, 0, 0));
        let aux1 = encoder.allocate_auxiliary();
        let aux2 = encoder.allocate_auxiliary();
        assert_eq!(aux1, 2);
        assert_eq!(aux2, 3);
        // Aux vars participate in num_variables() but not in package lookup.
        assert_eq!(encoder.num_variables(), 3);
        assert_eq!(encoder.get_package(aux1), None);
    }

    #[tokio::test]
    async fn encode_exactly_emits_unit_clause() {
        let registry = MockRegistry::new().with_versions("p", &["1.2.3"]);
        let mut encoder = ConstraintEncoder::new(Arc::new(registry));
        encoder
            .encode_constraint(&Constraint::Exactly {
                package: "p".into(),
                version: Version::new(1, 2, 3),
            })
            .await
            .unwrap();
        assert_eq!(encoder.clauses.len(), 1);
        let clause = &encoder.clauses[0];
        assert!(clause.is_unit());
        assert!(!clause.literals[0].negated);
    }

    #[tokio::test]
    async fn encode_exclude_emits_negative_unit_clause() {
        let registry = MockRegistry::new().with_versions("p", &["1.2.3"]);
        let mut encoder = ConstraintEncoder::new(Arc::new(registry));
        encoder
            .encode_constraint(&Constraint::Exclude {
                package: "p".into(),
                version: Version::new(1, 2, 3),
            })
            .await
            .unwrap();
        assert_eq!(encoder.clauses.len(), 1);
        let clause = &encoder.clauses[0];
        assert!(clause.is_unit());
        assert!(clause.literals[0].negated);
    }

    #[tokio::test]
    async fn encode_conflict_emits_binary_negation_clause() {
        let registry = MockRegistry::new()
            .with_versions("a", &["1.0.0"])
            .with_versions("b", &["2.0.0"]);
        let mut encoder = ConstraintEncoder::new(Arc::new(registry));
        encoder
            .encode_constraint(&Constraint::Conflict {
                package1: "a".into(),
                version1: Version::new(1, 0, 0),
                package2: "b".into(),
                version2: Version::new(2, 0, 0),
            })
            .await
            .unwrap();
        assert_eq!(encoder.clauses.len(), 1);
        let clause = &encoder.clauses[0];
        assert_eq!(clause.literals.len(), 2);
        assert!(clause.literals[0].negated);
        assert!(clause.literals[1].negated);
    }

    #[tokio::test]
    async fn encode_at_most_one_pairwise_for_small_sets() {
        let registry = MockRegistry::new().with_versions("p", &["1.0.0", "2.0.0", "3.0.0"]);
        let mut encoder = ConstraintEncoder::new(Arc::new(registry));
        encoder
            .encode_constraint(&Constraint::AtMostOne {
                package: "p".into(),
                versions: vec![
                    Version::new(1, 0, 0),
                    Version::new(2, 0, 0),
                    Version::new(3, 0, 0),
                ],
            })
            .await
            .unwrap();
        // 3 choose 2 = 3 pairwise binary clauses.
        assert_eq!(encoder.clauses.len(), 3);
        for clause in &encoder.clauses {
            assert_eq!(clause.literals.len(), 2);
            assert!(clause.literals.iter().all(|l| l.negated));
        }
    }

    #[tokio::test]
    async fn encode_at_most_one_sequential_for_large_sets() {
        // 10 versions: deep in sequential-encoding territory. Pairwise
        // would emit n*(n-1)/2 = 45 clauses; sequential emits 1 + 3*(n-2)
        // + 1 = 26 clauses, plus n-1 = 9 auxiliary variables.
        let mut encoder = ConstraintEncoder::new(Arc::new(MockRegistry::new()));
        let versions: Vec<Version> = (1..=10).map(|i| Version::new(i, 0, 0)).collect();
        encoder
            .encode_constraint(&Constraint::AtMostOne {
                package: "p".into(),
                versions: versions.clone(),
            })
            .await
            .unwrap();
        assert_eq!(
            encoder.clauses.len(),
            26,
            "expected sequential O(n) encoding"
        );
        // 10 package variables + 9 auxiliary variables = 19 total.
        assert_eq!(encoder.variables().num_variables(), 19);
    }

    #[tokio::test]
    async fn encode_at_least_one_emits_disjunction() {
        let mut encoder = ConstraintEncoder::new(Arc::new(MockRegistry::new()));
        encoder
            .encode_constraint(&Constraint::AtLeastOne {
                package: "p".into(),
                versions: vec![Version::new(1, 0, 0), Version::new(2, 0, 0)],
            })
            .await
            .unwrap();
        assert_eq!(encoder.clauses.len(), 1);
        let clause = &encoder.clauses[0];
        assert_eq!(clause.literals.len(), 2);
        assert!(clause.literals.iter().all(|l| !l.negated));
    }

    #[tokio::test]
    async fn encode_dependency_uses_local_versions() {
        // Empty MockRegistry — if the encoder falls back to the registry
        // it'll fail. The primed local_versions cache must be the only
        // source consulted.
        let mut encoder = ConstraintEncoder::new(Arc::new(MockRegistry::new()));
        let mut local = HashMap::new();
        local.insert(
            "left-pad".to_string(),
            vec![
                Version::new(1, 0, 0),
                Version::new(1, 1, 0),
                Version::new(2, 0, 0),
            ],
        );
        encoder.set_local_versions(local);

        encoder
            .encode_constraint(&Constraint::Dependency {
                package: "left-pad".into(),
                version_set: vs("^1.0.0"),
                dependent: None,
            })
            .await
            .unwrap();

        // Two satisfying versions (1.0.0 and 1.1.0), one disjunctive clause.
        assert_eq!(encoder.clauses.len(), 1);
        let clause = &encoder.clauses[0];
        assert_eq!(clause.literals.len(), 2);
    }

    #[tokio::test]
    async fn encode_dependency_propagates_no_matching_versions() {
        let registry = MockRegistry::new().with_versions("p", &["3.0.0"]);
        let mut encoder = ConstraintEncoder::new(Arc::new(registry));
        let err = encoder
            .encode_constraint(&Constraint::Dependency {
                package: "p".into(),
                version_set: vs("^1.0.0"),
                dependent: None,
            })
            .await
            .unwrap_err();
        // `no_matching_versions` synthesizes an `InvalidPackage` with a
        // descriptive `version` field rather than its own variant.
        assert!(
            matches!(err, ResolutionError::InvalidPackage { ref version, .. } if version == "no matching versions"),
            "expected no-matching-versions error, got {:?}",
            err,
        );
    }

    #[tokio::test]
    async fn encode_optional_dependency_silently_skips_when_unsatisfiable() {
        let registry = MockRegistry::new();
        let mut encoder = ConstraintEncoder::new(Arc::new(registry));
        encoder
            .encode_constraint(&Constraint::OptionalDependency {
                package: "missing".into(),
                version_set: vs("^1.0.0"),
                dependent: None,
                condition: None,
            })
            .await
            .unwrap();
        assert_eq!(
            encoder.clauses.len(),
            0,
            "optional must not emit clauses on UNSAT"
        );
    }

    #[tokio::test]
    async fn build_problem_stamps_variable_names() {
        let registry = MockRegistry::new().with_versions("p", &["1.0.0"]);
        let mut encoder = ConstraintEncoder::new(Arc::new(registry));
        encoder
            .encode_constraint(&Constraint::Exactly {
                package: "p".into(),
                version: Version::new(1, 0, 0),
            })
            .await
            .unwrap();
        let problem = encoder.build_problem();
        assert_eq!(problem.num_variables, 1);
        assert_eq!(problem.clauses.len(), 1);
        assert_eq!(problem.get_variable_name(1), Some("p@1.0.0"));
    }

    #[tokio::test]
    async fn encode_from_graph_emits_dependency_per_edge() {
        use crate::graph::{
            DependencyEdge, DependencyGraph, DependencyNode, DependencyType, GraphBuildConfig,
        };

        let mut graph = DependencyGraph::new(GraphBuildConfig::default());
        let root = graph.add_node(DependencyNode::with_version("root", Version::new(1, 0, 0)));
        let dep = graph.add_node(DependencyNode::with_version("dep", Version::new(1, 5, 0)));
        graph.add_edge(
            root,
            dep,
            DependencyEdge::new(DependencyType::Runtime, vs("^1.0.0")),
        );

        let registry = MockRegistry::new().with_versions("dep", &["1.5.0"]);
        let mut encoder = ConstraintEncoder::new(Arc::new(registry));
        encoder.encode_from_graph(&graph).await.unwrap();

        // One Dependency constraint => one implication clause.
        assert_eq!(encoder.clauses.len(), 1);
        let problem = encoder.build_problem();
        // 2 package variables, no at-most-one (one version each).
        assert_eq!(problem.num_variables, 2);
    }
}

#[cfg(test)]
mod proptests {
    //! Property-based tests for the CNF semantics produced by
    //! [`ConstraintEncoder`].
    //!
    //! Each property encodes a [`Constraint`] (sometimes with a
    //! "force selection" companion clause to avoid trivial all-false
    //! models), solves with the Varisat backend, and asserts the
    //! resulting [`SatModel`](crate::sat::SatModel) respects the
    //! constraint's intended semantics.
    //!
    //! `cases` is dialed down from proptest's default 256 to 32 —
    //! each case runs a SAT solve, so even small graphs add up.

    use super::*;
    use crate::registry::MockRegistry;
    use crate::sat::{
        SatModel, SatProblem, SatSolution, SolverBackend, SolverConfig, create_solver_with_backend,
    };
    use proptest::prelude::*;

    /// A fixed "world" used across the constraint properties. Two
    /// packages with several versions each gives enough surface for
    /// every constraint variant to operate non-trivially.
    fn world() -> (Arc<MockRegistry>, Vec<(String, Version)>) {
        let registry = Arc::new(
            MockRegistry::new()
                .with_versions("a", &["1.0.0", "2.0.0", "3.0.0"])
                .with_versions("b", &["1.0.0", "2.0.0"]),
        );
        let pairs = vec![
            ("a".to_string(), Version::new(1, 0, 0)),
            ("a".to_string(), Version::new(2, 0, 0)),
            ("a".to_string(), Version::new(3, 0, 0)),
            ("b".to_string(), Version::new(1, 0, 0)),
            ("b".to_string(), Version::new(2, 0, 0)),
        ];
        (registry, pairs)
    }

    /// Build a tokio runtime and block on the given future. Each
    /// proptest case gets its own runtime — wasteful on its own but
    /// trivial against the cost of a SAT solve.
    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)
    }

    /// Look up the SAT variable for `(name, version)` in a built
    /// problem by scanning the variable_names metadata.
    fn lookup_var(problem: &SatProblem, name: &str, version: &Version) -> Option<u32> {
        let needle = format!("{}@{}", name, version);
        problem
            .metadata
            .variable_names
            .iter()
            .find(|(_, n)| n.as_str() == needle)
            .map(|(v, _)| *v)
    }

    /// Encode a batch of constraints, build the problem, and solve.
    /// Returns `Some(model)` on SAT, `None` on UNSAT / Unknown / errors.
    async fn solve_constraints(
        registry: Arc<MockRegistry>,
        constraints: Vec<Constraint>,
    ) -> Option<(SatModel, SatProblem)> {
        let mut encoder = ConstraintEncoder::new(registry);
        for c in &constraints {
            encoder.encode_constraint(c).await.ok()?;
        }
        let problem = encoder.build_problem();
        let mut solver =
            create_solver_with_backend(SolverBackend::Varisat, SolverConfig::default())
                .await
                .ok()?;
        match solver.solve(&problem).await.ok()? {
            SatSolution::Satisfiable(m) => Some((m, problem)),
            _ => None,
        }
    }

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

        /// `AtMostOne` paired with `AtLeastOne` over the same set
        /// of versions ⇒ the model selects exactly one of them.
        #[test]
        fn at_most_one_with_at_least_one_picks_exactly_one(
            mask in 1u8..=0b111, // non-empty subset of a's three versions
        ) {
            let (registry, _pairs) = world();
            let all_a_versions = [
                Version::new(1, 0, 0),
                Version::new(2, 0, 0),
                Version::new(3, 0, 0),
            ];
            let selected_versions: Vec<Version> = (0..3)
                .filter(|i| mask & (1 << i) != 0)
                .map(|i| all_a_versions[i].clone())
                .collect();
            prop_assume!(!selected_versions.is_empty());

            let constraints = vec![
                Constraint::AtMostOne {
                    package: "a".into(),
                    versions: selected_versions.clone(),
                },
                Constraint::AtLeastOne {
                    package: "a".into(),
                    versions: selected_versions.clone(),
                },
            ];

            let result = block_on(solve_constraints(registry, constraints));
            let (model, problem) = result.ok_or_else(|| {
                TestCaseError::fail("expected SAT, got UNSAT/Unknown".to_string())
            })?;

            let true_count = selected_versions
                .iter()
                .filter_map(|v| lookup_var(&problem, "a", v))
                .filter(|var| model.get(*var) == Some(true))
                .count();
            prop_assert_eq!(true_count, 1, "expected exactly one selected version of a");
        }

        /// `Exactly { p, v }` forces the corresponding variable to
        /// true in any satisfying model.
        #[test]
        fn exactly_pins_variable(
            pkg_idx in 0usize..2,
            ver_idx in 0usize..2,
        ) {
            let (registry, _) = world();
            let (pkg, max_v) = if pkg_idx == 0 { ("a", 3) } else { ("b", 2) };
            let version = Version::new((ver_idx % max_v) as u64 + 1, 0, 0);

            let constraints = vec![Constraint::Exactly {
                package: pkg.into(),
                version: version.clone(),
            }];
            let result = block_on(solve_constraints(registry, constraints));
            let (model, problem) = result.ok_or_else(|| {
                TestCaseError::fail("expected SAT".to_string())
            })?;
            let var = lookup_var(&problem, pkg, &version)
                .ok_or_else(|| TestCaseError::fail("expected variable to exist".to_string()))?;
            prop_assert_eq!(model.get(var), Some(true));
        }

        /// `Exclude { p, v } + AtLeastOne` over `[v]` is UNSAT —
        /// the only way to satisfy AtLeastOne is to pick `v`, which
        /// Exclude forbids. So `solve_constraints` returns `None`.
        #[test]
        fn exclude_makes_at_least_one_over_excluded_unsat(
            pkg_idx in 0usize..2,
            ver_idx in 0usize..2,
        ) {
            let (registry, _) = world();
            let (pkg, max_v) = if pkg_idx == 0 { ("a", 3) } else { ("b", 2) };
            let version = Version::new((ver_idx % max_v) as u64 + 1, 0, 0);

            let constraints = vec![
                Constraint::Exclude {
                    package: pkg.into(),
                    version: version.clone(),
                },
                Constraint::AtLeastOne {
                    package: pkg.into(),
                    versions: vec![version.clone()],
                },
            ];
            let result = block_on(solve_constraints(registry, constraints));
            prop_assert!(result.is_none(), "expected UNSAT, got SAT model");
        }

        /// `Conflict { a@v1, b@v2 } + Exactly a@v1 + Exactly b@v2`
        /// is UNSAT — the two `Exactly` clauses force both true,
        /// but `Conflict` forbids both true.
        #[test]
        fn conflict_forbids_both_being_selected(
            v1_idx in 0usize..3,
            v2_idx in 0usize..2,
        ) {
            let (registry, _) = world();
            let v1 = Version::new(v1_idx as u64 + 1, 0, 0);
            let v2 = Version::new(v2_idx as u64 + 1, 0, 0);

            let constraints = vec![
                Constraint::Conflict {
                    package1: "a".into(),
                    version1: v1.clone(),
                    package2: "b".into(),
                    version2: v2.clone(),
                },
                Constraint::Exactly {
                    package: "a".into(),
                    version: v1,
                },
                Constraint::Exactly {
                    package: "b".into(),
                    version: v2,
                },
            ];
            let result = block_on(solve_constraints(registry, constraints));
            prop_assert!(result.is_none(), "expected UNSAT, got SAT");
        }

        /// `Dependency { dep: t, version_set, dependent: Some(p@v) }`
        /// + `Exactly p@v` (force the premise true) ⇒ at least one
        /// version of `t` satisfying `version_set` is true in the model.
        #[test]
        fn dependency_forces_satisfying_target_selection(
            premise_v_idx in 0usize..3,
        ) {
            let (registry, _) = world();
            let premise_v = Version::new(premise_v_idx as u64 + 1, 0, 0);
            // Dep edge: a@premise → b, with any version satisfying *
            // (so all three of b's versions are candidates).
            let constraints = vec![
                Constraint::Exactly {
                    package: "a".into(),
                    version: premise_v.clone(),
                },
                Constraint::Dependency {
                    package: "b".into(),
                    version_set: VersionSet::any(),
                    dependent: Some(format!("a@{}", premise_v)),
                },
            ];
            let result = block_on(solve_constraints(registry, constraints));
            let (model, problem) = result.ok_or_else(|| {
                TestCaseError::fail("expected SAT".to_string())
            })?;

            let b_versions = [Version::new(1, 0, 0), Version::new(2, 0, 0)];
            let selected_count = b_versions
                .iter()
                .filter_map(|v| lookup_var(&problem, "b", v))
                .filter(|var| model.get(*var) == Some(true))
                .count();
            prop_assert!(
                selected_count >= 1,
                "Dependency should force at least one version of b to be selected"
            );
        }
    }
}