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    pub fn line_file(&self) -> LineFile {
134        self.line_file.clone()
135    }
136
137    pub fn params_def_with_type(&self) -> &ParamDefWithType {
138        &self.params_def_with_type
139    }
140
141    pub fn facts(&self) -> &Vec<OrAndChainAtomicFact> {
142        &self.facts
143    }
144}
145
146fn exist_fact_string_without_exist_as_prefix(
147    param_defs: &ParamDefWithType,
148    facts: &Vec<OrAndChainAtomicFact>,
149) -> String {
150    format!(
151        "{} {} {}",
152        param_defs.to_string(),
153        ST,
154        curly_braced_vec_to_string_with_sep(
155            &facts
156                .iter()
157                .map(|fact| fact.to_string())
158                .collect::<Vec<String>>(),
159            format!("{} ", COMMA)
160        )
161    )
162}
163
164impl fmt::Display for ExistFact {
165    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
166        let head = if self.is_exist_unique {
167            EXIST_UNIQUE
168        } else {
169            EXIST
170        };
171        write!(
172            f,
173            "{} {}",
174            head,
175            self.exist_fact_string_without_exist_as_prefix()
176        )
177    }
178}
179
180// ---------- Display & key for FactInsideExistFact ----------
181impl fmt::Display for OrAndChainAtomicFact {
182    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
183        match self {
184            OrAndChainAtomicFact::AtomicFact(a) => write!(f, "{}", a),
185            OrAndChainAtomicFact::AndFact(a) => write!(f, "{}", a),
186            OrAndChainAtomicFact::ChainFact(c) => write!(f, "{}", c),
187            OrAndChainAtomicFact::OrFact(o) => write!(f, "{}", o),
188        }
189    }
190}
191
192impl OrAndChainAtomicFact {
193    pub fn key(&self) -> String {
194        match self {
195            OrAndChainAtomicFact::AtomicFact(a) => a.key(),
196            OrAndChainAtomicFact::AndFact(a) => a.key(),
197            OrAndChainAtomicFact::ChainFact(c) => c.key(),
198            OrAndChainAtomicFact::OrFact(o) => o.key(),
199        }
200    }
201    pub fn line_file(&self) -> LineFile {
202        match self {
203            OrAndChainAtomicFact::AtomicFact(a) => a.line_file(),
204            OrAndChainAtomicFact::AndFact(a) => a.line_file(),
205            OrAndChainAtomicFact::ChainFact(c) => c.line_file(),
206            OrAndChainAtomicFact::OrFact(o) => o.line_file.clone(),
207        }
208    }
209
210    pub fn with_new_line_file(self, line_file: LineFile) -> Self {
211        match self {
212            OrAndChainAtomicFact::AtomicFact(a) => {
213                OrAndChainAtomicFact::AtomicFact(a.with_new_line_file(line_file))
214            }
215            OrAndChainAtomicFact::AndFact(af) => OrAndChainAtomicFact::AndFact(AndFact::new(
216                af.facts
217                    .into_iter()
218                    .map(|x| x.with_new_line_file(line_file.clone()))
219                    .collect(),
220                line_file,
221            )),
222            OrAndChainAtomicFact::ChainFact(cf) => {
223                OrAndChainAtomicFact::ChainFact(ChainFact::new(cf.objs, cf.prop_names, line_file))
224            }
225            OrAndChainAtomicFact::OrFact(of) => OrAndChainAtomicFact::OrFact(OrFact::new(
226                of.facts
227                    .into_iter()
228                    .map(|x| x.with_new_line_file(line_file.clone()))
229                    .collect(),
230                line_file,
231            )),
232        }
233    }
234}
235
236impl OrAndChainAtomicFact {
237    pub fn from_ref_to_cloned_fact(&self) -> Fact {
238        match self {
239            OrAndChainAtomicFact::AtomicFact(a) => a.clone().into(),
240            OrAndChainAtomicFact::AndFact(a) => a.clone().into(),
241            OrAndChainAtomicFact::ChainFact(c) => c.clone().into(),
242            OrAndChainAtomicFact::OrFact(o) => o.clone().into(),
243        }
244    }
245
246    pub fn to_fact(self) -> Fact {
247        match self {
248            OrAndChainAtomicFact::AtomicFact(a) => Fact::AtomicFact(a),
249            OrAndChainAtomicFact::AndFact(a) => Fact::AndFact(a),
250            OrAndChainAtomicFact::ChainFact(c) => Fact::ChainFact(c),
251            OrAndChainAtomicFact::OrFact(o) => Fact::OrFact(o),
252        }
253    }
254
255    pub fn get_args_from_fact(&self) -> Vec<Obj> {
256        match self {
257            OrAndChainAtomicFact::AtomicFact(a) => a.get_args_from_fact(),
258            OrAndChainAtomicFact::AndFact(a) => a.get_args_from_fact(),
259            OrAndChainAtomicFact::ChainFact(c) => c.get_args_from_fact(),
260            OrAndChainAtomicFact::OrFact(o) => o.get_args_from_fact(),
261        }
262    }
263}
264
265impl ExistFact {
266    pub fn get_args_from_fact(&self) -> Vec<Obj> {
267        let mut args: Vec<Obj> = Vec::new();
268        for param_def_with_type in self.params_def_with_type.groups.iter() {
269            if let ParamType::Obj(obj) = &param_def_with_type.param_type {
270                args.push(obj.clone());
271            }
272        }
273
274        for fact in self.facts.iter() {
275            for arg in fact.get_args_from_fact() {
276                args.push(arg);
277            }
278        }
279
280        args
281    }
282}
litex/fact/exist_fact.rs

litex/fact/
exist_fact.rs
