Skip to content

Commit

Permalink
Move predicate normalization in constraint solver for better debugging
Browse files Browse the repository at this point in the history
  • Loading branch information
vl0w committed Apr 27, 2022
1 parent 47c5a0b commit 3ee584d
Showing 1 changed file with 12 additions and 7 deletions.
19 changes: 12 additions & 7 deletions prusti-viper/src/encoder/mir/specifications/constraints.rs
Original file line number Diff line number Diff line change
Expand Up @@ -162,13 +162,7 @@ pub mod trait_bounds {
.caller_bounds()
.iter()
.all(|predicate| {
// Normalize any associated type projections.
// This needs to be done because ghost constraints might contain "deeply nested"
// associated types, e.g. `T: A<SomeAssocType = <Self as B>::OtherAssocType`
// where `<Self as B>::OtherAssocType` can be normalized to some concrete type.
let normalized_predicate = env.normalize_to(predicate);

env.evaluate_predicate(normalized_predicate, param_env_lookup)
env.evaluate_predicate(predicate, param_env_lookup)
});

trace!("Constraint fulfilled: {all_bounds_satisfied}");
Expand Down Expand Up @@ -208,6 +202,17 @@ pub mod trait_bounds {
param_env
);

// Normalize any associated type projections.
// This needs to be done because ghost constraints might contain "deeply nested"
// associated types, e.g. `T: A<SomeAssocType = <Self as B>::OtherAssocType`
// where `<Self as B>::OtherAssocType` can be normalized to some concrete type.
let param_env = env.normalize_to(param_env);

trace!(
"Constraints after normalization: {:#?}",
param_env
);

param_env
}

Expand Down

0 comments on commit 3ee584d

Please sign in to comment.