track source_order in PathAssignments

This commit is contained in:
Douglas Creager 2025-12-14 20:19:08 -05:00
parent 8e13765b57
commit 298e2dcb4e
1 changed files with 100 additions and 70 deletions

View File

@ -81,7 +81,7 @@ use crate::types::{
BoundTypeVarIdentity, BoundTypeVarInstance, IntersectionType, Type, TypeVarBoundOrConstraints,
UnionType, walk_bound_type_var_type,
};
use crate::{Db, FxOrderSet};
use crate::{Db, FxOrderMap};
/// An extension trait for building constraint sets from [`Option`] values.
pub(crate) trait OptionConstraintsExtension<T> {
@ -1000,8 +1000,9 @@ impl<'db> Node<'db> {
// from it) causes the if_true edge to become impossible. We want to ignore
// impossible paths, and so we treat them as passing the "always satisfied" check.
let constraint = interior.constraint(db);
let source_order = interior.source_order(db);
let true_always_satisfied = path
.walk_edge(db, map, constraint.when_true(), |path, _| {
.walk_edge(db, map, constraint.when_true(), source_order, |path, _| {
interior
.if_true(db)
.is_always_satisfied_inner(db, map, path)
@ -1012,7 +1013,7 @@ impl<'db> Node<'db> {
}
// Ditto for the if_false branch
path.walk_edge(db, map, constraint.when_false(), |path, _| {
path.walk_edge(db, map, constraint.when_false(), source_order, |path, _| {
interior
.if_false(db)
.is_always_satisfied_inner(db, map, path)
@ -1049,8 +1050,9 @@ impl<'db> Node<'db> {
// from it) causes the if_true edge to become impossible. We want to ignore
// impossible paths, and so we treat them as passing the "never satisfied" check.
let constraint = interior.constraint(db);
let source_order = interior.source_order(db);
let true_never_satisfied = path
.walk_edge(db, map, constraint.when_true(), |path, _| {
.walk_edge(db, map, constraint.when_true(), source_order, |path, _| {
interior.if_true(db).is_never_satisfied_inner(db, map, path)
})
.unwrap_or(true);
@ -1059,7 +1061,7 @@ impl<'db> Node<'db> {
}
// Ditto for the if_false branch
path.walk_edge(db, map, constraint.when_false(), |path, _| {
path.walk_edge(db, map, constraint.when_false(), source_order, |path, _| {
interior
.if_false(db)
.is_never_satisfied_inner(db, map, path)
@ -2005,6 +2007,7 @@ impl<'db> InteriorNode<'db> {
path: &mut PathAssignments<'db>,
) -> Node<'db> {
let self_constraint = self.constraint(db);
let self_source_order = self.source_order(db);
if should_remove(self_constraint) {
// If we should remove constraints involving this typevar, then we replace this node
// with the OR of its if_false/if_true edges. That is, the result is true if there's
@ -2012,67 +2015,85 @@ impl<'db> InteriorNode<'db> {
//
// We also have to check if there are any derived facts that depend on the constraint
// we're about to remove. If so, we need to "remember" them by AND-ing them in with the
// corresponding branch. We currently reuse the `source_order` of the constraint being
// removed when we add these derived facts.
//
// TODO: This might not be stable enough, if we add more than one derived fact for this
// constraint. If we still see inconsistent test output, we might need a more complex
// way of tracking source order for derived facts.
let self_source_order = self.source_order(db);
// corresponding branch.
let if_true = path
.walk_edge(db, map, self_constraint.when_true(), |path, new_range| {
let branch = self
.if_true(db)
.walk_edge(
db,
map,
self_constraint.when_true(),
self_source_order,
|path, new_range| {
let branch =
self.if_true(db)
.abstract_one_inner(db, should_remove, map, path);
path.assignments[new_range]
.iter()
.filter(|assignment| {
.filter(|(assignment, _)| {
// Don't add back any derived facts if they are ones that we would have
// removed!
!should_remove(assignment.constraint())
})
.fold(branch, |branch, assignment| {
.fold(branch, |branch, (assignment, source_order)| {
branch.and(
db,
Node::new_satisfied_constraint(db, *assignment, self_source_order),
Node::new_satisfied_constraint(db, *assignment, *source_order),
)
})
})
},
)
.unwrap_or(Node::AlwaysFalse);
let if_false = path
.walk_edge(db, map, self_constraint.when_false(), |path, new_range| {
let branch = self
.if_false(db)
.walk_edge(
db,
map,
self_constraint.when_false(),
self_source_order,
|path, new_range| {
let branch =
self.if_false(db)
.abstract_one_inner(db, should_remove, map, path);
path.assignments[new_range]
.iter()
.filter(|assignment| {
.filter(|(assignment, _)| {
// Don't add back any derived facts if they are ones that we would have
// removed!
!should_remove(assignment.constraint())
})
.fold(branch, |branch, assignment| {
.fold(branch, |branch, (assignment, source_order)| {
branch.and(
db,
Node::new_satisfied_constraint(db, *assignment, self_source_order),
Node::new_satisfied_constraint(db, *assignment, *source_order),
)
})
})
},
)
.unwrap_or(Node::AlwaysFalse);
if_true.or(db, if_false)
} else {
// Otherwise, we abstract the if_false/if_true edges recursively.
let if_true = path
.walk_edge(db, map, self_constraint.when_true(), |path, _| {
.walk_edge(
db,
map,
self_constraint.when_true(),
self_source_order,
|path, _| {
self.if_true(db)
.abstract_one_inner(db, should_remove, map, path)
})
},
)
.unwrap_or(Node::AlwaysFalse);
let if_false = path
.walk_edge(db, map, self_constraint.when_false(), |path, _| {
.walk_edge(
db,
map,
self_constraint.when_false(),
self_source_order,
|path, _| {
self.if_false(db)
.abstract_one_inner(db, should_remove, map, path)
})
},
)
.unwrap_or(Node::AlwaysFalse);
// NB: We cannot use `Node::new` here, because the recursive calls might introduce new
// derived constraints into the result, and those constraints might appear before this
@ -3169,8 +3190,8 @@ impl<'db> SequentMap<'db> {
/// The collection of constraints that we know to be true or false at a certain point when
/// traversing a BDD.
#[derive(Debug, Default)]
struct PathAssignments<'db> {
assignments: FxOrderSet<ConstraintAssignment<'db>>,
pub(crate) struct PathAssignments<'db> {
assignments: FxOrderMap<ConstraintAssignment<'db>, usize>,
}
impl<'db> PathAssignments<'db> {
@ -3201,6 +3222,7 @@ impl<'db> PathAssignments<'db> {
db: &'db dyn Db,
map: &SequentMap<'db>,
assignment: ConstraintAssignment<'db>,
source_order: usize,
f: impl FnOnce(&mut Self, Range<usize>) -> R,
) -> Option<R> {
// Record a snapshot of the assignments that we already knew held — both so that we can
@ -3213,12 +3235,12 @@ impl<'db> PathAssignments<'db> {
target: "ty_python_semantic::types::constraints::PathAssignment",
before = %format_args!(
"[{}]",
self.assignments[..start].iter().map(|assignment| assignment.display(db)).format(", "),
self.assignments[..start].iter().map(|(assignment, _)| assignment.display(db)).format(", "),
),
edge = %assignment.display(db),
"walk edge",
);
let found_conflict = self.add_assignment(db, map, assignment);
let found_conflict = self.add_assignment(db, map, assignment, source_order);
let result = if found_conflict.is_err() {
// If that results in the path now being impossible due to a contradiction, return
// without invoking the callback.
@ -3233,7 +3255,7 @@ impl<'db> PathAssignments<'db> {
target: "ty_python_semantic::types::constraints::PathAssignment",
new = %format_args!(
"[{}]",
self.assignments[start..].iter().map(|assignment| assignment.display(db)).format(", "),
self.assignments[start..].iter().map(|(assignment, _)| assignment.display(db)).format(", "),
),
"new assignments",
);
@ -3248,7 +3270,7 @@ impl<'db> PathAssignments<'db> {
}
fn assignment_holds(&self, assignment: ConstraintAssignment<'db>) -> bool {
self.assignments.contains(&assignment)
self.assignments.contains_key(&assignment)
}
/// Adds a new assignment, along with any derived information that we can infer from the new
@ -3259,26 +3281,34 @@ impl<'db> PathAssignments<'db> {
db: &'db dyn Db,
map: &SequentMap<'db>,
assignment: ConstraintAssignment<'db>,
source_order: usize,
) -> Result<(), PathAssignmentConflict> {
// First add this assignment. If it causes a conflict, return that as an error. If we've
// already know this assignment holds, just return.
if self.assignments.contains(&assignment.negated()) {
if self.assignments.contains_key(&assignment.negated()) {
tracing::trace!(
target: "ty_python_semantic::types::constraints::PathAssignment",
assignment = %assignment.display(db),
facts = %format_args!(
"[{}]",
self.assignments.iter().map(|assignment| assignment.display(db)).format(", "),
self.assignments.iter().map(|(assignment, _)| assignment.display(db)).format(", "),
),
"found contradiction",
);
return Err(PathAssignmentConflict);
}
if !self.assignments.insert(assignment) {
if self.assignments.insert(assignment, source_order).is_some() {
return Ok(());
}
// Then use our sequents to add additional facts that we know to be true.
// Then use our sequents to add additional facts that we know to be true. We currently
// reuse the `source_order` of the "real" constraint passed into `walk_edge` when we add
// these derived facts.
//
// TODO: This might not be stable enough, if we add more than one derived fact for this
// constraint. If we still see inconsistent test output, we might need a more complex
// way of tracking source order for derived facts.
//
// TODO: This is very naive at the moment, partly for expediency, and partly because we
// don't anticipate the sequent maps to be very large. We might consider avoiding the
// brute-force search.
@ -3292,7 +3322,7 @@ impl<'db> PathAssignments<'db> {
ante = %ante.display(db),
facts = %format_args!(
"[{}]",
self.assignments.iter().map(|assignment| assignment.display(db)).format(", "),
self.assignments.iter().map(|(assignment, _)| assignment.display(db)).format(", "),
),
"found contradiction",
);
@ -3311,7 +3341,7 @@ impl<'db> PathAssignments<'db> {
ante2 = %ante2.display(db),
facts = %format_args!(
"[{}]",
self.assignments.iter().map(|assignment| assignment.display(db)).format(", "),
self.assignments.iter().map(|(assignment, _)| assignment.display(db)).format(", "),
),
"found contradiction",
);
@ -3324,7 +3354,7 @@ impl<'db> PathAssignments<'db> {
if self.assignment_holds(ante1.when_true())
&& self.assignment_holds(ante2.when_true())
{
self.add_assignment(db, map, post.when_true())?;
self.add_assignment(db, map, post.when_true(), source_order)?;
}
}
}
@ -3332,7 +3362,7 @@ impl<'db> PathAssignments<'db> {
for (ante, posts) in &map.single_implications {
for post in posts {
if self.assignment_holds(ante.when_true()) {
self.add_assignment(db, map, post.when_true())?;
self.add_assignment(db, map, post.when_true(), source_order)?;
}
}
}