[red-knot] Rename constraint to predicate (#16382)

In https://github.com/astral-sh/ruff/pull/16306#discussion_r1966290700,
@carljm pointed out that #16306 introduced a terminology problem, with
too many things called a "constraint". This is a follow-up PR that
renames `Constraint` to `Predicate` to hopefully clear things up a bit.
So now we have that:

- a _predicate_ is a Python expression that might influence type
inference
- a _narrowing constraint_ is a list of predicates that constraint the
type of a binding that is visible at a use
- a _visibility constraint_ is a ternary formula of predicates that
define whether a binding is visible or a statement is reachable

This is a pure renaming, with no behavioral changes.

crates/red_knot_python_semantic/src/semantic_index.rs

@@ -25,10 +25,10 @@ use crate::Db;
 pub mod ast_ids;
 pub mod attribute_assignment;
 mod builder;
-pub(crate) mod constraint;
 pub mod definition;
 pub mod expression;
 mod narrowing_constraints;
+pub(crate) mod predicate;
 pub mod symbol;
 mod use_def;
 mod visibility_constraints;

crates/red_knot_python_semantic/src/semantic_index/builder.rs

@@ -15,9 +15,6 @@ use crate::module_name::ModuleName;
 use crate::semantic_index::ast_ids::node_key::ExpressionNodeKey;
 use crate::semantic_index::ast_ids::AstIdsBuilder;
 use crate::semantic_index::attribute_assignment::{AttributeAssignment, AttributeAssignments};
-use crate::semantic_index::constraint::{
-    Constraint, ConstraintNode, PatternConstraint, PatternConstraintKind, ScopedConstraintId,
-};
 use crate::semantic_index::definition::{
     AssignmentDefinitionNodeRef, ComprehensionDefinitionNodeRef, Definition, DefinitionCategory,
     DefinitionNodeKey, DefinitionNodeRef, ExceptHandlerDefinitionNodeRef, ForStmtDefinitionNodeRef,
@@ -25,6 +22,9 @@ use crate::semantic_index::definition::{
     WithItemDefinitionNodeRef,
 };
 use crate::semantic_index::expression::{Expression, ExpressionKind};
+use crate::semantic_index::predicate::{
+    PatternPredicate, PatternPredicateKind, Predicate, PredicateNode, ScopedPredicateId,
+};
 use crate::semantic_index::symbol::{
     FileScopeId, NodeWithScopeKey, NodeWithScopeRef, Scope, ScopeId, ScopeKind, ScopedSymbolId,
     SymbolTableBuilder,
@@ -385,50 +385,60 @@ impl<'db> SemanticIndexBuilder<'db> {
         definition
     }
 
-    fn record_expression_constraint(&mut self, constraint_node: &ast::Expr) -> Constraint<'db> {
+    fn record_expression_narrowing_constraint(
-        let constraint = self.build_constraint(constraint_node);
+        &mut self,
-        self.record_constraint(constraint);
+        precide_node: &ast::Expr,
-        constraint
+    ) -> Predicate<'db> {
+        let predicate = self.build_predicate(precide_node);
+        self.record_narrowing_constraint(predicate);
+        predicate
     }
 
-    fn build_constraint(&mut self, constraint_node: &ast::Expr) -> Constraint<'db> {
+    fn build_predicate(&mut self, predicate_node: &ast::Expr) -> Predicate<'db> {
-        let expression = self.add_standalone_expression(constraint_node);
+        let expression = self.add_standalone_expression(predicate_node);
-        Constraint {
+        Predicate {
-            node: ConstraintNode::Expression(expression),
+            node: PredicateNode::Expression(expression),
             is_positive: true,
         }
     }
 
-    /// Adds a new constraint to the list of all constraints, but does not record it. Returns the
+    /// Adds a new predicate to the list of all predicates, but does not record it. Returns the
-    /// constraint ID for later recording using [`SemanticIndexBuilder::record_constraint_id`].
+    /// predicate ID for later recording using
-    fn add_constraint(&mut self, constraint: Constraint<'db>) -> ScopedConstraintId {
+    /// [`SemanticIndexBuilder::record_narrowing_constraint_id`].
-        self.current_use_def_map_mut().add_constraint(constraint)
+    fn add_predicate(&mut self, predicate: Predicate<'db>) -> ScopedPredicateId {
+        self.current_use_def_map_mut().add_predicate(predicate)
     }
 
-    /// Negates a constraint and adds it to the list of all constraints, does not record it.
+    /// Negates a predicate and adds it to the list of all predicates, does not record it.
-    fn add_negated_constraint(&mut self, constraint: Constraint<'db>) -> ScopedConstraintId {
+    fn add_negated_predicate(&mut self, predicate: Predicate<'db>) -> ScopedPredicateId {
-        let negated = Constraint {
+        let negated = Predicate {
-            node: constraint.node,
+            node: predicate.node,
             is_positive: false,
         };
-        self.current_use_def_map_mut().add_constraint(negated)
+        self.current_use_def_map_mut().add_predicate(negated)
     }
 
-    /// Records a previously added constraint by adding it to all live bindings.
+    /// Records a previously added narrowing constraint by adding it to all live bindings.
-    fn record_constraint_id(&mut self, constraint: ScopedConstraintId) {
+    fn record_narrowing_constraint_id(&mut self, predicate: ScopedPredicateId) {
         self.current_use_def_map_mut()
-            .record_constraint_id(constraint);
+            .record_narrowing_constraint(predicate);
     }
 
-    /// Adds and records a constraint, i.e. adds it to all live bindings.
+    /// Adds and records a narrowing constraint, i.e. adds it to all live bindings.
-    fn record_constraint(&mut self, constraint: Constraint<'db>) {
+    fn record_narrowing_constraint(&mut self, predicate: Predicate<'db>) {
-        self.current_use_def_map_mut().record_constraint(constraint);
+        let use_def = self.current_use_def_map_mut();
+        let predicate_id = use_def.add_predicate(predicate);
+        use_def.record_narrowing_constraint(predicate_id);
     }
 
-    /// Negates the given constraint and then adds it to all live bindings.
+    /// Negates the given predicate and then adds it as a narrowing constraint to all live
-    fn record_negated_constraint(&mut self, constraint: Constraint<'db>) -> ScopedConstraintId {
+    /// bindings.
-        let id = self.add_negated_constraint(constraint);
+    fn record_negated_narrowing_constraint(
-        self.record_constraint_id(id);
+        &mut self,
+        predicate: Predicate<'db>,
+    ) -> ScopedPredicateId {
+        let id = self.add_negated_predicate(predicate);
+        self.record_narrowing_constraint_id(id);
         id
     }
 
@@ -454,12 +464,12 @@ impl<'db> SemanticIndexBuilder<'db> {
     /// Records a visibility constraint by applying it to all live bindings and declarations.
     fn record_visibility_constraint(
         &mut self,
-        constraint: Constraint<'db>,
+        predicate: Predicate<'db>,
     ) -> ScopedVisibilityConstraintId {
-        let constraint_id = self.current_use_def_map_mut().add_constraint(constraint);
+        let predicate_id = self.current_use_def_map_mut().add_predicate(predicate);
         let id = self
             .current_visibility_constraints_mut()
-            .add_atom(constraint_id);
+            .add_atom(predicate_id);
         self.record_visibility_constraint_id(id);
         id
     }
@@ -526,12 +536,12 @@ impl<'db> SemanticIndexBuilder<'db> {
         }
     }
 
-    fn add_pattern_constraint(
+    fn add_pattern_narrowing_constraint(
         &mut self,
         subject: Expression<'db>,
         pattern: &ast::Pattern,
         guard: Option<&ast::Expr>,
-    ) -> Constraint<'db> {
+    ) -> Predicate<'db> {
         // This is called for the top-level pattern of each match arm. We need to create a
         // standalone expression for each arm of a match statement, since they can introduce
         // constraints on the match subject. (Or more accurately, for the match arm's pattern,
@@ -548,19 +558,19 @@ impl<'db> SemanticIndexBuilder<'db> {
         let kind = match pattern {
             ast::Pattern::MatchValue(pattern) => {
                 let value = self.add_standalone_expression(&pattern.value);
-                PatternConstraintKind::Value(value, guard)
+                PatternPredicateKind::Value(value, guard)
             }
             ast::Pattern::MatchSingleton(singleton) => {
-                PatternConstraintKind::Singleton(singleton.value, guard)
+                PatternPredicateKind::Singleton(singleton.value, guard)
             }
             ast::Pattern::MatchClass(pattern) => {
                 let cls = self.add_standalone_expression(&pattern.cls);
-                PatternConstraintKind::Class(cls, guard)
+                PatternPredicateKind::Class(cls, guard)
             }
-            _ => PatternConstraintKind::Unsupported,
+            _ => PatternPredicateKind::Unsupported,
         };
 
-        let pattern_constraint = PatternConstraint::new(
+        let pattern_predicate = PatternPredicate::new(
             self.db,
             self.file,
             self.current_scope(),
@@ -568,12 +578,12 @@ impl<'db> SemanticIndexBuilder<'db> {
             kind,
             countme::Count::default(),
         );
-        let constraint = Constraint {
+        let predicate = Predicate {
-            node: ConstraintNode::Pattern(pattern_constraint),
+            node: PredicateNode::Pattern(pattern_predicate),
             is_positive: true,
         };
-        self.current_use_def_map_mut().record_constraint(constraint);
+        self.record_narrowing_constraint(predicate);
-        constraint
+        predicate
     }
 
     /// Record an expression that needs to be a Salsa ingredient, because we need to infer its type
@@ -1116,10 +1126,10 @@ where
             ast::Stmt::If(node) => {
                 self.visit_expr(&node.test);
                 let mut no_branch_taken = self.flow_snapshot();
-                let mut last_constraint = self.record_expression_constraint(&node.test);
+                let mut last_predicate = self.record_expression_narrowing_constraint(&node.test);
                 self.visit_body(&node.body);
 
-                let visibility_constraint_id = self.record_visibility_constraint(last_constraint);
+                let visibility_constraint_id = self.record_visibility_constraint(last_predicate);
                 let mut vis_constraints = vec![visibility_constraint_id];
 
                 let mut post_clauses: Vec<FlowSnapshot> = vec![];
@@ -1145,14 +1155,14 @@ where
                     // we can only take an elif/else branch if none of the previous ones were
                     // taken
                     self.flow_restore(no_branch_taken.clone());
-                    self.record_negated_constraint(last_constraint);
+                    self.record_negated_narrowing_constraint(last_predicate);
 
-                    let elif_constraint = if let Some(elif_test) = clause_test {
+                    let elif_predicate = if let Some(elif_test) = clause_test {
                         self.visit_expr(elif_test);
                         // A test expression is evaluated whether the branch is taken or not
                         no_branch_taken = self.flow_snapshot();
-                        let constraint = self.record_expression_constraint(elif_test);
+                        let predicate = self.record_expression_narrowing_constraint(elif_test);
-                        Some(constraint)
+                        Some(predicate)
                     } else {
                         None
                     };
@@ -1162,9 +1172,9 @@ where
                     for id in &vis_constraints {
                         self.record_negated_visibility_constraint(*id);
                     }
-                    if let Some(elif_constraint) = elif_constraint {
+                    if let Some(elif_predicate) = elif_predicate {
-                        last_constraint = elif_constraint;
+                        last_predicate = elif_predicate;
-                        let id = self.record_visibility_constraint(elif_constraint);
+                        let id = self.record_visibility_constraint(elif_predicate);
                         vis_constraints.push(id);
                     }
                 }
@@ -1184,19 +1194,19 @@ where
                 self.visit_expr(test);
 
                 let pre_loop = self.flow_snapshot();
-                let constraint = self.record_expression_constraint(test);
+                let predicate = self.record_expression_narrowing_constraint(test);
 
                 // We need multiple copies of the visibility constraint for the while condition,
                 // since we need to model situations where the first evaluation of the condition
                 // returns True, but a later evaluation returns False.
-                let first_constraint_id = self.current_use_def_map_mut().add_constraint(constraint);
+                let first_predicate_id = self.current_use_def_map_mut().add_predicate(predicate);
-                let later_constraint_id = self.current_use_def_map_mut().add_constraint(constraint);
+                let later_predicate_id = self.current_use_def_map_mut().add_predicate(predicate);
                 let first_vis_constraint_id = self
                     .current_visibility_constraints_mut()
-                    .add_atom(first_constraint_id);
+                    .add_atom(first_predicate_id);
                 let later_vis_constraint_id = self
                     .current_visibility_constraints_mut()
-                    .add_atom(later_constraint_id);
+                    .add_atom(later_predicate_id);
 
                 // Save aside any break states from an outer loop
                 let saved_break_states = std::mem::take(&mut self.loop_break_states);
@@ -1234,7 +1244,7 @@ where
                 self.flow_restore(pre_loop.clone());
                 self.record_negated_visibility_constraint(first_vis_constraint_id);
                 self.flow_merge(post_body);
-                self.record_negated_constraint(constraint);
+                self.record_negated_narrowing_constraint(predicate);
                 self.visit_body(orelse);
                 self.record_negated_visibility_constraint(later_vis_constraint_id);
 
@@ -1383,7 +1393,7 @@ where
                     self.current_match_case = Some(CurrentMatchCase::new(&case.pattern));
                     self.visit_pattern(&case.pattern);
                     self.current_match_case = None;
-                    let constraint_id = self.add_pattern_constraint(
+                    let predicate = self.add_pattern_narrowing_constraint(
                         subject_expr,
                         &case.pattern,
                         case.guard.as_deref(),
@@ -1395,7 +1405,7 @@ where
                     for id in &vis_constraints {
                         self.record_negated_visibility_constraint(*id);
                     }
-                    let vis_constraint_id = self.record_visibility_constraint(constraint_id);
+                    let vis_constraint_id = self.record_visibility_constraint(predicate);
                     vis_constraints.push(vis_constraint_id);
                 }
 
@@ -1694,13 +1704,13 @@ where
             }) => {
                 self.visit_expr(test);
                 let pre_if = self.flow_snapshot();
-                let constraint = self.record_expression_constraint(test);
+                let predicate = self.record_expression_narrowing_constraint(test);
                 self.visit_expr(body);
-                let visibility_constraint = self.record_visibility_constraint(constraint);
+                let visibility_constraint = self.record_visibility_constraint(predicate);
                 let post_body = self.flow_snapshot();
                 self.flow_restore(pre_if.clone());
 
-                self.record_negated_constraint(constraint);
+                self.record_negated_narrowing_constraint(predicate);
                 self.visit_expr(orelse);
                 self.record_negated_visibility_constraint(visibility_constraint);
                 self.flow_merge(post_body);
@@ -1776,14 +1786,14 @@ where
                     // For the last value, we don't need to model control flow. There is short-circuiting
                     // anymore.
                     if index < values.len() - 1 {
-                        let constraint = self.build_constraint(value);
+                        let predicate = self.build_predicate(value);
-                        let constraint_id = match op {
+                        let predicate_id = match op {
-                            ast::BoolOp::And => self.add_constraint(constraint),
+                            ast::BoolOp::And => self.add_predicate(predicate),
-                            ast::BoolOp::Or => self.add_negated_constraint(constraint),
+                            ast::BoolOp::Or => self.add_negated_predicate(predicate),
                         };
                         let visibility_constraint = self
                             .current_visibility_constraints_mut()
-                            .add_atom(constraint_id);
+                            .add_atom(predicate_id);
 
                         let after_expr = self.flow_snapshot();
 
@@ -1801,7 +1811,7 @@ where
                         // the application of the visibility constraint until after the expression
                         // has been evaluated, so we only push it onto the stack here.
                         self.flow_restore(after_expr);
-                        self.record_constraint_id(constraint_id);
+                        self.record_narrowing_constraint_id(predicate_id);
                         visibility_constraints.push(visibility_constraint);
                     }
                 }

crates/red_knot_python_semantic/src/semantic_index/constraint.rs

@@ -1,77 +0,0 @@
-use ruff_db::files::File;
-use ruff_index::{newtype_index, IndexVec};
-use ruff_python_ast::Singleton;
-
-use crate::db::Db;
-use crate::semantic_index::expression::Expression;
-use crate::semantic_index::symbol::{FileScopeId, ScopeId};
-
-// A scoped identifier for each `Constraint` in a scope.
-#[newtype_index]
-#[derive(Ord, PartialOrd)]
-pub(crate) struct ScopedConstraintId;
-
-// A collection of constraints. This is currently stored in `UseDefMap`, which means we maintain a
-// separate set of constraints for each scope in a file.
-pub(crate) type Constraints<'db> = IndexVec<ScopedConstraintId, Constraint<'db>>;
-
-#[derive(Debug, Default)]
-pub(crate) struct ConstraintsBuilder<'db> {
-    constraints: IndexVec<ScopedConstraintId, Constraint<'db>>,
-}
-
-impl<'db> ConstraintsBuilder<'db> {
-    /// Adds a constraint. Note that we do not deduplicate constraints. If you add a `Constraint`
-    /// more than once, you will get distinct `ScopedConstraintId`s for each one. (This lets you
-    /// model constraint expressions that might evaluate to different values at different points of
-    /// execution.)
-    pub(crate) fn add_constraint(&mut self, constraint: Constraint<'db>) -> ScopedConstraintId {
-        self.constraints.push(constraint)
-    }
-
-    pub(crate) fn build(mut self) -> Constraints<'db> {
-        self.constraints.shrink_to_fit();
-        self.constraints
-    }
-}
-
-#[derive(Clone, Copy, Debug, Hash, PartialEq, Eq, salsa::Update)]
-pub(crate) struct Constraint<'db> {
-    pub(crate) node: ConstraintNode<'db>,
-    pub(crate) is_positive: bool,
-}
-
-#[derive(Clone, Copy, Debug, Hash, PartialEq, Eq, salsa::Update)]
-pub(crate) enum ConstraintNode<'db> {
-    Expression(Expression<'db>),
-    Pattern(PatternConstraint<'db>),
-}
-
-/// Pattern kinds for which we support type narrowing and/or static visibility analysis.
-#[derive(Debug, Clone, Hash, PartialEq, salsa::Update)]
-pub(crate) enum PatternConstraintKind<'db> {
-    Singleton(Singleton, Option<Expression<'db>>),
-    Value(Expression<'db>, Option<Expression<'db>>),
-    Class(Expression<'db>, Option<Expression<'db>>),
-    Unsupported,
-}
-
-#[salsa::tracked]
-pub(crate) struct PatternConstraint<'db> {
-    pub(crate) file: File,
-
-    pub(crate) file_scope: FileScopeId,
-
-    pub(crate) subject: Expression<'db>,
-
-    #[return_ref]
-    pub(crate) kind: PatternConstraintKind<'db>,
-
-    count: countme::Count<PatternConstraint<'static>>,
-}
-
-impl<'db> PatternConstraint<'db> {
-    pub(crate) fn scope(self, db: &'db dyn Db) -> ScopeId<'db> {
-        self.file_scope(db).to_scope_id(db, self.file(db))
-    }
-}

crates/red_knot_python_semantic/src/semantic_index/narrowing_constraints.rs

@@ -1,77 +1,77 @@
 //! # Narrowing constraints
 //!
-//! When building a semantic index for a file, we associate each binding with _narrowing
+//! When building a semantic index for a file, we associate each binding with a _narrowing
-//! constraints_. The narrowing constraint is used to constrain the type of the binding's symbol.
+//! constraint_, which constrains the type of the binding's symbol. Note that a binding can be
-//! Note that a binding can be associated with a different narrowing constraint at different points
+//! associated with a different narrowing constraint at different points in a file. See the
-//! in a file. See the [`use_def`][crate::semantic_index::use_def] module for more details.
+//! [`use_def`][crate::semantic_index::use_def] module for more details.
 //!
 //! This module defines how narrowing constraints are stored internally.
 //!
-//! A _narrowing constraint_ consists of a list of _clauses_, each of which corresponds with an
+//! A _narrowing constraint_ consists of a list of _predicates_, each of which corresponds with an
-//! expression in the source file (represented by a [`Constraint`]). We need to support the
+//! expression in the source file (represented by a [`Predicate`]). We need to support the
 //! following operations on narrowing constraints:
 //!
-//! - Adding a new clause to an existing constraint
+//! - Adding a new predicate to an existing constraint
-//! - Merging two constraints together, which produces the _intersection_ of their clauses
+//! - Merging two constraints together, which produces the _intersection_ of their predicates
-//! - Iterating through the clauses in a constraint
+//! - Iterating through the predicates in a constraint
 //!
-//! In particular, note that we do not need random access to the clauses in a constraint. That
+//! In particular, note that we do not need random access to the predicates in a constraint. That
 //! means that we can use a simple [_sorted association list_][ruff_index::list] as our data
 //! structure. That lets us use a single 32-bit integer to store each narrowing constraint, no
-//! matter how many clauses it contains. It also makes merging two narrowing constraints fast,
+//! matter how many predicates it contains. It also makes merging two narrowing constraints fast,
 //! since alists support fast intersection.
 //!
 //! Because we visit the contents of each scope in source-file order, and assign scoped IDs in
 //! source-file order, that means that we will tend to visit narrowing constraints in order by
-//! their IDs. This is exactly how to get the best performance from our alist implementation.
+//! their predicate IDs. This is exactly how to get the best performance from our alist
+//! implementation.
 //!
-//! [`Constraint`]: crate::semantic_index::constraint::Constraint
+//! [`Predicate`]: crate::semantic_index::predicate::Predicate
 
 use ruff_index::list::{ListBuilder, ListSetReverseIterator, ListStorage};
 use ruff_index::newtype_index;
 
-use crate::semantic_index::constraint::ScopedConstraintId;
+use crate::semantic_index::predicate::ScopedPredicateId;
 
 /// A narrowing constraint associated with a live binding.
 ///
-/// A constraint is a list of clauses, each of which is a [`Constraint`] that constrains the type
+/// A constraint is a list of [`Predicate`]s that each constrain the type of the binding's symbol.
-/// of the binding's symbol.
 ///
 /// An instance of this type represents a _non-empty_ narrowing constraint. You will often wrap
 /// this in `Option` and use `None` to represent an empty narrowing constraint.
 ///
-/// [`Constraint`]: crate::semantic_index::constraint::Constraint
+/// [`Predicate`]: crate::semantic_index::predicate::Predicate
 #[newtype_index]
 pub(crate) struct ScopedNarrowingConstraintId;
 
-/// One of the clauses in a narrowing constraint, which is a [`Constraint`] that constrains the
+/// One of the [`Predicate`]s in a narrowing constraint, which constraints the type of the
-/// type of the binding's symbol.
+/// binding's symbol.
 ///
-/// Note that those [`Constraint`]s are stored in [their own per-scope
+/// Note that those [`Predicate`]s are stored in [their own per-scope
-/// arena][crate::semantic_index::constraint::Constraints], so internally we use a
+/// arena][crate::semantic_index::predicate::Predicates], so internally we use a
-/// [`ScopedConstraintId`] to refer to the underlying constraint.
+/// [`ScopedPredicateId`] to refer to the underlying predicate.
 ///
-/// [`Constraint`]: crate::semantic_index::constraint::Constraint
+/// [`Predicate`]: crate::semantic_index::predicate::Predicate
 #[derive(Clone, Copy, Debug, Eq, Ord, PartialEq, PartialOrd)]
-pub(crate) struct ScopedNarrowingConstraintClause(ScopedConstraintId);
+pub(crate) struct ScopedNarrowingConstraintPredicate(ScopedPredicateId);
 
-impl ScopedNarrowingConstraintClause {
+impl ScopedNarrowingConstraintPredicate {
-    /// Returns (the ID of) the `Constraint` for this clause
+    /// Returns (the ID of) the `Predicate`
-    pub(crate) fn constraint(self) -> ScopedConstraintId {
+    pub(crate) fn predicate(self) -> ScopedPredicateId {
         self.0
     }
 }
 
-impl From<ScopedConstraintId> for ScopedNarrowingConstraintClause {
+impl From<ScopedPredicateId> for ScopedNarrowingConstraintPredicate {
-    fn from(constraint: ScopedConstraintId) -> ScopedNarrowingConstraintClause {
+    fn from(predicate: ScopedPredicateId) -> ScopedNarrowingConstraintPredicate {
-        ScopedNarrowingConstraintClause(constraint)
+        ScopedNarrowingConstraintPredicate(predicate)
     }
 }
 
 /// A collection of narrowing constraints for a given scope.
 #[derive(Debug, Eq, PartialEq)]
 pub(crate) struct NarrowingConstraints {
-    lists: ListStorage<ScopedNarrowingConstraintId, ScopedNarrowingConstraintClause>,
+    lists: ListStorage<ScopedNarrowingConstraintId, ScopedNarrowingConstraintPredicate>,
 }
 
 // Building constraints
@@ -80,7 +80,7 @@ pub(crate) struct NarrowingConstraints {
 /// A builder for creating narrowing constraints.
 #[derive(Debug, Default, Eq, PartialEq)]
 pub(crate) struct NarrowingConstraintsBuilder {
-    lists: ListBuilder<ScopedNarrowingConstraintId, ScopedNarrowingConstraintClause>,
+    lists: ListBuilder<ScopedNarrowingConstraintId, ScopedNarrowingConstraintPredicate>,
 }
 
 impl NarrowingConstraintsBuilder {
@@ -90,18 +90,18 @@ impl NarrowingConstraintsBuilder {
         }
     }
 
-    /// Adds a clause to an existing narrowing constraint.
+    /// Adds a predicate to an existing narrowing constraint.
-    pub(crate) fn add(
+    pub(crate) fn add_predicate_to_constraint(
         &mut self,
         constraint: Option<ScopedNarrowingConstraintId>,
-        clause: ScopedNarrowingConstraintClause,
+        predicate: ScopedNarrowingConstraintPredicate,
     ) -> Option<ScopedNarrowingConstraintId> {
-        self.lists.insert(constraint, clause)
+        self.lists.insert(constraint, predicate)
     }
 
-    /// Returns the intersection of two narrowing constraints. The result contains the clauses that
+    /// Returns the intersection of two narrowing constraints. The result contains the predicates
-    /// appear in both inputs.
+    /// that appear in both inputs.
-    pub(crate) fn intersect(
+    pub(crate) fn intersect_constraints(
         &mut self,
         a: Option<ScopedNarrowingConstraintId>,
         b: Option<ScopedNarrowingConstraintId>,
@@ -114,12 +114,12 @@ impl NarrowingConstraintsBuilder {
 // ---------
 
 pub(crate) type NarrowingConstraintsIterator<'a> = std::iter::Copied<
-    ListSetReverseIterator<'a, ScopedNarrowingConstraintId, ScopedNarrowingConstraintClause>,
+    ListSetReverseIterator<'a, ScopedNarrowingConstraintId, ScopedNarrowingConstraintPredicate>,
 >;
 
 impl NarrowingConstraints {
-    /// Iterates over the clauses in a narrowing constraint.
+    /// Iterates over the predicates in a narrowing constraint.
-    pub(crate) fn iter_clauses(
+    pub(crate) fn iter_predicates(
         &self,
         set: Option<ScopedNarrowingConstraintId>,
     ) -> NarrowingConstraintsIterator<'_> {
@@ -134,14 +134,14 @@ impl NarrowingConstraints {
 mod tests {
     use super::*;
 
-    impl ScopedNarrowingConstraintClause {
+    impl ScopedNarrowingConstraintPredicate {
         pub(crate) fn as_u32(self) -> u32 {
             self.0.as_u32()
         }
     }
 
     impl NarrowingConstraintsBuilder {
-        pub(crate) fn iter_constraints(
+        pub(crate) fn iter_predicates(
             &self,
             set: Option<ScopedNarrowingConstraintId>,
         ) -> NarrowingConstraintsIterator<'_> {

crates/red_knot_python_semantic/src/semantic_index/predicate.rs

@@ -0,0 +1,84 @@
+//! _Predicates_ are Python expressions whose runtime values can affect type inference.
+//!
+//! We currently use predicates in two places:
+//!
+//! - [_Narrowing constraints_][crate::semantic_index::narrowing_constraints] constrain the type of
+//!   a binding that is visible at a particular use.
+//! - [_Visibility constraints_][crate::semantic_index::visibility_constraints] determine the
+//!   static visibility of a binding, and the reachability of a statement.
+
+use ruff_db::files::File;
+use ruff_index::{newtype_index, IndexVec};
+use ruff_python_ast::Singleton;
+
+use crate::db::Db;
+use crate::semantic_index::expression::Expression;
+use crate::semantic_index::symbol::{FileScopeId, ScopeId};
+
+// A scoped identifier for each `Predicate` in a scope.
+#[newtype_index]
+#[derive(Ord, PartialOrd)]
+pub(crate) struct ScopedPredicateId;
+
+// A collection of predicates for a given scope.
+pub(crate) type Predicates<'db> = IndexVec<ScopedPredicateId, Predicate<'db>>;
+
+#[derive(Debug, Default)]
+pub(crate) struct PredicatesBuilder<'db> {
+    predicates: IndexVec<ScopedPredicateId, Predicate<'db>>,
+}
+
+impl<'db> PredicatesBuilder<'db> {
+    /// Adds a predicate. Note that we do not deduplicate predicates. If you add a `Predicate`
+    /// more than once, you will get distinct `ScopedPredicateId`s for each one. (This lets you
+    /// model predicates that might evaluate to different values at different points of execution.)
+    pub(crate) fn add_predicate(&mut self, predicate: Predicate<'db>) -> ScopedPredicateId {
+        self.predicates.push(predicate)
+    }
+
+    pub(crate) fn build(mut self) -> Predicates<'db> {
+        self.predicates.shrink_to_fit();
+        self.predicates
+    }
+}
+
+#[derive(Clone, Copy, Debug, Hash, PartialEq, Eq, salsa::Update)]
+pub(crate) struct Predicate<'db> {
+    pub(crate) node: PredicateNode<'db>,
+    pub(crate) is_positive: bool,
+}
+
+#[derive(Clone, Copy, Debug, Hash, PartialEq, Eq, salsa::Update)]
+pub(crate) enum PredicateNode<'db> {
+    Expression(Expression<'db>),
+    Pattern(PatternPredicate<'db>),
+}
+
+/// Pattern kinds for which we support type narrowing and/or static visibility analysis.
+#[derive(Debug, Clone, Hash, PartialEq, salsa::Update)]
+pub(crate) enum PatternPredicateKind<'db> {
+    Singleton(Singleton, Option<Expression<'db>>),
+    Value(Expression<'db>, Option<Expression<'db>>),
+    Class(Expression<'db>, Option<Expression<'db>>),
+    Unsupported,
+}
+
+#[salsa::tracked]
+pub(crate) struct PatternPredicate<'db> {
+    pub(crate) file: File,
+
+    pub(crate) file_scope: FileScopeId,
+
+    pub(crate) subject: Expression<'db>,
+
+    #[return_ref]
+    pub(crate) kind: PatternPredicateKind<'db>,
+
+    count: countme::Count<PatternPredicate<'static>>,
+}
+
+impl<'db> PatternPredicate<'db> {
+    pub(crate) fn scope(self, db: &'db dyn Db) -> ScopeId<'db> {
+        self.file_scope(db).to_scope_id(db, self.file(db))
+    }
+}

crates/red_knot_python_semantic/src/semantic_index/use_def.rs

@@ -165,7 +165,7 @@
 //! don't actually store these "list of visible definitions" as a vector of [`Definition`].
 //! Instead, [`SymbolBindings`] and [`SymbolDeclarations`] are structs which use bit-sets to track
 //! definitions (and constraints, in the case of bindings) in terms of [`ScopedDefinitionId`] and
-//! [`ScopedConstraintId`], which are indices into the `all_definitions` and `constraints`
+//! [`ScopedPredicateId`], which are indices into the `all_definitions` and `predicates`
 //! indexvecs in the [`UseDefMap`].
 //!
 //! There is another special kind of possible "definition" for a symbol: there might be a path from
@@ -264,13 +264,13 @@ use self::symbol_state::{
     SymbolBindings, SymbolDeclarations, SymbolState,
 };
 use crate::semantic_index::ast_ids::ScopedUseId;
-use crate::semantic_index::constraint::{
-    Constraint, Constraints, ConstraintsBuilder, ScopedConstraintId,
-};
 use crate::semantic_index::definition::Definition;
 use crate::semantic_index::narrowing_constraints::{
     NarrowingConstraints, NarrowingConstraintsBuilder, NarrowingConstraintsIterator,
 };
+use crate::semantic_index::predicate::{
+    Predicate, Predicates, PredicatesBuilder, ScopedPredicateId,
+};
 use crate::semantic_index::symbol::{FileScopeId, ScopedSymbolId};
 use crate::semantic_index::visibility_constraints::{
     ScopedVisibilityConstraintId, VisibilityConstraints, VisibilityConstraintsBuilder,
@@ -285,8 +285,8 @@ pub(crate) struct UseDefMap<'db> {
     /// this represents the implicit "unbound"/"undeclared" definition of every symbol.
     all_definitions: IndexVec<ScopedDefinitionId, Option<Definition<'db>>>,
 
-    /// Array of [`Constraint`] in this scope.
+    /// Array of predicates in this scope.
-    constraints: Constraints<'db>,
+    predicates: Predicates<'db>,
 
     /// Array of narrowing constraints in this scope.
     narrowing_constraints: NarrowingConstraints,
@@ -374,7 +374,7 @@ impl<'db> UseDefMap<'db> {
     ) -> BindingWithConstraintsIterator<'map, 'db> {
         BindingWithConstraintsIterator {
             all_definitions: &self.all_definitions,
-            constraints: &self.constraints,
+            predicates: &self.predicates,
             narrowing_constraints: &self.narrowing_constraints,
             visibility_constraints: &self.visibility_constraints,
             inner: bindings.iter(),
@@ -387,7 +387,7 @@ impl<'db> UseDefMap<'db> {
     ) -> DeclarationsIterator<'map, 'db> {
         DeclarationsIterator {
             all_definitions: &self.all_definitions,
-            constraints: &self.constraints,
+            predicates: &self.predicates,
             visibility_constraints: &self.visibility_constraints,
             inner: declarations.iter(),
         }
@@ -421,7 +421,7 @@ type EagerBindings = IndexVec<ScopedEagerBindingsId, SymbolBindings>;
 #[derive(Debug)]
 pub(crate) struct BindingWithConstraintsIterator<'map, 'db> {
     all_definitions: &'map IndexVec<ScopedDefinitionId, Option<Definition<'db>>>,
-    pub(crate) constraints: &'map Constraints<'db>,
+    pub(crate) predicates: &'map Predicates<'db>,
     pub(crate) narrowing_constraints: &'map NarrowingConstraints,
     pub(crate) visibility_constraints: &'map VisibilityConstraints,
     inner: LiveBindingsIterator<'map>,
@@ -431,7 +431,7 @@ impl<'map, 'db> Iterator for BindingWithConstraintsIterator<'map, 'db> {
     type Item = BindingWithConstraints<'map, 'db>;
 
     fn next(&mut self) -> Option<Self::Item> {
-        let constraints = self.constraints;
+        let predicates = self.predicates;
         let narrowing_constraints = self.narrowing_constraints;
 
         self.inner
@@ -439,9 +439,9 @@ impl<'map, 'db> Iterator for BindingWithConstraintsIterator<'map, 'db> {
             .map(|live_binding| BindingWithConstraints {
                 binding: self.all_definitions[live_binding.binding],
                 narrowing_constraint: ConstraintsIterator {
-                    constraints,
+                    predicates,
                     constraint_ids: narrowing_constraints
-                        .iter_clauses(live_binding.narrowing_constraint),
+                        .iter_predicates(live_binding.narrowing_constraint),
                 },
                 visibility_constraint: live_binding.visibility_constraint,
             })
@@ -457,17 +457,17 @@ pub(crate) struct BindingWithConstraints<'map, 'db> {
 }
 
 pub(crate) struct ConstraintsIterator<'map, 'db> {
-    constraints: &'map Constraints<'db>,
+    predicates: &'map Predicates<'db>,
     constraint_ids: NarrowingConstraintsIterator<'map>,
 }
 
 impl<'db> Iterator for ConstraintsIterator<'_, 'db> {
-    type Item = Constraint<'db>;
+    type Item = Predicate<'db>;
 
     fn next(&mut self) -> Option<Self::Item> {
         self.constraint_ids
             .next()
-            .map(|narrowing_constraint| self.constraints[narrowing_constraint.constraint()])
+            .map(|narrowing_constraint| self.predicates[narrowing_constraint.predicate()])
     }
 }
 
@@ -475,7 +475,7 @@ impl std::iter::FusedIterator for ConstraintsIterator<'_, '_> {}
 
 pub(crate) struct DeclarationsIterator<'map, 'db> {
     all_definitions: &'map IndexVec<ScopedDefinitionId, Option<Definition<'db>>>,
-    pub(crate) constraints: &'map Constraints<'db>,
+    pub(crate) predicates: &'map Predicates<'db>,
     pub(crate) visibility_constraints: &'map VisibilityConstraints,
     inner: LiveDeclarationsIterator<'map>,
 }
@@ -517,8 +517,8 @@ pub(super) struct UseDefMapBuilder<'db> {
     /// Append-only array of [`Definition`].
     all_definitions: IndexVec<ScopedDefinitionId, Option<Definition<'db>>>,
 
-    /// Builder of constraints.
+    /// Builder of predicates.
-    pub(super) constraints: ConstraintsBuilder<'db>,
+    pub(super) predicates: PredicatesBuilder<'db>,
 
     /// Builder of narrowing constraints.
     pub(super) narrowing_constraints: NarrowingConstraintsBuilder,
@@ -553,7 +553,7 @@ impl Default for UseDefMapBuilder<'_> {
     fn default() -> Self {
         Self {
             all_definitions: IndexVec::from_iter([None]),
-            constraints: ConstraintsBuilder::default(),
+            predicates: PredicatesBuilder::default(),
             narrowing_constraints: NarrowingConstraintsBuilder::default(),
             visibility_constraints: VisibilityConstraintsBuilder::default(),
             scope_start_visibility: ScopedVisibilityConstraintId::ALWAYS_TRUE,
@@ -586,23 +586,18 @@ impl<'db> UseDefMapBuilder<'db> {
         symbol_state.record_binding(def_id, self.scope_start_visibility);
     }
 
-    pub(super) fn add_constraint(&mut self, constraint: Constraint<'db>) -> ScopedConstraintId {
+    pub(super) fn add_predicate(&mut self, predicate: Predicate<'db>) -> ScopedPredicateId {
-        self.constraints.add_constraint(constraint)
+        self.predicates.add_predicate(predicate)
     }
 
-    pub(super) fn record_constraint_id(&mut self, constraint: ScopedConstraintId) {
+    pub(super) fn record_narrowing_constraint(&mut self, predicate: ScopedPredicateId) {
-        let narrowing_constraint = constraint.into();
+        let narrowing_constraint = predicate.into();
         for state in &mut self.symbol_states {
-            state.record_constraint(&mut self.narrowing_constraints, narrowing_constraint);
+            state
+                .record_narrowing_constraint(&mut self.narrowing_constraints, narrowing_constraint);
         }
     }
 
-    pub(super) fn record_constraint(&mut self, constraint: Constraint<'db>) -> ScopedConstraintId {
-        let new_constraint_id = self.add_constraint(constraint);
-        self.record_constraint_id(new_constraint_id);
-        new_constraint_id
-    }
-
     pub(super) fn record_visibility_constraint(
         &mut self,
         constraint: ScopedVisibilityConstraintId,
@@ -781,7 +776,7 @@ impl<'db> UseDefMapBuilder<'db> {
 
         UseDefMap {
             all_definitions: self.all_definitions,
-            constraints: self.constraints.build(),
+            predicates: self.predicates.build(),
             narrowing_constraints: self.narrowing_constraints.build(),
             visibility_constraints: self.visibility_constraints.build(),
             bindings_by_use: self.bindings_by_use,

crates/red_knot_python_semantic/src/semantic_index/use_def/symbol_state.rs

@@ -47,7 +47,7 @@ use ruff_index::newtype_index;
 use smallvec::{smallvec, SmallVec};
 
 use crate::semantic_index::narrowing_constraints::{
-    NarrowingConstraintsBuilder, ScopedNarrowingConstraintClause, ScopedNarrowingConstraintId,
+    NarrowingConstraintsBuilder, ScopedNarrowingConstraintId, ScopedNarrowingConstraintPredicate,
 };
 use crate::semantic_index::visibility_constraints::{
     ScopedVisibilityConstraintId, VisibilityConstraintsBuilder,
@@ -224,14 +224,14 @@ impl SymbolBindings {
     }
 
     /// Add given constraint to all live bindings.
-    pub(super) fn record_constraint(
+    pub(super) fn record_narrowing_constraint(
         &mut self,
         narrowing_constraints: &mut NarrowingConstraintsBuilder,
-        constraint: ScopedNarrowingConstraintClause,
+        predicate: ScopedNarrowingConstraintPredicate,
     ) {
         for binding in &mut self.live_bindings {
-            binding.narrowing_constraint =
+            binding.narrowing_constraint = narrowing_constraints
-                narrowing_constraints.add(binding.narrowing_constraint, constraint);
+                .add_predicate_to_constraint(binding.narrowing_constraint, predicate);
         }
     }
 
@@ -292,7 +292,7 @@ impl SymbolBindings {
                     // that applies on only one path is irrelevant to the resulting type from
                     // unioning the two paths, so we intersect the constraints.
                     let narrowing_constraint = narrowing_constraints
-                        .intersect(a.narrowing_constraint, b.narrowing_constraint);
+                        .intersect_constraints(a.narrowing_constraint, b.narrowing_constraint);
 
                     // For visibility constraints, we merge them using a ternary OR operation:
                     let visibility_constraint = visibility_constraints
@@ -340,13 +340,13 @@ impl SymbolState {
     }
 
     /// Add given constraint to all live bindings.
-    pub(super) fn record_constraint(
+    pub(super) fn record_narrowing_constraint(
         &mut self,
         narrowing_constraints: &mut NarrowingConstraintsBuilder,
-        constraint: ScopedNarrowingConstraintClause,
+        constraint: ScopedNarrowingConstraintPredicate,
     ) {
         self.bindings
-            .record_constraint(narrowing_constraints, constraint);
+            .record_narrowing_constraint(narrowing_constraints, constraint);
     }
 
     /// Add given visibility constraint to all live bindings.
@@ -402,7 +402,7 @@ impl SymbolState {
 mod tests {
     use super::*;
 
-    use crate::semantic_index::constraint::ScopedConstraintId;
+    use crate::semantic_index::predicate::ScopedPredicateId;
 
     #[track_caller]
     fn assert_bindings(
@@ -420,12 +420,12 @@ mod tests {
                 } else {
                     def_id.as_u32().to_string()
                 };
-                let constraints = narrowing_constraints
+                let predicates = narrowing_constraints
-                    .iter_constraints(live_binding.narrowing_constraint)
+                    .iter_predicates(live_binding.narrowing_constraint)
                     .map(|idx| idx.as_u32().to_string())
                     .collect::<Vec<_>>()
                     .join(", ");
-                format!("{def}<{constraints}>")
+                format!("{def}<{predicates}>")
             })
             .collect::<Vec<_>>();
         assert_eq!(actual, expected);
@@ -480,8 +480,8 @@ mod tests {
             ScopedDefinitionId::from_u32(1),
             ScopedVisibilityConstraintId::ALWAYS_TRUE,
         );
-        let constraint = ScopedConstraintId::from_u32(0).into();
+        let predicate = ScopedPredicateId::from_u32(0).into();
-        sym.record_constraint(&mut narrowing_constraints, constraint);
+        sym.record_narrowing_constraint(&mut narrowing_constraints, predicate);
 
         assert_bindings(&narrowing_constraints, &sym, &["1<0>"]);
     }
@@ -497,16 +497,16 @@ mod tests {
             ScopedDefinitionId::from_u32(1),
             ScopedVisibilityConstraintId::ALWAYS_TRUE,
         );
-        let constraint = ScopedConstraintId::from_u32(0).into();
+        let predicate = ScopedPredicateId::from_u32(0).into();
-        sym1a.record_constraint(&mut narrowing_constraints, constraint);
+        sym1a.record_narrowing_constraint(&mut narrowing_constraints, predicate);
 
         let mut sym1b = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
         sym1b.record_binding(
             ScopedDefinitionId::from_u32(1),
             ScopedVisibilityConstraintId::ALWAYS_TRUE,
         );
-        let constraint = ScopedConstraintId::from_u32(0).into();
+        let predicate = ScopedPredicateId::from_u32(0).into();
-        sym1b.record_constraint(&mut narrowing_constraints, constraint);
+        sym1b.record_narrowing_constraint(&mut narrowing_constraints, predicate);
 
         sym1a.merge(
             sym1b,
@@ -522,16 +522,16 @@ mod tests {
             ScopedDefinitionId::from_u32(2),
             ScopedVisibilityConstraintId::ALWAYS_TRUE,
         );
-        let constraint = ScopedConstraintId::from_u32(1).into();
+        let predicate = ScopedPredicateId::from_u32(1).into();
-        sym2a.record_constraint(&mut narrowing_constraints, constraint);
+        sym2a.record_narrowing_constraint(&mut narrowing_constraints, predicate);
 
         let mut sym1b = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
         sym1b.record_binding(
             ScopedDefinitionId::from_u32(2),
             ScopedVisibilityConstraintId::ALWAYS_TRUE,
         );
-        let constraint = ScopedConstraintId::from_u32(2).into();
+        let predicate = ScopedPredicateId::from_u32(2).into();
-        sym1b.record_constraint(&mut narrowing_constraints, constraint);
+        sym1b.record_narrowing_constraint(&mut narrowing_constraints, predicate);
 
         sym2a.merge(
             sym1b,
@@ -547,8 +547,8 @@ mod tests {
             ScopedDefinitionId::from_u32(3),
             ScopedVisibilityConstraintId::ALWAYS_TRUE,
         );
-        let constraint = ScopedConstraintId::from_u32(3).into();
+        let predicate = ScopedPredicateId::from_u32(3).into();
-        sym3a.record_constraint(&mut narrowing_constraints, constraint);
+        sym3a.record_narrowing_constraint(&mut narrowing_constraints, predicate);
 
         let sym2b = SymbolState::undefined(ScopedVisibilityConstraintId::ALWAYS_TRUE);
 

crates/red_knot_python_semantic/src/semantic_index/visibility_constraints.rs

@@ -178,8 +178,8 @@ use std::cmp::Ordering;
 use ruff_index::{Idx, IndexVec};
 use rustc_hash::FxHashMap;
 
-use crate::semantic_index::constraint::{
+use crate::semantic_index::predicate::{
-    Constraint, ConstraintNode, Constraints, PatternConstraintKind, ScopedConstraintId,
+    PatternPredicateKind, Predicate, PredicateNode, Predicates, ScopedPredicateId,
 };
 use crate::types::{infer_expression_type, Truthiness};
 use crate::Db;
@@ -188,7 +188,7 @@ use crate::Db;
 /// is just like a boolean formula, but with `Ambiguous` as a third potential result. See the
 /// module documentation for more details.)
 ///
-/// The primitive atoms of the formula are [`Constraint`]s, which express some property of the
+/// The primitive atoms of the formula are [`Predicate`]s, which express some property of the
 /// runtime state of the code that we are analyzing.
 ///
 /// We assume that each atom has a stable value each time that the formula is evaluated. An atom
@@ -197,7 +197,7 @@ use crate::Db;
 /// allows us to perform simplifications like `A ∨ !A → true` and `A ∧ !A → false`.
 ///
 /// That means that when you are constructing a formula, you might need to create distinct atoms
-/// for a particular [`Constraint`], if your formula needs to consider how a particular runtime
+/// for a particular [`Predicate`], if your formula needs to consider how a particular runtime
 /// property might be different at different points in the execution of the program.
 ///
 /// Visibility constraints are normalized, so equivalent constraints are guaranteed to have equal
@@ -225,7 +225,7 @@ impl std::fmt::Debug for ScopedVisibilityConstraintId {
 //
 // There are 3 terminals, with hard-coded constraint IDs: true, ambiguous, and false.
 //
-// _Atoms_ are the underlying Constraints, which are the variables that are evaluated by the
+// _Atoms_ are the underlying Predicates, which are the variables that are evaluated by the
 // ternary function.
 //
 // _Interior nodes_ provide the TDD structure for the formula. Interior nodes are stored in an
@@ -234,9 +234,9 @@ impl std::fmt::Debug for ScopedVisibilityConstraintId {
 #[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)]
 struct InteriorNode {
     /// A "variable" that is evaluated as part of a TDD ternary function. For visibility
-    /// constraints, this is a `Constraint` that represents some runtime property of the Python
+    /// constraints, this is a `Predicate` that represents some runtime property of the Python
     /// code that we are evaluating.
-    atom: ScopedConstraintId,
+    atom: ScopedPredicateId,
     if_true: ScopedVisibilityConstraintId,
     if_ambiguous: ScopedVisibilityConstraintId,
     if_false: ScopedVisibilityConstraintId,
@@ -343,23 +343,23 @@ impl VisibilityConstraintsBuilder {
             .or_insert_with(|| self.interiors.push(node))
     }
 
-    /// Adds a new visibility constraint that checks a single [`Constraint`].
+    /// Adds a new visibility constraint that checks a single [`Predicate`].
     ///
-    /// [`ScopedConstraintId`]s are the “variables” that are evaluated by a TDD. A TDD variable has
+    /// [`ScopedPredicateId`]s are the “variables” that are evaluated by a TDD. A TDD variable has
     /// the same value no matter how many times it appears in the ternary formula that the TDD
     /// represents.
     ///
-    /// However, we sometimes have to model how a `Constraint` can have a different runtime
+    /// However, we sometimes have to model how a `Predicate` can have a different runtime
     /// value at different points in the execution of the program. To handle this, you can take
-    /// advantage of the fact that the [`Constraints`] arena does not deduplicate `Constraint`s.
+    /// advantage of the fact that the [`Predicates`] arena does not deduplicate `Predicate`s.
-    /// You can add a `Constraint` multiple times, yielding different `ScopedConstraintId`s, which
+    /// You can add a `Predicate` multiple times, yielding different `ScopedPredicateId`s, which
     /// you can then create separate TDD atoms for.
     pub(crate) fn add_atom(
         &mut self,
-        constraint: ScopedConstraintId,
+        predicate: ScopedPredicateId,
     ) -> ScopedVisibilityConstraintId {
         self.add_interior(InteriorNode {
-            atom: constraint,
+            atom: predicate,
             if_true: ALWAYS_TRUE,
             if_ambiguous: AMBIGUOUS,
             if_false: ALWAYS_FALSE,
@@ -534,7 +534,7 @@ impl VisibilityConstraints {
     pub(crate) fn evaluate<'db>(
         &self,
         db: &'db dyn Db,
-        constraints: &Constraints<'db>,
+        predicates: &Predicates<'db>,
         mut id: ScopedVisibilityConstraintId,
     ) -> Truthiness {
         loop {
@@ -544,8 +544,8 @@ impl VisibilityConstraints {
                 ALWAYS_FALSE => return Truthiness::AlwaysFalse,
                 _ => self.interiors[id],
             };
-            let constraint = &constraints[node.atom];
+            let predicate = &predicates[node.atom];
-            match Self::analyze_single(db, constraint) {
+            match Self::analyze_single(db, predicate) {
                 Truthiness::AlwaysTrue => id = node.if_true,
                 Truthiness::Ambiguous => id = node.if_ambiguous,
                 Truthiness::AlwaysFalse => id = node.if_false,
@@ -553,14 +553,14 @@ impl VisibilityConstraints {
         }
     }
 
-    fn analyze_single(db: &dyn Db, constraint: &Constraint) -> Truthiness {
+    fn analyze_single(db: &dyn Db, predicate: &Predicate) -> Truthiness {
-        match constraint.node {
+        match predicate.node {
-            ConstraintNode::Expression(test_expr) => {
+            PredicateNode::Expression(test_expr) => {
                 let ty = infer_expression_type(db, test_expr);
-                ty.bool(db).negate_if(!constraint.is_positive)
+                ty.bool(db).negate_if(!predicate.is_positive)
             }
-            ConstraintNode::Pattern(inner) => match inner.kind(db) {
+            PredicateNode::Pattern(inner) => match inner.kind(db) {
-                PatternConstraintKind::Value(value, guard) => {
+                PatternPredicateKind::Value(value, guard) => {
                     let subject_expression = inner.subject(db);
                     let subject_ty = infer_expression_type(db, subject_expression);
                     let value_ty = infer_expression_type(db, *value);
@@ -579,9 +579,9 @@ impl VisibilityConstraints {
                         Truthiness::Ambiguous
                     }
                 }
-                PatternConstraintKind::Singleton(..)
+                PatternPredicateKind::Singleton(..)
-                | PatternConstraintKind::Class(..)
+                | PatternPredicateKind::Class(..)
-                | PatternConstraintKind::Unsupported => Truthiness::Ambiguous,
+                | PatternPredicateKind::Unsupported => Truthiness::Ambiguous,
             },
         }
     }

crates/red_knot_python_semantic/src/symbol.rs

@@ -538,7 +538,7 @@ fn symbol_from_bindings_impl<'db>(
     bindings_with_constraints: BindingWithConstraintsIterator<'_, 'db>,
     requires_explicit_reexport: RequiresExplicitReExport,
 ) -> Symbol<'db> {
-    let constraints = bindings_with_constraints.constraints;
+    let predicates = bindings_with_constraints.predicates;
     let visibility_constraints = bindings_with_constraints.visibility_constraints;
     let mut bindings_with_constraints = bindings_with_constraints.peekable();
 
@@ -552,7 +552,7 @@ fn symbol_from_bindings_impl<'db>(
             visibility_constraint,
             narrowing_constraint: _,
         }) if binding.map_or(true, is_non_exported) => {
-            visibility_constraints.evaluate(db, constraints, *visibility_constraint)
+            visibility_constraints.evaluate(db, predicates, *visibility_constraint)
         }
         _ => Truthiness::AlwaysFalse,
     };
@@ -570,7 +570,7 @@ fn symbol_from_bindings_impl<'db>(
             }
 
             let static_visibility =
-                visibility_constraints.evaluate(db, constraints, visibility_constraint);
+                visibility_constraints.evaluate(db, predicates, visibility_constraint);
 
             if static_visibility.is_always_false() {
                 return None;
@@ -629,7 +629,7 @@ fn symbol_from_declarations_impl<'db>(
     declarations: DeclarationsIterator<'_, 'db>,
     requires_explicit_reexport: RequiresExplicitReExport,
 ) -> SymbolFromDeclarationsResult<'db> {
-    let constraints = declarations.constraints;
+    let predicates = declarations.predicates;
     let visibility_constraints = declarations.visibility_constraints;
     let mut declarations = declarations.peekable();
 
@@ -642,7 +642,7 @@ fn symbol_from_declarations_impl<'db>(
             declaration,
             visibility_constraint,
         }) if declaration.map_or(true, is_non_exported) => {
-            visibility_constraints.evaluate(db, constraints, *visibility_constraint)
+            visibility_constraints.evaluate(db, predicates, *visibility_constraint)
         }
         _ => Truthiness::AlwaysFalse,
     };
@@ -659,7 +659,7 @@ fn symbol_from_declarations_impl<'db>(
             }
 
             let static_visibility =
-                visibility_constraints.evaluate(db, constraints, visibility_constraint);
+                visibility_constraints.evaluate(db, predicates, visibility_constraint);
 
             if static_visibility.is_always_false() {
                 None

crates/red_knot_python_semantic/src/types/narrow.rs

@@ -1,9 +1,9 @@
 use crate::semantic_index::ast_ids::HasScopedExpressionId;
-use crate::semantic_index::constraint::{
-    Constraint, ConstraintNode, PatternConstraint, PatternConstraintKind,
-};
 use crate::semantic_index::definition::Definition;
 use crate::semantic_index::expression::Expression;
+use crate::semantic_index::predicate::{
+    PatternPredicate, PatternPredicateKind, Predicate, PredicateNode,
+};
 use crate::semantic_index::symbol::{ScopeId, ScopedSymbolId, SymbolTable};
 use crate::semantic_index::symbol_table;
 use crate::types::infer::infer_same_file_expression_type;
@@ -37,18 +37,18 @@ use std::sync::Arc;
 /// constraint is applied to that definition, so we'd just return `None`.
 pub(crate) fn infer_narrowing_constraint<'db>(
     db: &'db dyn Db,
-    constraint: Constraint<'db>,
+    predicate: Predicate<'db>,
     definition: Definition<'db>,
 ) -> Option<Type<'db>> {
-    let constraints = match constraint.node {
+    let constraints = match predicate.node {
-        ConstraintNode::Expression(expression) => {
+        PredicateNode::Expression(expression) => {
-            if constraint.is_positive {
+            if predicate.is_positive {
                 all_narrowing_constraints_for_expression(db, expression)
             } else {
                 all_negative_narrowing_constraints_for_expression(db, expression)
             }
         }
-        ConstraintNode::Pattern(pattern) => all_narrowing_constraints_for_pattern(db, pattern),
+        PredicateNode::Pattern(pattern) => all_narrowing_constraints_for_pattern(db, pattern),
     };
     if let Some(constraints) = constraints {
         constraints.get(&definition.symbol(db)).copied()
@@ -61,9 +61,9 @@ pub(crate) fn infer_narrowing_constraint<'db>(
 #[salsa::tracked(return_ref)]
 fn all_narrowing_constraints_for_pattern<'db>(
     db: &'db dyn Db,
-    pattern: PatternConstraint<'db>,
+    pattern: PatternPredicate<'db>,
 ) -> Option<NarrowingConstraints<'db>> {
-    NarrowingConstraintsBuilder::new(db, ConstraintNode::Pattern(pattern), true).finish()
+    NarrowingConstraintsBuilder::new(db, PredicateNode::Pattern(pattern), true).finish()
 }
 
 #[allow(clippy::ref_option)]
@@ -72,7 +72,7 @@ fn all_narrowing_constraints_for_expression<'db>(
     db: &'db dyn Db,
     expression: Expression<'db>,
 ) -> Option<NarrowingConstraints<'db>> {
-    NarrowingConstraintsBuilder::new(db, ConstraintNode::Expression(expression), true).finish()
+    NarrowingConstraintsBuilder::new(db, PredicateNode::Expression(expression), true).finish()
 }
 
 #[allow(clippy::ref_option)]
@@ -81,7 +81,7 @@ fn all_negative_narrowing_constraints_for_expression<'db>(
     db: &'db dyn Db,
     expression: Expression<'db>,
 ) -> Option<NarrowingConstraints<'db>> {
-    NarrowingConstraintsBuilder::new(db, ConstraintNode::Expression(expression), false).finish()
+    NarrowingConstraintsBuilder::new(db, PredicateNode::Expression(expression), false).finish()
 }
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
@@ -166,25 +166,25 @@ fn merge_constraints_or<'db>(
 
 struct NarrowingConstraintsBuilder<'db> {
     db: &'db dyn Db,
-    constraint: ConstraintNode<'db>,
+    predicate: PredicateNode<'db>,
     is_positive: bool,
 }
 
 impl<'db> NarrowingConstraintsBuilder<'db> {
-    fn new(db: &'db dyn Db, constraint: ConstraintNode<'db>, is_positive: bool) -> Self {
+    fn new(db: &'db dyn Db, predicate: PredicateNode<'db>, is_positive: bool) -> Self {
         Self {
             db,
-            constraint,
+            predicate,
             is_positive,
         }
     }
 
     fn finish(mut self) -> Option<NarrowingConstraints<'db>> {
-        let constraints: Option<NarrowingConstraints<'db>> = match self.constraint {
+        let constraints: Option<NarrowingConstraints<'db>> = match self.predicate {
-            ConstraintNode::Expression(expression) => {
+            PredicateNode::Expression(expression) => {
-                self.evaluate_expression_constraint(expression, self.is_positive)
+                self.evaluate_expression_predicate(expression, self.is_positive)
             }
-            ConstraintNode::Pattern(pattern) => self.evaluate_pattern_constraint(pattern),
+            PredicateNode::Pattern(pattern) => self.evaluate_pattern_predicate(pattern),
         };
         if let Some(mut constraints) = constraints {
             constraints.shrink_to_fit();
@@ -194,16 +194,16 @@ impl<'db> NarrowingConstraintsBuilder<'db> {
         }
     }
 
-    fn evaluate_expression_constraint(
+    fn evaluate_expression_predicate(
         &mut self,
         expression: Expression<'db>,
         is_positive: bool,
     ) -> Option<NarrowingConstraints<'db>> {
         let expression_node = expression.node_ref(self.db).node();
-        self.evaluate_expression_node_constraint(expression_node, expression, is_positive)
+        self.evaluate_expression_node_predicate(expression_node, expression, is_positive)
     }
 
-    fn evaluate_expression_node_constraint(
+    fn evaluate_expression_node_predicate(
         &mut self,
         expression_node: &ruff_python_ast::Expr,
         expression: Expression<'db>,
@@ -217,28 +217,29 @@ impl<'db> NarrowingConstraintsBuilder<'db> {
             ast::Expr::Call(expr_call) => {
                 self.evaluate_expr_call(expr_call, expression, is_positive)
             }
-            ast::Expr::UnaryOp(unary_op) if unary_op.op == ast::UnaryOp::Not => self
+            ast::Expr::UnaryOp(unary_op) if unary_op.op == ast::UnaryOp::Not => {
-                .evaluate_expression_node_constraint(&unary_op.operand, expression, !is_positive),
+                self.evaluate_expression_node_predicate(&unary_op.operand, expression, !is_positive)
+            }
             ast::Expr::BoolOp(bool_op) => self.evaluate_bool_op(bool_op, expression, is_positive),
             _ => None, // TODO other test expression kinds
         }
     }
 
-    fn evaluate_pattern_constraint(
+    fn evaluate_pattern_predicate(
         &mut self,
-        pattern: PatternConstraint<'db>,
+        pattern: PatternPredicate<'db>,
     ) -> Option<NarrowingConstraints<'db>> {
         let subject = pattern.subject(self.db);
 
         match pattern.kind(self.db) {
-            PatternConstraintKind::Singleton(singleton, _guard) => {
+            PatternPredicateKind::Singleton(singleton, _guard) => {
                 self.evaluate_match_pattern_singleton(subject, *singleton)
             }
-            PatternConstraintKind::Class(cls, _guard) => {
+            PatternPredicateKind::Class(cls, _guard) => {
                 self.evaluate_match_pattern_class(subject, *cls)
             }
             // TODO: support more pattern kinds
-            PatternConstraintKind::Value(..) | PatternConstraintKind::Unsupported => None,
+            PatternPredicateKind::Value(..) | PatternPredicateKind::Unsupported => None,
         }
     }
 
@@ -247,9 +248,9 @@ impl<'db> NarrowingConstraintsBuilder<'db> {
     }
 
     fn scope(&self) -> ScopeId<'db> {
-        match self.constraint {
+        match self.predicate {
-            ConstraintNode::Expression(expression) => expression.scope(self.db),
+            PredicateNode::Expression(expression) => expression.scope(self.db),
-            ConstraintNode::Pattern(pattern) => pattern.scope(self.db),
+            PredicateNode::Pattern(pattern) => pattern.scope(self.db),
         }
     }
 
@@ -456,7 +457,7 @@ impl<'db> NarrowingConstraintsBuilder<'db> {
                     && expr_call.arguments.keywords.is_empty()
                     && class_type.class().is_known(self.db, KnownClass::Bool) =>
             {
-                self.evaluate_expression_node_constraint(
+                self.evaluate_expression_node_predicate(
                     &expr_call.arguments.args[0],
                     expression,
                     is_positive,
@@ -528,7 +529,7 @@ impl<'db> NarrowingConstraintsBuilder<'db> {
                     }
             })
             .map(|sub_expr| {
-                self.evaluate_expression_node_constraint(sub_expr, expression, is_positive)
+                self.evaluate_expression_node_predicate(sub_expr, expression, is_positive)
             })
             .collect::<Vec<_>>();
         match (expr_bool_op.op, is_positive) {