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(_)
33            | ParamType::NonemptySet(_)
34            | ParamType::FiniteSet(_) => Ok(()),
35            ParamType::Obj(param_set) => match param_set {
36                Obj::FnSet(fn_set) => {
37                    let ret_nonempty = IsNonemptySetFact::new(
38                        fn_set.body.ret_set.as_ref().clone(),
39                        default_line_file(),
40                    )
41                    .into();
42                    self.verify_fact_well_defined_and_store_and_infer(
43                        ret_nonempty,
44                        &VerifyState::new(2, false),
45                    )?;
46                    Ok(())
47                }
48                Obj::AnonymousFn(anon) => {
49                    let ret_nonempty = IsNonemptySetFact::new(
50                        anon.body.ret_set.as_ref().clone(),
51                        default_line_file(),
52                    )
53                    .into();
54                    self.verify_fact_well_defined_and_store_and_infer(
55                        ret_nonempty,
56                        &VerifyState::new(2, false),
57                    )?;
58                    Ok(())
59                }
60                Obj::SetBuilder(_) => Err(RuntimeError::ExecStmtError(RuntimeErrorStruct::new_with_just_msg("set builder param type is not supported yet in verify_param_type_nonempty_if_required"
61                        .to_string()))),
62                _ => {
63                    let nonempty_fact =
64                        IsNonemptySetFact::new(param_set.clone(), default_line_file());
65                    let ret=  self.verify_fact(
66                        &nonempty_fact.into(),
67                        &VerifyState::new(0, false),
68                    )?;
69                    if ret.is_unknown() {
70                        return Err(RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new_with_just_msg("param type is not nonempty".to_string()))));
71                    }
72                    Ok(())
73                }
74            },
75        }
76    }
77}
litex/verify/verify_helper.rs

litex/verify/
verify_helper.rs
