{-# LANGUAGE OverloadedStrings #-}
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]