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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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