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