fn fold_core_op()

in amzn-smt-eager-arithmetic/src/canonicalize.rs [221:277]

• 56 lines of code
• 6 McCabe index (conditional complexity)

    fn fold_core_op(&mut self, op: ICoreOp<ALL>) -> Result<Term, Self::Error> {
        let implies = |a: Term, b: Term| CoreOp::Imp([a, b].into()).into();
        Ok(match op.super_fold_with(self)? {
            CoreOp::Eq(args) => {
                let sort = (args.first())
                    .ok_or_else(|| UnknownSort(CoreOp::Eq(args.clone()).into()))
                    .and_then(|arg| arg.sort(self.context));
                if sort == Ok(ISort::int()) {
                    chained(args, |l, r| {
                        let (l, r) = Self::normalize_constraint(l, r);
                        CoreOp::Eq([l, r].into()).into()
                    })
                } else {
                    CoreOp::Eq(args).into()
                }
            }
            // TODO: can the bound be computed with `ite` and `distinct` applications left as-is?
            CoreOp::Ite(cond, consq, alt) => {
                let sort = consq.sort(self.context)?;
                debug_assert_eq!(
                    alt.sort(self.context)?,
                    sort,
                    "ite branches are of different sorts"
                );
                if sort == ISort::int() {
                    let res = Term::from(self.context.fresh_var(sort)?);
                    let if_true = {
                        let (l, r) = Self::normalize_constraint(res.clone(), consq);
                        CoreOp::Eq([l, r].into()).into()
                    };
                    self.new_asserts.push(implies(cond.clone(), if_true));
                    let if_false = {
                        let (l, r) = Self::normalize_constraint(res.clone(), alt);
                        CoreOp::Eq([l, r].into()).into()
                    };
                    self.new_asserts.push(implies(!cond, if_false));
                    res
                } else {
                    implies(cond.clone(), consq) & implies(!cond, alt)
                }
            }
            CoreOp::Distinct(args) => {
                let sort = (args.first())
                    .ok_or_else(|| UnknownSort(CoreOp::Distinct(args.clone()).into()))
                    .and_then(|arg| arg.sort(self.context));
                if sort == Ok(ISort::int()) {
                    pairwise(&args, |x, y| {
                        let (l, r) = Self::normalize_constraint(x, y);
                        !Term::from(CoreOp::Eq([l, r].into()))
                    })
                } else {
                    CoreOp::Distinct(args).into()
                }
            }
            op => op.into(),
        })
    }