litex/infer/
infer_set_relations.rs

1use crate::prelude::*;
2
3impl Runtime {
4    // Subset: `A $subset B` => `forall` fresh `x`: `x $in A` => `x $in B`.
5    // Example: knowing `S $subset T`, any member of `S` is a member of `T`.
6    pub fn infer_subset_fact(
7        &mut self,
8        subset_fact: &SubsetFact,
9    ) -> Result<InferResult, RuntimeError> {
10        let generated_param_name = self.generate_random_unused_name();
11        let parameter_definition = ParamGroupWithParamType::new(
12            vec![generated_param_name.clone()],
13            ParamType::Obj(subset_fact.left.clone()),
14        );
15        let in_fact_for_forall_then = InFact::new(
16            obj_for_bound_param_in_scope(generated_param_name.clone(), ParamObjType::Forall),
17            subset_fact.right.clone(),
18            subset_fact.line_file.clone(),
19        )
20        .into();
21        let inferred_forall_fact = ForallFact::new(
22            ParamDefWithType::new(vec![parameter_definition]),
23            vec![],
24            vec![in_fact_for_forall_then],
25            subset_fact.line_file.clone(),
26        )?
27        .into();
28
29        let mut infer_result = InferResult::new();
30        infer_result.new_fact(&inferred_forall_fact);
31        self.verify_well_defined_and_store_and_infer_with_default_verify_state(
32            inferred_forall_fact,
33        )
34        .map_err(|previous_error| {
35            RuntimeError::from(InferRuntimeError(RuntimeErrorStruct::new(
36                None,
37                format!(
38                    "failed to store inferred forall fact while inferring `{}`",
39                    subset_fact
40                ),
41                subset_fact.line_file.clone(),
42                Some(previous_error),
43                vec![],
44            )))
45        })?;
46        Ok(infer_result)
47    }
48
49    // Superset: `A $superset B` => `forall` fresh `x`: `x $in B` => `x $in A`.
50    // Example: knowing `T $superset S`, every `x $in S` satisfies `x $in T`.
51    pub fn infer_superset_fact(
52        &mut self,
53        superset_fact: &SupersetFact,
54    ) -> Result<InferResult, RuntimeError> {
55        let generated_param_name = self.generate_random_unused_name();
56        let parameter_definition = ParamGroupWithParamType::new(
57            vec![generated_param_name.clone()],
58            ParamType::Obj(superset_fact.right.clone()),
59        );
60        let in_fact_for_forall_then = InFact::new(
61            obj_for_bound_param_in_scope(generated_param_name.clone(), ParamObjType::Forall),
62            superset_fact.left.clone(),
63            superset_fact.line_file.clone(),
64        )
65        .into();
66        let inferred_forall_fact = ForallFact::new(
67            ParamDefWithType::new(vec![parameter_definition]),
68            vec![],
69            vec![in_fact_for_forall_then],
70            superset_fact.line_file.clone(),
71        )?
72        .into();
73
74        let mut infer_result = InferResult::new();
75        infer_result.new_fact(&inferred_forall_fact);
76        self.verify_well_defined_and_store_and_infer_with_default_verify_state(
77            inferred_forall_fact,
78        )
79        .map_err(|previous_error| {
80            RuntimeError::from(InferRuntimeError(RuntimeErrorStruct::new(
81                None,
82                format!(
83                    "failed to store inferred forall fact while inferring `{}`",
84                    superset_fact
85                ),
86                superset_fact.line_file.clone(),
87                Some(previous_error),
88                vec![],
89            )))
90        })?;
91        Ok(infer_result)
92    }
93}
litex/infer/infer_set_relations.rs

litex/infer/
infer_set_relations.rs
