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

    import SMTLib2.AST

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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