litex/verify/verify_builtin_rules/
set_relation_duality.rs

1use crate::prelude::*;
2
3impl Runtime {
4    /// Verify subset by duality: `a subset b` iff `b superset a`.
5    pub fn verify_subset_fact_with_builtin_rules(
6        &mut self,
7        subset_fact: &SubsetFact,
8        _verify_state: &VerifyState,
9    ) -> Result<StmtResult, RuntimeError> {
10        if subset_fact.left.to_string() == subset_fact.right.to_string() {
11            return Ok(
12                (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
13                    subset_fact.clone().into(),
14                    "subset_superset_duality".to_string(),
15                    Vec::new(),
16                ))
17                .into(),
18            );
19        }
20
21        let converted_superset_fact = SupersetFact::new(
22            subset_fact.right.clone(),
23            subset_fact.left.clone(),
24            subset_fact.line_file.clone(),
25        )
26        .into();
27        let verify_result = self
28            .verify_non_equational_atomic_fact_with_known_atomic_facts(&converted_superset_fact)?;
29        if verify_result.is_true() {
30            Ok(
31                (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
32                    subset_fact.clone().into(),
33                    "subset_superset_duality".to_string(),
34                    Vec::new(),
35                ))
36                .into(),
37            )
38        } else {
39            Ok((StmtUnknown::new()).into())
40        }
41    }
42
43    /// Verify superset by duality: `a superset b` iff `b subset a`.
44    pub fn verify_superset_fact_with_builtin_rules(
45        &mut self,
46        superset_fact: &SupersetFact,
47        _verify_state: &VerifyState,
48    ) -> Result<StmtResult, RuntimeError> {
49        if superset_fact.left.to_string() == superset_fact.right.to_string() {
50            return Ok(
51                (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
52                    superset_fact.clone().into(),
53                    "subset_superset_duality".to_string(),
54                    Vec::new(),
55                ))
56                .into(),
57            );
58        }
59        let converted_subset_fact = SubsetFact::new(
60            superset_fact.right.clone(),
61            superset_fact.left.clone(),
62            superset_fact.line_file.clone(),
63        )
64        .into();
65        let verify_result =
66            self.verify_non_equational_atomic_fact_with_known_atomic_facts(&converted_subset_fact)?;
67        if verify_result.is_true() {
68            Ok(
69                (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
70                    superset_fact.clone().into(),
71                    "subset_superset_duality".to_string(),
72                    Vec::new(),
73                ))
74                .into(),
75            )
76        } else {
77            Ok((StmtUnknown::new()).into())
78        }
79    }
80
81    /// Verify `not subset` by converting to the dual `not superset`.
82    pub fn verify_not_subset_fact_with_builtin_rules(
83        &mut self,
84        not_subset_fact: &NotSubsetFact,
85        _verify_state: &VerifyState,
86    ) -> Result<StmtResult, RuntimeError> {
87        let converted_not_superset_fact = NotSupersetFact::new(
88            not_subset_fact.right.clone(),
89            not_subset_fact.left.clone(),
90            not_subset_fact.line_file.clone(),
91        )
92        .into();
93        let verify_result = self.verify_non_equational_atomic_fact_with_known_atomic_facts(
94            &converted_not_superset_fact,
95        )?;
96        if verify_result.is_true() {
97            Ok(
98                (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
99                    not_subset_fact.clone().into(),
100                    "subset_superset_duality".to_string(),
101                    Vec::new(),
102                ))
103                .into(),
104            )
105        } else {
106            Ok((StmtUnknown::new()).into())
107        }
108    }
109
110    /// Verify `not superset` by converting to the dual `not subset`.
111    pub fn verify_not_superset_fact_with_builtin_rules(
112        &mut self,
113        not_superset_fact: &NotSupersetFact,
114        _verify_state: &VerifyState,
115    ) -> Result<StmtResult, RuntimeError> {
116        let converted_not_subset_fact = NotSubsetFact::new(
117            not_superset_fact.right.clone(),
118            not_superset_fact.left.clone(),
119            not_superset_fact.line_file.clone(),
120        )
121        .into();
122        let verify_result = self.verify_non_equational_atomic_fact_with_known_atomic_facts(
123            &converted_not_subset_fact,
124        )?;
125        if verify_result.is_true() {
126            Ok(
127                (FactualStmtSuccess::new_with_verified_by_builtin_rules_recording_stmt(
128                    not_superset_fact.clone().into(),
129                    "subset_superset_duality".to_string(),
130                    Vec::new(),
131                ))
132                .into(),
133            )
134        } else {
135            Ok((StmtUnknown::new()).into())
136        }
137    }
138}
litex/verify/verify_builtin_rules/set_relation_duality.rs

litex/verify/verify_builtin_rules/
set_relation_duality.rs
