litex/fact/
forall_fact_with_iff.rs

1use crate::prelude::*;
2use std::fmt;
3
4#[derive(Clone)]
5pub struct ForallFactWithIff {
6    pub forall_fact: ForallFact,
7    pub iff_facts: Vec<ExistOrAndChainAtomicFact>,
8    pub line_file: LineFile,
9}
10
11impl ForallFactWithIff {
12    pub fn new(
13        forall_fact: ForallFact,
14        iff_facts: Vec<ExistOrAndChainAtomicFact>,
15        line_file: LineFile,
16    ) -> Result<Self, RuntimeError> {
17        let forall_fact_with_iff = ForallFactWithIff {
18            forall_fact,
19            iff_facts,
20            line_file,
21        };
22        check_forall_fact_with_iff_has_no_duplicate_forall_free_parameter(&forall_fact_with_iff)?;
23        Ok(forall_fact_with_iff)
24    }
25}
26
27impl fmt::Display for ForallFactWithIff {
28    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
29        write!(
30            f,
31            "{}\n{}{}\n{}",
32            self.forall_fact,
33            to_string_and_add_four_spaces_at_beginning_of_each_line(&EQUIVALENT_SIGN, 1),
34            COLON,
35            vec_to_string_add_four_spaces_at_beginning_of_each_line(&self.iff_facts, 2)
36        )
37    }
38}
39
40impl ForallFactWithIff {
41    // 将 `forall ... iff` 拆成两个等价验证用的 `forall`：
42    // 1. `dom ∪ then ⊢ iff`（then 并入 dom）
43    // 2. `dom ∪ iff ⊢ then`（iff 并入 dom）
44    pub fn to_two_forall_facts(&self) -> Result<(ForallFact, ForallFact), RuntimeError> {
45        let f = &self.forall_fact;
46        let mut dom_then = f.dom_facts.clone();
47        dom_then.extend(
48            f.then_facts
49                .iter()
50                .cloned()
51                .map(ExistOrAndChainAtomicFact::to_fact),
52        );
53        let forall_then_implies_iff = ForallFact::new(
54            f.params_def_with_type.clone(),
55            dom_then,
56            self.iff_facts.clone(),
57            self.line_file.clone(),
58        )?;
59
60        let mut dom_iff = f.dom_facts.clone();
61        dom_iff.extend(
62            self.iff_facts
63                .iter()
64                .cloned()
65                .map(ExistOrAndChainAtomicFact::to_fact),
66        );
67        let forall_iff_implies_then = ForallFact::new(
68            f.params_def_with_type.clone(),
69            dom_iff,
70            f.then_facts.clone(),
71            self.line_file.clone(),
72        )?;
73
74        Ok((forall_then_implies_iff, forall_iff_implies_then))
75    }
76}
litex/fact/forall_fact_with_iff.rs

litex/fact/
forall_fact_with_iff.rs
