litex/runtime/
runtime_instantiate_fact.rs

1use crate::prelude::*;
2use std::collections::HashMap;
3
4impl Runtime {
5    fn line_file_after_inst(original: &LineFile, inst_to_line_file: Option<&LineFile>) -> LineFile {
6        inst_to_line_file
7            .cloned()
8            .unwrap_or_else(|| original.clone())
9    }
10
11    /// `inst_to_line_file`: `None` keeps each node's original line file (verify, exec, parsing).
12    /// `Some(lf)` assigns `lf` throughout the instance (infer: tie the new fact to the use site).
13    pub fn inst_fact(
14        &self,
15        fact: &Fact,
16        param_to_arg_map: &HashMap<String, Obj>,
17        to_inst_param_type: ParamObjType,
18        inst_to_line_file: Option<LineFile>,
19    ) -> Result<Fact, RuntimeError> {
20        let inst_lf = inst_to_line_file.as_ref();
21        Ok(match fact {
22            Fact::AtomicFact(atomic_fact) => Fact::AtomicFact(self.inst_atomic_fact(
23                atomic_fact,
24                param_to_arg_map,
25                to_inst_param_type,
26                inst_lf,
27            )?),
28            Fact::ExistFact(exist_fact) => Fact::ExistFact(self.inst_exist_fact(
29                exist_fact,
30                param_to_arg_map,
31                to_inst_param_type,
32                inst_lf,
33            )?),
34            Fact::OrFact(or_fact) => Fact::OrFact(self.inst_or_fact(
35                or_fact,
36                param_to_arg_map,
37                to_inst_param_type,
38                inst_lf,
39            )?),
40            Fact::AndFact(and_fact) => Fact::AndFact(self.inst_and_fact(
41                and_fact,
42                param_to_arg_map,
43                to_inst_param_type,
44                inst_lf,
45            )?),
46            Fact::ChainFact(chain_fact) => Fact::ChainFact(self.inst_chain_fact(
47                chain_fact,
48                param_to_arg_map,
49                to_inst_param_type,
50                inst_lf,
51            )?),
52            Fact::ForallFact(forall_fact) => Fact::ForallFact(self.inst_forall_fact(
53                forall_fact,
54                param_to_arg_map,
55                to_inst_param_type,
56                inst_lf,
57            )?),
58            Fact::ForallFactWithIff(forall_fact_with_iff) => {
59                Fact::ForallFactWithIff(self.inst_forall_fact_with_iff(
60                    forall_fact_with_iff,
61                    param_to_arg_map,
62                    to_inst_param_type,
63                    inst_lf,
64                )?)
65            }
66            Fact::NotForall(not_forall) => {
67                Fact::NotForall(NotForallFact::new(self.inst_forall_fact(
68                    &not_forall.forall_fact,
69                    param_to_arg_map,
70                    to_inst_param_type,
71                    inst_lf,
72                )?))
73            }
74        })
75    }
76
77    pub fn inst_exist_or_and_chain_atomic_fact(
78        &self,
79        fact: &ExistOrAndChainAtomicFact,
80        param_to_arg_map: &HashMap<String, Obj>,
81        to_inst_param_type: ParamObjType,
82        inst_lf: Option<&LineFile>,
83    ) -> Result<ExistOrAndChainAtomicFact, RuntimeError> {
84        Ok(match fact {
85            ExistOrAndChainAtomicFact::AtomicFact(atomic_fact) => {
86                ExistOrAndChainAtomicFact::AtomicFact(self.inst_atomic_fact(
87                    atomic_fact,
88                    param_to_arg_map,
89                    to_inst_param_type,
90                    inst_lf,
91                )?)
92            }
93            ExistOrAndChainAtomicFact::AndFact(and_fact) => ExistOrAndChainAtomicFact::AndFact(
94                self.inst_and_fact(and_fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
95            ),
96            ExistOrAndChainAtomicFact::ChainFact(chain_fact) => {
97                ExistOrAndChainAtomicFact::ChainFact(self.inst_chain_fact(
98                    chain_fact,
99                    param_to_arg_map,
100                    to_inst_param_type,
101                    inst_lf,
102                )?)
103            }
104            ExistOrAndChainAtomicFact::OrFact(or_fact) => ExistOrAndChainAtomicFact::OrFact(
105                self.inst_or_fact(or_fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
106            ),
107            ExistOrAndChainAtomicFact::ExistFact(exist_fact) => {
108                ExistOrAndChainAtomicFact::ExistFact(self.inst_exist_fact(
109                    exist_fact,
110                    param_to_arg_map,
111                    to_inst_param_type,
112                    inst_lf,
113                )?)
114            }
115        })
116    }
117
118    pub fn inst_exist_body_fact(
119        &self,
120        fact: &ExistBodyFact,
121        param_to_arg_map: &HashMap<String, Obj>,
122        to_inst_param_type: ParamObjType,
123        inst_lf: Option<&LineFile>,
124    ) -> Result<ExistBodyFact, RuntimeError> {
125        Ok(match fact {
126            ExistBodyFact::AtomicFact(atomic_fact) => ExistBodyFact::AtomicFact(
127                self.inst_atomic_fact(atomic_fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
128            ),
129            ExistBodyFact::AndFact(and_fact) => ExistBodyFact::AndFact(self.inst_and_fact(
130                and_fact,
131                param_to_arg_map,
132                to_inst_param_type,
133                inst_lf,
134            )?),
135            ExistBodyFact::ChainFact(chain_fact) => ExistBodyFact::ChainFact(
136                self.inst_chain_fact(chain_fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
137            ),
138            ExistBodyFact::OrFact(or_fact) => ExistBodyFact::OrFact(self.inst_or_fact(
139                or_fact,
140                param_to_arg_map,
141                to_inst_param_type,
142                inst_lf,
143            )?),
144            ExistBodyFact::InlineForall(forall_fact) => ExistBodyFact::InlineForall(
145                self.inst_forall_fact(forall_fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
146            ),
147        })
148    }
149
150    pub fn inst_or_and_chain_atomic_fact(
151        &self,
152        fact: &OrAndChainAtomicFact,
153        param_to_arg_map: &HashMap<String, Obj>,
154        to_inst_param_type: ParamObjType,
155        inst_lf: Option<&LineFile>,
156    ) -> Result<OrAndChainAtomicFact, RuntimeError> {
157        Ok(match fact {
158            OrAndChainAtomicFact::AtomicFact(atomic_fact) => OrAndChainAtomicFact::AtomicFact(
159                self.inst_atomic_fact(atomic_fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
160            ),
161            OrAndChainAtomicFact::AndFact(and_fact) => OrAndChainAtomicFact::AndFact(
162                self.inst_and_fact(and_fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
163            ),
164            OrAndChainAtomicFact::ChainFact(chain_fact) => OrAndChainAtomicFact::ChainFact(
165                self.inst_chain_fact(chain_fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
166            ),
167            OrAndChainAtomicFact::OrFact(or_fact) => OrAndChainAtomicFact::OrFact(
168                self.inst_or_fact(or_fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
169            ),
170        })
171    }
172
173    pub fn inst_and_chain_atomic_fact(
174        &self,
175        fact: &AndChainAtomicFact,
176        param_to_arg_map: &HashMap<String, Obj>,
177        to_inst_param_type: ParamObjType,
178        inst_lf: Option<&LineFile>,
179    ) -> Result<AndChainAtomicFact, RuntimeError> {
180        Ok(match fact {
181            AndChainAtomicFact::AtomicFact(atomic_fact) => AndChainAtomicFact::AtomicFact(
182                self.inst_atomic_fact(atomic_fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
183            ),
184            AndChainAtomicFact::AndFact(and_fact) => AndChainAtomicFact::AndFact(
185                self.inst_and_fact(and_fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
186            ),
187            AndChainAtomicFact::ChainFact(chain_fact) => AndChainAtomicFact::ChainFact(
188                self.inst_chain_fact(chain_fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
189            ),
190        })
191    }
192
193    pub fn inst_atomic_fact(
194        &self,
195        atomic_fact: &AtomicFact,
196        param_to_arg_map: &HashMap<String, Obj>,
197        to_inst_param_type: ParamObjType,
198        inst_lf: Option<&LineFile>,
199    ) -> Result<AtomicFact, RuntimeError> {
200        Ok(match atomic_fact {
201            AtomicFact::NormalAtomicFact(fact) => AtomicFact::NormalAtomicFact(
202                self.inst_normal_atomic_fact(fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
203            ),
204            AtomicFact::EqualFact(fact) => AtomicFact::EqualFact(self.inst_equal_fact(
205                fact,
206                param_to_arg_map,
207                to_inst_param_type,
208                inst_lf,
209            )?),
210            AtomicFact::LessFact(fact) => AtomicFact::LessFact(self.inst_less_fact(
211                fact,
212                param_to_arg_map,
213                to_inst_param_type,
214                inst_lf,
215            )?),
216            AtomicFact::GreaterFact(fact) => AtomicFact::GreaterFact(self.inst_greater_fact(
217                fact,
218                param_to_arg_map,
219                to_inst_param_type,
220                inst_lf,
221            )?),
222            AtomicFact::LessEqualFact(fact) => AtomicFact::LessEqualFact(
223                self.inst_less_equal_fact(fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
224            ),
225            AtomicFact::GreaterEqualFact(fact) => AtomicFact::GreaterEqualFact(
226                self.inst_greater_equal_fact(fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
227            ),
228            AtomicFact::IsSetFact(fact) => AtomicFact::IsSetFact(self.inst_is_set_fact(
229                fact,
230                param_to_arg_map,
231                to_inst_param_type,
232                inst_lf,
233            )?),
234            AtomicFact::IsNonemptySetFact(fact) => {
235                AtomicFact::IsNonemptySetFact(self.inst_is_nonempty_set_fact(
236                    fact,
237                    param_to_arg_map,
238                    to_inst_param_type,
239                    inst_lf,
240                )?)
241            }
242            AtomicFact::IsFiniteSetFact(fact) => AtomicFact::IsFiniteSetFact(
243                self.inst_is_finite_set_fact(fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
244            ),
245            AtomicFact::InFact(fact) => AtomicFact::InFact(self.inst_in_fact(
246                fact,
247                param_to_arg_map,
248                to_inst_param_type,
249                inst_lf,
250            )?),
251            AtomicFact::IsCartFact(fact) => AtomicFact::IsCartFact(self.inst_is_cart_fact(
252                fact,
253                param_to_arg_map,
254                to_inst_param_type,
255                inst_lf,
256            )?),
257            AtomicFact::IsTupleFact(fact) => AtomicFact::IsTupleFact(self.inst_is_tuple_fact(
258                fact,
259                param_to_arg_map,
260                to_inst_param_type,
261                inst_lf,
262            )?),
263            AtomicFact::SubsetFact(fact) => AtomicFact::SubsetFact(self.inst_subset_fact(
264                fact,
265                param_to_arg_map,
266                to_inst_param_type,
267                inst_lf,
268            )?),
269            AtomicFact::SupersetFact(fact) => AtomicFact::SupersetFact(self.inst_superset_fact(
270                fact,
271                param_to_arg_map,
272                to_inst_param_type,
273                inst_lf,
274            )?),
275            AtomicFact::NotNormalAtomicFact(fact) => {
276                AtomicFact::NotNormalAtomicFact(self.inst_not_normal_atomic_fact(
277                    fact,
278                    param_to_arg_map,
279                    to_inst_param_type,
280                    inst_lf,
281                )?)
282            }
283            AtomicFact::NotEqualFact(fact) => AtomicFact::NotEqualFact(self.inst_not_equal_fact(
284                fact,
285                param_to_arg_map,
286                to_inst_param_type,
287                inst_lf,
288            )?),
289            AtomicFact::NotLessFact(fact) => AtomicFact::NotLessFact(self.inst_not_less_fact(
290                fact,
291                param_to_arg_map,
292                to_inst_param_type,
293                inst_lf,
294            )?),
295            AtomicFact::NotGreaterFact(fact) => AtomicFact::NotGreaterFact(
296                self.inst_not_greater_fact(fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
297            ),
298            AtomicFact::NotLessEqualFact(fact) => AtomicFact::NotLessEqualFact(
299                self.inst_not_less_equal_fact(fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
300            ),
301            AtomicFact::NotGreaterEqualFact(fact) => {
302                AtomicFact::NotGreaterEqualFact(self.inst_not_greater_equal_fact(
303                    fact,
304                    param_to_arg_map,
305                    to_inst_param_type,
306                    inst_lf,
307                )?)
308            }
309            AtomicFact::NotIsSetFact(fact) => AtomicFact::NotIsSetFact(self.inst_not_is_set_fact(
310                fact,
311                param_to_arg_map,
312                to_inst_param_type,
313                inst_lf,
314            )?),
315            AtomicFact::NotIsNonemptySetFact(fact) => {
316                AtomicFact::NotIsNonemptySetFact(self.inst_not_is_nonempty_set_fact(
317                    fact,
318                    param_to_arg_map,
319                    to_inst_param_type,
320                    inst_lf,
321                )?)
322            }
323            AtomicFact::NotIsFiniteSetFact(fact) => {
324                AtomicFact::NotIsFiniteSetFact(self.inst_not_is_finite_set_fact(
325                    fact,
326                    param_to_arg_map,
327                    to_inst_param_type,
328                    inst_lf,
329                )?)
330            }
331            AtomicFact::NotInFact(fact) => AtomicFact::NotInFact(self.inst_not_in_fact(
332                fact,
333                param_to_arg_map,
334                to_inst_param_type,
335                inst_lf,
336            )?),
337            AtomicFact::NotIsCartFact(fact) => AtomicFact::NotIsCartFact(
338                self.inst_not_is_cart_fact(fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
339            ),
340            AtomicFact::NotIsTupleFact(fact) => AtomicFact::NotIsTupleFact(
341                self.inst_not_is_tuple_fact(fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
342            ),
343            AtomicFact::NotSubsetFact(fact) => AtomicFact::NotSubsetFact(
344                self.inst_not_subset_fact(fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
345            ),
346            AtomicFact::NotSupersetFact(fact) => AtomicFact::NotSupersetFact(
347                self.inst_not_superset_fact(fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
348            ),
349            AtomicFact::RestrictFact(fact) => AtomicFact::RestrictFact(self.inst_restrict_fact(
350                fact,
351                param_to_arg_map,
352                to_inst_param_type,
353                inst_lf,
354            )?),
355            AtomicFact::NotRestrictFact(fact) => AtomicFact::NotRestrictFact(
356                self.inst_not_restrict_fact(fact, param_to_arg_map, to_inst_param_type, inst_lf)?,
357            ),
358            AtomicFact::FnEqualInFact(fact) => AtomicFact::FnEqualInFact(FnEqualInFact::new(
359                self.inst_obj(&fact.left, param_to_arg_map, to_inst_param_type)?,
360                self.inst_obj(&fact.right, param_to_arg_map, to_inst_param_type)?,
361                self.inst_obj(&fact.set, param_to_arg_map, to_inst_param_type)?,
362                Self::line_file_after_inst(&fact.line_file, inst_lf),
363            )),
364            AtomicFact::FnEqualFact(fact) => AtomicFact::FnEqualFact(FnEqualFact::new(
365                self.inst_obj(&fact.left, param_to_arg_map, to_inst_param_type)?,
366                self.inst_obj(&fact.right, param_to_arg_map, to_inst_param_type)?,
367                Self::line_file_after_inst(&fact.line_file, inst_lf),
368            )),
369            AtomicFact::InjectiveFact(fact) => AtomicFact::InjectiveFact(InjectiveFact::new(
370                self.inst_obj(&fact.function, param_to_arg_map, to_inst_param_type)?,
371                Self::line_file_after_inst(&fact.line_file, inst_lf),
372            )),
373            AtomicFact::SurjectiveFact(fact) => AtomicFact::SurjectiveFact(SurjectiveFact::new(
374                self.inst_obj(&fact.function, param_to_arg_map, to_inst_param_type)?,
375                Self::line_file_after_inst(&fact.line_file, inst_lf),
376            )),
377            AtomicFact::BijectiveFact(fact) => AtomicFact::BijectiveFact(BijectiveFact::new(
378                self.inst_obj(&fact.function, param_to_arg_map, to_inst_param_type)?,
379                Self::line_file_after_inst(&fact.line_file, inst_lf),
380            )),
381            AtomicFact::NotInjectiveFact(fact) => {
382                AtomicFact::NotInjectiveFact(NotInjectiveFact::new(
383                    self.inst_obj(&fact.function, param_to_arg_map, to_inst_param_type)?,
384                    Self::line_file_after_inst(&fact.line_file, inst_lf),
385                ))
386            }
387            AtomicFact::NotSurjectiveFact(fact) => {
388                AtomicFact::NotSurjectiveFact(NotSurjectiveFact::new(
389                    self.inst_obj(&fact.function, param_to_arg_map, to_inst_param_type)?,
390                    Self::line_file_after_inst(&fact.line_file, inst_lf),
391                ))
392            }
393            AtomicFact::NotBijectiveFact(fact) => {
394                AtomicFact::NotBijectiveFact(NotBijectiveFact::new(
395                    self.inst_obj(&fact.function, param_to_arg_map, to_inst_param_type)?,
396                    Self::line_file_after_inst(&fact.line_file, inst_lf),
397                ))
398            }
399        })
400    }
401
402    pub fn inst_normal_atomic_fact(
403        &self,
404        normal_atomic_fact: &NormalAtomicFact,
405        param_to_arg_map: &HashMap<String, Obj>,
406        to_inst_param_type: ParamObjType,
407        inst_lf: Option<&LineFile>,
408    ) -> Result<NormalAtomicFact, RuntimeError> {
409        let mut body = Vec::with_capacity(normal_atomic_fact.body.len());
410        for obj in normal_atomic_fact.body.iter() {
411            body.push(self.inst_obj(obj, param_to_arg_map, to_inst_param_type)?);
412        }
413        Ok(NormalAtomicFact::new(
414            normal_atomic_fact.predicate.clone(),
415            body,
416            Self::line_file_after_inst(&normal_atomic_fact.line_file, inst_lf),
417        ))
418    }
419
420    pub fn inst_equal_fact(
421        &self,
422        equal_fact: &EqualFact,
423        param_to_arg_map: &HashMap<String, Obj>,
424        to_inst_param_type: ParamObjType,
425        inst_lf: Option<&LineFile>,
426    ) -> Result<EqualFact, RuntimeError> {
427        Ok(EqualFact::new(
428            self.inst_obj(&equal_fact.left, param_to_arg_map, to_inst_param_type)?,
429            self.inst_obj(&equal_fact.right, param_to_arg_map, to_inst_param_type)?,
430            Self::line_file_after_inst(&equal_fact.line_file, inst_lf),
431        ))
432    }
433
434    pub fn inst_less_fact(
435        &self,
436        less_fact: &LessFact,
437        param_to_arg_map: &HashMap<String, Obj>,
438        to_inst_param_type: ParamObjType,
439        inst_lf: Option<&LineFile>,
440    ) -> Result<LessFact, RuntimeError> {
441        Ok(LessFact::new(
442            self.inst_obj(&less_fact.left, param_to_arg_map, to_inst_param_type)?,
443            self.inst_obj(&less_fact.right, param_to_arg_map, to_inst_param_type)?,
444            Self::line_file_after_inst(&less_fact.line_file, inst_lf),
445        ))
446    }
447
448    pub fn inst_greater_fact(
449        &self,
450        greater_fact: &GreaterFact,
451        param_to_arg_map: &HashMap<String, Obj>,
452        to_inst_param_type: ParamObjType,
453        inst_lf: Option<&LineFile>,
454    ) -> Result<GreaterFact, RuntimeError> {
455        Ok(GreaterFact::new(
456            self.inst_obj(&greater_fact.left, param_to_arg_map, to_inst_param_type)?,
457            self.inst_obj(&greater_fact.right, param_to_arg_map, to_inst_param_type)?,
458            Self::line_file_after_inst(&greater_fact.line_file, inst_lf),
459        ))
460    }
461
462    pub fn inst_less_equal_fact(
463        &self,
464        less_equal_fact: &LessEqualFact,
465        param_to_arg_map: &HashMap<String, Obj>,
466        to_inst_param_type: ParamObjType,
467        inst_lf: Option<&LineFile>,
468    ) -> Result<LessEqualFact, RuntimeError> {
469        Ok(LessEqualFact::new(
470            self.inst_obj(&less_equal_fact.left, param_to_arg_map, to_inst_param_type)?,
471            self.inst_obj(&less_equal_fact.right, param_to_arg_map, to_inst_param_type)?,
472            Self::line_file_after_inst(&less_equal_fact.line_file, inst_lf),
473        ))
474    }
475
476    pub fn inst_greater_equal_fact(
477        &self,
478        greater_equal_fact: &GreaterEqualFact,
479        param_to_arg_map: &HashMap<String, Obj>,
480        to_inst_param_type: ParamObjType,
481        inst_lf: Option<&LineFile>,
482    ) -> Result<GreaterEqualFact, RuntimeError> {
483        Ok(GreaterEqualFact::new(
484            self.inst_obj(
485                &greater_equal_fact.left,
486                param_to_arg_map,
487                to_inst_param_type,
488            )?,
489            self.inst_obj(
490                &greater_equal_fact.right,
491                param_to_arg_map,
492                to_inst_param_type,
493            )?,
494            Self::line_file_after_inst(&greater_equal_fact.line_file, inst_lf),
495        ))
496    }
497
498    pub fn inst_is_set_fact(
499        &self,
500        is_set_fact: &IsSetFact,
501        param_to_arg_map: &HashMap<String, Obj>,
502        to_inst_param_type: ParamObjType,
503        inst_lf: Option<&LineFile>,
504    ) -> Result<IsSetFact, RuntimeError> {
505        Ok(IsSetFact::new(
506            self.inst_obj(&is_set_fact.set, param_to_arg_map, to_inst_param_type)?,
507            Self::line_file_after_inst(&is_set_fact.line_file, inst_lf),
508        ))
509    }
510
511    pub fn inst_is_nonempty_set_fact(
512        &self,
513        is_nonempty_set_fact: &IsNonemptySetFact,
514        param_to_arg_map: &HashMap<String, Obj>,
515        to_inst_param_type: ParamObjType,
516        inst_lf: Option<&LineFile>,
517    ) -> Result<IsNonemptySetFact, RuntimeError> {
518        Ok(IsNonemptySetFact::new(
519            self.inst_obj(
520                &is_nonempty_set_fact.set,
521                param_to_arg_map,
522                to_inst_param_type,
523            )?,
524            Self::line_file_after_inst(&is_nonempty_set_fact.line_file, inst_lf),
525        ))
526    }
527
528    pub fn inst_is_finite_set_fact(
529        &self,
530        is_finite_set_fact: &IsFiniteSetFact,
531        param_to_arg_map: &HashMap<String, Obj>,
532        to_inst_param_type: ParamObjType,
533        inst_lf: Option<&LineFile>,
534    ) -> Result<IsFiniteSetFact, RuntimeError> {
535        Ok(IsFiniteSetFact::new(
536            self.inst_obj(
537                &is_finite_set_fact.set,
538                param_to_arg_map,
539                to_inst_param_type,
540            )?,
541            Self::line_file_after_inst(&is_finite_set_fact.line_file, inst_lf),
542        ))
543    }
544
545    pub fn inst_in_fact(
546        &self,
547        in_fact: &InFact,
548        param_to_arg_map: &HashMap<String, Obj>,
549        to_inst_param_type: ParamObjType,
550        inst_lf: Option<&LineFile>,
551    ) -> Result<InFact, RuntimeError> {
552        Ok(InFact::new(
553            self.inst_obj(&in_fact.element, param_to_arg_map, to_inst_param_type)?,
554            self.inst_obj(&in_fact.set, param_to_arg_map, to_inst_param_type)?,
555            Self::line_file_after_inst(&in_fact.line_file, inst_lf),
556        ))
557    }
558
559    pub fn inst_is_cart_fact(
560        &self,
561        is_cart_fact: &IsCartFact,
562        param_to_arg_map: &HashMap<String, Obj>,
563        to_inst_param_type: ParamObjType,
564        inst_lf: Option<&LineFile>,
565    ) -> Result<IsCartFact, RuntimeError> {
566        Ok(IsCartFact::new(
567            self.inst_obj(&is_cart_fact.set, param_to_arg_map, to_inst_param_type)?,
568            Self::line_file_after_inst(&is_cart_fact.line_file, inst_lf),
569        ))
570    }
571
572    pub fn inst_is_tuple_fact(
573        &self,
574        is_tuple_fact: &IsTupleFact,
575        param_to_arg_map: &HashMap<String, Obj>,
576        to_inst_param_type: ParamObjType,
577        inst_lf: Option<&LineFile>,
578    ) -> Result<IsTupleFact, RuntimeError> {
579        Ok(IsTupleFact::new(
580            self.inst_obj(&is_tuple_fact.set, param_to_arg_map, to_inst_param_type)?,
581            Self::line_file_after_inst(&is_tuple_fact.line_file, inst_lf),
582        ))
583    }
584
585    pub fn inst_subset_fact(
586        &self,
587        subset_fact: &SubsetFact,
588        param_to_arg_map: &HashMap<String, Obj>,
589        to_inst_param_type: ParamObjType,
590        inst_lf: Option<&LineFile>,
591    ) -> Result<SubsetFact, RuntimeError> {
592        Ok(SubsetFact::new(
593            self.inst_obj(&subset_fact.left, param_to_arg_map, to_inst_param_type)?,
594            self.inst_obj(&subset_fact.right, param_to_arg_map, to_inst_param_type)?,
595            Self::line_file_after_inst(&subset_fact.line_file, inst_lf),
596        ))
597    }
598
599    pub fn inst_superset_fact(
600        &self,
601        superset_fact: &SupersetFact,
602        param_to_arg_map: &HashMap<String, Obj>,
603        to_inst_param_type: ParamObjType,
604        inst_lf: Option<&LineFile>,
605    ) -> Result<SupersetFact, RuntimeError> {
606        Ok(SupersetFact::new(
607            self.inst_obj(&superset_fact.left, param_to_arg_map, to_inst_param_type)?,
608            self.inst_obj(&superset_fact.right, param_to_arg_map, to_inst_param_type)?,
609            Self::line_file_after_inst(&superset_fact.line_file, inst_lf),
610        ))
611    }
612
613    pub fn inst_not_normal_atomic_fact(
614        &self,
615        not_normal_atomic_fact: &NotNormalAtomicFact,
616        param_to_arg_map: &HashMap<String, Obj>,
617        to_inst_param_type: ParamObjType,
618        inst_lf: Option<&LineFile>,
619    ) -> Result<NotNormalAtomicFact, RuntimeError> {
620        let mut body = Vec::with_capacity(not_normal_atomic_fact.body.len());
621        for obj in not_normal_atomic_fact.body.iter() {
622            body.push(self.inst_obj(obj, param_to_arg_map, to_inst_param_type)?);
623        }
624        Ok(NotNormalAtomicFact::new(
625            not_normal_atomic_fact.predicate.clone(),
626            body,
627            Self::line_file_after_inst(&not_normal_atomic_fact.line_file, inst_lf),
628        ))
629    }
630
631    pub fn inst_not_equal_fact(
632        &self,
633        not_equal_fact: &NotEqualFact,
634        param_to_arg_map: &HashMap<String, Obj>,
635        to_inst_param_type: ParamObjType,
636        inst_lf: Option<&LineFile>,
637    ) -> Result<NotEqualFact, RuntimeError> {
638        Ok(NotEqualFact::new(
639            self.inst_obj(&not_equal_fact.left, param_to_arg_map, to_inst_param_type)?,
640            self.inst_obj(&not_equal_fact.right, param_to_arg_map, to_inst_param_type)?,
641            Self::line_file_after_inst(&not_equal_fact.line_file, inst_lf),
642        ))
643    }
644
645    pub fn inst_not_less_fact(
646        &self,
647        not_less_fact: &NotLessFact,
648        param_to_arg_map: &HashMap<String, Obj>,
649        to_inst_param_type: ParamObjType,
650        inst_lf: Option<&LineFile>,
651    ) -> Result<NotLessFact, RuntimeError> {
652        Ok(NotLessFact::new(
653            self.inst_obj(&not_less_fact.left, param_to_arg_map, to_inst_param_type)?,
654            self.inst_obj(&not_less_fact.right, param_to_arg_map, to_inst_param_type)?,
655            Self::line_file_after_inst(&not_less_fact.line_file, inst_lf),
656        ))
657    }
658
659    pub fn inst_not_greater_fact(
660        &self,
661        not_greater_fact: &NotGreaterFact,
662        param_to_arg_map: &HashMap<String, Obj>,
663        to_inst_param_type: ParamObjType,
664        inst_lf: Option<&LineFile>,
665    ) -> Result<NotGreaterFact, RuntimeError> {
666        Ok(NotGreaterFact::new(
667            self.inst_obj(&not_greater_fact.left, param_to_arg_map, to_inst_param_type)?,
668            self.inst_obj(
669                &not_greater_fact.right,
670                param_to_arg_map,
671                to_inst_param_type,
672            )?,
673            Self::line_file_after_inst(&not_greater_fact.line_file, inst_lf),
674        ))
675    }
676
677    pub fn inst_not_less_equal_fact(
678        &self,
679        not_less_equal_fact: &NotLessEqualFact,
680        param_to_arg_map: &HashMap<String, Obj>,
681        to_inst_param_type: ParamObjType,
682        inst_lf: Option<&LineFile>,
683    ) -> Result<NotLessEqualFact, RuntimeError> {
684        Ok(NotLessEqualFact::new(
685            self.inst_obj(
686                &not_less_equal_fact.left,
687                param_to_arg_map,
688                to_inst_param_type,
689            )?,
690            self.inst_obj(
691                &not_less_equal_fact.right,
692                param_to_arg_map,
693                to_inst_param_type,
694            )?,
695            Self::line_file_after_inst(&not_less_equal_fact.line_file, inst_lf),
696        ))
697    }
698
699    pub fn inst_not_greater_equal_fact(
700        &self,
701        not_greater_equal_fact: &NotGreaterEqualFact,
702        param_to_arg_map: &HashMap<String, Obj>,
703        to_inst_param_type: ParamObjType,
704        inst_lf: Option<&LineFile>,
705    ) -> Result<NotGreaterEqualFact, RuntimeError> {
706        Ok(NotGreaterEqualFact::new(
707            self.inst_obj(
708                &not_greater_equal_fact.left,
709                param_to_arg_map,
710                to_inst_param_type,
711            )?,
712            self.inst_obj(
713                &not_greater_equal_fact.right,
714                param_to_arg_map,
715                to_inst_param_type,
716            )?,
717            Self::line_file_after_inst(&not_greater_equal_fact.line_file, inst_lf),
718        ))
719    }
720
721    pub fn inst_not_is_set_fact(
722        &self,
723        not_is_set_fact: &NotIsSetFact,
724        param_to_arg_map: &HashMap<String, Obj>,
725        to_inst_param_type: ParamObjType,
726        inst_lf: Option<&LineFile>,
727    ) -> Result<NotIsSetFact, RuntimeError> {
728        Ok(NotIsSetFact::new(
729            self.inst_obj(&not_is_set_fact.set, param_to_arg_map, to_inst_param_type)?,
730            Self::line_file_after_inst(&not_is_set_fact.line_file, inst_lf),
731        ))
732    }
733
734    pub fn inst_not_is_nonempty_set_fact(
735        &self,
736        not_is_nonempty_set_fact: &NotIsNonemptySetFact,
737        param_to_arg_map: &HashMap<String, Obj>,
738        to_inst_param_type: ParamObjType,
739        inst_lf: Option<&LineFile>,
740    ) -> Result<NotIsNonemptySetFact, RuntimeError> {
741        Ok(NotIsNonemptySetFact::new(
742            self.inst_obj(
743                &not_is_nonempty_set_fact.set,
744                param_to_arg_map,
745                to_inst_param_type,
746            )?,
747            Self::line_file_after_inst(&not_is_nonempty_set_fact.line_file, inst_lf),
748        ))
749    }
750
751    pub fn inst_not_is_finite_set_fact(
752        &self,
753        not_is_finite_set_fact: &NotIsFiniteSetFact,
754        param_to_arg_map: &HashMap<String, Obj>,
755        to_inst_param_type: ParamObjType,
756        inst_lf: Option<&LineFile>,
757    ) -> Result<NotIsFiniteSetFact, RuntimeError> {
758        Ok(NotIsFiniteSetFact::new(
759            self.inst_obj(
760                &not_is_finite_set_fact.set,
761                param_to_arg_map,
762                to_inst_param_type,
763            )?,
764            Self::line_file_after_inst(&not_is_finite_set_fact.line_file, inst_lf),
765        ))
766    }
767
768    pub fn inst_not_in_fact(
769        &self,
770        not_in_fact: &NotInFact,
771        param_to_arg_map: &HashMap<String, Obj>,
772        to_inst_param_type: ParamObjType,
773        inst_lf: Option<&LineFile>,
774    ) -> Result<NotInFact, RuntimeError> {
775        Ok(NotInFact::new(
776            self.inst_obj(&not_in_fact.element, param_to_arg_map, to_inst_param_type)?,
777            self.inst_obj(&not_in_fact.set, param_to_arg_map, to_inst_param_type)?,
778            Self::line_file_after_inst(&not_in_fact.line_file, inst_lf),
779        ))
780    }
781
782    pub fn inst_not_is_cart_fact(
783        &self,
784        not_is_cart_fact: &NotIsCartFact,
785        param_to_arg_map: &HashMap<String, Obj>,
786        to_inst_param_type: ParamObjType,
787        inst_lf: Option<&LineFile>,
788    ) -> Result<NotIsCartFact, RuntimeError> {
789        Ok(NotIsCartFact::new(
790            self.inst_obj(&not_is_cart_fact.set, param_to_arg_map, to_inst_param_type)?,
791            Self::line_file_after_inst(&not_is_cart_fact.line_file, inst_lf),
792        ))
793    }
794
795    pub fn inst_not_is_tuple_fact(
796        &self,
797        not_is_tuple_fact: &NotIsTupleFact,
798        param_to_arg_map: &HashMap<String, Obj>,
799        to_inst_param_type: ParamObjType,
800        inst_lf: Option<&LineFile>,
801    ) -> Result<NotIsTupleFact, RuntimeError> {
802        Ok(NotIsTupleFact::new(
803            self.inst_obj(&not_is_tuple_fact.set, param_to_arg_map, to_inst_param_type)?,
804            Self::line_file_after_inst(&not_is_tuple_fact.line_file, inst_lf),
805        ))
806    }
807
808    pub fn inst_not_subset_fact(
809        &self,
810        not_subset_fact: &NotSubsetFact,
811        param_to_arg_map: &HashMap<String, Obj>,
812        to_inst_param_type: ParamObjType,
813        inst_lf: Option<&LineFile>,
814    ) -> Result<NotSubsetFact, RuntimeError> {
815        Ok(NotSubsetFact::new(
816            self.inst_obj(&not_subset_fact.left, param_to_arg_map, to_inst_param_type)?,
817            self.inst_obj(&not_subset_fact.right, param_to_arg_map, to_inst_param_type)?,
818            Self::line_file_after_inst(&not_subset_fact.line_file, inst_lf),
819        ))
820    }
821
822    pub fn inst_not_superset_fact(
823        &self,
824        not_superset_fact: &NotSupersetFact,
825        param_to_arg_map: &HashMap<String, Obj>,
826        to_inst_param_type: ParamObjType,
827        inst_lf: Option<&LineFile>,
828    ) -> Result<NotSupersetFact, RuntimeError> {
829        Ok(NotSupersetFact::new(
830            self.inst_obj(
831                &not_superset_fact.left,
832                param_to_arg_map,
833                to_inst_param_type,
834            )?,
835            self.inst_obj(
836                &not_superset_fact.right,
837                param_to_arg_map,
838                to_inst_param_type,
839            )?,
840            Self::line_file_after_inst(&not_superset_fact.line_file, inst_lf),
841        ))
842    }
843
844    pub fn inst_exist_fact(
845        &self,
846        exist_fact: &ExistFactEnum,
847        param_to_arg_map: &HashMap<String, Obj>,
848        to_inst_param_type: ParamObjType,
849        inst_lf: Option<&LineFile>,
850    ) -> Result<ExistFactEnum, RuntimeError> {
851        let mut groups = Vec::with_capacity(exist_fact.params_def_with_type().groups.len());
852        for param_def_with_type in exist_fact.params_def_with_type().groups.iter() {
853            groups.push(ParamGroupWithParamType::new(
854                param_def_with_type.params.clone(),
855                self.inst_param_type(
856                    &param_def_with_type.param_type,
857                    param_to_arg_map,
858                    to_inst_param_type,
859                )?,
860            ));
861        }
862        let params_def_with_type = ParamDefWithType::new(groups);
863        let mut facts = Vec::with_capacity(exist_fact.facts().len());
864        for fact in exist_fact.facts().iter() {
865            facts.push(self.inst_exist_body_fact(
866                fact,
867                param_to_arg_map,
868                to_inst_param_type,
869                inst_lf,
870            )?);
871        }
872        let body = ExistFactBody::new(
873            params_def_with_type,
874            facts,
875            Self::line_file_after_inst(&exist_fact.body().line_file, inst_lf),
876        )?;
877        Ok(match exist_fact {
878            ExistFactEnum::ExistFact(_) => ExistFactEnum::ExistFact(body),
879            ExistFactEnum::ExistUniqueFact(_) => ExistFactEnum::ExistUniqueFact(body),
880            ExistFactEnum::NotExistFact(_) => ExistFactEnum::NotExistFact(body),
881        })
882    }
883
884    pub fn inst_or_fact(
885        &self,
886        or_fact: &OrFact,
887        param_to_arg_map: &HashMap<String, Obj>,
888        to_inst_param_type: ParamObjType,
889        inst_lf: Option<&LineFile>,
890    ) -> Result<OrFact, RuntimeError> {
891        let mut facts = Vec::with_capacity(or_fact.facts.len());
892        for fact in or_fact.facts.iter() {
893            facts.push(self.inst_and_chain_atomic_fact(
894                fact,
895                param_to_arg_map,
896                to_inst_param_type,
897                inst_lf,
898            )?);
899        }
900        Ok(OrFact::new(
901            facts,
902            Self::line_file_after_inst(&or_fact.line_file, inst_lf),
903        ))
904    }
905
906    pub fn inst_and_fact(
907        &self,
908        and_fact: &AndFact,
909        param_to_arg_map: &HashMap<String, Obj>,
910        to_inst_param_type: ParamObjType,
911        inst_lf: Option<&LineFile>,
912    ) -> Result<AndFact, RuntimeError> {
913        let mut facts = Vec::with_capacity(and_fact.facts.len());
914        for fact in and_fact.facts.iter() {
915            facts.push(self.inst_atomic_fact(
916                fact,
917                param_to_arg_map,
918                to_inst_param_type,
919                inst_lf,
920            )?);
921        }
922        Ok(AndFact::new(
923            facts,
924            Self::line_file_after_inst(&and_fact.line_file, inst_lf),
925        ))
926    }
927
928    pub fn inst_chain_fact(
929        &self,
930        chain_fact: &ChainFact,
931        param_to_arg_map: &HashMap<String, Obj>,
932        to_inst_param_type: ParamObjType,
933        inst_lf: Option<&LineFile>,
934    ) -> Result<ChainFact, RuntimeError> {
935        let mut objs = Vec::with_capacity(chain_fact.objs.len());
936        for obj in chain_fact.objs.iter() {
937            objs.push(self.inst_obj(obj, param_to_arg_map, to_inst_param_type)?);
938        }
939        Ok(ChainFact::new(
940            objs,
941            chain_fact.prop_names.clone(),
942            Self::line_file_after_inst(&chain_fact.line_file, inst_lf),
943        ))
944    }
945
946    pub fn inst_forall_fact(
947        &self,
948        forall_fact: &ForallFact,
949        param_to_arg_map: &HashMap<String, Obj>,
950        to_inst_param_type: ParamObjType,
951        inst_lf: Option<&LineFile>,
952    ) -> Result<ForallFact, RuntimeError> {
953        let mut groups = Vec::with_capacity(forall_fact.params_def_with_type.groups.len());
954        for param_def_with_type in forall_fact.params_def_with_type.groups.iter() {
955            groups.push(ParamGroupWithParamType::new(
956                param_def_with_type.params.clone(),
957                self.inst_param_type(
958                    &param_def_with_type.param_type,
959                    param_to_arg_map,
960                    to_inst_param_type,
961                )?,
962            ));
963        }
964        let params_def_with_type = ParamDefWithType::new(groups);
965        let mut dom_facts = Vec::with_capacity(forall_fact.dom_facts.len());
966        for dom_fact in forall_fact.dom_facts.iter() {
967            dom_facts.push(self.inst_fact(
968                dom_fact,
969                param_to_arg_map,
970                to_inst_param_type,
971                inst_lf.cloned(),
972            )?);
973        }
974        let mut then_facts = Vec::with_capacity(forall_fact.then_facts.len());
975        for then_fact in forall_fact.then_facts.iter() {
976            then_facts.push(self.inst_exist_or_and_chain_atomic_fact(
977                then_fact,
978                param_to_arg_map,
979                to_inst_param_type,
980                inst_lf,
981            )?);
982        }
983        Ok(ForallFact::new(
984            params_def_with_type,
985            dom_facts,
986            then_facts,
987            Self::line_file_after_inst(&forall_fact.line_file, inst_lf),
988        )?)
989    }
990
991    pub fn inst_forall_fact_with_iff(
992        &self,
993        forall_fact_with_iff: &ForallFactWithIff,
994        param_to_arg_map: &HashMap<String, Obj>,
995        to_inst_param_type: ParamObjType,
996        inst_lf: Option<&LineFile>,
997    ) -> Result<ForallFactWithIff, RuntimeError> {
998        let forall_fact = self.inst_forall_fact(
999            &forall_fact_with_iff.forall_fact,
1000            param_to_arg_map,
1001            to_inst_param_type,
1002            inst_lf,
1003        )?;
1004        let mut iff_facts = Vec::with_capacity(forall_fact_with_iff.iff_facts.len());
1005        for iff_fact in forall_fact_with_iff.iff_facts.iter() {
1006            iff_facts.push(self.inst_exist_or_and_chain_atomic_fact(
1007                iff_fact,
1008                param_to_arg_map,
1009                to_inst_param_type,
1010                inst_lf,
1011            )?);
1012        }
1013        Ok(ForallFactWithIff::new(
1014            forall_fact,
1015            iff_facts,
1016            Self::line_file_after_inst(&forall_fact_with_iff.line_file, inst_lf),
1017        )?)
1018    }
1019
1020    pub fn inst_restrict_fact(
1021        &self,
1022        restrict_fact: &RestrictFact,
1023        param_to_arg_map: &HashMap<String, Obj>,
1024        to_inst_param_type: ParamObjType,
1025        inst_lf: Option<&LineFile>,
1026    ) -> Result<RestrictFact, RuntimeError> {
1027        Ok(RestrictFact::new(
1028            self.inst_obj(&restrict_fact.obj, param_to_arg_map, to_inst_param_type)?,
1029            self.inst_obj(
1030                &restrict_fact.obj_can_restrict_to_fn_set,
1031                param_to_arg_map,
1032                to_inst_param_type,
1033            )?,
1034            Self::line_file_after_inst(&restrict_fact.line_file, inst_lf),
1035        ))
1036    }
1037
1038    pub fn inst_not_restrict_fact(
1039        &self,
1040        not_restrict_fact: &NotRestrictFact,
1041        param_to_arg_map: &HashMap<String, Obj>,
1042        to_inst_param_type: ParamObjType,
1043        inst_lf: Option<&LineFile>,
1044    ) -> Result<NotRestrictFact, RuntimeError> {
1045        Ok(NotRestrictFact::new(
1046            self.inst_obj(&not_restrict_fact.obj, param_to_arg_map, to_inst_param_type)?,
1047            self.inst_obj(
1048                &not_restrict_fact.obj_cannot_restrict_to_fn_set,
1049                param_to_arg_map,
1050                to_inst_param_type,
1051            )?,
1052            Self::line_file_after_inst(&not_restrict_fact.line_file, inst_lf),
1053        ))
1054    }
1055}
litex/runtime/runtime_instantiate_fact.rs

litex/runtime/
runtime_instantiate_fact.rs
