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

import SMTLib2.AST

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

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

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

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

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

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

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

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

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

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

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