{-# LANGUAGE OverloadedStrings, Safe #-}
module SMTLib1.QF_AUFBV (module SMTLib1.QF_AUFBV, module X) where
import SMTLib1.QF_BV as X
tArray :: Integer -> Integer -> Sort
tArray :: Integer -> Integer -> Ident
tArray Integer
x Integer
y = Name -> [Integer] -> Ident
I Name
"Array" [Integer
x,Integer
y]
select :: Term -> Term -> Term
select :: Term -> Term -> Term
select Term
a Term
i = Ident -> [Term] -> Term
App Ident
"select" [Term
a,Term
i]
store :: Term -> Term -> Term -> Term
store :: Term -> Term -> Term -> Term
store Term
a Term
i Term
v = Ident -> [Term] -> Term
App Ident
"store" [Term
a,Term
i,Term
v]