// add_match uses the memo in order to re-discover matches
// given a substitution.
// This requires that congruence has been restored and the memo is up to date.
add_match uses the memo in order to re-discover matches
given a substitution.
This requires that congruence has been restored and the memo is up to date.
add_match uses the memo in order to re - discover matches given a substitution . This requires that congruence has been restored and the memo is up to date .
pub(crate) fn add_match(
        &mut self,
        pattern: &PatternAst<L>,
        subst: &Subst,
        memo: &HashMap<L, Id>,
        unionfind: &mut UnionFind,
    ) -> Id {
        let nodes = pattern.as_ref().as_ref();
        let mut new_ids = Vec::with_capacity(nodes.len());
        let mut match_ids = Vec::with_capacity(nodes.len());
        for node in nodes {
            match node {
                ENodeOrVar::Var(var) => {
                    let bottom_id = unionfind.find(subst[*var]);
                    new_ids.push(unionfind.find(bottom_id));
                    match_ids.push(bottom_id);
                }
                ENodeOrVar::ENode(pattern_node) => {
                    let node = pattern_node
                        .clone()
                        .map_children(|i| new_ids[usize::from(i)]);
                    let new_congruent_node = pattern_node
                        .clone()
                        .map_children(|i| match_ids[usize::from(i)]);
                    if let Some(existing_id) = self.uncanon_memo.get(&new_congruent_node) {
                        new_ids.push(unionfind.find(*existing_id));
                        match_ids.push(*existing_id);
                    } else {
                        let congruent_id = *memo.get(&node).unwrap_or_else(|| {
                            panic!("Internal error! Pattern did not exist for substitution.");
                        });
                        let congruent_class = unionfind.find(congruent_id);
                        new_ids.push(congruent_class);
                        assert!(
                            node == self.explainfind[usize::from(congruent_id)]
                                .node
                                .clone()
                                .map_children(|id| unionfind.find(id))
                        );
                        let new_congruent_id =
                            self.add(new_congruent_node, unionfind.make_set(), congruent_id);
                        match_ids.push(new_congruent_id);
                        // make the congruent_id we found the leader
                        unionfind.union(congruent_class, new_congruent_id);
                        self.union(
                            new_congruent_id,
                            congruent_id,
                            Justification::Congruence,
                            false,
                        );
                    }
                }
            }
        }
        let last_id = *match_ids.last().unwrap();
        last_id
    }
pub ( crate ) fn add_match ( & mut self , pattern : & PatternAst < L > , subst : & Subst , memo : & HashMap < L , Id > , unionfind : & mut UnionFind , ) -> Id { let nodes = pattern . as_ref ( ) . as_ref ( ) ; let mut new_ids = Vec :: with_capacity ( nodes . len ( ) ) ; let mut match_ids = Vec :: with_capacity ( nodes . len ( ) ) ; for node in nodes { match node { ENodeOrVar :: Var ( var ) => { let bottom_id = unionfind . find ( subst [ * var ] ) ; new_ids . push ( unionfind . find ( bottom_id ) ) ; match_ids . push ( bottom_id ) ; } ENodeOrVar :: ENode ( pattern_node ) => { let node = pattern_node . clone ( ) . map_children ( | i | new_ids [ usize :: from ( i ) ] ) ; let new_congruent_node = pattern_node . clone ( ) . map_children ( | i | match_ids [ usize :: from ( i ) ] ) ; if let Some ( existing_id ) = self . uncanon_memo . get ( & new_congruent_node ) { new_ids . push ( unionfind . find ( * existing_id ) ) ; match_ids . push ( * existing_id ) ; } else { let congruent_id = * memo . get ( & node ) . unwrap_or_else ( | | { panic ! ( " " ) ; } ) ; let congruent_class = unionfind . find ( congruent_id ) ; new_ids . push ( congruent_class ) ; assert ! ( node self explainfind [ usize from ( congruent_id ) ] node clone ( ) map_children ( id unionfind find ( id ) ) ) ; let new_congruent_id = self . add ( new_congruent_node , unionfind . make_set ( ) , congruent_id ) ; match_ids . push ( new_congruent_id ) ; // make the congruent_id we found the leader unionfind . union ( congruent_class , new_congruent_id ) ; self . union ( new_congruent_id , congruent_id , Justification :: Congruence , false , ) ; } } } } let last_id = * match_ids . last ( ) . unwrap ( ) ; last_id }
add_match uses the memo in order to re-discover matches
given a substitution.
add_match uses the memo in order to re - discover matches given a substitution .
&mut self
pattern
&PatternAst<L>
subst
&Subst
memo
&HashMap<L, Id>
unionfind
&mut UnionFind