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