slotted_egraphs/explain/
mod.rs

1use crate::*;
2
3#[cfg(feature = "explanations")]
4mod proof;
5#[cfg(feature = "explanations")]
6pub use proof::*;
7
8#[cfg(feature = "explanations")]
9mod flat;
10#[cfg(feature = "explanations")]
11pub use flat::*;
12
13#[cfg(feature = "explanations")]
14mod front;
15#[cfg(feature = "explanations")]
16pub use front::*;
17
18#[cfg(feature = "explanations")]
19mod registry;
20#[cfg(feature = "explanations")]
21pub use registry::*;
22
23mod wrapper;
24pub use wrapper::*;
25
26#[cfg(feature = "explanations")]
27mod show;
28#[cfg(feature = "explanations")]
29pub use show::*;
30
31#[cfg(not(feature = "explanations"))]
32mod mock;
33#[cfg(not(feature = "explanations"))]
34pub use mock::*;
35
36#[cfg(feature = "explanations")]
37impl<L: Language, N: Analysis<L>> EGraph<L, N> {
38    pub fn explain_equivalence(&mut self, t1: RecExpr<L>, t2: RecExpr<L>) -> ProvenEq {
39        let i1 = self.add_syn_expr(t1);
40        let i2 = self.add_syn_expr(t2);
41
42        if !self.eq(&i1, &i2) {
43            panic!("Can't explain an equivalence that does not hold!");
44        }
45
46        let pai1 = self.proven_find_applied_id(&i1);
47        let ProvenAppliedId { elem: l1, proof: _ } = &pai1;
48
49        let pai2 = self.proven_find_applied_id(&i2);
50        let ProvenAppliedId {
51            elem: l2,
52            proof: prf2,
53        } = &pai2;
54
55        if CHECKS {
56            assert_eq!(l1.id, l2.id);
57        }
58        let id = l1.id;
59
60        let bij = l2.m.compose(&l1.m.inverse());
61        let symmetry_prf = &self.classes[&id].group.proven_contains(&bij).unwrap();
62        let ProvenAppliedId {
63            elem: _,
64            proof: prf1,
65        } = self.chain_pai_pp(&pai1, symmetry_prf);
66
67        let prf2 = self.prove_symmetry(prf2.clone());
68
69        let final_eq = Equation { l: i1, r: i2 };
70        let p = TransitivityProof(prf1, prf2.clone()).check(&final_eq, &self.proof_registry);
71
72        if CHECKS {
73            assert_proves_equation(&p, &final_eq);
74        }
75
76        p
77    }
78}
slotted_egraphs/explain/mod.rs

slotted_egraphs/explain/
mod.rs
