{-# 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]