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 28, 2022
1 parent 203f20b commit 35cb938
Showing 1 changed file with 9 additions and 9 deletions.
18 changes: 9 additions & 9 deletions prusti-viper/src/encoder/mir/specifications/constraints.rs
Original file line number Diff line number Diff line change
Expand Up @@ -161,15 +161,7 @@ pub mod trait_bounds {
let all_bounds_satisfied = param_env_constraint
.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)
});
.all(|predicate| env.evaluate_predicate(predicate, param_env_lookup));

trace!("Constraint fulfilled: {all_bounds_satisfied}");
all_bounds_satisfied
Expand Down Expand Up @@ -208,6 +200,14 @@ 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 35cb938

Please sign in to comment.