module SMTLib2.Int where
import SMTLib2.AST
tInt :: Type
tInt = TApp (I "Int" []) []
num :: Integral a => a -> Expr
num a = Lit (LitNum (toInteger a))
nNeg :: Expr -> Expr
nNeg x = app "-" [x]
nSub :: Expr -> Expr -> Expr
nSub x y = app "-" [x,y]
nAdd :: Expr -> Expr -> Expr
nAdd x y = app "+" [x,y]
nMul :: Expr -> Expr -> Expr
nMul x y = app "*" [x,y]
nDiv :: Expr -> Expr -> Expr
nDiv x y = app "div" [x,y]
nMod :: Expr -> Expr -> Expr
nMod x y = app "mod" [x,y]
nAbs :: Expr -> Expr
nAbs x = app "abs" [x]
nLeq :: Expr -> Expr -> Expr
nLeq x y = app "<=" [x,y]
nLt :: Expr -> Expr -> Expr
nLt x y = app "<" [x,y]
nGeq :: Expr -> Expr -> Expr
nGeq x y = app ">=" [x,y]
nGt :: Expr -> Expr -> Expr
nGt x y = app ">" [x,y]