fn adder()

in amzn-smt-eager-arithmetic/src/encoding.rs [605:646]

• 42 lines of code
• 13 McCabe index (conditional complexity)

fn adder(x: Reduced, y: Reduced, carry_in: Reduced) -> (Reduced, Reduced) {
    match (carry_in.const_bool(), x.const_bool(), y.const_bool()) {
        (Ok(cin), Ok(x), Ok(y)) => {
            let s = x ^ y ^ cin;
            let cout = (x && y) || (x && cin) || (y && cin);
            (s.into(), cout.into())
        }
        (Ok(x), Ok(y), Err(a)) | (Ok(x), Err(a), Ok(y)) | (Err(a), Ok(x), Ok(y)) => {
            let s = if x ^ y { !a.clone() } else { a.clone() };
            let cout = if x && y {
                true.into()
            } else if x || y {
                a.clone()
            } else {
                false.into()
            };
            (s, cout)
        }
        (Ok(x), Err(a), Err(b)) | (Err(a), Ok(x), Err(b)) | (Err(a), Err(b), Ok(x)) => {
            let s = if x {
                !(a.clone() ^ b.clone())
            } else {
                a.clone() ^ b.clone()
            };
            let cout = if x {
                a.clone() | b.clone()
            } else {
                a.clone() & b.clone()
            };
            (s, cout)
        }
        (Err(_), Err(_), Err(_)) => {
            let s = CoreOp::Xor(args![x.clone(), y.clone(), carry_in.clone()]).into();
            let cout = CoreOp::Or(args![
                x.clone() & y.clone(),
                x & carry_in.clone(),
                y & carry_in,
            ]);
            (s, cout.into())
        }
    }
}