diff options
| author | nsfisis <nsfisis@gmail.com> | 2026-02-22 18:25:16 +0900 |
|---|---|---|
| committer | nsfisis <nsfisis@gmail.com> | 2026-02-22 18:28:04 +0900 |
| commit | 84d137a19feb1f79f5bd711faff63a6bbe651cbf (patch) | |
| tree | 858dee19c5933ecda3f368cb586cf140b4e4c4d2 /crates/mozart-sat-resolver/src/error.rs | |
| parent | 07733b3b328f6e4ec23754fcb3504ddb196d65a3 (diff) | |
| download | php-mozart-84d137a19feb1f79f5bd711faff63a6bbe651cbf.tar.gz php-mozart-84d137a19feb1f79f5bd711faff63a6bbe651cbf.tar.zst php-mozart-84d137a19feb1f79f5bd711faff63a6bbe651cbf.zip | |
feat(resolver): replace pubgrub with Composer-ported SAT solver
Add mozart-sat-resolver crate implementing a CDCL SAT-based dependency
resolver ported from Composer's DependencyResolver. This replaces the
pubgrub library to ensure identical resolution behavior with Composer.
The new crate includes: pool (package storage with integer IDs),
rule/rule_set/rule_set_generator (constraint encoding), decisions
(assignment tracking), rule_watch_graph (2-watched literal BCP),
solver (CDCL loop with conflict analysis and clause learning),
policy (version preference), problem (Composer-style error messages),
and transaction (install/update/uninstall operation computation).
The registry resolver is rewritten to use PoolBuilder → RuleSetGenerator
→ Solver pipeline instead of pubgrub's DependencyProvider trait.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Diffstat (limited to 'crates/mozart-sat-resolver/src/error.rs')
| -rw-r--r-- | crates/mozart-sat-resolver/src/error.rs | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/crates/mozart-sat-resolver/src/error.rs b/crates/mozart-sat-resolver/src/error.rs new file mode 100644 index 0000000..e4b9841 --- /dev/null +++ b/crates/mozart-sat-resolver/src/error.rs @@ -0,0 +1,50 @@ +use std::fmt; + +/// A bug in the solver itself (should never happen in normal operation). +/// Equivalent to Composer's SolverBugException. +#[derive(Debug, Clone)] +pub struct SolverBugError { + pub message: String, +} + +impl fmt::Display for SolverBugError { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "Solver bug: {}", self.message) + } +} + +impl std::error::Error for SolverBugError {} + +/// Errors produced by the SAT solver. +#[derive(Debug)] +pub enum SolverError { + /// Internal solver bug (should never happen). + Bug(SolverBugError), + /// The dependency set is unsolvable. Contains problem descriptions. + Unsolvable(Vec<String>), +} + +impl fmt::Display for SolverError { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + SolverError::Bug(e) => write!(f, "{e}"), + SolverError::Unsolvable(problems) => { + for (i, problem) in problems.iter().enumerate() { + if i > 0 { + writeln!(f)?; + } + write!(f, " Problem {}: {problem}", i + 1)?; + } + Ok(()) + } + } + } +} + +impl std::error::Error for SolverError {} + +impl From<SolverBugError> for SolverError { + fn from(e: SolverBugError) -> Self { + SolverError::Bug(e) + } +} |
