1use super::known_fn::KnownFnInfo;
2use crate::prelude::*;
3use std::collections::HashMap;
4use std::fmt;
5use std::rc::Rc;
6
7pub struct Environment {
8 pub defined_identifiers: HashMap<IdentifierName, ParamObjType>,
9 pub defined_def_props: HashMap<PropName, DefPropStmt>,
10 pub defined_abstract_props: HashMap<AbstractPropName, DefAbstractPropStmt>,
11 pub defined_algorithms: HashMap<AlgoName, DefAlgoStmt>,
12 pub defined_structs: HashMap<StructName, DefStructStmt>,
13 pub defined_templates: HashMap<TemplateName, DefTemplateStmt>,
14
15 pub known_equality: HashMap<ObjString, (HashMap<ObjString, AtomicFact>, Rc<Vec<Obj>>)>,
16
17 pub known_atomic_facts_with_0_or_more_than_2_args:
18 HashMap<(AtomicFactKey, bool), Vec<AtomicFact>>,
19 pub known_atomic_facts_with_1_arg:
20 HashMap<(AtomicFactKey, bool), HashMap<ObjString, AtomicFact>>,
21 pub known_atomic_facts_with_2_args:
22 HashMap<(AtomicFactKey, bool), HashMap<(ObjString, ObjString), AtomicFact>>,
23
24 pub known_exist_facts: HashMap<ExistFactKey, Vec<ExistFactEnum>>,
25 pub known_or_facts: HashMap<OrFactKey, Vec<OrFact>>,
26
27 pub known_atomic_facts_in_forall_facts:
28 HashMap<(AtomicFactKey, bool), Vec<(AtomicFact, Rc<KnownForallFactParamsAndDom>)>>,
29 pub known_exist_facts_in_forall_facts:
30 HashMap<ExistFactKey, Vec<(ExistFactEnum, Rc<KnownForallFactParamsAndDom>)>>,
31 pub known_or_facts_in_forall_facts:
32 HashMap<OrFactKey, Vec<(OrFact, Rc<KnownForallFactParamsAndDom>)>>,
33
34 pub known_objs_equal_to_tuple: HashMap<ObjString, (Option<Tuple>, Option<Cart>, LineFile)>,
35 pub known_objs_equal_to_cart: HashMap<ObjString, (Cart, LineFile)>,
36 pub known_objs_equal_to_finite_seq_list:
37 HashMap<ObjString, (FiniteSeqListObj, Option<FiniteSeqSet>, LineFile)>,
38 pub known_objs_equal_to_matrix_list:
39 HashMap<ObjString, (MatrixListObj, Option<MatrixSet>, LineFile)>,
40 pub known_objs_equal_to_normalized_decimal_number: HashMap<ObjString, Number>,
41 pub known_objs_equal_to_set_builder: HashMap<ObjString, (SetBuilder, LineFile)>,
42
43 pub known_objs_in_fn_sets: HashMap<ObjString, KnownFnInfo>,
44
45 pub known_transitive_props: HashMap<String, ()>,
46 pub known_symmetric_props: HashMap<String, SymmetricPropValue>,
47 pub known_reflexive_props: HashMap<String, ()>,
48 pub known_antisymmetric_props: HashMap<String, ()>,
49
50 pub cache_well_defined_obj: HashMap<ObjString, ()>,
51 pub cache_known_fact: HashMap<FactString, LineFile>,
52}
53
54impl Environment {
55 pub fn new(
56 objs: HashMap<IdentifierName, ParamObjType>,
57 def_props: HashMap<PropName, DefPropStmt>,
58 abstract_props: HashMap<AbstractPropName, DefAbstractPropStmt>,
59 algorithms: HashMap<AlgoName, DefAlgoStmt>,
60 structs: HashMap<StructName, DefStructStmt>,
61 templates: HashMap<TemplateName, DefTemplateStmt>,
62 known_equality: HashMap<ObjString, (HashMap<ObjString, AtomicFact>, Rc<Vec<Obj>>)>,
63 known_fn_in_fn_set: HashMap<ObjString, KnownFnInfo>,
64 known_atomic_facts_with_0_or_more_than_2_args: HashMap<
65 (AtomicFactKey, bool),
66 Vec<AtomicFact>,
67 >,
68 known_atomic_facts_with_1_arg: HashMap<
69 (AtomicFactKey, bool),
70 HashMap<ObjString, AtomicFact>,
71 >,
72 known_atomic_facts_with_2_args: HashMap<
73 (AtomicFactKey, bool),
74 HashMap<(ObjString, ObjString), AtomicFact>,
75 >,
76 known_exist_facts: HashMap<ExistFactKey, Vec<ExistFactEnum>>,
77 known_atomic_facts_in_forall_facts: HashMap<
78 (AtomicFactKey, bool),
79 Vec<(AtomicFact, Rc<KnownForallFactParamsAndDom>)>,
80 >,
81 known_exist_facts_in_forall_facts: HashMap<
82 ExistFactKey,
83 Vec<(ExistFactEnum, Rc<KnownForallFactParamsAndDom>)>,
84 >,
85 known_or_facts: HashMap<OrFactKey, Vec<OrFact>>,
86 known_or_facts_in_forall_facts: HashMap<
87 OrFactKey,
88 Vec<(OrFact, Rc<KnownForallFactParamsAndDom>)>,
89 >,
90 known_tuple_objs: HashMap<ObjString, (Option<Tuple>, Option<Cart>, LineFile)>,
91 known_cart_objs: HashMap<ObjString, (Cart, LineFile)>,
92 known_finite_seq_list_objs: HashMap<
93 ObjString,
94 (FiniteSeqListObj, Option<FiniteSeqSet>, LineFile),
95 >,
96 known_matrix_list_objs: HashMap<ObjString, (MatrixListObj, Option<MatrixSet>, LineFile)>,
97 known_calculated_value_of_obj: HashMap<ObjString, Number>,
98 known_set_builder_objs: HashMap<ObjString, (SetBuilder, LineFile)>,
99 cache_known_valid_obj: HashMap<ObjString, ()>,
100 cache_known_fact: HashMap<FactString, LineFile>,
101 ) -> Self {
102 Environment {
103 defined_identifiers: objs,
104 defined_def_props: def_props,
105 defined_abstract_props: abstract_props,
106 defined_algorithms: algorithms,
107 defined_structs: structs,
108 defined_templates: templates,
109 known_equality,
110 known_objs_in_fn_sets: known_fn_in_fn_set,
111 known_atomic_facts_with_0_or_more_than_2_args,
112 known_atomic_facts_with_1_arg: known_atomic_facts_with_1_arg,
113 known_atomic_facts_with_2_args: known_atomic_facts_with_2_args,
114 known_exist_facts,
115 known_atomic_facts_in_forall_facts,
116 known_exist_facts_in_forall_facts,
117 known_or_facts,
118 known_or_facts_in_forall_facts,
119 known_objs_equal_to_tuple: known_tuple_objs,
120 known_objs_equal_to_cart: known_cart_objs,
121 known_objs_equal_to_finite_seq_list: known_finite_seq_list_objs,
122 known_objs_equal_to_matrix_list: known_matrix_list_objs,
123 known_objs_equal_to_normalized_decimal_number: known_calculated_value_of_obj,
124 known_objs_equal_to_set_builder: known_set_builder_objs,
125 known_transitive_props: HashMap::new(),
126 known_symmetric_props: HashMap::new(),
127 known_reflexive_props: HashMap::new(),
128 known_antisymmetric_props: HashMap::new(),
129 cache_well_defined_obj: cache_known_valid_obj,
130 cache_known_fact,
131 }
132 }
133}
134
135impl fmt::Display for Environment {
136 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
137 write!(f, "Environment {{\n")?;
138 write!(f, " objs: {:?}\n", self.defined_identifiers.len())?;
139 write!(f, " def_props: {:?}\n", self.defined_def_props.len())?;
140 write!(f, " algorithms: {:?}\n", self.defined_algorithms.len())?;
141 write!(f, " structs: {:?}\n", self.defined_structs.len())?;
142 write!(f, " templates: {:?}\n", self.defined_templates.len())?;
143 write!(f, " known_equality: {:?}\n", self.known_equality.len())?;
144 write!(
145 f,
146 " known_fn_in_fn_set: {:?}\n",
147 self.known_objs_in_fn_sets.len()
148 )?;
149 write!(
150 f,
151 " known_transitive_props: {:?}\n",
152 self.known_transitive_props.len()
153 )?;
154 write!(
155 f,
156 " known_symmetric_props: {} predicates, {} permutations\n",
157 self.known_symmetric_props.len(),
158 self.known_symmetric_props
159 .values()
160 .map(|v| v.len())
161 .sum::<usize>()
162 )?;
163 write!(
164 f,
165 " known_reflexive_props: {:?}\n",
166 self.known_reflexive_props.len()
167 )?;
168 write!(
169 f,
170 " known_antisymmetric_props: {:?}\n",
171 self.known_antisymmetric_props.len()
172 )?;
173 write!(
174 f,
175 " known_atomic_facts_with_0_or_more_than_two_params: {:?}\n",
176 self.known_atomic_facts_with_0_or_more_than_2_args.len()
177 )?;
178 write!(
179 f,
180 " known_atomic_facts_with_1_arg: {:?}\n",
181 self.known_atomic_facts_with_1_arg.len()
182 )?;
183 write!(
184 f,
185 " known_atomic_facts_with_2_args: {:?}\n",
186 self.known_atomic_facts_with_2_args.len()
187 )?;
188 write!(
189 f,
190 " known_exist_facts_with_more_than_two_params: {:?}\n",
191 self.known_exist_facts.len()
192 )?;
193 write!(
194 f,
195 " known_or_facts_with_more_than_two_params: {:?}\n",
196 self.known_or_facts.len()
197 )?;
198 write!(
199 f,
200 " known_atomic_facts_in_forall_facts: {:?}\n",
201 self.known_atomic_facts_in_forall_facts.len()
202 )?;
203 write!(
204 f,
205 " known_exist_facts_in_forall_facts: {:?}\n",
206 self.known_exist_facts_in_forall_facts.len()
207 )?;
208 write!(
209 f,
210 " known_or_facts_in_forall_facts: {:?}\n",
211 self.known_or_facts_in_forall_facts.len()
212 )?;
213 write!(
214 f,
215 " cache_known_valid_obj: {:?}\n",
216 self.cache_well_defined_obj.len()
217 )?;
218 write!(
219 f,
220 " cache_known_fact: {:?}\n",
221 self.cache_known_fact.len()
222 )?;
223 write!(f, "}}")
224 }
225}
226
227impl Environment {
228 pub fn store_atomic_fact_by_ref(
229 &mut self,
230 atomic_fact: &AtomicFact,
231 ) -> Result<(), RuntimeError> {
232 self.store_atomic_fact(atomic_fact.clone())
233 }
234
235 pub fn store_atomic_fact(&mut self, atomic_fact: AtomicFact) -> Result<(), RuntimeError> {
236 match atomic_fact {
237 AtomicFact::EqualFact(equal_fact) => self.store_equality(&equal_fact),
238 _ => {
239 let key: AtomicFactKey = atomic_fact.key();
240 let is_true = atomic_fact.is_true();
241 if atomic_fact.args().len() == 1 {
242 let arg_key: ObjString = atomic_fact.args()[0].to_string();
243 if let Some(map) = self
244 .known_atomic_facts_with_1_arg
245 .get_mut(&(key.clone(), is_true))
246 {
247 map.insert(arg_key, atomic_fact);
248 } else {
249 self.known_atomic_facts_with_1_arg
250 .insert((key, is_true), HashMap::from([(arg_key, atomic_fact)]));
251 }
252 } else if atomic_fact.args().len() == 2 {
253 let arg_key1: ObjString = atomic_fact.args()[0].to_string();
254 let arg_key2: ObjString = atomic_fact.args()[1].to_string();
255 if let Some(map) = self
256 .known_atomic_facts_with_2_args
257 .get_mut(&(key.clone(), is_true))
258 {
259 map.insert((arg_key1, arg_key2), atomic_fact);
260 } else {
261 self.known_atomic_facts_with_2_args.insert(
262 (key, is_true),
263 HashMap::from([((arg_key1, arg_key2), atomic_fact)]),
264 );
265 }
266 } else {
267 if let Some(vec_ref) = self
268 .known_atomic_facts_with_0_or_more_than_2_args
269 .get_mut(&(key.clone(), is_true))
270 {
271 vec_ref.push(atomic_fact);
272 } else {
273 self.known_atomic_facts_with_0_or_more_than_2_args
274 .insert((key, is_true), vec![atomic_fact]);
275 }
276 }
277 Ok(())
278 }
279 }
280 }
281
282 fn store_exist_fact(&mut self, exist_fact: ExistFactEnum) -> Result<(), RuntimeError> {
283 let key: ExistFactKey = exist_fact.key();
284 if let Some(vec_ref) = self.known_exist_facts.get_mut(&key) {
285 vec_ref.push(exist_fact);
286 } else {
287 self.known_exist_facts.insert(key, vec![exist_fact]);
288 }
289 Ok(())
290 }
291
292 fn store_or_fact(&mut self, or_fact: OrFact) -> Result<(), RuntimeError> {
293 let key: OrFactKey = or_fact.key();
294 if let Some(vec_ref) = self.known_or_facts.get_mut(&key) {
295 vec_ref.push(or_fact);
296 } else {
297 self.known_or_facts.insert(key, vec![or_fact]);
298 }
299 Ok(())
300 }
301
302 fn store_atomic_fact_in_forall_fact(
303 &mut self,
304 atomic_fact: AtomicFact,
305 forall_params_and_dom: Rc<KnownForallFactParamsAndDom>,
306 ) -> Result<(), RuntimeError> {
307 let key: AtomicFactKey = atomic_fact.key();
308 let is_true = atomic_fact.is_true();
309 if let Some(vec_ref) = self
310 .known_atomic_facts_in_forall_facts
311 .get_mut(&(key.clone(), is_true))
312 {
313 vec_ref.push((atomic_fact, forall_params_and_dom));
314 } else {
315 self.known_atomic_facts_in_forall_facts
316 .insert((key, is_true), vec![(atomic_fact, forall_params_and_dom)]);
317 }
318 Ok(())
319 }
320
321 fn store_or_fact_in_forall_fact(
322 &mut self,
323 or_fact: &OrFact,
324 forall_params_and_dom: Rc<KnownForallFactParamsAndDom>,
325 ) -> Result<(), RuntimeError> {
326 let key: OrFactKey = or_fact.key();
327 if let Some(vec_ref) = self.known_or_facts_in_forall_facts.get_mut(&key) {
328 vec_ref.push((or_fact.clone(), forall_params_and_dom));
329 } else {
330 self.known_or_facts_in_forall_facts
331 .insert(key, vec![(or_fact.clone(), forall_params_and_dom)]);
332 }
333 Ok(())
334 }
335
336 fn store_a_fact_in_forall_fact(
337 &mut self,
338 fact: &ExistOrAndChainAtomicFact,
339 forall_params_and_dom: Rc<KnownForallFactParamsAndDom>,
340 ) -> Result<(), RuntimeError> {
341 match fact {
342 ExistOrAndChainAtomicFact::AtomicFact(spec_fact) => {
343 self.store_atomic_fact_in_forall_fact(spec_fact.clone(), forall_params_and_dom)
344 }
345 ExistOrAndChainAtomicFact::OrFact(or_fact) => {
346 self.store_or_fact_in_forall_fact(&or_fact, forall_params_and_dom)
347 }
348 ExistOrAndChainAtomicFact::AndFact(and_fact) => {
349 self.store_and_fact_in_forall_fact(&and_fact, forall_params_and_dom)
350 }
351 ExistOrAndChainAtomicFact::ChainFact(chain_fact) => {
352 self.store_chain_fact_in_forall_fact(&chain_fact, forall_params_and_dom)
353 }
354 ExistOrAndChainAtomicFact::ExistFact(exist_fact) => {
355 self.store_exist_fact_in_forall_fact(&exist_fact, forall_params_and_dom)
356 }
357 }
358 }
359
360 fn store_chain_fact_in_forall_fact(
361 &mut self,
362 chain_fact: &ChainFact,
363 forall_params_and_dom: Rc<KnownForallFactParamsAndDom>,
364 ) -> Result<(), RuntimeError> {
365 for fact in chain_fact
366 .facts()
367 .map_err(RuntimeError::wrap_new_fact_as_store_conflict)?
368 .into_iter()
369 {
370 self.store_atomic_fact_in_forall_fact(fact, forall_params_and_dom.clone())?;
371 }
372 Ok(())
373 }
374
375 fn store_exist_fact_in_forall_fact(
376 &mut self,
377 exist_fact: &ExistFactEnum,
378 forall_params_and_dom: Rc<KnownForallFactParamsAndDom>,
379 ) -> Result<(), RuntimeError> {
380 let pair = || (exist_fact.clone(), forall_params_and_dom.clone());
381 let key: ExistFactKey = exist_fact.key();
382 if let Some(vec_ref) = self.known_exist_facts_in_forall_facts.get_mut(&key) {
383 vec_ref.push(pair());
384 } else {
385 self.known_exist_facts_in_forall_facts
386 .insert(key, vec![pair()]);
387 }
388 let alpha_key = exist_fact.alpha_normalized_key();
389 if alpha_key != exist_fact.key() {
390 if let Some(vec_ref) = self.known_exist_facts_in_forall_facts.get_mut(&alpha_key) {
391 vec_ref.push(pair());
392 } else {
393 self.known_exist_facts_in_forall_facts
394 .insert(alpha_key, vec![pair()]);
395 }
396 }
397 Ok(())
398 }
399
400 fn store_and_fact_in_forall_fact(
401 &mut self,
402 and_fact: &AndFact,
403 forall_params_and_dom: Rc<KnownForallFactParamsAndDom>,
404 ) -> Result<(), RuntimeError> {
405 for fact in and_fact.facts.iter() {
406 self.store_atomic_fact_in_forall_fact(fact.clone(), forall_params_and_dom.clone())?;
407 }
408 Ok(())
409 }
410
411 fn store_forall_fact(&mut self, forall_fact: Rc<ForallFact>) -> Result<(), RuntimeError> {
412 let forall_params_and_dom = Rc::new(KnownForallFactParamsAndDom::new(
413 forall_fact.params_def_with_type.clone(),
414 forall_fact.dom_facts.clone(),
415 forall_fact.line_file.clone(),
416 ));
417
418 for fact in forall_fact.then_facts.iter() {
419 self.store_a_fact_in_forall_fact(fact, forall_params_and_dom.clone())?;
420 }
421 Ok(())
422 }
423
424 fn store_and_fact(&mut self, and_fact: AndFact) -> Result<(), RuntimeError> {
425 for atomic_fact in and_fact.facts {
426 self.store_atomic_fact(atomic_fact)?;
427 }
428 Ok(())
429 }
430
431 fn store_forall_fact_with_iff(
432 &mut self,
433 forall_fact_with_iff: ForallFactWithIff,
434 ) -> Result<(), RuntimeError> {
435 let (forall_then_implies_iff, forall_iff_implies_then) =
436 forall_fact_with_iff.to_two_forall_facts()?;
437 self.store_forall_fact(Rc::new(forall_then_implies_iff))?;
438 self.store_forall_fact(Rc::new(forall_iff_implies_then))?;
439 Ok(())
440 }
441
442 pub fn store_fact(&mut self, fact: Fact) -> Result<(), RuntimeError> {
443 match fact {
444 Fact::AtomicFact(atomic_fact) => self.store_atomic_fact(atomic_fact),
445 Fact::ExistFact(exist_fact) => self.store_exist_fact(exist_fact),
446 Fact::OrFact(or_fact) => self.store_or_fact(or_fact),
447 Fact::AndFact(and_fact) => self.store_and_fact(and_fact),
448 Fact::ChainFact(chain_fact) => self.store_chain_fact(chain_fact),
449 Fact::ForallFact(forall_fact) => self.store_forall_fact(Rc::new(forall_fact)),
450 Fact::ForallFactWithIff(forall_fact_with_iff) => {
451 self.store_forall_fact_with_iff(forall_fact_with_iff)
452 }
453 Fact::NotForall(_) => Ok(()),
454 }
455 }
456
457 pub fn store_exist_fact_by_ref(
458 &mut self,
459 exist_fact: &ExistFactEnum,
460 ) -> Result<(), RuntimeError> {
461 self.store_exist_fact(exist_fact.clone())
462 }
463
464 pub fn store_exist_or_and_chain_atomic_fact(
465 &mut self,
466 fact: ExistOrAndChainAtomicFact,
467 ) -> Result<(), RuntimeError> {
468 match fact {
469 ExistOrAndChainAtomicFact::AtomicFact(atomic_fact) => {
470 self.store_atomic_fact(atomic_fact)
471 }
472 ExistOrAndChainAtomicFact::AndFact(and_fact) => self.store_and_fact(and_fact),
473 ExistOrAndChainAtomicFact::ChainFact(chain_fact) => self.store_chain_fact(chain_fact),
474 ExistOrAndChainAtomicFact::OrFact(or_fact) => self.store_or_fact(or_fact),
475 ExistOrAndChainAtomicFact::ExistFact(exist_fact) => self.store_exist_fact(exist_fact),
476 }
477 }
478
479 pub fn store_and_chain_atomic_fact(
480 &mut self,
481 and_chain_atomic_fact: AndChainAtomicFact,
482 ) -> Result<(), RuntimeError> {
483 match and_chain_atomic_fact {
484 AndChainAtomicFact::AtomicFact(atomic_fact) => self.store_atomic_fact(atomic_fact),
485 AndChainAtomicFact::AndFact(and_fact) => self.store_and_fact(and_fact),
486 AndChainAtomicFact::ChainFact(chain_fact) => self.store_chain_fact(chain_fact),
487 }
488 }
489
490 pub fn store_or_and_chain_atomic_fact(
491 &mut self,
492 fact: OrAndChainAtomicFact,
493 ) -> Result<(), RuntimeError> {
494 match fact {
495 OrAndChainAtomicFact::AtomicFact(atomic_fact) => self.store_atomic_fact(atomic_fact),
496 OrAndChainAtomicFact::AndFact(and_fact) => self.store_and_fact(and_fact),
497 OrAndChainAtomicFact::ChainFact(chain_fact) => self.store_chain_fact(chain_fact),
498 OrAndChainAtomicFact::OrFact(or_fact) => self.store_or_fact(or_fact),
499 }
500 }
501
502 fn store_chain_fact(&mut self, chain_fact: ChainFact) -> Result<(), RuntimeError> {
503 let atomic_facts = chain_fact
504 .facts_with_order_transitive_closure()
505 .map_err(RuntimeError::wrap_new_fact_as_store_conflict)?;
506 for atomic_fact in atomic_facts {
507 self.store_atomic_fact(atomic_fact)?;
508 }
509 Ok(())
510 }
511
512 pub fn store_chain_fact_by_ref(&mut self, chain_fact: &ChainFact) -> Result<(), RuntimeError> {
513 self.store_chain_fact(chain_fact.clone())
514 }
515
516 pub fn store_equality(&mut self, equality: &EqualFact) -> Result<(), RuntimeError> {
517 let left_as_string: ObjString = equality.left.to_string();
518 let right_as_string: ObjString = equality.right.to_string();
519 if left_as_string == right_as_string {
520 return Ok(());
521 }
522
523 let left_rc = self
524 .known_equality
525 .get(&left_as_string)
526 .map(|(_, rc)| Rc::clone(rc));
527 let right_rc = self
528 .known_equality
529 .get(&right_as_string)
530 .map(|(_, rc)| Rc::clone(rc));
531
532 let equal_atomic_fact = AtomicFact::EqualFact(equality.clone());
533
534 match (left_rc, right_rc) {
535 (Some(ref left_class_rc), Some(ref right_class_rc)) => {
536 if Rc::ptr_eq(left_class_rc, right_class_rc) {
537 return Ok(());
538 }
539 let merged_vec: Vec<Obj> = {
540 let left_vec: &Vec<Obj> = left_class_rc.as_ref();
541 let right_vec: &Vec<Obj> = right_class_rc.as_ref();
542 let mut merged = Vec::with_capacity(left_vec.len() + right_vec.len());
543 for obj in left_vec.iter().chain(right_vec.iter()) {
544 merged.push(obj.clone());
545 }
546 merged.sort_by(|a_obj, b_obj| a_obj.to_string().cmp(&b_obj.to_string()));
547 merged.dedup_by(|a_obj, b_obj| a_obj.to_string() == b_obj.to_string());
548 merged
549 };
550 let new_equiv_rc = Rc::new(merged_vec);
551
552 let keys_in_either_class: Vec<ObjString> = self
553 .known_equality
554 .iter()
555 .filter(|(_, (_, class_rc))| {
556 Rc::ptr_eq(class_rc, left_class_rc) || Rc::ptr_eq(class_rc, right_class_rc)
557 })
558 .map(|(k, _)| k.clone())
559 .collect();
560
561 for key_in_class in keys_in_either_class {
562 let removed_entry = match self.known_equality.remove(&key_in_class) {
563 Some(entry) => entry,
564 None => continue,
565 };
566 let (mut direct_equality_proof_map, _) = removed_entry;
567 if key_in_class == left_as_string {
568 direct_equality_proof_map
569 .insert(right_as_string.clone(), equal_atomic_fact.clone());
570 }
571 if key_in_class == right_as_string {
572 direct_equality_proof_map
573 .insert(left_as_string.clone(), equal_atomic_fact.clone());
574 }
575 self.known_equality.insert(
576 key_in_class,
577 (direct_equality_proof_map, Rc::clone(&new_equiv_rc)),
578 );
579 }
580 }
581 (Some(existing_class_rc), None) => {
582 let mut new_vec = (*existing_class_rc).clone();
583 new_vec.push(equality.right.clone());
584 let new_equiv_rc = Rc::new(new_vec);
585
586 let keys_in_existing_class: Vec<ObjString> = self
587 .known_equality
588 .iter()
589 .filter(|(_, (_, class_rc))| Rc::ptr_eq(class_rc, &existing_class_rc))
590 .map(|(k, _)| k.clone())
591 .collect();
592
593 for key_in_class in keys_in_existing_class {
594 let removed_entry = match self.known_equality.remove(&key_in_class) {
595 Some(entry) => entry,
596 None => continue,
597 };
598 let (mut direct_equality_proof_map, _) = removed_entry;
599 if key_in_class == left_as_string {
600 direct_equality_proof_map
601 .insert(right_as_string.clone(), equal_atomic_fact.clone());
602 }
603 self.known_equality.insert(
604 key_in_class,
605 (direct_equality_proof_map, Rc::clone(&new_equiv_rc)),
606 );
607 }
608
609 let mut proof_for_new_right: HashMap<ObjString, AtomicFact> = HashMap::new();
610 proof_for_new_right.insert(left_as_string.clone(), equal_atomic_fact.clone());
611 self.known_equality
612 .insert(right_as_string, (proof_for_new_right, new_equiv_rc));
613 }
614 (None, Some(existing_class_rc)) => {
615 let mut new_vec = (*existing_class_rc).clone();
616 new_vec.push(equality.left.clone());
617 let new_equiv_rc = Rc::new(new_vec);
618
619 let keys_in_existing_class: Vec<ObjString> = self
620 .known_equality
621 .iter()
622 .filter(|(_, (_, class_rc))| Rc::ptr_eq(class_rc, &existing_class_rc))
623 .map(|(k, _)| k.clone())
624 .collect();
625
626 for key_in_class in keys_in_existing_class {
627 let removed_entry = match self.known_equality.remove(&key_in_class) {
628 Some(entry) => entry,
629 None => continue,
630 };
631 let (mut direct_equality_proof_map, _) = removed_entry;
632 if key_in_class == right_as_string {
633 direct_equality_proof_map
634 .insert(left_as_string.clone(), equal_atomic_fact.clone());
635 }
636 self.known_equality.insert(
637 key_in_class,
638 (direct_equality_proof_map, Rc::clone(&new_equiv_rc)),
639 );
640 }
641
642 let mut proof_for_new_left: HashMap<ObjString, AtomicFact> = HashMap::new();
643 proof_for_new_left.insert(right_as_string.clone(), equal_atomic_fact.clone());
644 self.known_equality
645 .insert(left_as_string, (proof_for_new_left, new_equiv_rc));
646 }
647 (None, None) => {
648 let equiv_members = vec![equality.left.clone(), equality.right.clone()];
649 let new_equiv_rc = Rc::new(equiv_members);
650
651 let mut left_direct_proof_map: HashMap<ObjString, AtomicFact> = HashMap::new();
652 left_direct_proof_map.insert(right_as_string.clone(), equal_atomic_fact.clone());
653
654 let mut right_direct_proof_map: HashMap<ObjString, AtomicFact> = HashMap::new();
655 right_direct_proof_map.insert(left_as_string.clone(), equal_atomic_fact);
656
657 self.known_equality.insert(
658 left_as_string.clone(),
659 (left_direct_proof_map, Rc::clone(&new_equiv_rc)),
660 );
661 self.known_equality
662 .insert(right_as_string, (right_direct_proof_map, new_equiv_rc));
663 }
664 }
665
666 if let Some(derived) =
667 super::equality_linear_derive::maybe_derived_linear_equal_fact(equality)
668 {
669 if derived.left.to_string() != derived.right.to_string() {
670 self.store_equality(&derived)?;
671 }
672 }
673 Ok(())
674 }
675}
676
677impl Environment {
678 pub fn new_empty_env() -> Self {
679 Environment::new(
680 HashMap::new(),
681 HashMap::new(),
682 HashMap::new(),
683 HashMap::new(),
684 HashMap::new(),
685 HashMap::new(),
686 HashMap::new(),
687 HashMap::new(),
688 HashMap::new(),
689 HashMap::new(),
690 HashMap::new(),
691 HashMap::new(),
692 HashMap::new(),
693 HashMap::new(),
694 HashMap::new(),
695 HashMap::new(),
696 HashMap::new(),
697 HashMap::new(),
698 HashMap::new(),
699 HashMap::new(),
700 HashMap::new(),
701 HashMap::new(),
702 HashMap::new(),
703 HashMap::new(),
704 )
705 }
706}
707
708impl Environment {
709 pub fn store_transitive_prop_name(&mut self, prop_name: String) {
710 self.known_transitive_props.insert(prop_name, ());
711 }
712
713 pub fn store_reflexive_prop_name(&mut self, prop_name: String) {
714 self.known_reflexive_props.insert(prop_name, ());
715 }
716
717 pub fn store_antisymmetric_prop_name(&mut self, prop_name: String) {
718 self.known_antisymmetric_props.insert(prop_name, ());
719 }
720
721 pub fn store_symmetric_prop_permutation(
722 &mut self,
723 prop_name: String,
724 gather: Vec<usize>,
725 line_file: LineFile,
726 ) -> Result<(), RuntimeError> {
727 let n = gather.len();
728 if n < 2 {
729 return Err(
730 StoreFactRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(
731 "store_symmetric_prop_permutation: arity must be at least 2".to_string(),
732 line_file,
733 ))
734 .into(),
735 );
736 }
737 if !symmetric_gather_is_valid_permutation(&gather, n) {
738 return Err(
739 StoreFactRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(
740 "store_symmetric_prop_permutation: gather is not a valid permutation"
741 .to_string(),
742 line_file,
743 ))
744 .into(),
745 );
746 }
747 if symmetric_gather_is_identity(&gather) {
748 return Err(
749 StoreFactRuntimeError(RuntimeErrorStruct::new_with_msg_and_line_file(
750 "store_symmetric_prop_permutation: identity permutation is not allowed"
751 .to_string(),
752 line_file,
753 ))
754 .into(),
755 );
756 }
757 if let Some(existing) = self.known_symmetric_props.get(&prop_name) {
758 if let Some(first) = existing.first() {
759 if first.len() != n {
760 return Err(StoreFactRuntimeError(
761 RuntimeErrorStruct::new_with_msg_and_line_file(
762 format!(
763 "store_symmetric_prop_permutation: `{}` already has arity {}, got {}",
764 prop_name,
765 first.len(),
766 n
767 ),
768 line_file,
769 ),
770 )
771 .into());
772 }
773 }
774 }
775 let entry = self
776 .known_symmetric_props
777 .entry(prop_name)
778 .or_insert_with(Vec::new);
779 if entry.iter().any(|g| g == &gather) {
780 return Ok(());
781 }
782 entry.push(gather);
783 Ok(())
784 }
785}
786
787impl Environment {
788 pub fn store_fact_to_cache_known_fact(
789 &mut self,
790 fact_key: FactString,
791 fact_line_file: LineFile,
792 ) -> Result<(), RuntimeError> {
793 self.cache_known_fact.insert(fact_key, fact_line_file);
794 Ok(())
795 }
796}
797
798pub struct KnownForallFactParamsAndDom {
799 pub params_def: ParamDefWithType,
800 pub dom: Vec<Fact>,
801 pub line_file: LineFile,
802}
803
804impl KnownForallFactParamsAndDom {
805 pub fn new(params: ParamDefWithType, dom: Vec<Fact>, line_file: LineFile) -> Self {
806 KnownForallFactParamsAndDom {
807 params_def: params,
808 dom,
809 line_file,
810 }
811 }
812}
813
814pub type SymmetricPropValue = Vec<Vec<usize>>;
815
816fn symmetric_gather_is_identity(gather: &[usize]) -> bool {
817 gather.iter().enumerate().all(|(i, &g)| g == i)
818}
819
820fn symmetric_gather_is_valid_permutation(gather: &[usize], n: usize) -> bool {
821 if gather.len() != n {
822 return false;
823 }
824 let mut seen = vec![false; n];
825 for &i in gather {
826 if i >= n {
827 return false;
828 }
829 if seen[i] {
830 return false;
831 }
832 seen[i] = true;
833 }
834 true
835}