litex/fact/
fact.rs

1use crate::prelude::*;
2use std::fmt;
3#[derive(Clone)]
4pub enum Fact {
5    AtomicFact(AtomicFact),
6    ExistFact(ExistFactEnum),
7    OrFact(OrFact),
8    AndFact(AndFact),
9    ChainFact(ChainFact),
10    ForallFact(ForallFact),
11    ForallFactWithIff(ForallFactWithIff),
12    NotForall(NotForallFact),
13}
14
15impl fmt::Debug for Fact {
16    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
17        write!(f, "{}", self)
18    }
19}
20
21impl Fact {
22    pub fn fact_type_string(&self) -> String {
23        match self {
24            Fact::AtomicFact(_) => "AtomicFact".to_string(),
25            Fact::ExistFact(_) => "ExistFact".to_string(),
26            Fact::OrFact(_) => "OrFact".to_string(),
27            Fact::AndFact(_) => "AndFact".to_string(),
28            Fact::ChainFact(_) => "ChainFact".to_string(),
29            Fact::ForallFact(_) => "ForallFact".to_string(),
30            Fact::ForallFactWithIff(_) => "ForallFactWithIff".to_string(),
31            Fact::NotForall(_) => "NotForallFact".to_string(),
32        }
33    }
34}
35
36impl fmt::Display for Fact {
37    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
38        match self {
39            Fact::AtomicFact(atomic_fact) => write!(f, "{}", atomic_fact),
40            Fact::ExistFact(exist_fact) => write!(f, "{}", exist_fact),
41            Fact::OrFact(or_fact) => write!(f, "{}", or_fact),
42            Fact::AndFact(and_fact) => write!(f, "{}", and_fact),
43            Fact::ChainFact(chain_fact) => write!(f, "{}", chain_fact),
44            Fact::ForallFact(forall_fact) => write!(f, "{}", forall_fact),
45            Fact::ForallFactWithIff(forall_fact_with_iff) => write!(f, "{}", forall_fact_with_iff),
46            Fact::NotForall(not_forall) => write!(f, "{}", not_forall),
47        }
48    }
49}
50
51impl Fact {
52    pub fn line_file(&self) -> LineFile {
53        match self {
54            Fact::AtomicFact(a) => a.line_file(),
55            Fact::ExistFact(e) => e.line_file(),
56            Fact::OrFact(o) => o.line_file.clone(),
57            Fact::AndFact(a) => a.line_file(),
58            Fact::ChainFact(c) => c.line_file(),
59            Fact::ForallFact(f) => f.line_file.clone(),
60            Fact::ForallFactWithIff(f) => f.line_file.clone(),
61            Fact::NotForall(f) => f.line_file(),
62        }
63    }
64
65    pub fn with_line_file(self, line_file: LineFile) -> Self {
66        match self {
67            Fact::AtomicFact(a) => Fact::AtomicFact(a.with_line_file(line_file)),
68            Fact::ExistFact(mut e) => {
69                match &mut e {
70                    ExistFactEnum::ExistFact(b)
71                    | ExistFactEnum::ExistUniqueFact(b)
72                    | ExistFactEnum::NotExistFact(b) => b.line_file = line_file,
73                }
74                Fact::ExistFact(e)
75            }
76            Fact::OrFact(mut o) => {
77                o.line_file = line_file;
78                Fact::OrFact(o)
79            }
80            Fact::AndFact(mut a) => {
81                a.line_file = line_file;
82                Fact::AndFact(a)
83            }
84            Fact::ChainFact(mut c) => {
85                c.line_file = line_file;
86                Fact::ChainFact(c)
87            }
88            Fact::ForallFact(mut f) => {
89                f.line_file = line_file;
90                Fact::ForallFact(f)
91            }
92            Fact::ForallFactWithIff(mut f) => {
93                f.line_file = line_file;
94                Fact::ForallFactWithIff(f)
95            }
96            Fact::NotForall(mut f) => {
97                f.forall_fact.line_file = line_file;
98                Fact::NotForall(f)
99            }
100        }
101    }
102
103    pub fn into_stmt(self) -> Stmt {
104        self.into()
105    }
106}
107
108#[derive(Clone)]
109pub struct NotForallFact {
110    pub forall_fact: ForallFact,
111}
112
113impl NotForallFact {
114    pub fn new(forall_fact: ForallFact) -> Self {
115        Self { forall_fact }
116    }
117
118    pub fn line_file(&self) -> LineFile {
119        self.forall_fact.line_file.clone()
120    }
121}
122
123impl fmt::Display for NotForallFact {
124    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
125        write!(f, "{} {}", NOT, self.forall_fact)
126    }
127}
128
129impl From<AtomicFact> for Fact {
130    fn from(atomic_fact: AtomicFact) -> Self {
131        Fact::AtomicFact(atomic_fact)
132    }
133}
134
135impl From<OrFact> for Fact {
136    fn from(or_fact: OrFact) -> Self {
137        Fact::OrFact(or_fact)
138    }
139}
140
141impl From<ForallFact> for Fact {
142    fn from(forall_fact: ForallFact) -> Self {
143        Fact::ForallFact(forall_fact)
144    }
145}
146
147impl From<ExistFactEnum> for Fact {
148    fn from(exist_fact: ExistFactEnum) -> Self {
149        Fact::ExistFact(exist_fact)
150    }
151}
152
153impl From<AndFact> for Fact {
154    fn from(and_fact: AndFact) -> Self {
155        Fact::AndFact(and_fact)
156    }
157}
158
159impl From<ChainFact> for Fact {
160    fn from(chain_fact: ChainFact) -> Self {
161        Fact::ChainFact(chain_fact)
162    }
163}
164
165impl From<AndChainAtomicFact> for Fact {
166    fn from(f: AndChainAtomicFact) -> Self {
167        match f {
168            AndChainAtomicFact::AtomicFact(a) => a.into(),
169            AndChainAtomicFact::AndFact(a) => a.into(),
170            AndChainAtomicFact::ChainFact(c) => c.into(),
171        }
172    }
173}
174
175impl From<OrAndChainAtomicFact> for Fact {
176    fn from(f: OrAndChainAtomicFact) -> Self {
177        match f {
178            OrAndChainAtomicFact::AtomicFact(a) => a.into(),
179            OrAndChainAtomicFact::AndFact(a) => a.into(),
180            OrAndChainAtomicFact::ChainFact(c) => c.into(),
181            OrAndChainAtomicFact::OrFact(o) => o.into(),
182        }
183    }
184}
185
186impl From<ForallFactWithIff> for Fact {
187    fn from(forall_fact_with_iff: ForallFactWithIff) -> Self {
188        Fact::ForallFactWithIff(forall_fact_with_iff)
189    }
190}
191
192impl From<NotForallFact> for Fact {
193    fn from(not_forall_fact: NotForallFact) -> Self {
194        Fact::NotForall(not_forall_fact)
195    }
196}
litex/fact/fact.rs

litex/fact/
fact.rs
