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