litex/infer/
infer_atomic_fact.rs

1use crate::prelude::*;
2
3impl Runtime {
4    // Dispatch `infer` for a single atomic fact (see `docs/Manual.md#inference`).
5    pub fn infer_atomic_fact(
6        &mut self,
7        atomic_fact: &AtomicFact,
8    ) -> Result<InferResult, RuntimeError> {
9        match atomic_fact {
10            // Equality: numeric bindings, cart/tuple/seq/matrix structure, `0 = a - b` => `a = b`.
11            AtomicFact::EqualFact(equal_fact) => self.infer_equal_fact(equal_fact),
12            // Membership `x $in S`: unfold `S` (list, set builder, intervals, standard sets, …).
13            AtomicFact::InFact(in_fact) => self.infer_in_fact(in_fact),
14            // Predicate atom `P(...)`: parameter typing plus each `iff` clause from `P`'s definition.
15            AtomicFact::NormalAtomicFact(normal_atomic_fact) => {
16                self.infer_normal_atomic_fact(normal_atomic_fact)
17            }
18            // `A $subset B` => `forall` fresh `x $in A: x $in B`.
19            AtomicFact::SubsetFact(subset_fact) => self.infer_subset_fact(subset_fact),
20            // `A $superset B` => `forall` fresh `x $in B: x $in A`.
21            AtomicFact::SupersetFact(superset_fact) => self.infer_superset_fact(superset_fact),
22            AtomicFact::RestrictFact(rf) => self.infer_restrict_fact(rf),
23            // One-sided numeric comparison: if the other side is a resolved constant, infer sign vs 0.
24            AtomicFact::LessFact(_)
25            | AtomicFact::GreaterFact(_)
26            | AtomicFact::LessEqualFact(_)
27            | AtomicFact::GreaterEqualFact(_) => {
28                self.infer_numeric_order_sign_from_order_atomic(atomic_fact)
29            }
30            // e.g. negated atoms, `is_set`, `not_restrict_fn_in`: no inference on this path.
31            _ => Ok(InferResult::new()),
32        }
33    }
34}
litex/infer/infer_atomic_fact.rs

litex/infer/
infer_atomic_fact.rs
