in amzn-smt-ir/src/logic/bitvecs.rs [108:172]
fn sort(&self, ctx: &mut Ctx) -> Result<ISort, UnknownSort<Term<L>>> {
use BvOp::*;
let unknown = || UnknownSort(Term::from(self.clone()));
macro_rules! bvwidth {
($sort:expr) => {
$sort.bv_width().ok_or_else(unknown)
};
}
Ok(match self {
Concat(l, r) => {
let (l, r) = (l.sort(ctx)?, r.sort(ctx)?);
let (i, j) = (bvwidth!(&l)?, bvwidth!(&r)?);
ISort::bitvec(i + j)
}
Extract([i, j], _) => match (i.as_ref(), j.as_ref()) {
(Index::Numeral(i), Index::Numeral(j)) => ISort::bitvec(Numeral::one() + i - j),
_ => return Err(unknown()),
},
BvNot(arg) | BvNeg(arg) => arg.sort(ctx)?,
BvAnd(args) | BvOr(args) | BvAdd(args) | BvMul(args) | BvXor(args) => {
let sort = args.first().ok_or_else(unknown)?.sort(ctx)?;
#[cfg(debug_assertions)]
for arg in args.iter().skip(1) {
assert_eq!(arg.sort(ctx)?, sort);
}
sort
}
BvUdiv(l, r)
| BvUrem(l, r)
| BvShl(l, r)
| BvLshr(l, r)
| BvNand(l, r)
| BvNor(l, r)
| BvXnor(l, r)
| BvSub(l, r)
| BvSdiv(l, r)
| BvSrem(l, r)
| BvSmod(l, r)
| BvAshr(l, r) => {
let sort = l.sort(ctx)?;
debug_assert_eq!(r.sort(ctx)?, sort);
sort
}
BvUlt(..) | BvUle(..) | BvUgt(..) | BvUge(..) | BvSlt(..) | BvSle(..) | BvSgt(..)
| BvSge(..) => ISort::bool(),
BvComp(..) => ISort::bitvec(Numeral::one()),
Repeat([i], arg) => match i.as_ref() {
Index::Numeral(i) => {
let sort = arg.sort(ctx)?;
ISort::bitvec(i * bvwidth!(&sort)?)
}
_ => return Err(unknown()),
},
ZeroExtend([i], arg) | SignExtend([i], arg) => match i.as_ref() {
Index::Numeral(i) => {
let sort = arg.sort(ctx)?;
ISort::bitvec(i + bvwidth!(&sort)?)
}
_ => return Err(unknown()),
},
RotateLeft(_, arg) | RotateRight(_, arg) => arg.sort(ctx)?,
})
}