    {-# 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 n = I "BitVec" [n]

    isBitVec :: Sort -> Maybe Integer
    isBitVec (I "BitVec" [n]) = Just n
    isBitVec _                = Nothing

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    bv :: Integer -> Integer -> Term
    bv x m = if x >= 0 then lit x else bvneg (lit (negate x))
      where lit y = App (I (fromString ("bv" ++ show y)) [m]) []

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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