{-# LANGUAGE OverloadedStrings, Safe #-}
module SMTLib2.BitVector where

import SMTLib2.AST

tBitVec :: Integer -> Type
tBitVec :: Integer -> Type
tBitVec Integer
n = Ident -> [Type] -> Type
TApp (Name -> [Integer] -> Ident
I Name
"BitVec" [Integer
n]) []

bv :: Integer -> Integer -> Expr
bv :: Integer -> Integer -> Expr
bv Integer
num Integer
w = Literal -> Expr
Lit (Integer -> Integer -> Literal
LitBV Integer
num Integer
w)

concat :: Expr -> Expr -> Expr
concat :: Expr -> Expr -> Expr
concat Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"concat" [Expr
x,Expr
y]

extract :: Integer -> Integer -> Expr -> Expr
extract :: Integer -> Integer -> Expr -> Expr
extract Integer
i Integer
j Expr
x = Ident -> [Expr] -> Expr
app (Name -> [Integer] -> Ident
I Name
"extract" [Integer
i,Integer
j]) [Expr
x]

bvnot :: Expr -> Expr
bvnot :: Expr -> Expr
bvnot Expr
x = Ident -> [Expr] -> Expr
app Ident
"bvnot" [Expr
x]

bvand :: Expr -> Expr -> Expr
bvand :: Expr -> Expr -> Expr
bvand Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvand" [Expr
x,Expr
y]

bvor :: Expr -> Expr -> Expr
bvor :: Expr -> Expr -> Expr
bvor Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvor" [Expr
x,Expr
y]

bvneg :: Expr -> Expr
bvneg :: Expr -> Expr
bvneg Expr
x = Ident -> [Expr] -> Expr
app Ident
"bvneg" [Expr
x]

bvadd :: Expr -> Expr -> Expr
bvadd :: Expr -> Expr -> Expr
bvadd Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvadd" [Expr
x,Expr
y]

bvmul :: Expr -> Expr -> Expr
bvmul :: Expr -> Expr -> Expr
bvmul Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvmul" [Expr
x,Expr
y]

bvudiv :: Expr -> Expr -> Expr
bvudiv :: Expr -> Expr -> Expr
bvudiv Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvudiv" [Expr
x,Expr
y]

bvurem :: Expr -> Expr -> Expr
bvurem :: Expr -> Expr -> Expr
bvurem Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvurem" [Expr
x,Expr
y]

bvshl :: Expr -> Expr -> Expr
bvshl :: Expr -> Expr -> Expr
bvshl Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvshl" [Expr
x,Expr
y]

bvlshr :: Expr -> Expr -> Expr
bvlshr :: Expr -> Expr -> Expr
bvlshr Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvlshr" [Expr
x,Expr
y]

bvult :: Expr -> Expr -> Expr
bvult :: Expr -> Expr -> Expr
bvult Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvult" [Expr
x,Expr
y]

bvnand :: Expr -> Expr -> Expr
bvnand :: Expr -> Expr -> Expr
bvnand Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvnand" [Expr
x,Expr
y]

bvnor :: Expr -> Expr -> Expr
bvnor :: Expr -> Expr -> Expr
bvnor Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvnor" [Expr
x,Expr
y]

bvxor :: Expr -> Expr -> Expr
bvxor :: Expr -> Expr -> Expr
bvxor Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvxor" [Expr
x,Expr
y]

bvxnor :: Expr -> Expr -> Expr
bvxnor :: Expr -> Expr -> Expr
bvxnor Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvxnor" [Expr
x,Expr
y]

bvcomp :: Expr -> Expr -> Expr
bvcomp :: Expr -> Expr -> Expr
bvcomp Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvcomp" [Expr
x,Expr
y]

bvsub :: Expr -> Expr -> Expr
bvsub :: Expr -> Expr -> Expr
bvsub Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvsub" [Expr
x,Expr
y]

bvsdiv :: Expr -> Expr -> Expr
bvsdiv :: Expr -> Expr -> Expr
bvsdiv Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvsdiv" [Expr
x,Expr
y]

bvsrem :: Expr -> Expr -> Expr
bvsrem :: Expr -> Expr -> Expr
bvsrem Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvsrem" [Expr
x,Expr
y]

bvsmod :: Expr -> Expr -> Expr
bvsmod :: Expr -> Expr -> Expr
bvsmod Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvsmod" [Expr
x,Expr
y]

bvashr :: Expr -> Expr -> Expr
bvashr :: Expr -> Expr -> Expr
bvashr Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvashr" [Expr
x,Expr
y]

repeat :: Integer -> Expr -> Expr -> Expr
repeat :: Integer -> Expr -> Expr -> Expr
repeat Integer
i Expr
x Expr
y = Ident -> [Expr] -> Expr
app (Name -> [Integer] -> Ident
I Name
"repeat" [Integer
i]) [Expr
x,Expr
y]

zero_extend :: Integer -> Expr -> Expr
zero_extend :: Integer -> Expr -> Expr
zero_extend Integer
i Expr
x = Ident -> [Expr] -> Expr
app (Name -> [Integer] -> Ident
I Name
"zero_extend" [Integer
i]) [Expr
x]

sign_extend :: Integer -> Expr -> Expr
sign_extend :: Integer -> Expr -> Expr
sign_extend Integer
i Expr
x = Ident -> [Expr] -> Expr
app (Name -> [Integer] -> Ident
I Name
"sign_extend" [Integer
i]) [Expr
x]

rotate_left :: Integer -> Expr -> Expr
rotate_left :: Integer -> Expr -> Expr
rotate_left Integer
i Expr
x = Ident -> [Expr] -> Expr
app (Name -> [Integer] -> Ident
I Name
"rotate_left" [Integer
i]) [Expr
x]

rotate_right :: Integer -> Expr -> Expr
rotate_right :: Integer -> Expr -> Expr
rotate_right Integer
i Expr
x = Ident -> [Expr] -> Expr
app (Name -> [Integer] -> Ident
I Name
"rotate_right" [Integer
i]) [Expr
x]

bvule :: Expr -> Expr -> Expr
bvule :: Expr -> Expr -> Expr
bvule Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvule" [Expr
x,Expr
y]

bvugt :: Expr -> Expr -> Expr
bvugt :: Expr -> Expr -> Expr
bvugt Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvugt" [Expr
x,Expr
y]

bvuge :: Expr -> Expr -> Expr
bvuge :: Expr -> Expr -> Expr
bvuge Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvuge" [Expr
x,Expr
y]

bvslt :: Expr -> Expr -> Expr
bvslt :: Expr -> Expr -> Expr
bvslt Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvslt" [Expr
x,Expr
y]

bvsle :: Expr -> Expr -> Expr
bvsle :: Expr -> Expr -> Expr
bvsle Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvsle" [Expr
x,Expr
y]

bvsgt :: Expr -> Expr -> Expr
bvsgt :: Expr -> Expr -> Expr
bvsgt Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvsgt" [Expr
x,Expr
y]

bvsge :: Expr -> Expr -> Expr
bvsge :: Expr -> Expr -> Expr
bvsge Expr
x Expr
y = Ident -> [Expr] -> Expr
app Ident
"bvsge" [Expr
x,Expr
y]