fn encode_plus()

in amzn-smt-eager-arithmetic/src/encoding.rs [391:421]


    fn encode_plus(&mut self, l: Reduced, r: Reduced) -> anyhow::Result<Reduced> {
        if l.is_zero() {
            return Ok(r);
        } else if r.is_zero() {
            return Ok(l);
        }

        let op = BasicOp::Plus(l.clone(), r.clone());
        let cache = &self.encoded;
        if let Some(encoded) =
            (cache.get(&op)).or_else(|| cache.get(&BasicOp::Plus(r.clone(), l.clone())))
        {
            return Ok(encoded.clone());
        }

        let encoded = encode_bitwise_op!(
            self,
            &l,
            &r,
            |l, r| self.encode_plus_bitwise(l.map_into(), r.map_into(), false.into()),
            |l, r| if let (Constant::Numeral(l), Constant::Numeral(r)) = (l, r) {
                Constant::Numeral(l + r).into()
            } else {
                bail!("non-integer constants passed to '+'")
            }
        )
        .with_context(|| format!("failed to encode op: (+ {} {})", l, r))?;

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