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]