litex/verify/
verify_helper.rs

1use crate::prelude::*;
2
3impl Runtime {
4    /// If the fact string is in the known-facts cache, return the cached verification result.
5    pub fn verify_fact_from_cache_using_display_string(&self, fact: &Fact) -> Option<StmtResult> {
6        let key = fact.to_string();
7        let (cache_ok, cite_fact_source) = self.cache_known_facts_contains(&key);
8        if cache_ok {
9            Some(
10                (FactualStmtSuccess::new_with_verified_by_known_fact(
11                    fact.clone(),
12                    VerifiedByResult::cached_fact(fact.clone(), cite_fact_source),
13                    Vec::new(),
14                ))
15                .into(),
16            )
17        } else {
18            None
19        }
20    }
21
22    /// If check_type_nonempty is true and param_type is Obj(set), verifies that the set is nonempty and stores the fact.
23    pub fn verify_param_type_nonempty_if_required(
24        &mut self,
25        param_type: &ParamType,
26        check_type_nonempty: bool,
27    ) -> Result<(), RuntimeError> {
28        if !check_type_nonempty {
29            return Ok(());
30        }
31        match param_type {
32            ParamType::Set(_) | ParamType::NonemptySet(_) | ParamType::FiniteSet(_) => Ok(()),
33            ParamType::Obj(param_set) => match param_set {
34                Obj::FnSet(fn_set) => {
35                    let ret_nonempty = IsNonemptySetFact::new(
36                        fn_set.body.ret_set.as_ref().clone(),
37                        default_line_file(),
38                    )
39                    .into();
40                    self.verify_fact_well_defined_and_store_and_infer(
41                        ret_nonempty,
42                        &VerifyState::new(2, false),
43                    )?;
44                    Ok(())
45                }
46                Obj::AnonymousFn(anon) => {
47                    let ret_nonempty = IsNonemptySetFact::new(
48                        anon.body.ret_set.as_ref().clone(),
49                        default_line_file(),
50                    )
51                    .into();
52                    self.verify_fact_well_defined_and_store_and_infer(
53                        ret_nonempty,
54                        &VerifyState::new(2, false),
55                    )?;
56                    Ok(())
57                }
58                _ => {
59                    let nonempty_fact =
60                        IsNonemptySetFact::new(param_set.clone(), default_line_file());
61                    let ret =
62                        self.verify_fact(&nonempty_fact.into(), &VerifyState::new(0, false))?;
63                    if ret.is_unknown() {
64                        return Err(RuntimeError::from(VerifyRuntimeError(
65                            RuntimeErrorStruct::new_with_just_msg(
66                                "param type is not nonempty".to_string(),
67                            ),
68                        )));
69                    }
70                    Ok(())
71                }
72            },
73        }
74    }
75}
litex/verify/verify_helper.rs

litex/verify/
verify_helper.rs
