fn fold_core_op()

in amzn-smt-ir/src/cnf.rs [330:417]

• 85 lines of code
• 4 McCabe index (conditional complexity)

    fn fold_core_op(&mut self, op: ICoreOp<T>) -> Result<Self::Output, Self::Error> {
        if let Some(out) = self.cache.get(&op) {
            return Ok(*out);
        }

        use CoreOp::*;

        let encoded = match op.as_ref() {
            True => {
                let v = Literal::t(self.gen_var());
                self.clauses.push(clause![v]);
                v
            }
            False => {
                let v = Literal::t(self.gen_var());
                self.clauses.push(clause![!v]);
                v
            }
            Not(arg) => {
                let mut standard = || -> Result<_, Self::Error> {
                    let arg = arg.fold_with(self)?;
                    Ok(!arg)
                };
                if let Term::CoreOp(op) = arg {
                    match op.as_ref() {
                        CoreOp::Not(t) => t.fold_with(self)?,
                        CoreOp::And(args) => {
                            let args = args.fold_with(self)?;
                            self.nand(&args)
                        }
                        CoreOp::Or(args) => {
                            let args = args.fold_with(self)?;
                            self.nor(&args)
                        }
                        CoreOp::Xor(args) => {
                            let args = args.fold_with(self)?;
                            self.xnor(args)
                        }
                        _ => standard()?,
                    }
                } else {
                    standard()?
                }
            }
            And(args) => {
                let args = args.fold_with(self)?;
                self.and(&args)
            }
            Or(args) => {
                let args = args.fold_with(self)?;
                self.or(&args)
            }
            Xor(args) => {
                let args = args.fold_with(self)?;
                self.xor(args)
            }
            Imp(args) => {
                let args = args.fold_with(self)?;
                self.imp(args)
            }
            Eq(args) => {
                let args = args.fold_with(self)?;
                self.eq(args)
            }
            Distinct(args) => {
                let args = args.fold_with(self)?;
                let constraints: Vec<_> = args
                    .into_iter()
                    .tuple_combinations()
                    .map(|(a, b)| self.xor([a, b]))
                    .collect();
                self.and(&constraints)
            }
            Ite(i, consq, alt) => {
                let (i, consq, alt) = (
                    i.fold_with(self)?,
                    consq.fold_with(self)?,
                    alt.fold_with(self)?,
                );
                let true_constraint = self.imp([i, consq]);
                let false_constraint = self.imp([!i, alt]);
                self.and(&[true_constraint, false_constraint])
            }
        };

        self.cache.insert(op, encoded);
        Ok(encoded)
    }