    {-# 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 -> Sort
    tBitVec n :: Integer
    n = Name -> [Integer] -> Sort
    I "BitVec" [Integer
    n]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    bv :: Integer -> Integer -> Term
    bv :: Integer -> Integer -> Term
    bv x :: Integer
    x m :: Integer
    m = if Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= 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 y :: a
    y = Sort -> [Term] -> Term
    App (Name -> [Integer] -> Sort
    I (String -> Name
    forall a. IsString a => String -> a
    fromString ("bv" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    y)) [Integer
    m]) []

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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