fn fold_theory_op()

in amzn-smt-eager-arithmetic/src/encoding.rs [94:146]

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

    fn fold_theory_op(&mut self, op: IOp<ALL>) -> Result<Term<Self::U>, Self::Error> {
        use ArithOp::*;
        use BvOp::*;
        use Op::*;

        Ok(match op.as_ref() {
            Arith(Plus(args)) => (args.fold_with(self)?.into_iter().map(Ok))
                .reduce(|l, r| self.encode_plus(l?, r?))
                .transpose()?
                .unwrap_or_else(|| Constant::Numeral(0u8.into()).into()),
            Arith(Minus(args)) => (args.fold_with(self)?.into_iter().map(Ok))
                .reduce(|l, r| self.encode_minus(l?, r?))
                .transpose()?
                .unwrap_or_else(|| Constant::Numeral(0u8.into()).into()),
            Arith(Neg(arg)) => {
                let arg = arg.fold_with(self)?;
                self.encode_neg(arg)?
            }
            Arith(Gte(args)) => try_chained(args.fold_with(self)?, |l, r| self.encode_gte(l, r))?,
            Arith(Gt(args)) => try_chained(args.fold_with(self)?, |l, r| {
                self.encode_gte(r, l).map(|t| !t)
            })?,
            Arith(Lte(args)) => try_chained(args.fold_with(self)?, |l, r| self.encode_gte(r, l))?,
            BitVec(BvUle(l, r)) => {
                let (l, r) = (l, r).fold_with(self)?;
                self.encode_bvuge(r, l)?
            }
            Arith(Lt(args)) => try_chained(args.fold_with(self)?, |l, r| {
                self.encode_gte(l, r).map(|t| !t)
            })?,
            Arith(Mul(args)) => match args.as_slice() {
                [c, x] => {
                    let z = Constant::Numeral(Numeral::zero()).into();
                    if c.is_zero() {
                        z
                    } else {
                        let x = x.fold_with(self)?;
                        let (c, pos) = int_term(c)
                            .expect("canonicalization produced malformed multiplication");
                        let c = c.to_usize().unwrap();
                        let sum = (0..c).try_fold(z, |acc, _| self.encode_plus(acc, x.clone()))?;
                        if pos {
                            sum
                        } else {
                            self.encode_neg(sum)?
                        }
                    }
                }
                _ => panic!("canonicalization produced malformed multiplication"),
            },
            op => bail!("unsupported function: {}", op),
        })
    }