fn sort()

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