simple-smt 0.5.0 → 0.5.1

raw patch · 3 files changed

+30/−2 lines, 3 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGES +3/−1
• SimpleSMT.hs +26/−0
• simple-smt.cabal +1/−1

@@ -1,1 +1,3 @@-0.4: Fixes definiiton of `geq`+0.5.1:  Add 'define' commands+0.5:    Adds more bit-wise operations+0.4:    Fixes definiiton of `geq`

@@ -27,6 +27,8 @@   , pop, popMany   , declare   , declareFun+  , define+  , defineFun   , assert   , check   , Result(..)@@ -289,6 +291,30 @@ declareFun proc f as r =   do ackCommand proc $ fun "declare-fun" [ Atom f, List as, r ]      return (const f)++-- | Declare a constant.  A common abbreviation for 'declareFun'.+-- For convenience, returns the defined name as a constant expression.+define :: Solver ->+          String {- ^ New symbol -} ->+          SExpr  {- ^ Symbol type -} ->+          SExpr  {- ^ Symbol definition -} ->+          IO SExpr+define proc f t e = defineFun proc f [] t e++-- | Define a function or a constant.+-- For convenience, returns an the defined name as a constant expression.+defineFun :: Solver ->+             String           {- ^ New symbol -} ->+             [(String,SExpr)] {- ^ Parameters, with types -} ->+             SExpr            {- ^ Type of result -} ->+             SExpr            {- ^ Definition -} ->+             IO SExpr+defineFun proc f as t e =+  do ackCommand proc $ fun "define-fun"+                     $ [ Atom f, List [ List [const x,a] | (x,a) <- as ], t, e]+     return (const f)++  -- | Assume a fact. assert :: Solver -> SExpr -> IO ()

@@ -1,5 +1,5 @@ name:                simple-smt-version:             0.5.0+version:             0.5.1 synopsis:            A simple way to interact with an SMT solver process. description:         A simple way to interact with an SMT solver process. license:             BSD3