smtLib 1.0.2 → 1.0.3

raw patch · 2 files changed

+47/−1 lines, 2 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

- SMTLib1.AST: (.<.) :: Term -> Term -> Formula

- SMTLib1.AST: (.>.) :: Term -> Term -> Formula

- SMTLib1.AST: (=/=) :: Term -> Term -> Formula

- SMTLib1.AST: (===) :: Term -> Term -> Formula

- SMTLib1.AST: And :: Conn

- SMTLib1.AST: App :: Ident -> [Term] -> Term

- SMTLib1.AST: Attr :: Name -> Maybe String -> Annot

- SMTLib1.AST: Bind :: Name -> Sort -> Binder

- SMTLib1.AST: CmdAnnot :: Annot -> Command

- SMTLib1.AST: CmdAssumption :: Formula -> Command

- SMTLib1.AST: CmdExtraFuns :: [FunDecl] -> Command

- SMTLib1.AST: CmdExtraPreds :: [PredDecl] -> Command

- SMTLib1.AST: CmdExtraSorts :: [Sort] -> Command

- SMTLib1.AST: CmdFormula :: Formula -> Command

- SMTLib1.AST: CmdLogic :: Ident -> Command

- SMTLib1.AST: CmdNotes :: String -> Command

- SMTLib1.AST: CmdStatus :: Status -> Command

- SMTLib1.AST: Conn :: Conn -> [Formula] -> Formula

- SMTLib1.AST: Exists :: Quant

- SMTLib1.AST: FAnnot :: Formula -> [Annot] -> Formula

- SMTLib1.AST: FFalse :: Formula

- SMTLib1.AST: FLet :: Name -> Formula -> Formula -> Formula

- SMTLib1.AST: FPred :: Ident -> [Term] -> Formula

- SMTLib1.AST: FTrue :: Formula

- SMTLib1.AST: FVar :: Name -> Formula

- SMTLib1.AST: Forall :: Quant

- SMTLib1.AST: FunDecl :: Ident -> [Sort] -> Sort -> [Annot] -> FunDecl

- SMTLib1.AST: I :: Name -> [Integer] -> Ident

- SMTLib1.AST: ITE :: Formula -> Term -> Term -> Term

- SMTLib1.AST: IfThenElse :: Conn

- SMTLib1.AST: Iff :: Conn

- SMTLib1.AST: Implies :: Conn

- SMTLib1.AST: Let :: Name -> Term -> Formula -> Formula

- SMTLib1.AST: Lit :: Literal -> Term

- SMTLib1.AST: LitFrac :: Rational -> Literal

- SMTLib1.AST: LitNum :: Integer -> Literal

- SMTLib1.AST: LitStr :: String -> Literal

- SMTLib1.AST: N :: String -> Name

- SMTLib1.AST: Not :: Conn

- SMTLib1.AST: Or :: Conn

- SMTLib1.AST: PredDecl :: Ident -> [Sort] -> [Annot] -> PredDecl

- SMTLib1.AST: Quant :: Quant -> [Binder] -> Formula -> Formula

- SMTLib1.AST: Sat :: Status

- SMTLib1.AST: Script :: Ident -> [Command] -> Script

- SMTLib1.AST: TAnnot :: Term -> [Annot] -> Term

- SMTLib1.AST: Unknown :: Status

- SMTLib1.AST: Unsat :: Status

- SMTLib1.AST: Var :: Name -> Term

- SMTLib1.AST: Xor :: Conn

- SMTLib1.AST: assume :: Formula -> Command

- SMTLib1.AST: attrName :: Annot -> Name

- SMTLib1.AST: attrVal :: Annot -> Maybe String

- SMTLib1.AST: bindSort :: Binder -> Sort

- SMTLib1.AST: bindVar :: Binder -> Name

- SMTLib1.AST: constDef :: Ident -> Sort -> Command

- SMTLib1.AST: data Annot

- SMTLib1.AST: data Binder

- SMTLib1.AST: data Command

- SMTLib1.AST: data Conn

- SMTLib1.AST: data Formula

- SMTLib1.AST: data FunDecl

- SMTLib1.AST: data Ident

- SMTLib1.AST: data Literal

- SMTLib1.AST: data PredDecl

- SMTLib1.AST: data Quant

- SMTLib1.AST: data Script

- SMTLib1.AST: data Status

- SMTLib1.AST: data Term

- SMTLib1.AST: funAnnots :: FunDecl -> [Annot]

- SMTLib1.AST: funArgs :: FunDecl -> [Sort]

- SMTLib1.AST: funDef :: Ident -> [Sort] -> Sort -> Command

- SMTLib1.AST: funName :: FunDecl -> Ident

- SMTLib1.AST: funRes :: FunDecl -> Sort

- SMTLib1.AST: goal :: Formula -> Command

- SMTLib1.AST: instance Eq Annot

- SMTLib1.AST: instance Eq Binder

- SMTLib1.AST: instance Eq Conn

- SMTLib1.AST: instance Eq Formula

- SMTLib1.AST: instance Eq Ident

- SMTLib1.AST: instance Eq Literal

- SMTLib1.AST: instance Eq Name

- SMTLib1.AST: instance Eq Quant

- SMTLib1.AST: instance Eq Term

- SMTLib1.AST: instance Fractional Term

- SMTLib1.AST: instance IsString Ident

- SMTLib1.AST: instance IsString Name

- SMTLib1.AST: instance IsString Term

- SMTLib1.AST: instance Num Term

- SMTLib1.AST: instance Ord Annot

- SMTLib1.AST: instance Ord Binder

- SMTLib1.AST: instance Ord Conn

- SMTLib1.AST: instance Ord Formula

- SMTLib1.AST: instance Ord Ident

- SMTLib1.AST: instance Ord Literal

- SMTLib1.AST: instance Ord Name

- SMTLib1.AST: instance Ord Quant

- SMTLib1.AST: instance Ord Term

- SMTLib1.AST: instance Show Annot

- SMTLib1.AST: instance Show Binder

- SMTLib1.AST: instance Show Conn

- SMTLib1.AST: instance Show Formula

- SMTLib1.AST: instance Show Ident

- SMTLib1.AST: instance Show Literal

- SMTLib1.AST: instance Show Name

- SMTLib1.AST: instance Show Quant

- SMTLib1.AST: instance Show Term

- SMTLib1.AST: logic :: Ident -> Command

- SMTLib1.AST: newtype Name

- SMTLib1.AST: predAnnots :: PredDecl -> [Annot]

- SMTLib1.AST: predArgs :: PredDecl -> [Sort]

- SMTLib1.AST: predName :: PredDecl -> Ident

- SMTLib1.AST: scrCommands :: Script -> [Command]

- SMTLib1.AST: scrName :: Script -> Ident

- SMTLib1.AST: tInt :: Sort

- SMTLib1.AST: type Sort = Ident

- SMTLib1.PP: class PP t

- SMTLib1.PP: instance PP Annot

- SMTLib1.PP: instance PP Binder

- SMTLib1.PP: instance PP Command

- SMTLib1.PP: instance PP Conn

- SMTLib1.PP: instance PP Formula

- SMTLib1.PP: instance PP FunDecl

- SMTLib1.PP: instance PP Ident

- SMTLib1.PP: instance PP Literal

- SMTLib1.PP: instance PP Name

- SMTLib1.PP: instance PP PredDecl

- SMTLib1.PP: instance PP Quant

- SMTLib1.PP: instance PP Script

- SMTLib1.PP: instance PP Status

- SMTLib1.PP: instance PP Term

- SMTLib1.PP: pp :: PP t => t -> Doc

- SMTLib2.AST: Annot :: Expr -> [Attr] -> Expr

- SMTLib2.AST: App :: Ident -> (Maybe Type) -> [Expr] -> Expr

- SMTLib2.AST: Attr :: Name -> Maybe AttrVal -> Attr

- SMTLib2.AST: Bind :: Name -> Type -> Binder

- SMTLib2.AST: CmdAssert :: Expr -> Command

- SMTLib2.AST: CmdCheckSat :: Command

- SMTLib2.AST: CmdDeclareFun :: Name -> [Type] -> Type -> Command

- SMTLib2.AST: CmdDeclareType :: Name -> Integer -> Command

- SMTLib2.AST: CmdDefineFun :: Name -> [Binder] -> Type -> Expr -> Command

- SMTLib2.AST: CmdDefineType :: Name -> [Name] -> Type -> Command

- SMTLib2.AST: CmdExit :: Command

- SMTLib2.AST: CmdGetAssertions :: Command

- SMTLib2.AST: CmdGetInfo :: InfoFlag -> Command

- SMTLib2.AST: CmdGetOption :: Name -> Command

- SMTLib2.AST: CmdGetProof :: Command

- SMTLib2.AST: CmdGetUnsatCore :: Command

- SMTLib2.AST: CmdGetValue :: [Expr] -> Command

- SMTLib2.AST: CmdPop :: Integer -> Command

- SMTLib2.AST: CmdPush :: Integer -> Command

- SMTLib2.AST: CmdSetInfo :: Attr -> Command

- SMTLib2.AST: CmdSetLogic :: Name -> Command

- SMTLib2.AST: CmdSetOption :: Option -> Command

- SMTLib2.AST: Defn :: Name -> Expr -> Defn

- SMTLib2.AST: Exists :: Quant

- SMTLib2.AST: Forall :: Quant

- SMTLib2.AST: I :: Name -> [Integer] -> Ident

- SMTLib2.AST: InfoAllStatistics :: InfoFlag

- SMTLib2.AST: InfoAttr :: Attr -> InfoFlag

- SMTLib2.AST: InfoAuthors :: InfoFlag

- SMTLib2.AST: InfoErrorBehavior :: InfoFlag

- SMTLib2.AST: InfoName :: InfoFlag

- SMTLib2.AST: InfoReasonUnknown :: InfoFlag

- SMTLib2.AST: InfoStatus :: InfoFlag

- SMTLib2.AST: InfoVersion :: InfoFlag

- SMTLib2.AST: Let :: [Defn] -> Expr -> Expr

- SMTLib2.AST: Lit :: Literal -> Expr

- SMTLib2.AST: LitBV :: Integer -> Integer -> Literal

- SMTLib2.AST: LitFrac :: Rational -> Literal

- SMTLib2.AST: LitNum :: Integer -> Literal

- SMTLib2.AST: LitStr :: String -> Literal

- SMTLib2.AST: N :: String -> Name

- SMTLib2.AST: OptAttr :: Attr -> Option

- SMTLib2.AST: OptDiagnosticOutputChannel :: String -> Option

- SMTLib2.AST: OptExpandDefinitions :: Bool -> Option

- SMTLib2.AST: OptInteractiveMode :: Bool -> Option

- SMTLib2.AST: OptPrintSuccess :: Bool -> Option

- SMTLib2.AST: OptProduceAssignments :: Bool -> Option

- SMTLib2.AST: OptProduceModels :: Bool -> Option

- SMTLib2.AST: OptProduceProofs :: Bool -> Option

- SMTLib2.AST: OptProduceUnsatCores :: Bool -> Option

- SMTLib2.AST: OptRandomSeed :: Integer -> Option

- SMTLib2.AST: OptRegularOutputChannel :: String -> Option

- SMTLib2.AST: OptVerbosity :: Integer -> Option

- SMTLib2.AST: Quant :: Quant -> [Binder] -> Expr -> Expr

- SMTLib2.AST: Script :: [Command] -> Script

- SMTLib2.AST: TApp :: Ident -> [Type] -> Type

- SMTLib2.AST: TVar :: Name -> Type

- SMTLib2.AST: app :: Ident -> [Expr] -> Expr

- SMTLib2.AST: attrName :: Attr -> Name

- SMTLib2.AST: attrVal :: Attr -> Maybe AttrVal

- SMTLib2.AST: bindType :: Binder -> Type

- SMTLib2.AST: bindVar :: Binder -> Name

- SMTLib2.AST: data Attr

- SMTLib2.AST: data Binder

- SMTLib2.AST: data Command

- SMTLib2.AST: data Defn

- SMTLib2.AST: data Expr

- SMTLib2.AST: data Ident

- SMTLib2.AST: data InfoFlag

- SMTLib2.AST: data Literal

- SMTLib2.AST: data Option

- SMTLib2.AST: data Quant

- SMTLib2.AST: data Type

- SMTLib2.AST: defExpr :: Defn -> Expr

- SMTLib2.AST: defVar :: Defn -> Name

- SMTLib2.AST: instance Eq Attr

- SMTLib2.AST: instance Eq Binder

- SMTLib2.AST: instance Eq Defn

- SMTLib2.AST: instance Eq Expr

- SMTLib2.AST: instance Eq Ident

- SMTLib2.AST: instance Eq Literal

- SMTLib2.AST: instance Eq Name

- SMTLib2.AST: instance Eq Quant

- SMTLib2.AST: instance Eq Type

- SMTLib2.AST: instance Fractional Expr

- SMTLib2.AST: instance IsString Expr

- SMTLib2.AST: instance IsString Ident

- SMTLib2.AST: instance IsString Name

- SMTLib2.AST: instance IsString Type

- SMTLib2.AST: instance Num Expr

- SMTLib2.AST: instance Ord Attr

- SMTLib2.AST: instance Ord Binder

- SMTLib2.AST: instance Ord Defn

- SMTLib2.AST: instance Ord Expr

- SMTLib2.AST: instance Ord Ident

- SMTLib2.AST: instance Ord Literal

- SMTLib2.AST: instance Ord Name

- SMTLib2.AST: instance Ord Quant

- SMTLib2.AST: instance Ord Type

- SMTLib2.AST: instance Show Attr

- SMTLib2.AST: instance Show Binder

- SMTLib2.AST: instance Show Defn

- SMTLib2.AST: instance Show Expr

- SMTLib2.AST: instance Show Ident

- SMTLib2.AST: instance Show Literal

- SMTLib2.AST: instance Show Name

- SMTLib2.AST: instance Show Quant

- SMTLib2.AST: instance Show Type

- SMTLib2.AST: newtype Name

- SMTLib2.AST: newtype Script

- SMTLib2.AST: type AttrVal = Expr

- SMTLib2.PP: class PP t

- SMTLib2.PP: instance PP Attr

- SMTLib2.PP: instance PP Binder

- SMTLib2.PP: instance PP Bool

- SMTLib2.PP: instance PP Command

- SMTLib2.PP: instance PP Defn

- SMTLib2.PP: instance PP Expr

- SMTLib2.PP: instance PP Ident

- SMTLib2.PP: instance PP InfoFlag

- SMTLib2.PP: instance PP Integer

- SMTLib2.PP: instance PP Literal

- SMTLib2.PP: instance PP Name

- SMTLib2.PP: instance PP Option

- SMTLib2.PP: instance PP Quant

- SMTLib2.PP: instance PP Script

- SMTLib2.PP: instance PP Type

- SMTLib2.PP: pp :: PP t => t -> Doc

- SMTLib2.PP: ppString :: String -> Doc

+ SMTLib2.Int: nAbs :: Expr -> Expr

+ SMTLib2.Int: nAdd :: Expr -> Expr -> Expr

+ SMTLib2.Int: nDiv :: Expr -> Expr -> Expr

+ SMTLib2.Int: nGeq :: Expr -> Expr -> Expr

+ SMTLib2.Int: nGt :: Expr -> Expr -> Expr

+ SMTLib2.Int: nLeq :: Expr -> Expr -> Expr

+ SMTLib2.Int: nLt :: Expr -> Expr -> Expr

+ SMTLib2.Int: nMod :: Expr -> Expr -> Expr

+ SMTLib2.Int: nMul :: Expr -> Expr -> Expr

+ SMTLib2.Int: nNeg :: Expr -> Expr

+ SMTLib2.Int: nSub :: Expr -> Expr -> Expr

+ SMTLib2.Int: num :: Integral a => a -> Expr

+ SMTLib2.Int: tInt :: Type

Files

smtLib.cabal +4/−1
src/SMTLib2/Int.hs +43/−0

smtLib.cabal view

@@ -1,5 +1,5 @@ Name:           smtLib-Version:        1.0.2+Version:        1.0.3 License:        BSD3 License-file:   LICENSE Author:         Iavor S. Diatchki@@ -25,6 +25,9 @@     SMTLib2.Core     SMTLib2.BitVector     SMTLib2.Array+    SMTLib2.Int++  other-modules:     SMTLib1.AST     SMTLib1.PP     SMTLib2.AST

+ src/SMTLib2/Int.hs view

@@ -0,0 +1,43 @@+{-# LANGUAGE OverloadedStrings #-}+module SMTLib2.Int where++import SMTLib2.AST++tInt :: Type+tInt = TApp (I "Int" []) []++num :: Integral a => a -> Expr+num a = Lit (LitNum (toInteger a))++nNeg :: Expr -> Expr+nNeg x = app "-" [x]++nSub :: Expr -> Expr -> Expr+nSub x y = app "-" [x,y]++nAdd :: Expr -> Expr -> Expr+nAdd x y = app "+" [x,y]++nMul :: Expr -> Expr -> Expr+nMul x y = app "*" [x,y]++nDiv :: Expr -> Expr -> Expr+nDiv x y = app "div" [x,y]++nMod :: Expr -> Expr -> Expr+nMod x y = app "mod" [x,y]++nAbs :: Expr -> Expr+nAbs x = app "abs" [x]++nLeq :: Expr -> Expr -> Expr+nLeq x y = app "<=" [x,y]++nLt :: Expr -> Expr -> Expr+nLt x y = app "<" [x,y]++nGeq :: Expr -> Expr -> Expr+nGeq x y = app ">=" [x,y]++nGt :: Expr -> Expr -> Expr+nGt x y = app ">" [x,y]