    {-# LANGUAGE OverloadedStrings, Safe #-}
    module SMTLib2.BitVector where

    import SMTLib2.AST

    tBitVec :: Integer -> Type
    tBitVec :: Integer -> Type
    tBitVec n :: Integer
    n = Ident -> [Type] -> Type
    TApp (Name -> [Integer] -> Ident
    I "BitVec" [Integer
    n]) []

    bv :: Integer -> Integer -> Expr
    bv :: Integer -> Integer -> Expr
    bv num :: Integer
    num w :: Integer
    w = Literal -> Expr
    Lit (Integer -> Integer -> Literal
    LitBV Integer
    num Integer
    w)

    concat :: Expr -> Expr -> Expr
    concat :: Expr -> Expr -> Expr
    concat x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "concat" [Expr
    x,Expr
    y]

    extract :: Integer -> Integer -> Expr -> Expr
    extract :: Integer -> Integer -> Expr -> Expr
    extract i :: Integer
    i j :: Integer
    j x :: Expr
    x = Ident -> [Expr] -> Expr
    app (Name -> [Integer] -> Ident
    I "extract" [Integer
    i,Integer
    j]) [Expr
    x]

    bvnot :: Expr -> Expr
    bvnot :: Expr -> Expr
    bvnot x :: Expr
    x = Ident -> [Expr] -> Expr
    app "bvnot" [Expr
    x]

    bvand :: Expr -> Expr -> Expr
    bvand :: Expr -> Expr -> Expr
    bvand x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvand" [Expr
    x,Expr
    y]

    bvor :: Expr -> Expr -> Expr
    bvor :: Expr -> Expr -> Expr
    bvor x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvor" [Expr
    x,Expr
    y]

    bvneg :: Expr -> Expr
    bvneg :: Expr -> Expr
    bvneg x :: Expr
    x = Ident -> [Expr] -> Expr
    app "bvneg" [Expr
    x]

    bvadd :: Expr -> Expr -> Expr
    bvadd :: Expr -> Expr -> Expr
    bvadd x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvadd" [Expr
    x,Expr
    y]

    bvmul :: Expr -> Expr -> Expr
    bvmul :: Expr -> Expr -> Expr
    bvmul x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvmul" [Expr
    x,Expr
    y]

    bvudiv :: Expr -> Expr -> Expr
    bvudiv :: Expr -> Expr -> Expr
    bvudiv x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvudiv" [Expr
    x,Expr
    y]

    bvurem :: Expr -> Expr -> Expr
    bvurem :: Expr -> Expr -> Expr
    bvurem x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvurem" [Expr
    x,Expr
    y]

    bvshl :: Expr -> Expr -> Expr
    bvshl :: Expr -> Expr -> Expr
    bvshl x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvshl" [Expr
    x,Expr
    y]

    bvlshr :: Expr -> Expr -> Expr
    bvlshr :: Expr -> Expr -> Expr
    bvlshr x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvlshr" [Expr
    x,Expr
    y]

    bvult :: Expr -> Expr -> Expr
    bvult :: Expr -> Expr -> Expr
    bvult x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvult" [Expr
    x,Expr
    y]

    bvnand :: Expr -> Expr -> Expr
    bvnand :: Expr -> Expr -> Expr
    bvnand x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvnand" [Expr
    x,Expr
    y]

    bvnor :: Expr -> Expr -> Expr
    bvnor :: Expr -> Expr -> Expr
    bvnor x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvnor" [Expr
    x,Expr
    y]

    bvxor :: Expr -> Expr -> Expr
    bvxor :: Expr -> Expr -> Expr
    bvxor x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvxor" [Expr
    x,Expr
    y]

    bvxnor :: Expr -> Expr -> Expr
    bvxnor :: Expr -> Expr -> Expr
    bvxnor x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvxnor" [Expr
    x,Expr
    y]

    bvcomp :: Expr -> Expr -> Expr
    bvcomp :: Expr -> Expr -> Expr
    bvcomp x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvcomp" [Expr
    x,Expr
    y]

    bvsub :: Expr -> Expr -> Expr
    bvsub :: Expr -> Expr -> Expr
    bvsub x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvsub" [Expr
    x,Expr
    y]

    bvsdiv :: Expr -> Expr -> Expr
    bvsdiv :: Expr -> Expr -> Expr
    bvsdiv x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvsdiv" [Expr
    x,Expr
    y]

    bvsrem :: Expr -> Expr -> Expr
    bvsrem :: Expr -> Expr -> Expr
    bvsrem x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvsrem" [Expr
    x,Expr
    y]

    bvsmod :: Expr -> Expr -> Expr
    bvsmod :: Expr -> Expr -> Expr
    bvsmod x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvsmod" [Expr
    x,Expr
    y]

    bvashr :: Expr -> Expr -> Expr
    bvashr :: Expr -> Expr -> Expr
    bvashr x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvashr" [Expr
    x,Expr
    y]

    repeat :: Integer -> Expr -> Expr -> Expr
    repeat :: Integer -> Expr -> Expr -> Expr
    repeat i :: Integer
    i x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app (Name -> [Integer] -> Ident
    I "repeat" [Integer
    i]) [Expr
    x,Expr
    y]

    zero_extend :: Integer -> Expr -> Expr
    zero_extend :: Integer -> Expr -> Expr
    zero_extend i :: Integer
    i x :: Expr
    x = Ident -> [Expr] -> Expr
    app (Name -> [Integer] -> Ident
    I "zero_extend" [Integer
    i]) [Expr
    x]

    sign_extend :: Integer -> Expr -> Expr
    sign_extend :: Integer -> Expr -> Expr
    sign_extend i :: Integer
    i x :: Expr
    x = Ident -> [Expr] -> Expr
    app (Name -> [Integer] -> Ident
    I "sign_extend" [Integer
    i]) [Expr
    x]

    rotate_left :: Integer -> Expr -> Expr
    rotate_left :: Integer -> Expr -> Expr
    rotate_left i :: Integer
    i x :: Expr
    x = Ident -> [Expr] -> Expr
    app (Name -> [Integer] -> Ident
    I "rotate_left" [Integer
    i]) [Expr
    x]

    rotate_right :: Integer -> Expr -> Expr
    rotate_right :: Integer -> Expr -> Expr
    rotate_right i :: Integer
    i x :: Expr
    x = Ident -> [Expr] -> Expr
    app (Name -> [Integer] -> Ident
    I "rotate_right" [Integer
    i]) [Expr
    x]

    bvule :: Expr -> Expr -> Expr
    bvule :: Expr -> Expr -> Expr
    bvule x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvule" [Expr
    x,Expr
    y]

    bvugt :: Expr -> Expr -> Expr
    bvugt :: Expr -> Expr -> Expr
    bvugt x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvugt" [Expr
    x,Expr
    y]

    bvuge :: Expr -> Expr -> Expr
    bvuge :: Expr -> Expr -> Expr
    bvuge x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvuge" [Expr
    x,Expr
    y]

    bvslt :: Expr -> Expr -> Expr
    bvslt :: Expr -> Expr -> Expr
    bvslt x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvslt" [Expr
    x,Expr
    y]

    bvsle :: Expr -> Expr -> Expr
    bvsle :: Expr -> Expr -> Expr
    bvsle x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvsle" [Expr
    x,Expr
    y]

    bvsgt :: Expr -> Expr -> Expr
    bvsgt :: Expr -> Expr -> Expr
    bvsgt x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvsgt" [Expr
    x,Expr
    y]

    bvsge :: Expr -> Expr -> Expr
    bvsge :: Expr -> Expr -> Expr
    bvsge x :: Expr
    x y :: Expr
    y = Ident -> [Expr] -> Expr
    app "bvsge" [Expr
    x,Expr
    y]