fn make_terms_equal()

in z3tracer/src/model.rs [630:668]

• 39 lines of code
• 2 McCabe index (conditional complexity)

    fn make_terms_equal(
        &mut self,
        id0: &Ident,
        id1: &Ident,
        ext_qi_deps: &[QiRef],
        ext_proof_deps: &[ProofRef],
    ) -> Ident {
        let cid0 = self.term_equality_class(id0);
        let cid1 = self.term_equality_class(id1);
        use std::cmp::Ordering::*;
        let (id0, cid0, id1, cid1) = match cid0.cmp(&cid1) {
            Equal => {
                return cid1;
            }
            // Use the older term as class root.
            Less => (id1, cid1, id0, cid0),
            Greater => (id0, cid0, id1, cid1),
        };
        // Need to update the entry of cid0 and re-import deps from
        // id1.
        let cdata = self.scoped_term_data(id1);
        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(&cid0);
        data.eq_class = Some(cid1.clone());
        data.qi_deps.extend(c_qi_deps);
        data.proof_deps.extend(c_proof_deps);
        // Adding external deps as well.
        data.qi_deps.extend(ext_qi_deps.iter().cloned());
        data.proof_deps.extend(ext_proof_deps.iter().cloned());
        if self.config.log_internal_term_equalities {
            eprintln!(
                "{}: @{} {:?} -> {:?} ==> {:?} <- {:?}",
                self.processed_logs, self.current_scope.level, id0, cid0, cid1, id1
            );
        }
        cid1
    }