litex/verify/
verify_known_atomic_facts.rs

1use crate::prelude::*;
2
3impl Runtime {
4    pub fn verify_non_equational_atomic_fact_with_known_atomic_facts(
5        &mut self,
6        atomic_fact: &AtomicFact,
7    ) -> Result<StmtResult, RuntimeError> {
8        let result = if atomic_fact.number_of_args() == 1 {
9            self.verify_atomic_fact_not_equality_with_known_atomic_fact_with_1_param(atomic_fact)?
10        } else if atomic_fact.number_of_args() == 2 {
11            self.verify_atomic_fact_not_equality_with_known_atomic_fact_with_2_params(atomic_fact)?
12        } else {
13            self.verify_atomic_fact_not_equality_with_known_atomic_fact_with_0_or_more_than_2_params(
14                atomic_fact,
15            )?
16        };
17
18        if result.is_true() {
19            return Ok(result);
20        }
21
22        Ok(result)
23    }
24
25    fn verify_atomic_fact_not_equality_with_known_atomic_fact_with_1_param(
26        &mut self,
27        atomic_fact: &AtomicFact,
28    ) -> Result<StmtResult, RuntimeError> {
29        let mut all_objs_equal_to_arg =
30            self.get_all_objs_equal_to_given(&atomic_fact.args()[0].to_string());
31
32        if let Some(calculated_obj) = self.resolve_obj_to_number(&atomic_fact.args()[0]) {
33            if calculated_obj.to_string() != atomic_fact.args()[0].to_string() {
34                let equal_tos = self.get_all_objs_equal_to_given(&calculated_obj.to_string());
35                all_objs_equal_to_arg.extend(equal_tos);
36            }
37        }
38
39        if all_objs_equal_to_arg.is_empty() {
40            all_objs_equal_to_arg.push(atomic_fact.args()[0].to_string());
41        }
42
43        for environment in self.iter_environments_from_top() {
44            let result = Self::verify_atomic_fact_not_equality_with_known_atomic_fact_with_1_param_with_facts_in_environment(environment, atomic_fact, &all_objs_equal_to_arg)?;
45            if result.is_true() {
46                return Ok(result);
47            }
48        }
49
50        let arg = atomic_fact.args()[0].clone();
51        let arg_resolved = self.resolve_obj(&arg);
52        if arg_resolved.to_string() != arg.to_string() {
53            let rewritten =
54                Self::atomic_fact_with_resolved_unary_operand(atomic_fact, arg_resolved);
55            return self
56                .verify_atomic_fact_not_equality_with_known_atomic_fact_with_1_param(&rewritten);
57        }
58
59        Ok((StmtUnknown::new()).into())
60    }
61
62    fn verify_atomic_fact_not_equality_with_known_atomic_fact_with_2_params(
63        &mut self,
64        atomic_fact: &AtomicFact,
65    ) -> Result<StmtResult, RuntimeError> {
66        let mut all_objs_equal_to_arg0 =
67            self.get_all_objs_equal_to_given(&atomic_fact.args()[0].to_string());
68        if let Some(calculated_obj) = self.resolve_obj_to_number(&atomic_fact.args()[0]) {
69            if calculated_obj.to_string() != atomic_fact.args()[0].to_string() {
70                let equal_tos = self.get_all_objs_equal_to_given(&calculated_obj.to_string());
71                all_objs_equal_to_arg0.extend(equal_tos);
72            }
73        }
74        if all_objs_equal_to_arg0.is_empty() {
75            all_objs_equal_to_arg0.push(atomic_fact.args()[0].to_string());
76        }
77        let mut all_objs_equal_to_arg1 =
78            self.get_all_objs_equal_to_given(&atomic_fact.args()[1].to_string());
79        if let Some(calculated_obj) = self.resolve_obj_to_number(&atomic_fact.args()[1]) {
80            if calculated_obj.to_string() != atomic_fact.args()[1].to_string() {
81                let equal_tos = self.get_all_objs_equal_to_given(&calculated_obj.to_string());
82                all_objs_equal_to_arg1.extend(equal_tos);
83            }
84        }
85        if all_objs_equal_to_arg1.is_empty() {
86            all_objs_equal_to_arg1.push(atomic_fact.args()[1].to_string());
87        }
88
89        for environment in self.iter_environments_from_top() {
90            let result = Self::verify_atomic_fact_not_equality_with_known_atomic_fact_with_2_params_with_facts_in_environment(environment, atomic_fact, &all_objs_equal_to_arg0, &all_objs_equal_to_arg1)?;
91            if result.is_true() {
92                return Ok(result);
93            }
94        }
95
96        let left = atomic_fact.args()[0].clone();
97        let right = atomic_fact.args()[1].clone();
98        let left_resolved = self.resolve_obj(&left);
99        let right_resolved = self.resolve_obj(&right);
100        if left_resolved.to_string() != left.to_string()
101            || right_resolved.to_string() != right.to_string()
102        {
103            let rewritten = Self::atomic_fact_with_resolved_binary_operands(
104                atomic_fact,
105                left_resolved,
106                right_resolved,
107            );
108            return self
109                .verify_atomic_fact_not_equality_with_known_atomic_fact_with_2_params(&rewritten);
110        }
111
112        Ok((StmtUnknown::new()).into())
113    }
114
115    fn verify_atomic_fact_not_equality_with_known_atomic_fact_with_0_or_more_than_2_params(
116        &mut self,
117        atomic_fact: &AtomicFact,
118    ) -> Result<StmtResult, RuntimeError> {
119        let mut all_objs_equal_to_each_arg: Vec<Vec<String>> = Vec::new();
120        for arg in atomic_fact.args().iter() {
121            let mut all_objs_equal_to_current_arg =
122                self.get_all_objs_equal_to_given(&arg.to_string());
123            if all_objs_equal_to_current_arg.is_empty() {
124                all_objs_equal_to_current_arg.push(arg.to_string());
125            }
126            all_objs_equal_to_each_arg.push(all_objs_equal_to_current_arg);
127        }
128
129        for environment in self.iter_environments_from_top() {
130            let result = Self::verify_atomic_fact_not_equality_with_known_atomic_fact_with_0_or_more_than_2_params_with_facts_in_environment(
131                environment,
132                atomic_fact,
133                &all_objs_equal_to_each_arg,
134            )?;
135            if result.is_true() {
136                return Ok(result);
137            }
138        }
139
140        let old_args = atomic_fact.args();
141        let mut new_args: Vec<Obj> = Vec::with_capacity(old_args.len());
142        let mut any_changed = false;
143        for a in old_args.iter() {
144            let r = self.resolve_obj(a);
145            if r.to_string() != a.to_string() {
146                any_changed = true;
147            }
148            new_args.push(r);
149        }
150        if any_changed {
151            let rewritten = Self::atomic_fact_with_resolved_predicate_args(atomic_fact, new_args);
152            return self
153                .verify_atomic_fact_not_equality_with_known_atomic_fact_with_0_or_more_than_2_params(
154                    &rewritten,
155                );
156        }
157
158        Ok((StmtUnknown::new()).into())
159    }
160
161    fn atomic_fact_with_resolved_unary_operand(fact: &AtomicFact, x: Obj) -> AtomicFact {
162        let line_file = fact.line_file();
163        match fact {
164            AtomicFact::IsSetFact(_) => IsSetFact::new(x, line_file).into(),
165            AtomicFact::IsNonemptySetFact(_) => IsNonemptySetFact::new(x, line_file).into(),
166            AtomicFact::IsFiniteSetFact(_) => IsFiniteSetFact::new(x, line_file).into(),
167            AtomicFact::IsCartFact(_) => IsCartFact::new(x, line_file).into(),
168            AtomicFact::IsTupleFact(_) => IsTupleFact::new(x, line_file).into(),
169            AtomicFact::NotIsSetFact(_) => NotIsSetFact::new(x, line_file).into(),
170            AtomicFact::NotIsNonemptySetFact(_) => NotIsNonemptySetFact::new(x, line_file).into(),
171            AtomicFact::NotIsFiniteSetFact(_) => NotIsFiniteSetFact::new(x, line_file).into(),
172            AtomicFact::NotIsCartFact(_) => NotIsCartFact::new(x, line_file).into(),
173            AtomicFact::NotIsTupleFact(_) => NotIsTupleFact::new(x, line_file).into(),
174            AtomicFact::NormalAtomicFact(n) => {
175                NormalAtomicFact::new(n.predicate.clone(), vec![x], line_file).into()
176            }
177            AtomicFact::NotNormalAtomicFact(n) => {
178                NotNormalAtomicFact::new(n.predicate.clone(), vec![x], line_file).into()
179            }
180            _ => unreachable!(
181                "atomic_fact_with_resolved_unary_operand: expected a one-argument atomic fact"
182            ),
183        }
184    }
185
186    fn atomic_fact_with_resolved_binary_operands(
187        fact: &AtomicFact,
188        left: Obj,
189        right: Obj,
190    ) -> AtomicFact {
191        let line_file = fact.line_file();
192        match fact {
193            AtomicFact::EqualFact(_) => EqualFact::new(left, right, line_file).into(),
194            AtomicFact::LessFact(_) => LessFact::new(left, right, line_file).into(),
195            AtomicFact::GreaterFact(_) => GreaterFact::new(left, right, line_file).into(),
196            AtomicFact::LessEqualFact(_) => LessEqualFact::new(left, right, line_file).into(),
197            AtomicFact::GreaterEqualFact(_) => GreaterEqualFact::new(left, right, line_file).into(),
198            AtomicFact::InFact(_) => InFact::new(left, right, line_file).into(),
199            AtomicFact::SubsetFact(_) => SubsetFact::new(left, right, line_file).into(),
200            AtomicFact::SupersetFact(_) => SupersetFact::new(left, right, line_file).into(),
201            AtomicFact::NotEqualFact(_) => NotEqualFact::new(left, right, line_file).into(),
202            AtomicFact::NotLessFact(_) => NotLessFact::new(left, right, line_file).into(),
203            AtomicFact::NotGreaterFact(_) => NotGreaterFact::new(left, right, line_file).into(),
204            AtomicFact::NotLessEqualFact(_) => NotLessEqualFact::new(left, right, line_file).into(),
205            AtomicFact::NotGreaterEqualFact(_) => {
206                NotGreaterEqualFact::new(left, right, line_file).into()
207            }
208            AtomicFact::NotInFact(_) => NotInFact::new(left, right, line_file).into(),
209            AtomicFact::NotSubsetFact(_) => NotSubsetFact::new(left, right, line_file).into(),
210            AtomicFact::NotSupersetFact(_) => NotSupersetFact::new(left, right, line_file).into(),
211            AtomicFact::RestrictFact(_) => RestrictFact::new(left, right, line_file).into(),
212            AtomicFact::NotRestrictFact(_) => NotRestrictFact::new(left, right, line_file).into(),
213            AtomicFact::NormalAtomicFact(x) => {
214                NormalAtomicFact::new(x.predicate.clone(), vec![left, right], line_file).into()
215            }
216            AtomicFact::NotNormalAtomicFact(x) => {
217                NotNormalAtomicFact::new(x.predicate.clone(), vec![left, right], line_file).into()
218            }
219            _ => unreachable!(
220                "atomic_fact_with_resolved_binary_operands: expected a two-argument atomic fact"
221            ),
222        }
223    }
224
225    fn atomic_fact_with_resolved_predicate_args(fact: &AtomicFact, args: Vec<Obj>) -> AtomicFact {
226        let line_file = fact.line_file();
227        match fact {
228            AtomicFact::NormalAtomicFact(x) => {
229                NormalAtomicFact::new(x.predicate.clone(), args, line_file).into()
230            }
231            AtomicFact::NotNormalAtomicFact(x) => {
232                NotNormalAtomicFact::new(x.predicate.clone(), args, line_file).into()
233            }
234            _ => unreachable!(
235                "atomic_fact_with_resolved_predicate_args: expected NormalAtomicFact or NotNormalAtomicFact"
236            ),
237        }
238    }
239
240    fn verify_atomic_fact_not_equality_with_known_atomic_fact_with_1_param_with_facts_in_environment(
241        environment: &Environment,
242        atomic_fact: &AtomicFact,
243        all_objs_equal_to_arg: &Vec<String>,
244    ) -> Result<StmtResult, RuntimeError> {
245        if let Some(known_facts_map) = environment
246            .known_atomic_facts_with_1_arg
247            .get(&(atomic_fact.key(), atomic_fact.is_true()))
248        {
249            for obj in all_objs_equal_to_arg.iter() {
250                if let Some(known_atomic_fact) = known_facts_map.get(obj) {
251                    return Ok((FactualStmtSuccess::new_with_verified_by_known_fact(
252                        atomic_fact.clone().into(),
253                        VerifiedByResult::cited_fact(
254                            atomic_fact.clone().into(),
255                            known_atomic_fact.clone().into(),
256                            None,
257                        ),
258                        Vec::new(),
259                    ))
260                    .into());
261                }
262            }
263        }
264
265        Ok((StmtUnknown::new()).into())
266    }
267
268    fn verify_atomic_fact_not_equality_with_known_atomic_fact_with_2_params_with_facts_in_environment(
269        environment: &Environment,
270        atomic_fact: &AtomicFact,
271        all_objs_equal_to_arg0: &Vec<String>,
272        all_objs_equal_to_arg1: &Vec<String>,
273    ) -> Result<StmtResult, RuntimeError> {
274        if let Some(known_facts_map) = environment
275            .known_atomic_facts_with_2_args
276            .get(&(atomic_fact.key(), atomic_fact.is_true()))
277        {
278            for obj0 in all_objs_equal_to_arg0.iter() {
279                for obj1 in all_objs_equal_to_arg1.iter() {
280                    if let Some(known_atomic_fact) =
281                        known_facts_map.get(&(obj0.clone(), obj1.clone()))
282                    {
283                        return Ok((FactualStmtSuccess::new_with_verified_by_known_fact(
284                            atomic_fact.clone().into(),
285                            VerifiedByResult::cited_fact(
286                                atomic_fact.clone().into(),
287                                known_atomic_fact.clone().into(),
288                                None,
289                            ),
290                            Vec::new(),
291                        ))
292                        .into());
293                    }
294                }
295            }
296        }
297
298        // Order facts are stored under `<` vs `>` etc.; e.g. known `a > 0` must match goal `0 < a`.
299        if let Some(alt) = atomic_fact.transposed_binary_order_equivalent() {
300            if let Some(known_facts_map) = environment
301                .known_atomic_facts_with_2_args
302                .get(&(alt.key(), alt.is_true()))
303            {
304                for obj0 in all_objs_equal_to_arg1.iter() {
305                    for obj1 in all_objs_equal_to_arg0.iter() {
306                        if let Some(known_atomic_fact) =
307                            known_facts_map.get(&(obj0.clone(), obj1.clone()))
308                        {
309                            return Ok((FactualStmtSuccess::new_with_verified_by_known_fact(
310                                atomic_fact.clone().into(),
311                                VerifiedByResult::cited_fact(
312                                    atomic_fact.clone().into(),
313                                    known_atomic_fact.clone().into(),
314                                    None,
315                                ),
316                                Vec::new(),
317                            ))
318                            .into());
319                        }
320                    }
321                }
322            }
323        }
324
325        Ok((StmtUnknown::new()).into())
326    }
327
328    fn verify_atomic_fact_not_equality_with_known_atomic_fact_with_0_or_more_than_2_params_with_facts_in_environment(
329        environment: &Environment,
330        atomic_fact: &AtomicFact,
331        all_objs_equal_to_each_arg: &Vec<Vec<String>>,
332    ) -> Result<StmtResult, RuntimeError> {
333        if let Some(known_facts) = environment
334            .known_atomic_facts_with_0_or_more_than_2_args
335            .get(&(atomic_fact.key(), atomic_fact.is_true()))
336        {
337            for known_fact in known_facts.iter() {
338                if known_fact.args().len() != atomic_fact.args().len() {
339                    let message = format!(
340                        "known atomic fact {} has different number of args than the given fact {}",
341                        known_fact.to_string(),
342                        atomic_fact.to_string()
343                    );
344                    return Err({
345                        VerifyRuntimeError(RuntimeErrorStruct::new(
346                            Some(Fact::from(atomic_fact.clone()).into_stmt()),
347                            message.clone(),
348                            atomic_fact.line_file(),
349                            Some(
350                                UnknownRuntimeError(RuntimeErrorStruct::new(
351                                    Some(Fact::from(atomic_fact.clone()).into_stmt()),
352                                    message,
353                                    atomic_fact.line_file(),
354                                    None,
355                                    vec![],
356                                ))
357                                .into(),
358                            ),
359                            vec![],
360                        ))
361                        .into()
362                    });
363                }
364                let mut all_args_match = true;
365                for (index, known_arg) in known_fact.args().iter().enumerate() {
366                    let known_arg_string = known_arg.to_string();
367                    if !all_objs_equal_to_each_arg[index].contains(&known_arg_string) {
368                        all_args_match = false;
369                        break;
370                    }
371                }
372                if all_args_match {
373                    return Ok((FactualStmtSuccess::new_with_verified_by_known_fact(
374                        atomic_fact.clone().into(),
375                        VerifiedByResult::cited_fact(
376                            atomic_fact.clone().into(),
377                            known_fact.clone().into(),
378                            None,
379                        ),
380                        Vec::new(),
381                    ))
382                    .into());
383                }
384            }
385        }
386
387        Ok((StmtUnknown::new()).into())
388    }
389}
litex/verify/verify_known_atomic_facts.rs

litex/verify/
verify_known_atomic_facts.rs
