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

import SMTLib2.AST

tBool :: Type
tBool :: Type
tBool = "Bool"

true :: Expr
true :: Expr
true = Ident -> [Expr] -> Expr
app "true" []

false :: Expr
false :: Expr
false = Ident -> [Expr] -> Expr
app "false" []

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

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

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

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

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

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

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

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