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)
}