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, cache_line_file) = self.cache_known_facts_contains(&key);
8        if cache_ok {
9            Some(
10                (FactualStmtSuccess::new_with_verified_by_known_fact_source_recording_facts(
11                    fact.clone(),
12                    key,
13                    None,
14                    Some(cache_line_file),
15                    Vec::new(),
16                ))
17                .into(),
18            )
19        } else {
20            None
21        }
22    }
23
24    /// If check_type_nonempty is true and param_type is Obj(set), verifies that the set is nonempty and stores the fact.
25    pub fn verify_param_type_nonempty_if_required(
26        &mut self,
27        param_type: &ParamType,
28        check_type_nonempty: bool,
29    ) -> Result<(), RuntimeError> {
30        if !check_type_nonempty {
31            return Ok(());
32        }
33        match param_type {
34            ParamType::Set(_) | ParamType::NonemptySet(_) | ParamType::FiniteSet(_) => Ok(()),
35            ParamType::Restrictive(fn_set) => {
36                let ret_nonempty = IsNonemptySetFact::new(
37                    fn_set.body.ret_set.as_ref().clone(),
38                    default_line_file(),
39                )
40                .into();
41                self.verify_fact_well_defined_and_store_and_infer(
42                    ret_nonempty,
43                    &VerifyState::new(2, false),
44                )?;
45                Ok(())
46            }
47            ParamType::Obj(param_set) => match param_set {
48                Obj::FnSet(fn_set) => {
49                    let ret_nonempty = IsNonemptySetFact::new(
50                        fn_set.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::AnonymousFn(anon) => {
61                    let ret_nonempty = IsNonemptySetFact::new(
62                        anon.body.ret_set.as_ref().clone(),
63                        default_line_file(),
64                    )
65                    .into();
66                    self.verify_fact_well_defined_and_store_and_infer(
67                        ret_nonempty,
68                        &VerifyState::new(2, false),
69                    )?;
70                    Ok(())
71                }
72                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"
73                        .to_string()))),
74                _ => {
75                    let nonempty_fact =
76                        IsNonemptySetFact::new(param_set.clone(), default_line_file());
77                    let ret=  self.verify_fact(
78                        &nonempty_fact.into(),
79                        &VerifyState::new(0, false),
80                    )?;
81                    if ret.is_unknown() {
82                        return Err(RuntimeError::from(VerifyRuntimeError(RuntimeErrorStruct::new_with_just_msg("param type is not nonempty".to_string()))));
83                    }
84                    Ok(())
85                }
86            },
87        }
88    }
89}
litex/verify/verify_helper.rs

litex/verify/
verify_helper.rs
