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