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

import SMTLib2.AST

tBool :: Type
tBool = "Bool"

true :: Expr
true = app "true" []

false :: Expr
false = app "false" []

not :: Expr -> Expr
not p = app "not" [p]

(==>) :: Expr -> Expr -> Expr
p ==> q = app "=>" [p,q]

and :: Expr -> Expr -> Expr
and p q = app "and" [p,q]

or :: Expr -> Expr -> Expr
or p q = app "or" [p,q]

xor :: Expr -> Expr -> Expr
xor p q = app "xor" [p,q]

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

(=/=) :: Expr -> Expr -> Expr
x =/= y = app "distinct" [x,y]

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