litex/verify/verify_builtin_rules/
non_equational_dispatch.rs

1use crate::prelude::*;
2
3impl Runtime {
4    pub fn verify_non_equational_atomic_fact_with_builtin_rules(
5        &mut self,
6        atomic_fact: &AtomicFact,
7        verify_state: &VerifyState,
8    ) -> Result<StmtResult, RuntimeError> {
9        match atomic_fact {
10            AtomicFact::EqualFact(_) => unreachable!(),
11            AtomicFact::NotEqualFact(not_equal_fact) => {
12                self._verify_not_equal_fact_with_builtin_rules(not_equal_fact, verify_state)
13            }
14            AtomicFact::InFact(in_fact) => {
15                self.verify_in_fact_with_builtin_rules(in_fact, verify_state)
16            }
17            AtomicFact::NotInFact(not_in_fact) => {
18                self.verify_not_in_fact_with_builtin_rules(not_in_fact, verify_state)
19            }
20            AtomicFact::SubsetFact(subset_fact) => {
21                self.verify_subset_fact_with_builtin_rules(subset_fact, verify_state)
22            }
23            AtomicFact::SupersetFact(superset_fact) => {
24                self.verify_superset_fact_with_builtin_rules(superset_fact, verify_state)
25            }
26            AtomicFact::NotSubsetFact(not_subset_fact) => {
27                self.verify_not_subset_fact_with_builtin_rules(not_subset_fact, verify_state)
28            }
29            AtomicFact::NotSupersetFact(not_superset_fact) => {
30                self.verify_not_superset_fact_with_builtin_rules(not_superset_fact, verify_state)
31            }
32            AtomicFact::NotLessFact(_)
33            | AtomicFact::NotGreaterFact(_)
34            | AtomicFact::NotLessEqualFact(_)
35            | AtomicFact::NotGreaterEqualFact(_)
36            | AtomicFact::LessFact(_)
37            | AtomicFact::GreaterFact(_)
38            | AtomicFact::LessEqualFact(_)
39            | AtomicFact::GreaterEqualFact(_) => {
40                self.verify_order_atomic_fact_numeric_builtin_only(atomic_fact)
41            }
42            AtomicFact::IsSetFact(is_set_fact) => Ok(
43                (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
44                    is_set_fact.clone().into(),
45                    "Every object is a set.".to_string(),
46                    Vec::new(),
47                ))
48                .into(),
49            ),
50            AtomicFact::IsNonemptySetFact(is_nonempty_set_fact) => self
51                ._verify_is_nonempty_set_fact_with_builtin_rules(
52                    is_nonempty_set_fact,
53                    verify_state,
54                ),
55            AtomicFact::IsFiniteSetFact(is_finite_set_fact) => {
56                self._verify_is_finite_set_fact_with_builtin_rules(is_finite_set_fact, verify_state)
57            }
58            AtomicFact::IsCartFact(is_cart_fact) => {
59                self._verify_is_cart_fact_with_builtin_rules(is_cart_fact, verify_state)
60            }
61            AtomicFact::IsTupleFact(is_tuple_fact) => {
62                self._verify_is_tuple_fact_with_builtin_rules(is_tuple_fact, verify_state)
63            }
64            AtomicFact::NotIsNonemptySetFact(not_is_nonempty_set_fact) => self
65                ._verify_not_is_nonempty_set_fact_with_builtin_rules(
66                    not_is_nonempty_set_fact,
67                    verify_state,
68                ),
69            AtomicFact::FnEqualInFact(fe) => {
70                self.verify_fn_equal_in_fact_with_builtin_rules(fe, verify_state)
71            }
72            AtomicFact::FnEqualFact(fe) => {
73                self.verify_fn_equal_fact_with_builtin_rules(fe, verify_state)
74            }
75            _ => Ok((StmtUnknown::new()).into()),
76        }
77    }
78
79    pub fn non_equational_atomic_fact_holds_by_full_verify_pipeline(
80        &mut self,
81        atomic_fact: &AtomicFact,
82        verify_state: &VerifyState,
83    ) -> Result<bool, RuntimeError> {
84        let verify_result =
85            self.verify_non_equational_atomic_fact(atomic_fact, verify_state, true)?;
86        Ok(verify_result.is_true())
87    }
88}
litex/verify/verify_builtin_rules/non_equational_dispatch.rs

litex/verify/verify_builtin_rules/
non_equational_dispatch.rs
