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    ) -> Self {
17        ForallFactWithIff {
18            forall_fact,
19            iff_facts,
20            line_file,
21        }
22    }
23}
24
25impl fmt::Display for ForallFactWithIff {
26    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
27        write!(
28            f,
29            "{}\n{}{}\n{}",
30            self.forall_fact,
31            to_string_and_add_four_spaces_at_beginning_of_each_line(&EQUIVALENT_SIGN, 1),
32            COLON,
33            vec_to_string_add_four_spaces_at_beginning_of_each_line(&self.iff_facts, 2)
34        )
35    }
36}
37
38impl ForallFactWithIff {
39    // 将 `forall ... iff` 拆成两个等价验证用的 `forall`：
40    // 1. `dom ∪ then ⊢ iff`（then 并入 dom）
41    // 2. `dom ∪ iff ⊢ then`（iff 并入 dom）
42    pub fn to_two_forall_facts(&self) -> (ForallFact, ForallFact) {
43        let f = &self.forall_fact;
44        let mut dom_then = f.dom_facts.clone();
45        dom_then.extend(f.then_facts.clone());
46        let forall_then_implies_iff = ForallFact::new(
47            f.params_def_with_type.clone(),
48            dom_then,
49            self.iff_facts.clone(),
50            self.line_file.clone(),
51        );
52
53        let mut dom_iff = f.dom_facts.clone();
54        dom_iff.extend(self.iff_facts.clone());
55        let forall_iff_implies_then = ForallFact::new(
56            f.params_def_with_type.clone(),
57            dom_iff,
58            f.then_facts.clone(),
59            self.line_file.clone(),
60        );
61
62        (forall_then_implies_iff, forall_iff_implies_then)
63    }
64}
litex/fact/forall_fact_with_iff.rs

litex/fact/
forall_fact_with_iff.rs
