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

import SMTLib2.AST

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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