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