Skip to content

Commit

Permalink
refactor: don't store term in structs (#60)
Browse files Browse the repository at this point in the history 
* refactor: dont pass satisfier to prior_cause

* refactor: dont store term in Assignment

* refactor: dont store term in AlmostSatisfied

* refactor: conflict_resolution can return package directly
  • Loading branch information
@Eh2406
Eh2406 authored Nov 15, 2020
1 parent cda126a commit 215e3f4
Show file tree
Hide file tree
Showing 5 changed files with 32 additions and 61 deletions.
4 changes: 1 addition & 3 deletions src/internal/assignment.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,8 +24,6 @@ pub enum Assignment<P: Package, V: Version> {
Derivation {
/// The package corresponding to the derivation.
package: P,
/// Term of the derivation.
term: Term<V>,
/// Incompatibility cause of the derivation.
cause: Incompatibility<P, V>,
},
Expand All @@ -46,7 +44,7 @@ impl<P: Package, V: Version> Assignment<P, V> {
pub fn as_term(&self) -> Term<V> {
match &self {
Self::Decision { version, .. } => Term::exact(version.clone()),
Self::Derivation { term, .. } => term.clone(),
Self::Derivation { package, cause } => cause.get(&package).unwrap().negate(),
}
}
}
43 changes: 13 additions & 30 deletions src/internal/core.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,26 +77,17 @@ impl<P: Package, V: Version> State<P, V> {
// If the partial solution satisfies the incompatibility
// we must perform conflict resolution.
Relation::Satisfied => {
let root_cause = self.conflict_resolution(&incompat)?;
// root_cause is guaranteed to be almost satisfied by the partial solution
// according to PubGrub documentation.
match self.partial_solution.relation(&root_cause) {
Relation::AlmostSatisfied((package_almost, term)) => {
changed = vec![package_almost.clone()];
// Add (not term) to the partial solution with incompat as cause.
self.partial_solution.add_derivation(package_almost, term.negate(), root_cause);
}
_ => return Err(PubGrubError::Failure("This should never happen, root_cause is guaranteed to be almost satisfied by the partial solution".into())),
}
let (package_almost, root_cause) = self.conflict_resolution(&incompat)?;
changed = vec![package_almost.clone()];
// Add to the partial solution with incompat as cause.
self.partial_solution
.add_derivation(package_almost, root_cause);
}
Relation::AlmostSatisfied((package_almost, term)) => {
Relation::AlmostSatisfied(package_almost) => {
changed.push(package_almost.clone());
// Add (not term) to the partial solution with incompat as cause.
self.partial_solution.add_derivation(
package_almost,
term.negate(),
incompat.clone(),
);
self.partial_solution
.add_derivation(package_almost, incompat.clone());
}
_ => {}
}
Expand All @@ -115,7 +106,7 @@ impl<P: Package, V: Version> State<P, V> {
fn conflict_resolution(
&mut self,
incompatibility: &Incompatibility<P, V>,
) -> Result<Incompatibility<P, V>, PubGrubError<P, V>> {
) -> Result<(P, Incompatibility<P, V>), PubGrubError<P, V>> {
let mut current_incompat = incompatibility.clone();
let mut current_incompat_changed = false;
loop {
Expand All @@ -128,38 +119,30 @@ impl<P: Package, V: Version> State<P, V> {
.partial_solution
.find_satisfier_and_previous_satisfier_level(&current_incompat);
match satisfier {
Decision { .. } => {
Decision { package, .. } => {
self.backtrack(
current_incompat.clone(),
current_incompat_changed,
previous_satisfier_level,
);
return Ok(current_incompat);
return Ok((package, current_incompat));
}
Derivation {
cause,
term,
package,
} => {
Derivation { cause, package } => {
if previous_satisfier_level != satisfier_level {
self.backtrack(
current_incompat.clone(),
current_incompat_changed,
previous_satisfier_level,
);
return Ok(current_incompat);
return Ok((package, current_incompat));
} else {
let id = self.incompatibility_store.len();
let prior_cause = Incompatibility::prior_cause(
id,
&current_incompat,
&cause,
&package,
&term,
);
// eprintln!("\ncause 1: {}", &current_incompat);
// eprintln!("cause 2: {}", &cause);
// eprintln!("prior cause: {}\n", &prior_cause);
self.incompatibility_store.push(prior_cause.clone());
current_incompat = prior_cause;
current_incompat_changed = true;
Expand Down
34 changes: 13 additions & 21 deletions src/internal/incompatibility.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ pub enum Relation<P: Package, V: Version> {
Contradicted(PackageTerm<P, V>),
/// If S satisfies all but one of I's terms and is inconclusive for the remaining term,
/// we say S "almost satisfies" I and we call the remaining term the "unsatisfied term".
AlmostSatisfied(PackageTerm<P, V>),
AlmostSatisfied(P),
/// Otherwise, we say that their relation is inconclusive.
Inconclusive,
}
Expand Down Expand Up @@ -203,27 +203,20 @@ impl<P: Package, V: Version> Incompatibility<P, V> {
}

/// Prior cause of two incompatibilities using the rule of resolution.
pub fn prior_cause(
id: usize,
incompat: &Self,
satisfier_cause: &Self,
package: &P,
satisfier: &Term<V>,
) -> Self {
pub fn prior_cause(id: usize, incompat: &Self, satisfier_cause: &Self, package: &P) -> Self {
let kind = Kind::DerivedFrom(incompat.id, satisfier_cause.id);
let mut t1 = incompat.package_terms.clone();
let mut t2 = satisfier_cause.package_terms.clone();
t1.remove(package);
t2.remove(package);
let mut prior_cause_terms = Self::intersection(&t1, &t2);
let term = incompat.package_terms.get(package).unwrap();
let p_term = term.union(&satisfier.negate());
if p_term != Term::any() {
prior_cause_terms.insert(package.clone(), p_term);
let mut incompat1 = incompat.package_terms.clone();
let mut incompat2 = satisfier_cause.package_terms.clone();
let t1 = incompat1.remove(package).unwrap();
let t2 = incompat2.remove(package).unwrap();
let mut package_terms = Self::intersection(&incompat1, &incompat2);
let term = t1.union(&t2);
if term != Term::any() {
package_terms.insert(package.clone(), term);
}
Self {
id,
package_terms: prior_cause_terms,
package_terms,
kind,
}
}
Expand All @@ -244,8 +237,7 @@ impl<P: Package, V: Version> Incompatibility<P, V> {
// but we systematically remove those from incompatibilities
// so we're safe on that front.
if relation == Relation::Satisfied {
relation =
Relation::AlmostSatisfied((package.clone(), incompat_term.clone()));
relation = Relation::AlmostSatisfied(package.clone());
} else {
relation = Relation::Inconclusive;
}
Expand Down Expand Up @@ -379,7 +371,7 @@ pub mod tests {
i3.insert("p1", t1);
i3.insert("p3", t3);

let i_resolution = Incompatibility::prior_cause(0, &i1, &i2, &"p2", &t2.negate());
let i_resolution = Incompatibility::prior_cause(0, &i1, &i2, &"p2");
assert_eq!(i_resolution.package_terms, i3);
}

Expand Down
4 changes: 3 additions & 1 deletion src/internal/memory.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,9 @@ impl<P: Package, V: Version> Memory<P, V> {
pub fn add_assignment(&mut self, assignment: &Assignment<P, V>) {
match assignment {
Decision { package, version } => self.add_decision(package.clone(), version.clone()),
Derivation { package, term, .. } => self.add_derivation(package.clone(), term.clone()),
Derivation { package, cause } => {
self.add_derivation(package.clone(), cause.get(&package).unwrap().negate())
}
}
}

Expand Down
8 changes: 2 additions & 6 deletions src/internal/partial_solution.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -88,12 +88,8 @@ impl<P: Package, V: Version> PartialSolution<P, V> {
}

/// Add a derivation to the partial solution.
pub fn add_derivation(&mut self, package: P, term: Term<V>, cause: Incompatibility<P, V>) {
self.add_assignment(Derivation {
package,
term,
cause,
});
pub fn add_derivation(&mut self, package: P, cause: Incompatibility<P, V>) {
self.add_assignment(Derivation { package, cause });
}

/// If a partial solution has, for every positive derivation,
Expand Down

0 comments on commit 215e3f4

Please sign in to comment.