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

import SMTLib2.AST

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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