@@ -143,6 +143,8 @@ pub enum SatisfierSearch<P: Package, VS: VersionSet> {
143
143
} ,
144
144
}
145
145
146
+ type SatisfiedMap < ' i , P , VS > = SmallMap < & ' i P , ( Option < IncompId < P , VS > > , u32 , DecisionLevel ) > ;
147
+
146
148
impl < P : Package , VS : VersionSet , Priority : Ord + Clone > PartialSolution < P , VS , Priority > {
147
149
/// Initialize an empty PartialSolution.
148
150
pub fn empty ( ) -> Self {
@@ -390,37 +392,33 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
390
392
}
391
393
392
394
/// Figure out if the satisfier and previous satisfier are of different decision levels.
393
- pub fn satisfier_search (
395
+ pub fn satisfier_search < ' i > (
394
396
& self ,
395
- incompat : & Incompatibility < P , VS > ,
397
+ incompat : & ' i Incompatibility < P , VS > ,
396
398
store : & Arena < Incompatibility < P , VS > > ,
397
- ) -> ( P , SatisfierSearch < P , VS > ) {
399
+ ) -> ( & ' i P , SatisfierSearch < P , VS > ) {
398
400
let satisfied_map = Self :: find_satisfier ( incompat, & self . package_assignments ) ;
399
- let ( satisfier_package, & ( satisfier_index , _, satisfier_decision_level) ) = satisfied_map
401
+ let ( & satisfier_package, & ( satisfier_cause , _, satisfier_decision_level) ) = satisfied_map
400
402
. iter ( )
401
403
. max_by_key ( |( _p, ( _, global_index, _) ) | global_index)
402
404
. unwrap ( ) ;
403
- let satisfier_package = satisfier_package. clone ( ) ;
404
405
let previous_satisfier_level = Self :: find_previous_satisfier (
405
406
incompat,
406
- & satisfier_package,
407
+ satisfier_package,
407
408
satisfied_map,
408
409
& self . package_assignments ,
409
410
store,
410
411
) ;
411
- if previous_satisfier_level < satisfier_decision_level {
412
- let search_result = SatisfierSearch :: DifferentDecisionLevels {
413
- previous_satisfier_level,
414
- } ;
415
- ( satisfier_package, search_result)
412
+ let search_result = if previous_satisfier_level >= satisfier_decision_level {
413
+ SatisfierSearch :: SameDecisionLevels {
414
+ satisfier_cause : satisfier_cause. unwrap ( ) ,
415
+ }
416
416
} else {
417
- let satisfier_pa = self . package_assignments . get ( & satisfier_package) . unwrap ( ) ;
418
- let dd = & satisfier_pa. dated_derivations [ satisfier_index] ;
419
- let search_result = SatisfierSearch :: SameDecisionLevels {
420
- satisfier_cause : dd. cause ,
421
- } ;
422
- ( satisfier_package, search_result)
423
- }
417
+ SatisfierSearch :: DifferentDecisionLevels {
418
+ previous_satisfier_level,
419
+ }
420
+ } ;
421
+ ( satisfier_package, search_result)
424
422
}
425
423
426
424
/// A satisfier is the earliest assignment in partial solution such that the incompatibility
@@ -432,52 +430,51 @@ impl<P: Package, VS: VersionSet, Priority: Ord + Clone> PartialSolution<P, VS, P
432
430
/// Question: This is possible since we added a "global_index" to every dated_derivation.
433
431
/// It would be nice if we could get rid of it, but I don't know if then it will be possible
434
432
/// to return a coherent previous_satisfier_level.
435
- fn find_satisfier (
436
- incompat : & Incompatibility < P , VS > ,
433
+ fn find_satisfier < ' i > (
434
+ incompat : & ' i Incompatibility < P , VS > ,
437
435
package_assignments : & FnvIndexMap < P , PackageAssignments < P , VS > > ,
438
- ) -> SmallMap < P , ( usize , u32 , DecisionLevel ) > {
436
+ ) -> SatisfiedMap < ' i , P , VS > {
439
437
let mut satisfied = SmallMap :: Empty ;
440
438
for ( package, incompat_term) in incompat. iter ( ) {
441
439
let pa = package_assignments. get ( package) . expect ( "Must exist" ) ;
442
- satisfied. insert (
443
- package. clone ( ) ,
444
- pa. satisfier ( package, incompat_term, & Term :: any ( ) ) ,
445
- ) ;
440
+ satisfied. insert ( package, pa. satisfier ( package, & incompat_term. negate ( ) ) ) ;
446
441
}
447
442
satisfied
448
443
}
449
444
450
445
/// Earliest assignment in the partial solution before satisfier
451
446
/// such that incompatibility is satisfied by the partial solution up to
452
447
/// and including that assignment plus satisfier.
453
- fn find_previous_satisfier (
448
+ fn find_previous_satisfier < ' i > (
454
449
incompat : & Incompatibility < P , VS > ,
455
- satisfier_package : & P ,
456
- mut satisfied_map : SmallMap < P , ( usize , u32 , DecisionLevel ) > ,
450
+ satisfier_package : & ' i P ,
451
+ mut satisfied_map : SatisfiedMap < ' i , P , VS > ,
457
452
package_assignments : & FnvIndexMap < P , PackageAssignments < P , VS > > ,
458
453
store : & Arena < Incompatibility < P , VS > > ,
459
454
) -> DecisionLevel {
460
455
// First, let's retrieve the previous derivations and the initial accum_term.
461
456
let satisfier_pa = package_assignments. get ( satisfier_package) . unwrap ( ) ;
462
- let ( satisfier_index , _gidx, _dl) = satisfied_map. get_mut ( satisfier_package) . unwrap ( ) ;
457
+ let ( satisfier_cause , _gidx, _dl) = satisfied_map. get ( & satisfier_package) . unwrap ( ) ;
463
458
464
- let accum_term = if * satisfier_index == satisfier_pa. dated_derivations . len ( ) {
459
+ let accum_term = if let & Some ( cause) = satisfier_cause {
460
+ store[ cause] . get ( satisfier_package) . unwrap ( ) . negate ( )
461
+ } else {
465
462
match & satisfier_pa. assignments_intersection {
466
463
AssignmentsIntersection :: Derivations ( _) => panic ! ( "must be a decision" ) ,
467
464
AssignmentsIntersection :: Decision ( ( _, _, term) ) => term. clone ( ) ,
468
465
}
469
- } else {
470
- let dd = & satisfier_pa. dated_derivations [ * satisfier_index] ;
471
- store[ dd. cause ] . get ( satisfier_package) . unwrap ( ) . negate ( )
472
466
} ;
473
467
474
468
let incompat_term = incompat
475
469
. get ( satisfier_package)
476
470
. expect ( "satisfier package not in incompat" ) ;
477
471
478
472
satisfied_map. insert (
479
- satisfier_package. clone ( ) ,
480
- satisfier_pa. satisfier ( satisfier_package, incompat_term, & accum_term) ,
473
+ satisfier_package,
474
+ satisfier_pa. satisfier (
475
+ satisfier_package,
476
+ & accum_term. intersection ( & incompat_term. negate ( ) ) ,
477
+ ) ,
481
478
) ;
482
479
483
480
// Finally, let's identify the decision level of that previous satisfier.
@@ -497,44 +494,34 @@ impl<P: Package, VS: VersionSet> PackageAssignments<P, VS> {
497
494
fn satisfier (
498
495
& self ,
499
496
package : & P ,
500
- incompat_term : & Term < VS > ,
501
497
start_term : & Term < VS > ,
502
- ) -> ( usize , u32 , DecisionLevel ) {
498
+ ) -> ( Option < IncompId < P , VS > > , u32 , DecisionLevel ) {
499
+ let empty = Term :: empty ( ) ;
503
500
// Indicate if we found a satisfier in the list of derivations, otherwise it will be the decision.
504
- for ( idx, dated_derivation) in self . dated_derivations . iter ( ) . enumerate ( ) {
505
- if dated_derivation
506
- . accumulated_intersection
507
- . intersection ( start_term)
508
- . subset_of ( incompat_term)
509
- {
510
- // We found the derivation causing satisfaction.
511
- return (
512
- idx,
513
- dated_derivation. global_index ,
514
- dated_derivation. decision_level ,
515
- ) ;
516
- }
501
+ let idx = self
502
+ . dated_derivations
503
+ . as_slice ( )
504
+ . partition_point ( |dd| dd. accumulated_intersection . intersection ( start_term) != empty) ;
505
+ if let Some ( dd) = self . dated_derivations . get ( idx) {
506
+ debug_assert_eq ! ( dd. accumulated_intersection. intersection( start_term) , empty) ;
507
+ return ( Some ( dd. cause ) , dd. global_index , dd. decision_level ) ;
517
508
}
518
509
// If it wasn't found in the derivations,
519
510
// it must be the decision which is last (if called in the right context).
520
511
match & self . assignments_intersection {
521
- AssignmentsIntersection :: Decision ( ( global_index, _, _) ) => (
522
- self . dated_derivations . len ( ) ,
523
- * global_index,
524
- self . highest_decision_level ,
525
- ) ,
512
+ AssignmentsIntersection :: Decision ( ( global_index, _, _) ) => {
513
+ ( None , * global_index, self . highest_decision_level )
514
+ }
526
515
AssignmentsIntersection :: Derivations ( accumulated_intersection) => {
527
516
unreachable ! (
528
517
concat!(
529
518
"while processing package {}: " ,
530
- "accum_term = {} isn't a subset of incompat_term = {}, " ,
519
+ "accum_term = {} has overlap with incompat_term = {}, " ,
531
520
"which means the last assignment should have been a decision, " ,
532
521
"but instead it was a derivation. This shouldn't be possible! " ,
533
522
"(Maybe your Version ordering is broken?)"
534
523
) ,
535
- package,
536
- accumulated_intersection. intersection( start_term) ,
537
- incompat_term
524
+ package, accumulated_intersection, start_term
538
525
)
539
526
}
540
527
}
0 commit comments