packages feed

smtLib 1.0.4 → 1.0.5

raw patch · 3 files changed

+52/−7 lines, 3 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

+ SMTLib1: (.<.) :: Term -> Term -> Formula
+ SMTLib1: (.>.) :: Term -> Term -> Formula
+ SMTLib1: (=/=) :: Term -> Term -> Formula
+ SMTLib1: (===) :: Term -> Term -> Formula
+ SMTLib1: And :: Conn
+ SMTLib1: App :: Ident -> [Term] -> Term
+ SMTLib1: Attr :: Name -> Maybe String -> Annot
+ SMTLib1: Bind :: Name -> Sort -> Binder
+ SMTLib1: CmdAnnot :: Annot -> Command
+ SMTLib1: CmdAssumption :: Formula -> Command
+ SMTLib1: CmdExtraFuns :: [FunDecl] -> Command
+ SMTLib1: CmdExtraPreds :: [PredDecl] -> Command
+ SMTLib1: CmdExtraSorts :: [Sort] -> Command
+ SMTLib1: CmdFormula :: Formula -> Command
+ SMTLib1: CmdLogic :: Ident -> Command
+ SMTLib1: CmdNotes :: String -> Command
+ SMTLib1: CmdStatus :: Status -> Command
+ SMTLib1: Conn :: Conn -> [Formula] -> Formula
+ SMTLib1: Exists :: Quant
+ SMTLib1: FAnnot :: Formula -> [Annot] -> Formula
+ SMTLib1: FFalse :: Formula
+ SMTLib1: FLet :: Name -> Formula -> Formula -> Formula
+ SMTLib1: FPred :: Ident -> [Term] -> Formula
+ SMTLib1: FTrue :: Formula
+ SMTLib1: FVar :: Name -> Formula
+ SMTLib1: Forall :: Quant
+ SMTLib1: FunDecl :: Ident -> [Sort] -> Sort -> [Annot] -> FunDecl
+ SMTLib1: I :: Name -> [Integer] -> Ident
+ SMTLib1: ITE :: Formula -> Term -> Term -> Term
+ SMTLib1: IfThenElse :: Conn
+ SMTLib1: Iff :: Conn
+ SMTLib1: Implies :: Conn
+ SMTLib1: Let :: Name -> Term -> Formula -> Formula
+ SMTLib1: Lit :: Literal -> Term
+ SMTLib1: LitFrac :: Rational -> Literal
+ SMTLib1: LitNum :: Integer -> Literal
+ SMTLib1: LitStr :: String -> Literal
+ SMTLib1: N :: String -> Name
+ SMTLib1: Not :: Conn
+ SMTLib1: Or :: Conn
+ SMTLib1: PredDecl :: Ident -> [Sort] -> [Annot] -> PredDecl
+ SMTLib1: Quant :: Quant -> [Binder] -> Formula -> Formula
+ SMTLib1: Sat :: Status
+ SMTLib1: Script :: Ident -> [Command] -> Script
+ SMTLib1: TAnnot :: Term -> [Annot] -> Term
+ SMTLib1: Unknown :: Status
+ SMTLib1: Unsat :: Status
+ SMTLib1: Var :: Name -> Term
+ SMTLib1: Xor :: Conn
+ SMTLib1: assume :: Formula -> Command
+ SMTLib1: attrName :: Annot -> Name
+ SMTLib1: attrVal :: Annot -> Maybe String
+ SMTLib1: bindSort :: Binder -> Sort
+ SMTLib1: bindVar :: Binder -> Name
+ SMTLib1: constDef :: Ident -> Sort -> Command
+ SMTLib1: data Annot
+ SMTLib1: data Binder
+ SMTLib1: data Command
+ SMTLib1: data Conn
+ SMTLib1: data Formula
+ SMTLib1: data FunDecl
+ SMTLib1: data Ident
+ SMTLib1: data Literal
+ SMTLib1: data PredDecl
+ SMTLib1: data Quant
+ SMTLib1: data Script
+ SMTLib1: data Status
+ SMTLib1: data Term
+ SMTLib1: funAnnots :: FunDecl -> [Annot]
+ SMTLib1: funArgs :: FunDecl -> [Sort]
+ SMTLib1: funDef :: Ident -> [Sort] -> Sort -> Command
+ SMTLib1: funName :: FunDecl -> Ident
+ SMTLib1: funRes :: FunDecl -> Sort
+ SMTLib1: goal :: Formula -> Command
+ SMTLib1: logic :: Ident -> Command
+ SMTLib1: newtype Name
+ SMTLib1: predAnnots :: PredDecl -> [Annot]
+ SMTLib1: predArgs :: PredDecl -> [Sort]
+ SMTLib1: predName :: PredDecl -> Ident
+ SMTLib1: scrCommands :: Script -> [Command]
+ SMTLib1: scrName :: Script -> Ident
+ SMTLib1: tInt :: Sort
+ SMTLib1: type Sort = Ident
+ SMTLib2: Annot :: Expr -> [Attr] -> Expr
+ SMTLib2: App :: Ident -> (Maybe Type) -> [Expr] -> Expr
+ SMTLib2: Attr :: Name -> Maybe AttrVal -> Attr
+ SMTLib2: Bind :: Name -> Type -> Binder
+ SMTLib2: CmdAssert :: Expr -> Command
+ SMTLib2: CmdCheckSat :: Command
+ SMTLib2: CmdDeclareFun :: Name -> [Type] -> Type -> Command
+ SMTLib2: CmdDeclareType :: Name -> Integer -> Command
+ SMTLib2: CmdDefineFun :: Name -> [Binder] -> Type -> Expr -> Command
+ SMTLib2: CmdDefineType :: Name -> [Name] -> Type -> Command
+ SMTLib2: CmdExit :: Command
+ SMTLib2: CmdGetAssertions :: Command
+ SMTLib2: CmdGetInfo :: InfoFlag -> Command
+ SMTLib2: CmdGetOption :: Name -> Command
+ SMTLib2: CmdGetProof :: Command
+ SMTLib2: CmdGetUnsatCore :: Command
+ SMTLib2: CmdGetValue :: [Expr] -> Command
+ SMTLib2: CmdPop :: Integer -> Command
+ SMTLib2: CmdPush :: Integer -> Command
+ SMTLib2: CmdSetInfo :: Attr -> Command
+ SMTLib2: CmdSetLogic :: Name -> Command
+ SMTLib2: CmdSetOption :: Option -> Command
+ SMTLib2: Defn :: Name -> Expr -> Defn
+ SMTLib2: Exists :: Quant
+ SMTLib2: Forall :: Quant
+ SMTLib2: I :: Name -> [Integer] -> Ident
+ SMTLib2: InfoAllStatistics :: InfoFlag
+ SMTLib2: InfoAttr :: Attr -> InfoFlag
+ SMTLib2: InfoAuthors :: InfoFlag
+ SMTLib2: InfoErrorBehavior :: InfoFlag
+ SMTLib2: InfoName :: InfoFlag
+ SMTLib2: InfoReasonUnknown :: InfoFlag
+ SMTLib2: InfoStatus :: InfoFlag
+ SMTLib2: InfoVersion :: InfoFlag
+ SMTLib2: Let :: [Defn] -> Expr -> Expr
+ SMTLib2: Lit :: Literal -> Expr
+ SMTLib2: LitBV :: Integer -> Integer -> Literal
+ SMTLib2: LitFrac :: Rational -> Literal
+ SMTLib2: LitNum :: Integer -> Literal
+ SMTLib2: LitStr :: String -> Literal
+ SMTLib2: N :: String -> Name
+ SMTLib2: OptAttr :: Attr -> Option
+ SMTLib2: OptDiagnosticOutputChannel :: String -> Option
+ SMTLib2: OptExpandDefinitions :: Bool -> Option
+ SMTLib2: OptInteractiveMode :: Bool -> Option
+ SMTLib2: OptPrintSuccess :: Bool -> Option
+ SMTLib2: OptProduceAssignments :: Bool -> Option
+ SMTLib2: OptProduceModels :: Bool -> Option
+ SMTLib2: OptProduceProofs :: Bool -> Option
+ SMTLib2: OptProduceUnsatCores :: Bool -> Option
+ SMTLib2: OptRandomSeed :: Integer -> Option
+ SMTLib2: OptRegularOutputChannel :: String -> Option
+ SMTLib2: OptVerbosity :: Integer -> Option
+ SMTLib2: Quant :: Quant -> [Binder] -> Expr -> Expr
+ SMTLib2: Script :: [Command] -> Script
+ SMTLib2: TApp :: Ident -> [Type] -> Type
+ SMTLib2: TVar :: Name -> Type
+ SMTLib2: app :: Ident -> [Expr] -> Expr
+ SMTLib2: attrName :: Attr -> Name
+ SMTLib2: attrVal :: Attr -> Maybe AttrVal
+ SMTLib2: bindType :: Binder -> Type
+ SMTLib2: bindVar :: Binder -> Name
+ SMTLib2: data Attr
+ SMTLib2: data Binder
+ SMTLib2: data Command
+ SMTLib2: data Defn
+ SMTLib2: data Expr
+ SMTLib2: data Ident
+ SMTLib2: data InfoFlag
+ SMTLib2: data Literal
+ SMTLib2: data Option
+ SMTLib2: data Quant
+ SMTLib2: data Type
+ SMTLib2: defExpr :: Defn -> Expr
+ SMTLib2: defVar :: Defn -> Name
+ SMTLib2: newtype Name
+ SMTLib2: newtype Script
+ SMTLib2: type AttrVal = Expr

Files

smtLib.cabal view
@@ -1,5 +1,5 @@ Name:           smtLib-Version:        1.0.4+Version:        1.0.5 License:        BSD3 License-file:   LICENSE Author:         Iavor S. Diatchki
src/SMTLib1.hs view
@@ -1,6 +1,33 @@ {-# LANGUAGE Safe #-}-module SMTLib1 (module X) where+module SMTLib1+  ( Name(..)+  , Ident(..)+  , Quant(..)+  , Conn(..)+  , Formula(..)+  , Sort+  , Binder(..)+  , Term(..)+  , Literal(..)+  , Annot(..)+  , FunDecl(..)+  , PredDecl(..)+  , Status(..)+  , Command(..)+  , Script(..) -import SMTLib1.AST as X-import SMTLib1.PP as X+  , (===)+  , (=/=)+  , (.<.)+  , (.>.)+  , tInt+  , funDef+  , constDef+  , logic+  , assume+  , goal+  ) where++import SMTLib1.AST+import SMTLib1.PP()
src/SMTLib2.hs view
@@ -1,6 +1,24 @@ {-# LANGUAGE Safe #-}-module SMTLib2 (module X) where+module SMTLib2+  ( Script(..)+  , Binder(..)+  , Defn(..)+  , Type(..)+  , Expr(..) -import SMTLib2.AST as X-import SMTLib2.PP as X+  , Name(..)+  , Ident(..)+  , Quant(..)+  , Literal(..)+  , Attr(..)+  , AttrVal+  , Command(..)+  , Option(..)+  , InfoFlag(..)++  , app+  ) where++import SMTLib2.AST+import SMTLib2.PP()