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

    import SMTLib1.QF_BV as X

    -- | 'tArray i n' is an array indexed by bitvectors of widht 'i',
    -- and storing bitvectors of width 'n'.
    tArray :: Integer -> Integer -> Sort
    tArray :: Integer -> Integer -> Sort
    tArray x :: Integer
    x y :: Integer
    y = Name -> [Integer] -> Sort
    I "Array" [Integer
    x,Integer
    y]

    -- | @select array index@
    select :: Term -> Term -> Term
    select :: Term -> Term -> Term
    select a :: Term
    a i :: Term
    i = Sort -> [Term] -> Term
    App "select" [Term
    a,Term
    i]

    -- | @store array index value@
    store :: Term -> Term -> Term -> Term
    store :: Term -> Term -> Term -> Term
    store a :: Term
    a i :: Term
    i v :: Term
    v = Sort -> [Term] -> Term
    App "store" [Term
    a,Term
    i,Term
    v]