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        })
370    }
371
372    pub fn inst_normal_atomic_fact(
373        &self,
374        normal_atomic_fact: &NormalAtomicFact,
375        param_to_arg_map: &HashMap<String, Obj>,
376        to_inst_param_type: ParamObjType,
377        inst_lf: Option<&LineFile>,
378    ) -> Result<NormalAtomicFact, RuntimeError> {
379        let mut body = Vec::with_capacity(normal_atomic_fact.body.len());
380        for obj in normal_atomic_fact.body.iter() {
381            body.push(self.inst_obj(obj, param_to_arg_map, to_inst_param_type)?);
382        }
383        Ok(NormalAtomicFact::new(
384            normal_atomic_fact.predicate.clone(),
385            body,
386            Self::line_file_after_inst(&normal_atomic_fact.line_file, inst_lf),
387        ))
388    }
389
390    pub fn inst_equal_fact(
391        &self,
392        equal_fact: &EqualFact,
393        param_to_arg_map: &HashMap<String, Obj>,
394        to_inst_param_type: ParamObjType,
395        inst_lf: Option<&LineFile>,
396    ) -> Result<EqualFact, RuntimeError> {
397        Ok(EqualFact::new(
398            self.inst_obj(&equal_fact.left, param_to_arg_map, to_inst_param_type)?,
399            self.inst_obj(&equal_fact.right, param_to_arg_map, to_inst_param_type)?,
400            Self::line_file_after_inst(&equal_fact.line_file, inst_lf),
401        ))
402    }
403
404    pub fn inst_less_fact(
405        &self,
406        less_fact: &LessFact,
407        param_to_arg_map: &HashMap<String, Obj>,
408        to_inst_param_type: ParamObjType,
409        inst_lf: Option<&LineFile>,
410    ) -> Result<LessFact, RuntimeError> {
411        Ok(LessFact::new(
412            self.inst_obj(&less_fact.left, param_to_arg_map, to_inst_param_type)?,
413            self.inst_obj(&less_fact.right, param_to_arg_map, to_inst_param_type)?,
414            Self::line_file_after_inst(&less_fact.line_file, inst_lf),
415        ))
416    }
417
418    pub fn inst_greater_fact(
419        &self,
420        greater_fact: &GreaterFact,
421        param_to_arg_map: &HashMap<String, Obj>,
422        to_inst_param_type: ParamObjType,
423        inst_lf: Option<&LineFile>,
424    ) -> Result<GreaterFact, RuntimeError> {
425        Ok(GreaterFact::new(
426            self.inst_obj(&greater_fact.left, param_to_arg_map, to_inst_param_type)?,
427            self.inst_obj(&greater_fact.right, param_to_arg_map, to_inst_param_type)?,
428            Self::line_file_after_inst(&greater_fact.line_file, inst_lf),
429        ))
430    }
431
432    pub fn inst_less_equal_fact(
433        &self,
434        less_equal_fact: &LessEqualFact,
435        param_to_arg_map: &HashMap<String, Obj>,
436        to_inst_param_type: ParamObjType,
437        inst_lf: Option<&LineFile>,
438    ) -> Result<LessEqualFact, RuntimeError> {
439        Ok(LessEqualFact::new(
440            self.inst_obj(&less_equal_fact.left, param_to_arg_map, to_inst_param_type)?,
441            self.inst_obj(&less_equal_fact.right, param_to_arg_map, to_inst_param_type)?,
442            Self::line_file_after_inst(&less_equal_fact.line_file, inst_lf),
443        ))
444    }
445
446    pub fn inst_greater_equal_fact(
447        &self,
448        greater_equal_fact: &GreaterEqualFact,
449        param_to_arg_map: &HashMap<String, Obj>,
450        to_inst_param_type: ParamObjType,
451        inst_lf: Option<&LineFile>,
452    ) -> Result<GreaterEqualFact, RuntimeError> {
453        Ok(GreaterEqualFact::new(
454            self.inst_obj(
455                &greater_equal_fact.left,
456                param_to_arg_map,
457                to_inst_param_type,
458            )?,
459            self.inst_obj(
460                &greater_equal_fact.right,
461                param_to_arg_map,
462                to_inst_param_type,
463            )?,
464            Self::line_file_after_inst(&greater_equal_fact.line_file, inst_lf),
465        ))
466    }
467
468    pub fn inst_is_set_fact(
469        &self,
470        is_set_fact: &IsSetFact,
471        param_to_arg_map: &HashMap<String, Obj>,
472        to_inst_param_type: ParamObjType,
473        inst_lf: Option<&LineFile>,
474    ) -> Result<IsSetFact, RuntimeError> {
475        Ok(IsSetFact::new(
476            self.inst_obj(&is_set_fact.set, param_to_arg_map, to_inst_param_type)?,
477            Self::line_file_after_inst(&is_set_fact.line_file, inst_lf),
478        ))
479    }
480
481    pub fn inst_is_nonempty_set_fact(
482        &self,
483        is_nonempty_set_fact: &IsNonemptySetFact,
484        param_to_arg_map: &HashMap<String, Obj>,
485        to_inst_param_type: ParamObjType,
486        inst_lf: Option<&LineFile>,
487    ) -> Result<IsNonemptySetFact, RuntimeError> {
488        Ok(IsNonemptySetFact::new(
489            self.inst_obj(
490                &is_nonempty_set_fact.set,
491                param_to_arg_map,
492                to_inst_param_type,
493            )?,
494            Self::line_file_after_inst(&is_nonempty_set_fact.line_file, inst_lf),
495        ))
496    }
497
498    pub fn inst_is_finite_set_fact(
499        &self,
500        is_finite_set_fact: &IsFiniteSetFact,
501        param_to_arg_map: &HashMap<String, Obj>,
502        to_inst_param_type: ParamObjType,
503        inst_lf: Option<&LineFile>,
504    ) -> Result<IsFiniteSetFact, RuntimeError> {
505        Ok(IsFiniteSetFact::new(
506            self.inst_obj(
507                &is_finite_set_fact.set,
508                param_to_arg_map,
509                to_inst_param_type,
510            )?,
511            Self::line_file_after_inst(&is_finite_set_fact.line_file, inst_lf),
512        ))
513    }
514
515    pub fn inst_in_fact(
516        &self,
517        in_fact: &InFact,
518        param_to_arg_map: &HashMap<String, Obj>,
519        to_inst_param_type: ParamObjType,
520        inst_lf: Option<&LineFile>,
521    ) -> Result<InFact, RuntimeError> {
522        Ok(InFact::new(
523            self.inst_obj(&in_fact.element, param_to_arg_map, to_inst_param_type)?,
524            self.inst_obj(&in_fact.set, param_to_arg_map, to_inst_param_type)?,
525            Self::line_file_after_inst(&in_fact.line_file, inst_lf),
526        ))
527    }
528
529    pub fn inst_is_cart_fact(
530        &self,
531        is_cart_fact: &IsCartFact,
532        param_to_arg_map: &HashMap<String, Obj>,
533        to_inst_param_type: ParamObjType,
534        inst_lf: Option<&LineFile>,
535    ) -> Result<IsCartFact, RuntimeError> {
536        Ok(IsCartFact::new(
537            self.inst_obj(&is_cart_fact.set, param_to_arg_map, to_inst_param_type)?,
538            Self::line_file_after_inst(&is_cart_fact.line_file, inst_lf),
539        ))
540    }
541
542    pub fn inst_is_tuple_fact(
543        &self,
544        is_tuple_fact: &IsTupleFact,
545        param_to_arg_map: &HashMap<String, Obj>,
546        to_inst_param_type: ParamObjType,
547        inst_lf: Option<&LineFile>,
548    ) -> Result<IsTupleFact, RuntimeError> {
549        Ok(IsTupleFact::new(
550            self.inst_obj(&is_tuple_fact.set, param_to_arg_map, to_inst_param_type)?,
551            Self::line_file_after_inst(&is_tuple_fact.line_file, inst_lf),
552        ))
553    }
554
555    pub fn inst_subset_fact(
556        &self,
557        subset_fact: &SubsetFact,
558        param_to_arg_map: &HashMap<String, Obj>,
559        to_inst_param_type: ParamObjType,
560        inst_lf: Option<&LineFile>,
561    ) -> Result<SubsetFact, RuntimeError> {
562        Ok(SubsetFact::new(
563            self.inst_obj(&subset_fact.left, param_to_arg_map, to_inst_param_type)?,
564            self.inst_obj(&subset_fact.right, param_to_arg_map, to_inst_param_type)?,
565            Self::line_file_after_inst(&subset_fact.line_file, inst_lf),
566        ))
567    }
568
569    pub fn inst_superset_fact(
570        &self,
571        superset_fact: &SupersetFact,
572        param_to_arg_map: &HashMap<String, Obj>,
573        to_inst_param_type: ParamObjType,
574        inst_lf: Option<&LineFile>,
575    ) -> Result<SupersetFact, RuntimeError> {
576        Ok(SupersetFact::new(
577            self.inst_obj(&superset_fact.left, param_to_arg_map, to_inst_param_type)?,
578            self.inst_obj(&superset_fact.right, param_to_arg_map, to_inst_param_type)?,
579            Self::line_file_after_inst(&superset_fact.line_file, inst_lf),
580        ))
581    }
582
583    pub fn inst_not_normal_atomic_fact(
584        &self,
585        not_normal_atomic_fact: &NotNormalAtomicFact,
586        param_to_arg_map: &HashMap<String, Obj>,
587        to_inst_param_type: ParamObjType,
588        inst_lf: Option<&LineFile>,
589    ) -> Result<NotNormalAtomicFact, RuntimeError> {
590        let mut body = Vec::with_capacity(not_normal_atomic_fact.body.len());
591        for obj in not_normal_atomic_fact.body.iter() {
592            body.push(self.inst_obj(obj, param_to_arg_map, to_inst_param_type)?);
593        }
594        Ok(NotNormalAtomicFact::new(
595            not_normal_atomic_fact.predicate.clone(),
596            body,
597            Self::line_file_after_inst(&not_normal_atomic_fact.line_file, inst_lf),
598        ))
599    }
600
601    pub fn inst_not_equal_fact(
602        &self,
603        not_equal_fact: &NotEqualFact,
604        param_to_arg_map: &HashMap<String, Obj>,
605        to_inst_param_type: ParamObjType,
606        inst_lf: Option<&LineFile>,
607    ) -> Result<NotEqualFact, RuntimeError> {
608        Ok(NotEqualFact::new(
609            self.inst_obj(&not_equal_fact.left, param_to_arg_map, to_inst_param_type)?,
610            self.inst_obj(&not_equal_fact.right, param_to_arg_map, to_inst_param_type)?,
611            Self::line_file_after_inst(&not_equal_fact.line_file, inst_lf),
612        ))
613    }
614
615    pub fn inst_not_less_fact(
616        &self,
617        not_less_fact: &NotLessFact,
618        param_to_arg_map: &HashMap<String, Obj>,
619        to_inst_param_type: ParamObjType,
620        inst_lf: Option<&LineFile>,
621    ) -> Result<NotLessFact, RuntimeError> {
622        Ok(NotLessFact::new(
623            self.inst_obj(&not_less_fact.left, param_to_arg_map, to_inst_param_type)?,
624            self.inst_obj(&not_less_fact.right, param_to_arg_map, to_inst_param_type)?,
625            Self::line_file_after_inst(&not_less_fact.line_file, inst_lf),
626        ))
627    }
628
629    pub fn inst_not_greater_fact(
630        &self,
631        not_greater_fact: &NotGreaterFact,
632        param_to_arg_map: &HashMap<String, Obj>,
633        to_inst_param_type: ParamObjType,
634        inst_lf: Option<&LineFile>,
635    ) -> Result<NotGreaterFact, RuntimeError> {
636        Ok(NotGreaterFact::new(
637            self.inst_obj(&not_greater_fact.left, param_to_arg_map, to_inst_param_type)?,
638            self.inst_obj(
639                &not_greater_fact.right,
640                param_to_arg_map,
641                to_inst_param_type,
642            )?,
643            Self::line_file_after_inst(&not_greater_fact.line_file, inst_lf),
644        ))
645    }
646
647    pub fn inst_not_less_equal_fact(
648        &self,
649        not_less_equal_fact: &NotLessEqualFact,
650        param_to_arg_map: &HashMap<String, Obj>,
651        to_inst_param_type: ParamObjType,
652        inst_lf: Option<&LineFile>,
653    ) -> Result<NotLessEqualFact, RuntimeError> {
654        Ok(NotLessEqualFact::new(
655            self.inst_obj(
656                &not_less_equal_fact.left,
657                param_to_arg_map,
658                to_inst_param_type,
659            )?,
660            self.inst_obj(
661                &not_less_equal_fact.right,
662                param_to_arg_map,
663                to_inst_param_type,
664            )?,
665            Self::line_file_after_inst(&not_less_equal_fact.line_file, inst_lf),
666        ))
667    }
668
669    pub fn inst_not_greater_equal_fact(
670        &self,
671        not_greater_equal_fact: &NotGreaterEqualFact,
672        param_to_arg_map: &HashMap<String, Obj>,
673        to_inst_param_type: ParamObjType,
674        inst_lf: Option<&LineFile>,
675    ) -> Result<NotGreaterEqualFact, RuntimeError> {
676        Ok(NotGreaterEqualFact::new(
677            self.inst_obj(
678                &not_greater_equal_fact.left,
679                param_to_arg_map,
680                to_inst_param_type,
681            )?,
682            self.inst_obj(
683                &not_greater_equal_fact.right,
684                param_to_arg_map,
685                to_inst_param_type,
686            )?,
687            Self::line_file_after_inst(&not_greater_equal_fact.line_file, inst_lf),
688        ))
689    }
690
691    pub fn inst_not_is_set_fact(
692        &self,
693        not_is_set_fact: &NotIsSetFact,
694        param_to_arg_map: &HashMap<String, Obj>,
695        to_inst_param_type: ParamObjType,
696        inst_lf: Option<&LineFile>,
697    ) -> Result<NotIsSetFact, RuntimeError> {
698        Ok(NotIsSetFact::new(
699            self.inst_obj(&not_is_set_fact.set, param_to_arg_map, to_inst_param_type)?,
700            Self::line_file_after_inst(&not_is_set_fact.line_file, inst_lf),
701        ))
702    }
703
704    pub fn inst_not_is_nonempty_set_fact(
705        &self,
706        not_is_nonempty_set_fact: &NotIsNonemptySetFact,
707        param_to_arg_map: &HashMap<String, Obj>,
708        to_inst_param_type: ParamObjType,
709        inst_lf: Option<&LineFile>,
710    ) -> Result<NotIsNonemptySetFact, RuntimeError> {
711        Ok(NotIsNonemptySetFact::new(
712            self.inst_obj(
713                &not_is_nonempty_set_fact.set,
714                param_to_arg_map,
715                to_inst_param_type,
716            )?,
717            Self::line_file_after_inst(&not_is_nonempty_set_fact.line_file, inst_lf),
718        ))
719    }
720
721    pub fn inst_not_is_finite_set_fact(
722        &self,
723        not_is_finite_set_fact: &NotIsFiniteSetFact,
724        param_to_arg_map: &HashMap<String, Obj>,
725        to_inst_param_type: ParamObjType,
726        inst_lf: Option<&LineFile>,
727    ) -> Result<NotIsFiniteSetFact, RuntimeError> {
728        Ok(NotIsFiniteSetFact::new(
729            self.inst_obj(
730                &not_is_finite_set_fact.set,
731                param_to_arg_map,
732                to_inst_param_type,
733            )?,
734            Self::line_file_after_inst(&not_is_finite_set_fact.line_file, inst_lf),
735        ))
736    }
737
738    pub fn inst_not_in_fact(
739        &self,
740        not_in_fact: &NotInFact,
741        param_to_arg_map: &HashMap<String, Obj>,
742        to_inst_param_type: ParamObjType,
743        inst_lf: Option<&LineFile>,
744    ) -> Result<NotInFact, RuntimeError> {
745        Ok(NotInFact::new(
746            self.inst_obj(&not_in_fact.element, param_to_arg_map, to_inst_param_type)?,
747            self.inst_obj(&not_in_fact.set, param_to_arg_map, to_inst_param_type)?,
748            Self::line_file_after_inst(&not_in_fact.line_file, inst_lf),
749        ))
750    }
751
752    pub fn inst_not_is_cart_fact(
753        &self,
754        not_is_cart_fact: &NotIsCartFact,
755        param_to_arg_map: &HashMap<String, Obj>,
756        to_inst_param_type: ParamObjType,
757        inst_lf: Option<&LineFile>,
758    ) -> Result<NotIsCartFact, RuntimeError> {
759        Ok(NotIsCartFact::new(
760            self.inst_obj(&not_is_cart_fact.set, param_to_arg_map, to_inst_param_type)?,
761            Self::line_file_after_inst(&not_is_cart_fact.line_file, inst_lf),
762        ))
763    }
764
765    pub fn inst_not_is_tuple_fact(
766        &self,
767        not_is_tuple_fact: &NotIsTupleFact,
768        param_to_arg_map: &HashMap<String, Obj>,
769        to_inst_param_type: ParamObjType,
770        inst_lf: Option<&LineFile>,
771    ) -> Result<NotIsTupleFact, RuntimeError> {
772        Ok(NotIsTupleFact::new(
773            self.inst_obj(&not_is_tuple_fact.set, param_to_arg_map, to_inst_param_type)?,
774            Self::line_file_after_inst(&not_is_tuple_fact.line_file, inst_lf),
775        ))
776    }
777
778    pub fn inst_not_subset_fact(
779        &self,
780        not_subset_fact: &NotSubsetFact,
781        param_to_arg_map: &HashMap<String, Obj>,
782        to_inst_param_type: ParamObjType,
783        inst_lf: Option<&LineFile>,
784    ) -> Result<NotSubsetFact, RuntimeError> {
785        Ok(NotSubsetFact::new(
786            self.inst_obj(&not_subset_fact.left, param_to_arg_map, to_inst_param_type)?,
787            self.inst_obj(&not_subset_fact.right, param_to_arg_map, to_inst_param_type)?,
788            Self::line_file_after_inst(&not_subset_fact.line_file, inst_lf),
789        ))
790    }
791
792    pub fn inst_not_superset_fact(
793        &self,
794        not_superset_fact: &NotSupersetFact,
795        param_to_arg_map: &HashMap<String, Obj>,
796        to_inst_param_type: ParamObjType,
797        inst_lf: Option<&LineFile>,
798    ) -> Result<NotSupersetFact, RuntimeError> {
799        Ok(NotSupersetFact::new(
800            self.inst_obj(
801                &not_superset_fact.left,
802                param_to_arg_map,
803                to_inst_param_type,
804            )?,
805            self.inst_obj(
806                &not_superset_fact.right,
807                param_to_arg_map,
808                to_inst_param_type,
809            )?,
810            Self::line_file_after_inst(&not_superset_fact.line_file, inst_lf),
811        ))
812    }
813
814    pub fn inst_exist_fact(
815        &self,
816        exist_fact: &ExistFactEnum,
817        param_to_arg_map: &HashMap<String, Obj>,
818        to_inst_param_type: ParamObjType,
819        inst_lf: Option<&LineFile>,
820    ) -> Result<ExistFactEnum, RuntimeError> {
821        let mut groups = Vec::with_capacity(exist_fact.params_def_with_type().groups.len());
822        for param_def_with_type in exist_fact.params_def_with_type().groups.iter() {
823            groups.push(ParamGroupWithParamType::new(
824                param_def_with_type.params.clone(),
825                self.inst_param_type(
826                    &param_def_with_type.param_type,
827                    param_to_arg_map,
828                    to_inst_param_type,
829                )?,
830            ));
831        }
832        let params_def_with_type = ParamDefWithType::new(groups);
833        let mut facts = Vec::with_capacity(exist_fact.facts().len());
834        for fact in exist_fact.facts().iter() {
835            facts.push(self.inst_exist_body_fact(
836                fact,
837                param_to_arg_map,
838                to_inst_param_type,
839                inst_lf,
840            )?);
841        }
842        let body = ExistFactBody::new(
843            params_def_with_type,
844            facts,
845            Self::line_file_after_inst(&exist_fact.body().line_file, inst_lf),
846        )?;
847        Ok(match exist_fact {
848            ExistFactEnum::ExistFact(_) => ExistFactEnum::ExistFact(body),
849            ExistFactEnum::ExistUniqueFact(_) => ExistFactEnum::ExistUniqueFact(body),
850            ExistFactEnum::NotExistFact(_) => ExistFactEnum::NotExistFact(body),
851        })
852    }
853
854    pub fn inst_or_fact(
855        &self,
856        or_fact: &OrFact,
857        param_to_arg_map: &HashMap<String, Obj>,
858        to_inst_param_type: ParamObjType,
859        inst_lf: Option<&LineFile>,
860    ) -> Result<OrFact, RuntimeError> {
861        let mut facts = Vec::with_capacity(or_fact.facts.len());
862        for fact in or_fact.facts.iter() {
863            facts.push(self.inst_and_chain_atomic_fact(
864                fact,
865                param_to_arg_map,
866                to_inst_param_type,
867                inst_lf,
868            )?);
869        }
870        Ok(OrFact::new(
871            facts,
872            Self::line_file_after_inst(&or_fact.line_file, inst_lf),
873        ))
874    }
875
876    pub fn inst_and_fact(
877        &self,
878        and_fact: &AndFact,
879        param_to_arg_map: &HashMap<String, Obj>,
880        to_inst_param_type: ParamObjType,
881        inst_lf: Option<&LineFile>,
882    ) -> Result<AndFact, RuntimeError> {
883        let mut facts = Vec::with_capacity(and_fact.facts.len());
884        for fact in and_fact.facts.iter() {
885            facts.push(self.inst_atomic_fact(
886                fact,
887                param_to_arg_map,
888                to_inst_param_type,
889                inst_lf,
890            )?);
891        }
892        Ok(AndFact::new(
893            facts,
894            Self::line_file_after_inst(&and_fact.line_file, inst_lf),
895        ))
896    }
897
898    pub fn inst_chain_fact(
899        &self,
900        chain_fact: &ChainFact,
901        param_to_arg_map: &HashMap<String, Obj>,
902        to_inst_param_type: ParamObjType,
903        inst_lf: Option<&LineFile>,
904    ) -> Result<ChainFact, RuntimeError> {
905        let mut objs = Vec::with_capacity(chain_fact.objs.len());
906        for obj in chain_fact.objs.iter() {
907            objs.push(self.inst_obj(obj, param_to_arg_map, to_inst_param_type)?);
908        }
909        Ok(ChainFact::new(
910            objs,
911            chain_fact.prop_names.clone(),
912            Self::line_file_after_inst(&chain_fact.line_file, inst_lf),
913        ))
914    }
915
916    pub fn inst_forall_fact(
917        &self,
918        forall_fact: &ForallFact,
919        param_to_arg_map: &HashMap<String, Obj>,
920        to_inst_param_type: ParamObjType,
921        inst_lf: Option<&LineFile>,
922    ) -> Result<ForallFact, RuntimeError> {
923        let mut groups = Vec::with_capacity(forall_fact.params_def_with_type.groups.len());
924        for param_def_with_type in forall_fact.params_def_with_type.groups.iter() {
925            groups.push(ParamGroupWithParamType::new(
926                param_def_with_type.params.clone(),
927                self.inst_param_type(
928                    &param_def_with_type.param_type,
929                    param_to_arg_map,
930                    to_inst_param_type,
931                )?,
932            ));
933        }
934        let params_def_with_type = ParamDefWithType::new(groups);
935        let mut dom_facts = Vec::with_capacity(forall_fact.dom_facts.len());
936        for dom_fact in forall_fact.dom_facts.iter() {
937            dom_facts.push(self.inst_fact(
938                dom_fact,
939                param_to_arg_map,
940                to_inst_param_type,
941                inst_lf.cloned(),
942            )?);
943        }
944        let mut then_facts = Vec::with_capacity(forall_fact.then_facts.len());
945        for then_fact in forall_fact.then_facts.iter() {
946            then_facts.push(self.inst_exist_or_and_chain_atomic_fact(
947                then_fact,
948                param_to_arg_map,
949                to_inst_param_type,
950                inst_lf,
951            )?);
952        }
953        Ok(ForallFact::new(
954            params_def_with_type,
955            dom_facts,
956            then_facts,
957            Self::line_file_after_inst(&forall_fact.line_file, inst_lf),
958        )?)
959    }
960
961    pub fn inst_forall_fact_with_iff(
962        &self,
963        forall_fact_with_iff: &ForallFactWithIff,
964        param_to_arg_map: &HashMap<String, Obj>,
965        to_inst_param_type: ParamObjType,
966        inst_lf: Option<&LineFile>,
967    ) -> Result<ForallFactWithIff, RuntimeError> {
968        let forall_fact = self.inst_forall_fact(
969            &forall_fact_with_iff.forall_fact,
970            param_to_arg_map,
971            to_inst_param_type,
972            inst_lf,
973        )?;
974        let mut iff_facts = Vec::with_capacity(forall_fact_with_iff.iff_facts.len());
975        for iff_fact in forall_fact_with_iff.iff_facts.iter() {
976            iff_facts.push(self.inst_exist_or_and_chain_atomic_fact(
977                iff_fact,
978                param_to_arg_map,
979                to_inst_param_type,
980                inst_lf,
981            )?);
982        }
983        Ok(ForallFactWithIff::new(
984            forall_fact,
985            iff_facts,
986            Self::line_file_after_inst(&forall_fact_with_iff.line_file, inst_lf),
987        )?)
988    }
989
990    pub fn inst_restrict_fact(
991        &self,
992        restrict_fact: &RestrictFact,
993        param_to_arg_map: &HashMap<String, Obj>,
994        to_inst_param_type: ParamObjType,
995        inst_lf: Option<&LineFile>,
996    ) -> Result<RestrictFact, RuntimeError> {
997        Ok(RestrictFact::new(
998            self.inst_obj(&restrict_fact.obj, param_to_arg_map, to_inst_param_type)?,
999            self.inst_obj(
1000                &restrict_fact.obj_can_restrict_to_fn_set,
1001                param_to_arg_map,
1002                to_inst_param_type,
1003            )?,
1004            Self::line_file_after_inst(&restrict_fact.line_file, inst_lf),
1005        ))
1006    }
1007
1008    pub fn inst_not_restrict_fact(
1009        &self,
1010        not_restrict_fact: &NotRestrictFact,
1011        param_to_arg_map: &HashMap<String, Obj>,
1012        to_inst_param_type: ParamObjType,
1013        inst_lf: Option<&LineFile>,
1014    ) -> Result<NotRestrictFact, RuntimeError> {
1015        Ok(NotRestrictFact::new(
1016            self.inst_obj(&not_restrict_fact.obj, param_to_arg_map, to_inst_param_type)?,
1017            self.inst_obj(
1018                &not_restrict_fact.obj_cannot_restrict_to_fn_set,
1019                param_to_arg_map,
1020                to_inst_param_type,
1021            )?,
1022            Self::line_file_after_inst(&not_restrict_fact.line_file, inst_lf),
1023        ))
1024    }
1025}
litex/runtime/runtime_instantiate_fact.rs

litex/runtime/
runtime_instantiate_fact.rs
