fn determine_special_case()

in amzn-smt-eager-arithmetic/src/stats.rs [65:119]

• 48 lines of code
• 8 McCabe index (conditional complexity)

    fn determine_special_case(&self) -> SpecialCase {
        use ArithOp::*;
        use Op::*;

        let (mut k, mut equality_logic) = (0, self.mu_b.is_zero());
        let bad = || {
            unreachable!(
                "only terms of the form `({<=,<,=,>=,>} (+ ...) ...)` are added to constraints"
            )
        };
        for t in self.constraints.iter() {
            if !matches!(t, Term::CoreOp(op) if matches!(op.as_ref(), CoreOp::Eq(..))) {
                equality_logic = false;
            }
            let args = match t {
                Term::CoreOp(op) => match op.as_ref() {
                    CoreOp::Eq(args) => args,
                    _ => bad(),
                },
                Term::OtherOp(op) => match op.as_ref() {
                    Arith(Gte(args) | Gt(args) | Lte(args) | Lt(args)) => args,
                    _ => bad(),
                },
                _ => bad(),
            };
            let lhs = match args.first() {
                Some(Term::OtherOp(op)) => match op.as_ref() {
                    Arith(Plus(args)) => args.as_slice(),
                    _ => bad(),
                },
                _ => bad(),
            };
            // Check if this is the LHS of a separation constraint (SC)
            match lhs {
                // x >= c (SC)
                [Term::Variable(_)] => {}
                // -x >= c === x <= -c (SC)
                [Term::OtherOp(op)]
                // x - y >= c (SC)
                | [Term::Variable(_), Term::OtherOp(op)]
                // y - x >= c (SC)
                | [Term::OtherOp(op), Term::Variable(_)]
                    if matches!(op.as_ref(), Arith(Neg(Term::Variable(_)))) => {}
                // Not a separation constraint
                _ => {
                    k += 1;
                }
            }
        }
        match NonZeroU32::new(k) {
            Some(k) => SpecialCase::None { k },
            None if equality_logic => SpecialCase::EqualityLogic,
            None => SpecialCase::SeparationLogic,
        }
    }