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