litex/fact/
exist_fact.rs

1use crate::prelude::*;
2use std::fmt;
3
4#[derive(Clone)]
5pub enum OrAndChainAtomicFact {
6    AtomicFact(AtomicFact),
7    AndFact(AndFact),
8    ChainFact(ChainFact),
9    OrFact(OrFact),
10}
11
12impl From<OrAndChainAtomicFact> for ExistOrAndChainAtomicFact {
13    fn from(f: OrAndChainAtomicFact) -> Self {
14        match f {
15            OrAndChainAtomicFact::AtomicFact(a) => ExistOrAndChainAtomicFact::AtomicFact(a),
16            OrAndChainAtomicFact::AndFact(a) => ExistOrAndChainAtomicFact::AndFact(a),
17            OrAndChainAtomicFact::ChainFact(c) => ExistOrAndChainAtomicFact::ChainFact(c),
18            OrAndChainAtomicFact::OrFact(o) => ExistOrAndChainAtomicFact::OrFact(o),
19        }
20    }
21}
22
23impl OrAndChainAtomicFact {
24    pub fn replace_bound_identifier(self, from: &str, to: &str) -> Self {
25        if from == to {
26            return self;
27        }
28        match self {
29            OrAndChainAtomicFact::AtomicFact(a) => {
30                OrAndChainAtomicFact::AtomicFact(a.replace_bound_identifier(from, to))
31            }
32            OrAndChainAtomicFact::AndFact(af) => OrAndChainAtomicFact::AndFact(AndFact::new(
33                af.facts
34                    .into_iter()
35                    .map(|x| x.replace_bound_identifier(from, to))
36                    .collect(),
37                af.line_file,
38            )),
39            OrAndChainAtomicFact::ChainFact(cf) => OrAndChainAtomicFact::ChainFact(ChainFact::new(
40                cf.objs
41                    .into_iter()
42                    .map(|o| Obj::replace_bound_identifier(o, from, to))
43                    .collect(),
44                cf.prop_names,
45                cf.line_file,
46            )),
47            OrAndChainAtomicFact::OrFact(of) => OrAndChainAtomicFact::OrFact(OrFact::new(
48                of.facts
49                    .into_iter()
50                    .map(|x| x.replace_bound_identifier(from, to))
51                    .collect(),
52                of.line_file,
53            )),
54        }
55    }
56}
57
58impl From<AtomicFact> for OrAndChainAtomicFact {
59    fn from(atomic_fact: AtomicFact) -> Self {
60        OrAndChainAtomicFact::AtomicFact(atomic_fact)
61    }
62}
63
64impl From<GreaterEqualFact> for OrAndChainAtomicFact {
65    fn from(f: GreaterEqualFact) -> Self {
66        AtomicFact::from(f).into()
67    }
68}
69
70impl From<LessFact> for OrAndChainAtomicFact {
71    fn from(f: LessFact) -> Self {
72        AtomicFact::from(f).into()
73    }
74}
75
76impl From<EqualFact> for OrAndChainAtomicFact {
77    fn from(f: EqualFact) -> Self {
78        AtomicFact::from(f).into()
79    }
80}
81
82// `exist` and `exist_unique` share this AST: same parameters and braced facts; `is_exist_unique` selects the keyword.
83// For `exist_unique`, verification must also discharge the companion uniqueness `forall`; storing the existential
84// also stores that generated `forall` (see environment / verify paths).
85#[derive(Clone)]
86pub struct ExistFact {
87    pub params_def_with_type: ParamDefWithType,
88    pub facts: Vec<OrAndChainAtomicFact>,
89    pub is_exist_unique: bool,
90    pub line_file: LineFile,
91}
92
93impl ExistFact {
94    pub fn new(
95        params_def_with_type: ParamDefWithType,
96        facts: Vec<OrAndChainAtomicFact>,
97        is_exist_unique: bool,
98        line_file: LineFile,
99    ) -> Self {
100        ExistFact {
101            params_def_with_type,
102            facts,
103            is_exist_unique,
104            line_file,
105        }
106    }
107
108    pub fn exist_fact_string_without_exist_as_prefix(&self) -> String {
109        exist_fact_string_without_exist_as_prefix(&self.params_def_with_type, &self.facts)
110    }
111
112    pub fn key(&self) -> String {
113        let head = if self.is_exist_unique {
114            EXIST_UNIQUE
115        } else {
116            EXIST
117        };
118        format!(
119            "{} {}{}{}",
120            head,
121            LEFT_CURLY_BRACE,
122            vec_to_string_join_by_comma(
123                &self
124                    .facts
125                    .iter()
126                    .map(|fact| fact.key())
127                    .collect::<Vec<String>>()
128            ),
129            RIGHT_CURLY_BRACE
130        )
131    }
132
133    /// Key for indexing `known_exist_facts_in_forall_facts`: exist witnesses renamed to `#0`, `#1`, …
134    /// so different witness names match the same stored shape.
135    pub fn alpha_normalized_key(&self) -> String {
136        let names = self.params_def_with_type.collect_param_names();
137        let mut normalized_facts: Vec<OrAndChainAtomicFact> = self.facts.clone();
138        for (i, name) in names.iter().enumerate() {
139            let ph = format!("#{}", i);
140            normalized_facts = normalized_facts
141                .into_iter()
142                .map(|f| f.replace_bound_identifier(name, &ph))
143                .collect();
144        }
145        let head = if self.is_exist_unique {
146            EXIST_UNIQUE
147        } else {
148            EXIST
149        };
150        format!(
151            "{} {}{}{}",
152            head,
153            LEFT_CURLY_BRACE,
154            vec_to_string_join_by_comma(
155                &normalized_facts
156                    .iter()
157                    .map(|fact| fact.key())
158                    .collect::<Vec<String>>()
159            ),
160            RIGHT_CURLY_BRACE
161        )
162    }
163
164    pub fn line_file(&self) -> LineFile {
165        self.line_file.clone()
166    }
167
168    pub fn params_def_with_type(&self) -> &ParamDefWithType {
169        &self.params_def_with_type
170    }
171
172    pub fn facts(&self) -> &Vec<OrAndChainAtomicFact> {
173        &self.facts
174    }
175}
176
177fn exist_fact_string_without_exist_as_prefix(
178    param_defs: &ParamDefWithType,
179    facts: &Vec<OrAndChainAtomicFact>,
180) -> String {
181    format!(
182        "{} {} {}",
183        param_defs.to_string(),
184        ST,
185        curly_braced_vec_to_string_with_sep(
186            &facts
187                .iter()
188                .map(|fact| fact.to_string())
189                .collect::<Vec<String>>(),
190            format!("{} ", COMMA)
191        )
192    )
193}
194
195impl fmt::Display for ExistFact {
196    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
197        let head = if self.is_exist_unique {
198            EXIST_UNIQUE
199        } else {
200            EXIST
201        };
202        write!(
203            f,
204            "{} {}",
205            head,
206            self.exist_fact_string_without_exist_as_prefix()
207        )
208    }
209}
210
211// ---------- Display & key for FactInsideExistFact ----------
212impl fmt::Display for OrAndChainAtomicFact {
213    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
214        match self {
215            OrAndChainAtomicFact::AtomicFact(a) => write!(f, "{}", a),
216            OrAndChainAtomicFact::AndFact(a) => write!(f, "{}", a),
217            OrAndChainAtomicFact::ChainFact(c) => write!(f, "{}", c),
218            OrAndChainAtomicFact::OrFact(o) => write!(f, "{}", o),
219        }
220    }
221}
222
223impl OrAndChainAtomicFact {
224    pub fn key(&self) -> String {
225        match self {
226            OrAndChainAtomicFact::AtomicFact(a) => a.key(),
227            OrAndChainAtomicFact::AndFact(a) => a.key(),
228            OrAndChainAtomicFact::ChainFact(c) => c.key(),
229            OrAndChainAtomicFact::OrFact(o) => o.key(),
230        }
231    }
232    pub fn line_file(&self) -> LineFile {
233        match self {
234            OrAndChainAtomicFact::AtomicFact(a) => a.line_file(),
235            OrAndChainAtomicFact::AndFact(a) => a.line_file(),
236            OrAndChainAtomicFact::ChainFact(c) => c.line_file(),
237            OrAndChainAtomicFact::OrFact(o) => o.line_file.clone(),
238        }
239    }
240
241    pub fn with_new_line_file(self, line_file: LineFile) -> Self {
242        match self {
243            OrAndChainAtomicFact::AtomicFact(a) => {
244                OrAndChainAtomicFact::AtomicFact(a.with_new_line_file(line_file))
245            }
246            OrAndChainAtomicFact::AndFact(af) => OrAndChainAtomicFact::AndFact(AndFact::new(
247                af.facts
248                    .into_iter()
249                    .map(|x| x.with_new_line_file(line_file.clone()))
250                    .collect(),
251                line_file,
252            )),
253            OrAndChainAtomicFact::ChainFact(cf) => {
254                OrAndChainAtomicFact::ChainFact(ChainFact::new(cf.objs, cf.prop_names, line_file))
255            }
256            OrAndChainAtomicFact::OrFact(of) => OrAndChainAtomicFact::OrFact(OrFact::new(
257                of.facts
258                    .into_iter()
259                    .map(|x| x.with_new_line_file(line_file.clone()))
260                    .collect(),
261                line_file,
262            )),
263        }
264    }
265}
266
267impl OrAndChainAtomicFact {
268    pub fn from_ref_to_cloned_fact(&self) -> Fact {
269        match self {
270            OrAndChainAtomicFact::AtomicFact(a) => a.clone().into(),
271            OrAndChainAtomicFact::AndFact(a) => a.clone().into(),
272            OrAndChainAtomicFact::ChainFact(c) => c.clone().into(),
273            OrAndChainAtomicFact::OrFact(o) => o.clone().into(),
274        }
275    }
276
277    pub fn to_fact(self) -> Fact {
278        match self {
279            OrAndChainAtomicFact::AtomicFact(a) => Fact::AtomicFact(a),
280            OrAndChainAtomicFact::AndFact(a) => Fact::AndFact(a),
281            OrAndChainAtomicFact::ChainFact(c) => Fact::ChainFact(c),
282            OrAndChainAtomicFact::OrFact(o) => Fact::OrFact(o),
283        }
284    }
285
286    pub fn get_args_from_fact(&self) -> Vec<Obj> {
287        match self {
288            OrAndChainAtomicFact::AtomicFact(a) => a.get_args_from_fact(),
289            OrAndChainAtomicFact::AndFact(a) => a.get_args_from_fact(),
290            OrAndChainAtomicFact::ChainFact(c) => c.get_args_from_fact(),
291            OrAndChainAtomicFact::OrFact(o) => o.get_args_from_fact(),
292        }
293    }
294}
295
296impl ExistFact {
297    pub fn get_args_from_fact(&self) -> Vec<Obj> {
298        let mut args: Vec<Obj> = Vec::new();
299        for param_def_with_type in self.params_def_with_type.groups.iter() {
300            if let ParamType::Obj(obj) = &param_def_with_type.param_type {
301                args.push(obj.clone());
302            }
303        }
304
305        for fact in self.facts.iter() {
306            for arg in fact.get_args_from_fact() {
307                args.push(arg);
308            }
309        }
310
311        args
312    }
313}
litex/fact/exist_fact.rs

litex/fact/
exist_fact.rs
