    {-# LANGUAGE OverloadedStrings, Safe #-}
    module SMTLib1.QF_BV (module X, module SMTLib1.QF_BV) where

    import SMTLib1 as X
    import Data.String(IsString(..))

    tBitVec :: Integer -> Sort
    tBitVec :: Integer -> Ident
    tBitVec Integer
    n = Name -> [Integer] -> Ident
    I Name
    "BitVec" [Integer
    n]

    isBitVec :: Sort -> Maybe Integer
    isBitVec :: Ident -> Maybe Integer
    isBitVec (I Name
    "BitVec" [Integer
    n]) = Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    n
    isBitVec Ident
    _                = Maybe Integer
    forall a. Maybe a
    Nothing

    -- | BitVec[1]
    bit0 :: Term
    bit0 :: Term
    bit0 = Ident -> [Term] -> Term
    App Ident
    "bit0" []

    -- | BitVec[1]
    bit1 :: Term
    bit1 :: Term
    bit1 = Ident -> [Term] -> Term
    App Ident
    "bit1" []

    -- | [m] -> [n] -> [m+n]
    concat :: Term -> Term -> Term
    concat :: Term -> Term -> Term
    concat Term
    x Term
    y = Ident -> [Term] -> Term
    App Ident
    "concat" [Term
    x,Term
    y]

    extract :: Integer -> Integer -> Term -> Term
    extract :: Integer -> Integer -> Term -> Term
    extract Integer
    i Integer
    j Term
    t = Ident -> [Term] -> Term
    App (Name -> [Integer] -> Ident
    I Name
    "extract" [Integer
    i,Integer
    j]) [Term
    t]

    bvnot :: Term -> Term
    bvnot :: Term -> Term
    bvnot Term
    t = Ident -> [Term] -> Term
    App Ident
    "bvnot" [Term
    t]

    bvand :: Term -> Term -> Term
    bvand :: Term -> Term -> Term
    bvand Term
    s Term
    t = Ident -> [Term] -> Term
    App Ident
    "bvand" [Term
    s,Term
    t]

    bvor :: Term -> Term -> Term
    bvor :: Term -> Term -> Term
    bvor Term
    s Term
    t = Ident -> [Term] -> Term
    App Ident
    "bvor" [Term
    s,Term
    t]

    bvneg :: Term -> Term
    bvneg :: Term -> Term
    bvneg Term
    t  = Ident -> [Term] -> Term
    App Ident
    "bvneg" [Term
    t]

    bvadd :: Term -> Term -> Term
    bvadd :: Term -> Term -> Term
    bvadd Term
    s Term
    t = Ident -> [Term] -> Term
    App Ident
    "bvadd" [Term
    s,Term
    t]

    bvmul :: Term -> Term -> Term
    bvmul :: Term -> Term -> Term
    bvmul Term
    s Term
    t = Ident -> [Term] -> Term
    App Ident
    "bvmul" [Term
    s,Term
    t]

    bvudiv :: Term -> Term -> Term
    bvudiv :: Term -> Term -> Term
    bvudiv Term
    s Term
    t = Ident -> [Term] -> Term
    App Ident
    "bvudiv" [Term
    s,Term
    t]

    bvurem :: Term -> Term -> Term
    bvurem :: Term -> Term -> Term
    bvurem Term
    s Term
    t = Ident -> [Term] -> Term
    App Ident
    "bvurem" [Term
    s,Term
    t]

    bvshl :: Term -> Term -> Term
    bvshl :: Term -> Term -> Term
    bvshl Term
    s Term
    t = Ident -> [Term] -> Term
    App Ident
    "bvshl" [Term
    s,Term
    t]

    bvlshr :: Term -> Term -> Term
    bvlshr :: Term -> Term -> Term
    bvlshr Term
    s Term
    t = Ident -> [Term] -> Term
    App Ident
    "bvlshr" [Term
    s,Term
    t]

    bv :: Integer -> Integer -> Term
    bv :: Integer -> Integer -> Term
    bv Integer
    x Integer
    m = if Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    0 then Integer -> Term
    forall {a}. Show a => a -> Term
    lit Integer
    x else Term -> Term
    bvneg (Integer -> Term
    forall {a}. Show a => a -> Term
    lit (Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    x))
      where lit :: a -> Term
    lit a
    y = Ident -> [Term] -> Term
    App (Name -> [Integer] -> Ident
    I ([Char] -> Name
    forall a. IsString a => [Char] -> a
    fromString ([Char]
    "bv" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ a -> [Char]
    forall a. Show a => a -> [Char]
    show a
    y)) [Integer
    m]) []

    bvnand :: Term -> Term -> Term
    bvnand :: Term -> Term -> Term
    bvnand Term
    s Term
    t = Ident -> [Term] -> Term
    App Ident
    "bvnand" [Term
    s,Term
    t]

    bvnor :: Term -> Term -> Term
    bvnor :: Term -> Term -> Term
    bvnor Term
    s Term
    t = Ident -> [Term] -> Term
    App Ident
    "bvnor" [Term
    s,Term
    t]

    bvxor :: Term -> Term -> Term
    bvxor :: Term -> Term -> Term
    bvxor Term
    s Term
    t = Ident -> [Term] -> Term
    App Ident
    "bvxor" [Term
    s,Term
    t]

    bvxnor :: Term -> Term -> Term
    bvxnor :: Term -> Term -> Term
    bvxnor Term
    s Term
    t = Ident -> [Term] -> Term
    App Ident
    "bvxnor" [Term
    s,Term
    t]

    bvcomp :: Term -> Term -> Term
    bvcomp :: Term -> Term -> Term
    bvcomp Term
    s Term
    t = Ident -> [Term] -> Term
    App Ident
    "bvcomp" [Term
    s,Term
    t]

    bvsub :: Term -> Term -> Term
    bvsub :: Term -> Term -> Term
    bvsub Term
    s Term
    t = Ident -> [Term] -> Term
    App Ident
    "bvsub" [Term
    s,Term
    t]

    bvsdiv :: Term -> Term -> Term
    bvsdiv :: Term -> Term -> Term
    bvsdiv Term
    s Term
    t = Ident -> [Term] -> Term
    App Ident
    "bvsdiv" [Term
    s,Term
    t]

    bvsrem :: Term -> Term -> Term
    bvsrem :: Term -> Term -> Term
    bvsrem Term
    s Term
    t = Ident -> [Term] -> Term
    App Ident
    "bvsrem" [Term
    s,Term
    t]

    bvsmod :: Term -> Term -> Term
    bvsmod :: Term -> Term -> Term
    bvsmod Term
    s Term
    t = Ident -> [Term] -> Term
    App Ident
    "bvsmod" [Term
    s,Term
    t]

    bvashr :: Term -> Term -> Term
    bvashr :: Term -> Term -> Term
    bvashr Term
    s Term
    t = Ident -> [Term] -> Term
    App Ident
    "bvashr" [Term
    s,Term
    t]

    repeat :: Integer -> Term -> Term
    repeat :: Integer -> Term -> Term
    repeat Integer
    i Term
    t = Ident -> [Term] -> Term
    App (Name -> [Integer] -> Ident
    I Name
    "repeat" [Integer
    i]) [Term
    t]

    zero_extend :: Integer -> Term -> Term
    zero_extend :: Integer -> Term -> Term
    zero_extend Integer
    i Term
    t = Ident -> [Term] -> Term
    App (Name -> [Integer] -> Ident
    I Name
    "zero_extend" [Integer
    i]) [Term
    t]

    sign_extend :: Integer -> Term -> Term
    sign_extend :: Integer -> Term -> Term
    sign_extend Integer
    i Term
    t = Ident -> [Term] -> Term
    App (Name -> [Integer] -> Ident
    I Name
    "sign_extend" [Integer
    i]) [Term
    t]

    rotate_left :: Integer -> Term -> Term
    rotate_left :: Integer -> Term -> Term
    rotate_left Integer
    i Term
    t = Ident -> [Term] -> Term
    App (Name -> [Integer] -> Ident
    I Name
    "rotate_left" [Integer
    i]) [Term
    t]

    rotate_right :: Integer -> Term -> Term
    rotate_right :: Integer -> Term -> Term
    rotate_right Integer
    i Term
    t = Ident -> [Term] -> Term
    App (Name -> [Integer] -> Ident
    I Name
    "rotate_right" [Integer
    i]) [Term
    t]

    bvule :: Term -> Term -> Formula
    bvule :: Term -> Term -> Formula
    bvule Term
    s Term
    t = Ident -> [Term] -> Formula
    FPred Ident
    "bvule" [Term
    s,Term
    t]

    bvugt :: Term -> Term -> Formula
    bvugt :: Term -> Term -> Formula
    bvugt Term
    s Term
    t = Ident -> [Term] -> Formula
    FPred Ident
    "bvugt" [Term
    s,Term
    t]

    bvuge :: Term -> Term -> Formula
    bvuge :: Term -> Term -> Formula
    bvuge Term
    s Term
    t = Ident -> [Term] -> Formula
    FPred Ident
    "bvuge" [Term
    s,Term
    t]

    bvslt :: Term -> Term -> Formula
    bvslt :: Term -> Term -> Formula
    bvslt Term
    s Term
    t = Ident -> [Term] -> Formula
    FPred Ident
    "bvslt" [Term
    s,Term
    t]

    bvsle :: Term -> Term -> Formula
    bvsle :: Term -> Term -> Formula
    bvsle Term
    s Term
    t = Ident -> [Term] -> Formula
    FPred Ident
    "bvsle" [Term
    s,Term
    t]

    bvsgt :: Term -> Term -> Formula
    bvsgt :: Term -> Term -> Formula
    bvsgt Term
    s Term
    t = Ident -> [Term] -> Formula
    FPred Ident
    "bvsgt" [Term
    s,Term
    t]

    bvsge :: Term -> Term -> Formula
    bvsge :: Term -> Term -> Formula
    bvsge Term
    s Term
    t = Ident -> [Term] -> Formula
    FPred Ident
    "bvsge" [Term
    s,Term
    t]