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 into_stmt(self) -> Stmt {
66        self.into()
67    }
68}
69
70#[derive(Clone)]
71pub struct NotForallFact {
72    pub forall_fact: ForallFact,
73}
74
75impl NotForallFact {
76    pub fn new(forall_fact: ForallFact) -> Self {
77        Self { forall_fact }
78    }
79
80    pub fn line_file(&self) -> LineFile {
81        self.forall_fact.line_file.clone()
82    }
83}
84
85impl fmt::Display for NotForallFact {
86    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
87        write!(f, "{} {}", NOT, self.forall_fact)
88    }
89}
90
91impl From<AtomicFact> for Fact {
92    fn from(atomic_fact: AtomicFact) -> Self {
93        Fact::AtomicFact(atomic_fact)
94    }
95}
96
97impl From<OrFact> for Fact {
98    fn from(or_fact: OrFact) -> Self {
99        Fact::OrFact(or_fact)
100    }
101}
102
103impl From<ForallFact> for Fact {
104    fn from(forall_fact: ForallFact) -> Self {
105        Fact::ForallFact(forall_fact)
106    }
107}
108
109impl From<ExistFactEnum> for Fact {
110    fn from(exist_fact: ExistFactEnum) -> Self {
111        Fact::ExistFact(exist_fact)
112    }
113}
114
115impl From<AndFact> for Fact {
116    fn from(and_fact: AndFact) -> Self {
117        Fact::AndFact(and_fact)
118    }
119}
120
121impl From<ChainFact> for Fact {
122    fn from(chain_fact: ChainFact) -> Self {
123        Fact::ChainFact(chain_fact)
124    }
125}
126
127impl From<AndChainAtomicFact> for Fact {
128    fn from(f: AndChainAtomicFact) -> Self {
129        match f {
130            AndChainAtomicFact::AtomicFact(a) => a.into(),
131            AndChainAtomicFact::AndFact(a) => a.into(),
132            AndChainAtomicFact::ChainFact(c) => c.into(),
133        }
134    }
135}
136
137impl From<OrAndChainAtomicFact> for Fact {
138    fn from(f: OrAndChainAtomicFact) -> Self {
139        match f {
140            OrAndChainAtomicFact::AtomicFact(a) => a.into(),
141            OrAndChainAtomicFact::AndFact(a) => a.into(),
142            OrAndChainAtomicFact::ChainFact(c) => c.into(),
143            OrAndChainAtomicFact::OrFact(o) => o.into(),
144        }
145    }
146}
147
148impl From<ForallFactWithIff> for Fact {
149    fn from(forall_fact_with_iff: ForallFactWithIff) -> Self {
150        Fact::ForallFactWithIff(forall_fact_with_iff)
151    }
152}
153
154impl From<NotForallFact> for Fact {
155    fn from(not_forall_fact: NotForallFact) -> Self {
156        Fact::NotForall(not_forall_fact)
157    }
158}
litex/fact/fact.rs

litex/fact/
fact.rs
