fn term_equality_class()

in z3tracer/src/model.rs [340:370]

• 31 lines of code
• 5 McCabe index (conditional complexity)

    fn term_equality_class(&mut self, id: &Ident) -> Ident {
        // Query and consolidate the equality class of id.
        let data = self.scoped_term_data(id);
        if data.eq_class.is_none() {
            // id is a root but somehow we never queried its class (until now).
            self.scoped_term_data_mut(id).eq_class = Some(id.clone());
            return id.clone();
        }
        let cid = data.eq_class.clone().unwrap();
        if &cid == id {
            // id == cid is still a root.
            return cid;
        }
        // Since cid != id, we have to check if cid is still a class root.
        let new_cid = self.term_equality_class(&cid);
        if new_cid == cid {
            // cid is still a root.
            return cid;
        }
        // cid is no longer a root. Need to update the entry of id and
        // re-import deps from cid.
        let cdata = self.scoped_term_data(&cid);
        let c_qi_deps = cdata.qi_deps.clone();
        let c_proof_deps = cdata.proof_deps.clone();
        self.current_scope.needs_consolidation = true;
        let data = self.scoped_term_data_mut(id);
        data.eq_class = Some(new_cid.clone());
        data.qi_deps.extend(c_qi_deps);
        data.proof_deps.extend(c_proof_deps);
        new_cid
    }