litex/infer/
infer_dispatch.rs

1use crate::prelude::*;
2
3impl Runtime {
4    /// Dispatch infer by fact kind.
5    /// Example: `a $subset b` enters atomic infer branch.
6    pub fn infer(&mut self, fact: &Fact) -> Result<InferResult, RuntimeError> {
7        match fact {
8            Fact::AtomicFact(atomic_fact) => self.infer_atomic_fact(atomic_fact),
9            Fact::ExistFact(exist_fact) => self.infer_exist_fact(exist_fact),
10            Fact::OrFact(or_fact) => self.infer_or_fact(or_fact),
11            Fact::AndFact(and_fact) => self.infer_and_fact(and_fact),
12            Fact::ChainFact(chain_fact) => self.infer_chain_fact(chain_fact),
13            Fact::ForallFact(forall_fact) => self.infer_forall_fact(forall_fact),
14            Fact::ForallFactWithIff(forall_fact_with_iff) => {
15                self.infer_forall_fact_with_iff(forall_fact_with_iff)
16            }
17            Fact::NotForall(not_forall) => self.infer_not_forall_fact(not_forall),
18        }
19    }
20
21    pub fn infer_exist_or_and_chain_atomic_fact(
22        &mut self,
23        fact: &ExistOrAndChainAtomicFact,
24    ) -> Result<InferResult, RuntimeError> {
25        match fact {
26            ExistOrAndChainAtomicFact::AtomicFact(atomic_fact) => {
27                self.infer_atomic_fact(atomic_fact)
28            }
29            ExistOrAndChainAtomicFact::AndFact(and_fact) => self.infer_and_fact(and_fact),
30            ExistOrAndChainAtomicFact::ChainFact(chain_fact) => self.infer_chain_fact(chain_fact),
31            ExistOrAndChainAtomicFact::OrFact(or_fact) => self.infer_or_fact(or_fact),
32            ExistOrAndChainAtomicFact::ExistFact(exist_fact) => self.infer_exist_fact(exist_fact),
33        }
34    }
35
36    pub fn infer_or_and_chain_atomic_fact(
37        &mut self,
38        fact: &OrAndChainAtomicFact,
39    ) -> Result<InferResult, RuntimeError> {
40        match fact {
41            OrAndChainAtomicFact::AtomicFact(atomic_fact) => self.infer_atomic_fact(atomic_fact),
42            OrAndChainAtomicFact::AndFact(and_fact) => self.infer_and_fact(and_fact),
43            OrAndChainAtomicFact::ChainFact(chain_fact) => self.infer_chain_fact(chain_fact),
44            OrAndChainAtomicFact::OrFact(or_fact) => self.infer_or_fact(or_fact),
45        }
46    }
47
48    fn infer_exist_fact(
49        &mut self,
50        exist_fact: &ExistFactEnum,
51    ) -> Result<InferResult, RuntimeError> {
52        let mut out = InferResult::new();
53        if exist_fact.is_exist_unique() && exist_fact.params_def_with_type().number_of_params() > 0
54        {
55            let uniq = self.build_exist_unique_uniqueness_forall_fact(exist_fact)?;
56            out.new_infer_result_inside(
57                self.store_forall_fact_without_well_defined_verified_and_infer(uniq)?,
58            );
59        } else if exist_fact.is_not_exist()
60            && exist_fact.params_def_with_type().number_of_params() > 0
61        {
62            let forall = self.build_not_exist_demorgan_forall_fact(exist_fact)?;
63            if forall
64                .error_messages_if_forall_param_missing_in_some_then_clause()
65                .is_empty()
66            {
67                out.new_fact(&forall.clone().into());
68            }
69            out.new_infer_result_inside(
70                self.store_forall_fact_without_well_defined_verified_and_infer(forall)?,
71            );
72        }
73        Ok(out)
74    }
75
76    fn infer_or_fact(&mut self, _or_fact: &OrFact) -> Result<InferResult, RuntimeError> {
77        Ok(InferResult::new())
78    }
79
80    fn infer_and_fact(&mut self, _and_fact: &AndFact) -> Result<InferResult, RuntimeError> {
81        Ok(InferResult::new())
82    }
83
84    fn infer_chain_fact(&mut self, chain_fact: &ChainFact) -> Result<InferResult, RuntimeError> {
85        let atomic_facts = match chain_fact.facts_with_order_transitive_closure() {
86            Ok(v) => v,
87            Err(_) => return Ok(InferResult::new()),
88        };
89        let mut infer_result = InferResult::new();
90        for atomic_fact in atomic_facts {
91            if let AtomicFact::EqualFact(equal_fact) = atomic_fact {
92                infer_result.new_infer_result_inside(self.infer_equal_fact(&equal_fact)?);
93            }
94        }
95        Ok(infer_result)
96    }
97
98    // Do not record the whole forall in CLI/JSON `infer_facts`; inner then-clauses are stored as separate facts.
99    fn infer_forall_fact(
100        &mut self,
101        _forall_fact: &ForallFact,
102    ) -> Result<InferResult, RuntimeError> {
103        Ok(InferResult::new())
104    }
105
106    fn infer_forall_fact_with_iff(
107        &mut self,
108        _forall_fact_with_iff: &ForallFactWithIff,
109    ) -> Result<InferResult, RuntimeError> {
110        Ok(InferResult::new())
111    }
112}
litex/infer/infer_dispatch.rs

litex/infer/
infer_dispatch.rs
