diff options
Diffstat (limited to 'crates/mozart-core/src/dependency_resolver/solver.rs')
| -rw-r--r-- | crates/mozart-core/src/dependency_resolver/solver.rs | 1008 |
1 files changed, 1008 insertions, 0 deletions
diff --git a/crates/mozart-core/src/dependency_resolver/solver.rs b/crates/mozart-core/src/dependency_resolver/solver.rs new file mode 100644 index 0000000..4abb888 --- /dev/null +++ b/crates/mozart-core/src/dependency_resolver/solver.rs @@ -0,0 +1,1008 @@ +use super::decisions::Decisions; +use super::error::{SolverBugError, SolverError}; +use super::policy::DefaultPolicy; +use super::pool::{Literal, PackageId, Pool, literal_to_package_id}; +use super::problem::Problem; +use super::rule::{ReasonData, Rule, RuleReason, RuleType}; +use super::rule_set::{RuleId, RuleSet}; +use super::rule_watch_graph::RuleWatchGraph; +use indexmap::{IndexMap, IndexSet}; + +/// Result of solving: the list of package IDs to install. +#[derive(Debug)] +pub struct SolverResult { + /// Package IDs decided for installation. + pub installed: Vec<PackageId>, +} + +/// Main SAT solver implementing CDCL (Conflict-Driven Clause Learning). +/// +/// Port of Composer's Solver.php. +pub struct Solver<'a> { + pool: &'a Pool, + policy: DefaultPolicy, + rules: RuleSet, + watch_graph: RuleWatchGraph, + decisions: Decisions, + /// Fixed packages by ID. + fixed_map: IndexSet<PackageId>, + /// Current propagation index in decision queue. + propagate_index: usize, + /// Branch points: (alternative literals, decision level). + branches: Vec<(Vec<Literal>, i32)>, + /// Problems found during solving. + problems: Vec<Problem>, + /// Learned rule pool: for each learned rule, the chain of rules that led to it. + learned_pool: Vec<Vec<RuleId>>, + /// Map from rule ID → learned pool index. + learned_why: IndexMap<RuleId, usize>, +} + +impl<'a> Solver<'a> { + /// Create a new solver with the given rules, pool, policy, and fixed package set. + pub fn new( + rules: RuleSet, + pool: &'a Pool, + policy: DefaultPolicy, + fixed_packages: IndexSet<PackageId>, + ) -> Self { + Solver { + pool, + policy, + rules, + watch_graph: RuleWatchGraph::new(), + decisions: Decisions::new(), + fixed_map: fixed_packages, + propagate_index: 0, + branches: Vec::new(), + problems: Vec::new(), + learned_pool: Vec::new(), + learned_why: IndexMap::new(), + } + } + + /// Solve the dependency resolution problem. + /// Returns the set of packages to install, or an error. + pub fn solve(mut self) -> Result<SolverResult, SolverError> { + // Insert all rules into watch graph + let rule_count = self.rules.len(); + for id in 0..rule_count { + let rule = self.rules.rule_by_id(id); + self.watch_graph.insert(id, rule); + } + + // Make decisions based on assertion rules (unit clauses) + self.make_assertion_rule_decisions()?; + + // Run the main SAT loop + self.run_sat()?; + + if !self.problems.is_empty() { + let messages: Vec<String> = self + .problems + .iter() + .map(|p| p.pretty_string(self.pool, &self.rules)) + .collect(); + return Err(SolverError::Unsolvable(messages)); + } + + // Collect installed packages + let mut installed = Vec::new(); + for i in 0..self.decisions.len() { + let decision = self.decisions.at_offset(i); + if decision.literal > 0 { + installed.push(literal_to_package_id(decision.literal)); + } + } + + Ok(SolverResult { installed }) + } + + /// Process assertion rules (unit clauses) — make immediate decisions. + /// + /// Port of Composer's Solver::makeAssertionRuleDecisions. + fn make_assertion_rule_decisions(&mut self) -> Result<(), SolverError> { + let decision_start = if self.decisions.is_empty() { + 0 + } else { + self.decisions.len() - 1 + }; + + let mut rule_index: usize = 0; + while rule_index < self.rules.len() { + let rule = self.rules.rule_by_id(rule_index); + + if !rule.is_assertion() || rule.is_disabled() { + rule_index += 1; + continue; + } + + let literal = rule.literals()[0]; + + if !self.decisions.decided(literal) { + self.decisions.decide(literal, 1, rule_index)?; + rule_index += 1; + continue; + } + + if self.decisions.satisfy(literal) { + rule_index += 1; + continue; + } + + // Found a conflict + let rule_type = self.rules.rule_by_id(rule_index).rule_type; + + if rule_type == RuleType::Learned { + self.rules.rule_by_id_mut(rule_index).disable(); + rule_index += 1; + continue; + } + + let conflict_rule_id = self.decisions.decision_rule(literal)?; + let conflict_type = self.rules.rule_by_id(conflict_rule_id).rule_type; + + if conflict_type == RuleType::Package { + let mut problem = Problem::new(); + problem.add_rule(rule_index); + problem.add_rule(conflict_rule_id); + self.rules.rule_by_id_mut(rule_index).disable(); + self.problems.push(problem); + rule_index += 1; + continue; + } + + // Conflict with another root require/fixed package + let mut problem = Problem::new(); + problem.add_rule(rule_index); + problem.add_rule(conflict_rule_id); + + // Push all request assertion rules asserting this literal + let pkg_id = literal_to_package_id(literal); + let request_rule_ids: Vec<RuleId> = self + .rules + .iter_type(RuleType::Request) + .filter(|(_, r)| { + !r.is_disabled() + && r.is_assertion() + && literal_to_package_id(r.literals()[0]) == pkg_id + }) + .map(|(id, _)| id) + .collect(); + + for rid in &request_rule_ids { + problem.add_rule(*rid); + } + self.problems.push(problem); + + for rid in request_rule_ids { + self.rules.rule_by_id_mut(rid).disable(); + } + + self.decisions.reset_to_offset(decision_start); + rule_index = 0; // restart + } + + Ok(()) + } + + /// Unit propagation: propagate decisions through the watch graph. + /// + /// Port of Composer's Solver::propagate. + fn propagate(&mut self, level: i32) -> Result<Option<RuleId>, SolverBugError> { + while self.decisions.valid_offset(self.propagate_index) { + let decision = self.decisions.at_offset(self.propagate_index).clone(); + self.propagate_index += 1; + + let conflict = self.watch_graph.propagate_literal( + decision.literal, + level, + &mut self.decisions, + &self.rules, + )?; + + if conflict.is_some() { + return Ok(conflict); + } + } + + Ok(None) + } + + /// Revert decisions to a given level. + /// + /// Port of Composer's Solver::revert. + fn revert(&mut self, level: i32) { + while !self.decisions.is_empty() { + let literal = self.decisions.last_literal(); + if self.decisions.undecided(literal) { + break; + } + let decision_level = self.decisions.decision_level(literal); + if decision_level <= level { + break; + } + self.decisions.revert_last(); + self.propagate_index = self.decisions.len(); + } + + while !self.branches.is_empty() && self.branches.last().unwrap().1 >= level { + self.branches.pop(); + } + } + + /// Make a decision, propagate, and learn from conflicts. + /// + /// Port of Composer's Solver::setPropagateLearn. + fn set_propagate_learn( + &mut self, + mut level: i32, + literal: Literal, + rule_id: RuleId, + ) -> Result<i32, SolverError> { + level += 1; + self.decisions.decide(literal, level, rule_id)?; + + loop { + let conflict = self.propagate(level)?; + + let Some(conflict_rule_id) = conflict else { + break; + }; + + if level == 1 { + self.analyze_unsolvable(conflict_rule_id); + return Ok(0); + } + + // Conflict analysis + let (learn_literal, new_level, new_rule, why) = + self.analyze(level, conflict_rule_id)?; + + if new_level <= 0 || new_level >= level { + return Err(SolverBugError { + message: format!( + "Trying to revert to invalid level {new_level} from level {level}." + ), + } + .into()); + } + + level = new_level; + self.revert(level); + + // Add learned rule + self.rules.add(new_rule, RuleType::Learned); + let new_rule_id = self.rules.len() - 1; + + self.learned_why.insert(new_rule_id, why); + + let rule_ref = self.rules.rule_by_id(new_rule_id); + self.watch_graph.insert(new_rule_id, rule_ref); + + // Adjust watch2 to highest level literal + let last_node = self.watch_graph.last_node_idx(); + let rule_for_watch = self.rules.rule_by_id(new_rule_id); + self.watch_graph + .watch2_on_highest(last_node, rule_for_watch, &self.decisions); + + self.decisions.decide(learn_literal, level, new_rule_id)?; + } + + Ok(level) + } + + /// Choose best package from candidates and install. + /// + /// Port of Composer's Solver::selectAndInstall. + fn select_and_install( + &mut self, + level: i32, + decision_queue: Vec<Literal>, + rule_id: RuleId, + ) -> Result<i32, SolverError> { + let required_package = self + .rules + .rule_by_id(rule_id) + .required_package() + .map(|s| s.to_string()); + let mut literals = self.policy.select_preferred_packages( + self.pool, + &decision_queue, + required_package.as_deref(), + ); + + let selected = literals.remove(0); + + // If there are remaining alternatives, save as branch point + if !literals.is_empty() { + self.branches.push((literals, level)); + } + + self.set_propagate_learn(level, selected, rule_id) + } + + /// First UIP conflict analysis. + /// + /// Port of Composer's Solver::analyze. + fn analyze( + &mut self, + level: i32, + conflict_rule_id: RuleId, + ) -> Result<(Literal, i32, Rule, usize), SolverError> { + let mut rule_level: i32 = 1; + let mut num: i32 = 0; + let mut l1num: i32 = 0; + let mut seen: IndexSet<PackageId> = IndexSet::new(); + let mut learned_literal: Option<Literal> = None; + let mut other_learned_literals: Vec<Literal> = Vec::new(); + + let mut decision_id = self.decisions.len(); + + self.learned_pool.push(Vec::new()); + let pool_idx = self.learned_pool.len() - 1; + + let mut current_rule_id = conflict_rule_id; + + loop { + self.learned_pool[pool_idx].push(current_rule_id); + + let rule = self.rules.rule_by_id(current_rule_id); + let rule_literals = rule.literals().to_vec(); + let is_multi_conflict = rule.is_multi_conflict; + + for &literal in &rule_literals { + // MultiConflictRule: skip undecided literals + if is_multi_conflict && !self.decisions.decided(literal) { + continue; + } + + // Skip the one true literal + if self.decisions.satisfy(literal) { + continue; + } + + let pkg_id = literal_to_package_id(literal); + if seen.contains(&pkg_id) { + continue; + } + seen.insert(pkg_id); + + let l = self.decisions.decision_level(literal); + + if l == 1 { + l1num += 1; + } else if l == level { + num += 1; + } else { + other_learned_literals.push(literal); + if l > rule_level { + rule_level = l; + } + } + } + + // l1 retry loop + let mut l1retry = true; + while l1retry { + l1retry = false; + + if num == 0 { + l1num -= 1; + if l1num == 0 { + // All level 1 literals done + let why = pool_idx; + let ll = learned_literal.ok_or_else(|| SolverBugError { + message: format!( + "Did not find a learnable literal in analyzed rule {conflict_rule_id}." + ), + })?; + + let mut all_literals = vec![ll]; + all_literals.extend_from_slice(&other_learned_literals); + + let new_rule = + Rule::new(all_literals, RuleReason::Learned, ReasonData::Learned(why)); + + return Ok((ll, rule_level, new_rule, why)); + } + } + + loop { + if decision_id == 0 { + return Err(SolverBugError { + message: format!( + "Reached invalid decision id 0 while analyzing rule {conflict_rule_id}." + ), + } + .into()); + } + + decision_id -= 1; + let decision = self.decisions.at_offset(decision_id); + let literal = decision.literal; + + if seen.contains(&literal_to_package_id(literal)) { + break; + } + } + + let decision = self.decisions.at_offset(decision_id); + let literal = decision.literal; + + seen.shift_remove(&literal_to_package_id(literal)); + + if num != 0 { + num -= 1; + if num == 0 { + learned_literal = Some(-literal); + + if l1num == 0 { + // Done + let why = pool_idx; + let ll = learned_literal.unwrap(); + + let mut all_literals = vec![ll]; + all_literals.extend_from_slice(&other_learned_literals); + + let new_rule = Rule::new( + all_literals, + RuleReason::Learned, + ReasonData::Learned(why), + ); + + return Ok((ll, rule_level, new_rule, why)); + } + + // Only level 1 marks left + for other in &other_learned_literals { + seen.shift_remove(&literal_to_package_id(*other)); + } + l1num += 1; + l1retry = true; + } else { + let decision = self.decisions.at_offset(decision_id); + let next_rule_id = decision.rule_id; + let next_rule = self.rules.rule_by_id(next_rule_id); + + if next_rule.is_multi_conflict { + // Handle multi-conflict rule + let mcr_literals = next_rule.literals().to_vec(); + for &rule_literal in &mcr_literals { + let pkg_id = literal_to_package_id(rule_literal); + if !seen.contains(&pkg_id) && self.decisions.satisfy(-rule_literal) + { + self.learned_pool[pool_idx].push(next_rule_id); + let l = self.decisions.decision_level(rule_literal); + if l == 1 { + l1num += 1; + } else if l == level { + num += 1; + } else { + other_learned_literals.push(rule_literal); + if l > rule_level { + rule_level = l; + } + } + seen.insert(pkg_id); + break; + } + } + l1retry = true; + } + } + } + } + + let decision = self.decisions.at_offset(decision_id); + current_rule_id = decision.rule_id; + } + } + + /// Recursively collect rules involved in an unsolvable conflict. + fn analyze_unsolvable_rule( + &self, + problem: &mut Problem, + conflict_rule_id: RuleId, + rule_seen: &mut IndexSet<RuleId>, + ) { + if rule_seen.contains(&conflict_rule_id) { + return; + } + rule_seen.insert(conflict_rule_id); + + let rule = self.rules.rule_by_id(conflict_rule_id); + + if rule.rule_type == RuleType::Learned { + if let Some(&why) = self.learned_why.get(&conflict_rule_id) + && let Some(problem_rules) = self.learned_pool.get(why) + { + for &pr_id in problem_rules { + if !rule_seen.contains(&pr_id) { + self.analyze_unsolvable_rule(problem, pr_id, rule_seen); + } + } + } + return; + } + + if rule.rule_type == RuleType::Package { + // Package rules cannot be part of a problem + return; + } + + problem.next_section(); + problem.add_rule(conflict_rule_id); + } + + /// Analyze an unsolvable conflict at level 1. + /// + /// Port of Composer's Solver::analyzeUnsolvable. + fn analyze_unsolvable(&mut self, conflict_rule_id: RuleId) { + let mut problem = Problem::new(); + problem.add_rule(conflict_rule_id); + + let mut rule_seen = IndexSet::new(); + self.analyze_unsolvable_rule(&mut problem, conflict_rule_id, &mut rule_seen); + + // Collect related decisions + let mut seen: IndexSet<PackageId> = IndexSet::new(); + let conflict_literals = self.rules.rule_by_id(conflict_rule_id).literals().to_vec(); + for &lit in &conflict_literals { + if self.decisions.satisfy(lit) { + continue; + } + seen.insert(literal_to_package_id(lit)); + } + + // Walk decisions in reverse + for i in (0..self.decisions.len()).rev() { + let decision = self.decisions.at_offset(i); + let dec_literal = decision.literal; + let pkg_id = literal_to_package_id(dec_literal); + + if !seen.contains(&pkg_id) { + continue; + } + + let why = decision.rule_id; + problem.add_rule(why); + self.analyze_unsolvable_rule(&mut problem, why, &mut rule_seen); + + let why_literals = self.rules.rule_by_id(why).literals().to_vec(); + for &lit in &why_literals { + if self.decisions.satisfy(lit) { + continue; + } + seen.insert(literal_to_package_id(lit)); + } + } + + self.problems.push(problem); + } + + /// Main SAT loop. + /// + /// Port of Composer's Solver::runSat. + fn run_sat(&mut self) -> Result<(), SolverError> { + self.propagate_index = 0; + + let mut level: i32 = 1; + let mut system_level: i32 = level + 1; + + loop { + // Step 1: propagate at level 1 + if level == 1 { + let conflict = self.propagate(level)?; + if let Some(conflict_rule_id) = conflict { + self.analyze_unsolvable(conflict_rule_id); + return Ok(()); + } + } + + // Step 2: handle root require/fixed package rules + if level < system_level { + let mut made_decision = false; + + // Collect request rule IDs first to avoid borrow issues + let request_rule_ids: Vec<RuleId> = self + .rules + .iter_type(RuleType::Request) + .map(|(id, _)| id) + .collect(); + + let mut all_satisfied = true; + + for &rule_id in &request_rule_ids { + let rule = self.rules.rule_by_id(rule_id); + if !rule.is_enabled() { + continue; + } + + let mut decision_queue: Vec<Literal> = Vec::new(); + let mut none_satisfied = true; + + for &lit in rule.literals() { + if self.decisions.satisfy(lit) { + none_satisfied = false; + break; + } + if lit > 0 && self.decisions.undecided(lit) { + decision_queue.push(lit); + } + } + + if none_satisfied && !decision_queue.is_empty() { + // Prune: prefer fixed packages + let pruned: Vec<Literal> = decision_queue + .iter() + .filter(|&&lit| self.fixed_map.contains(&literal_to_package_id(lit))) + .copied() + .collect(); + + if !pruned.is_empty() { + decision_queue = pruned; + } + } + + if none_satisfied && !decision_queue.is_empty() { + let old_level = level; + level = self.select_and_install(level, decision_queue, rule_id)?; + + if level == 0 { + return Ok(()); + } + if level <= old_level { + made_decision = true; + break; + } + } + + // Check if there are more rules to process + all_satisfied = false; + } + + system_level = level + 1; + + if made_decision || !all_satisfied { + // Check if we still have unsatisfied request rules + let has_unsatisfied = request_rule_ids.iter().any(|&rule_id| { + let rule = self.rules.rule_by_id(rule_id); + if !rule.is_enabled() { + return false; + } + let mut none_satisfied = true; + for &lit in rule.literals() { + if self.decisions.satisfy(lit) { + none_satisfied = false; + break; + } + } + if !none_satisfied { + return false; + } + rule.literals() + .iter() + .any(|&lit| lit > 0 && self.decisions.undecided(lit)) + }); + + if has_unsatisfied { + continue; + } + } + } + + if level < system_level { + system_level = level; + } + + // Step 3: fulfill all unresolved rules + let mut rules_count = self.rules.len(); + let mut i: usize = 0; + let mut n: usize = 0; + let mut made_decision = false; + + while n < rules_count { + if i == rules_count { + i = 0; + } + + let rule = self.rules.rule_by_id(i); + let literals = rule.literals().to_vec(); + + i += 1; + n += 1; + + if rule.is_disabled() { + continue; + } + + let mut decision_queue: Vec<Literal> = Vec::new(); + let mut skip = false; + + for &lit in &literals { + if lit <= 0 { + if !self.decisions.decided_install(lit) { + skip = true; + break; + } + } else { + if self.decisions.decided_install(lit) { + skip = true; + break; + } + if self.decisions.undecided(lit) { + decision_queue.push(lit); + } + } + } + + if skip { + continue; + } + + // Need at least 2 undecided positive literals + if decision_queue.len() < 2 { + continue; + } + + let rule_id = i - 1; + level = self.select_and_install(level, decision_queue, rule_id)?; + + if level == 0 { + return Ok(()); + } + + // Something changed, restart scan + rules_count = self.rules.len(); + n = 0; + i = 0; + made_decision = true; + } + + if level < system_level && made_decision { + continue; + } + + // Step 4: minimization (backjumping) + if !self.branches.is_empty() { + let mut last_literal: Option<Literal> = None; + let mut last_level: Option<i32> = None; + let mut last_branch_index: usize = 0; + let mut last_branch_offset: usize = 0; + + for i in (0..self.branches.len()).rev() { + let (ref literals, l) = self.branches[i]; + for (offset, &literal) in literals.iter().enumerate() { + if literal > 0 && self.decisions.decision_level(literal) > l + 1 { + last_literal = Some(literal); + last_branch_index = i; + last_branch_offset = offset; + last_level = Some(l); + } + } + } + + if let Some(literal) = last_literal { + let last_l = last_level.unwrap(); + self.branches[last_branch_index] + .0 + .remove(last_branch_offset); + + level = last_l; + self.revert(level); + + let why = self.decisions.last_reason(); + + level = self.set_propagate_learn(level, literal, why)?; + + if level == 0 { + return Ok(()); + } + + continue; + } + } + + break; + } + + Ok(()) + } +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::dependency_resolver::pool::PoolPackageInput; + use crate::dependency_resolver::rule::{ReasonData, Rule, RuleReason, RuleType}; + + fn make_input(name: &str, version: &str) -> PoolPackageInput { + PoolPackageInput { + name: name.to_string(), + version: version.to_string(), + pretty_version: version.to_string(), + requires: vec![], + replaces: vec![], + provides: vec![], + conflicts: vec![], + is_fixed: false, + is_alias_of: None, + } + } + + /// Helper: create a simple problem and solve it. + /// Creates a pool with N dummy packages (1..=max_id). + fn make_rules_and_solve( + rules: Vec<(Rule, RuleType)>, + fixed: IndexSet<PackageId>, + max_id: u32, + ) -> Result<SolverResult, SolverError> { + let mut rs = RuleSet::new(); + for (rule, rt) in rules { + rs.add(rule, rt); + } + let inputs: Vec<_> = (1..=max_id) + .map(|i| make_input(&format!("pkg/{i}"), &format!("{i}.0.0.0"))) + .collect(); + let pool = Pool::new(inputs, vec![]); + let policy = DefaultPolicy::default(); + let solver = Solver::new(rs, &pool, policy, fixed); + solver.solve() + } + + #[test] + fn test_single_package_required() { + // Root requires package 1 + let result = make_rules_and_solve( + vec![( + Rule::new(vec![1], RuleReason::RootRequire, ReasonData::None), + RuleType::Request, + )], + IndexSet::new(), + 3, + ) + .unwrap(); + + assert_eq!(result.installed, vec![1]); + } + + #[test] + fn test_two_packages_required() { + // Root requires either package 1 or 2, and also requires 3 + let result = make_rules_and_solve( + vec![ + ( + Rule::new(vec![1, 2], RuleReason::RootRequire, ReasonData::None), + RuleType::Request, + ), + ( + Rule::new(vec![3], RuleReason::RootRequire, ReasonData::None), + RuleType::Request, + ), + ], + IndexSet::new(), + 3, + ) + .unwrap(); + + assert!(result.installed.contains(&3)); + // Should install one of 1 or 2 + assert!(result.installed.contains(&1) || result.installed.contains(&2)); + } + + #[test] + fn test_dependency_chain() { + // Root requires 1. Package 1 requires 2. + // Rule for root: (1) + // Rule for dep: (-1 | 2) + let result = make_rules_and_solve( + vec![ + ( + Rule::new(vec![1], RuleReason::RootRequire, ReasonData::None), + RuleType::Request, + ), + ( + Rule::new(vec![-1, 2], RuleReason::PackageRequires, ReasonData::None), + RuleType::Package, + ), + ], + IndexSet::new(), + 3, + ) + .unwrap(); + + assert!(result.installed.contains(&1)); + assert!(result.installed.contains(&2)); + } + + #[test] + fn test_conflict_resolution() { + // Root requires 1 or 2. Package 1 conflicts with 3. + // Package 2 requires 3. + // Rules: + // Request: (1 | 2) + // Package: (-1 | -3) -- conflict + // Package: (-2 | 3) -- dep + // Request: (3) -- root also requires 3 + let result = make_rules_and_solve( + vec![ + ( + Rule::new(vec![1, 2], RuleReason::RootRequire, ReasonData::None), + RuleType::Request, + ), + ( + Rule::two_literals(-1, -3, RuleReason::PackageConflict, ReasonData::None), + RuleType::Package, + ), + ( + Rule::new(vec![-2, 3], RuleReason::PackageRequires, ReasonData::None), + RuleType::Package, + ), + ( + Rule::new(vec![3], RuleReason::RootRequire, ReasonData::None), + RuleType::Request, + ), + ], + IndexSet::new(), + 3, + ) + .unwrap(); + + // Package 3 is required, so 1 conflicts, must choose 2 + assert!(result.installed.contains(&2)); + assert!(result.installed.contains(&3)); + assert!(!result.installed.contains(&1)); + } + + #[test] + fn test_same_name_conflict() { + // Two versions of same package: 1 and 2. Root requires either. + // Same-name rule: (-1 | -2) + let result = make_rules_and_solve( + vec![ + ( + Rule::new(vec![1, 2], RuleReason::RootRequire, ReasonData::None), + RuleType::Request, + ), + ( + Rule::two_literals(-1, -2, RuleReason::PackageSameName, ReasonData::None), + RuleType::Package, + ), + ], + IndexSet::new(), + 3, + ) + .unwrap(); + + // Should install exactly one + let has_1 = result.installed.contains(&1); + let has_2 = result.installed.contains(&2); + assert!(has_1 ^ has_2, "Should install exactly one of 1 or 2"); + } + + #[test] + fn test_unsolvable() { + // Root requires 1. Root requires 2. But 1 and 2 conflict. + let result = make_rules_and_solve( + vec![ + ( + Rule::new(vec![1], RuleReason::RootRequire, ReasonData::None), + RuleType::Request, + ), + ( + Rule::new(vec![2], RuleReason::RootRequire, ReasonData::None), + RuleType::Request, + ), + ( + Rule::two_literals(-1, -2, RuleReason::PackageConflict, ReasonData::None), + RuleType::Package, + ), + ], + IndexSet::new(), + 3, + ); + + assert!(result.is_err()); + } +} |