litex/execute/by_stmt/
enumerate_by_stmt.rs

1use crate::prelude::*;
2
3impl Runtime {
4    pub fn exec_by_enumerate_finite_set_stmt(
5        &mut self,
6        stmt: &ByEnumerateFiniteSetStmt,
7    ) -> Result<StmtResult, RuntimeError> {
8        let (params, param_sets) = stmt
9            .expanded_list_set_params()
10            .map_err(|msg| short_exec_error(stmt.clone().into(), msg, None, vec![]))?;
11
12        let corresponding_forall_fact = stmt
13            .to_corresponding_forall_fact()
14            .map_err(|msg| short_exec_error(stmt.clone().into(), msg, None, vec![]))?;
15
16        self.verify_forall_fact_params_and_dom_well_defined(
17            &stmt.forall_fact,
18            &VerifyState::new(0, false),
19        )
20        .map_err(|well_defined_error| {
21            short_exec_error(
22                stmt.clone().into(),
23                format!(
24                    "by enumerate finite_set: forall parameters or domain is not well-defined (`{}`)",
25                    stmt.forall_fact
26                ),
27                Some(well_defined_error),
28                vec![],
29            )
30        })?;
31
32        let enumerate_cartesian_product_is_empty =
33            param_sets.iter().any(|list_set| list_set.list.is_empty());
34        if enumerate_cartesian_product_is_empty {
35            let infer_result_from_stored_forall_fact = self
36                .verify_well_defined_and_store_and_infer_with_default_verify_state(
37                    corresponding_forall_fact.clone(),
38                )
39                .map_err(|store_fact_error| {
40                    short_exec_error(
41                        stmt.clone().into(),
42                        format!(
43                            "by enumerate finite_set: failed to store corresponding forall `{}`",
44                            corresponding_forall_fact
45                        ),
46                        Some(store_fact_error),
47                        vec![],
48                    )
49                })?;
50            let infer_result = Self::infer_result_with_generated_forall_and_store_infer(
51                &corresponding_forall_fact,
52                infer_result_from_stored_forall_fact,
53            );
54            return Ok(
55                (NonFactualStmtSuccess::new(stmt.clone().into(), infer_result, vec![])).into(),
56            );
57        }
58
59        let mut current_parameter_index_assignment =
60            Self::by_enumerate_start_index_assignment(&param_sets);
61        loop {
62            self.exec_by_enumerate_stmt_for_one_assignment(
63                stmt,
64                &params,
65                &param_sets,
66                &current_parameter_index_assignment,
67            )?;
68            let next_parameter_index_assignment = Self::by_enumerate_next_index_assignment(
69                &param_sets,
70                &current_parameter_index_assignment,
71            );
72            match next_parameter_index_assignment {
73                Some(next_parameter_index_assignment) => {
74                    current_parameter_index_assignment = next_parameter_index_assignment;
75                }
76                None => break,
77            }
78        }
79
80        let infer_result_from_stored_forall_fact = self
81            .verify_well_defined_and_store_and_infer_with_default_verify_state(
82                corresponding_forall_fact.clone(),
83            )
84            .map_err(|store_fact_error| {
85                short_exec_error(
86                    stmt.clone().into(),
87                    format!(
88                        "by enumerate finite_set: failed to store corresponding forall `{}`",
89                        corresponding_forall_fact
90                    ),
91                    Some(store_fact_error),
92                    vec![],
93                )
94            })?;
95
96        let infer_result = Self::infer_result_with_generated_forall_and_store_infer(
97            &corresponding_forall_fact,
98            infer_result_from_stored_forall_fact,
99        );
100
101        Ok((NonFactualStmtSuccess::new(stmt.clone().into(), infer_result, vec![])).into())
102    }
103
104    fn infer_result_with_generated_forall_and_store_infer(
105        generated_forall_fact: &Fact,
106        infer_after_store: InferResult,
107    ) -> InferResult {
108        let mut infer_result = InferResult::new();
109        infer_result.new_fact(generated_forall_fact);
110        infer_result.new_infer_result_inside(infer_after_store);
111        infer_result
112    }
113
114    fn by_enumerate_start_index_assignment(param_sets: &[ListSet]) -> Vec<usize> {
115        let mut start_index_assignment: Vec<usize> = Vec::new();
116        for _ in param_sets.iter() {
117            start_index_assignment.push(0);
118        }
119        start_index_assignment
120    }
121
122    fn by_enumerate_next_index_assignment(
123        param_sets: &[ListSet],
124        current_parameter_index_assignment: &Vec<usize>,
125    ) -> Option<Vec<usize>> {
126        let mut next_parameter_index_assignment = current_parameter_index_assignment.clone();
127        for reversed_position in 0..next_parameter_index_assignment.len() {
128            let position_from_right = next_parameter_index_assignment.len() - 1 - reversed_position;
129            let current_index = next_parameter_index_assignment[position_from_right];
130            let current_list_set_length = param_sets[position_from_right].list.len();
131            if current_index + 1 < current_list_set_length {
132                next_parameter_index_assignment[position_from_right] = current_index + 1;
133                return Some(next_parameter_index_assignment);
134            }
135            next_parameter_index_assignment[position_from_right] = 0;
136        }
137        None
138    }
139
140    fn exec_by_enumerate_stmt_for_one_assignment(
141        &mut self,
142        stmt: &ByEnumerateFiniteSetStmt,
143        params: &[String],
144        param_sets: &[ListSet],
145        parameter_index_assignment: &Vec<usize>,
146    ) -> Result<(), RuntimeError> {
147        self.run_in_local_env(|rt| {
148            rt.exec_by_enumerate_stmt_for_one_assignment_body(
149                stmt,
150                params,
151                param_sets,
152                parameter_index_assignment,
153            )
154        })
155    }
156
157    fn exec_by_enumerate_stmt_for_one_assignment_body(
158        &mut self,
159        stmt: &ByEnumerateFiniteSetStmt,
160        params: &[String],
161        param_sets: &[ListSet],
162        parameter_index_assignment: &Vec<usize>,
163    ) -> Result<(), RuntimeError> {
164        for (parameter_position, parameter_name) in params.iter().enumerate() {
165            let assigned_obj = (*param_sets[parameter_position].list
166                [parameter_index_assignment[parameter_position]])
167                .clone();
168            self.store_free_param_or_identifier_name(parameter_name, ParamObjType::Forall)?;
169            let parameter_equal_to_assigned_obj_atomic_fact = EqualFact::new(
170                obj_for_bound_param_in_scope(parameter_name.to_string(), ParamObjType::Forall),
171                assigned_obj,
172                stmt.line_file.clone(),
173            )
174            .into();
175            self.store_atomic_fact_without_well_defined_verified_and_infer(
176                parameter_equal_to_assigned_obj_atomic_fact,
177            )?;
178        }
179
180        let verify_state = VerifyState::new(0, false);
181        for dom_fact in stmt.forall_fact.dom_facts.iter() {
182            let verify_dom_result = self.verify_fact(dom_fact, &verify_state)?;
183            if verify_dom_result.is_true() {
184                self.verify_well_defined_and_store_and_infer_with_default_verify_state(
185                    dom_fact.clone(),
186                )?;
187            } else if verify_dom_result.is_unknown() {
188                if let Some(negated_domain) = Self::negated_domain_fact_for_by_for_skip(dom_fact) {
189                    let verify_negation_result =
190                        self.verify_fact(&negated_domain, &verify_state)?;
191                    if verify_negation_result.is_true() {
192                        return Ok(());
193                    }
194                }
195                return Err(short_exec_error(
196                    stmt.clone().into(),
197                    format!(
198                        "by enumerate finite_set: domain fact `{}` is not decided (could not verify it or its negation)",
199                        dom_fact
200                    ),
201                    None,
202                    vec![],
203                ));
204            }
205        }
206
207        for proof_stmt in stmt.proof.iter() {
208            self.exec_stmt(proof_stmt)?;
209        }
210        for fact_to_prove in stmt.forall_fact.then_facts.iter() {
211            let verified_result =
212                self.verify_exist_or_and_chain_atomic_fact(fact_to_prove, &verify_state)?;
213            if verified_result.is_unknown() {
214                return Err(short_exec_error(
215                    stmt.clone().into(),
216                    format!(
217                        "by enumerate finite_set: failed to prove `{}`",
218                        fact_to_prove
219                    ),
220                    None,
221                    vec![],
222                ));
223            }
224        }
225        Ok(())
226    }
227}
litex/execute/by_stmt/enumerate_by_stmt.rs

litex/execute/by_stmt/
enumerate_by_stmt.rs
