fn check_literal_equality()

in z3tracer/src/model.rs [749:783]

• 33 lines of code
• 10 McCabe index (conditional complexity)

    fn check_literal_equality(
        &self,
        eid: &Ident,
        id1: &Ident,
        id2: &Ident,
    ) -> RawResult<Option<usize>> {
        let term = self.term(eid)?;
        let assignment = self.term_assignment(eid);
        // Normal case.
        if let Some([eid1, eid2]) = term.matches_equality() {
            let proof = self.term_proof(eid);
            let scope_index = maybe_index_min(
                proof.map(|p| p.scope_index),
                assignment.map(|p| p.scope_index),
            );
            if scope_index.is_none() {
                return Err(RawError::MissingProof(eid.clone()));
            }
            if (&eid1 == id1 && &eid2 == id2) || (&eid1 == id2 && &eid2 == id1) {
                return Ok(scope_index);
            }
        }
        // Assigned term.
        if eid == id1 {
            match (assignment, self.term(id2)?) {
                (Some(assignment), Term::App { name, args, .. })
                    if args.is_empty() && assignment.as_str() == name.as_str() =>
                {
                    return Ok(Some(assignment.scope_index));
                }
                _ => (),
            }
        }
        Ok(None)
    }