z3 4.3 → 4.3.1

raw patch · 4 files changed

+50/−3 lines, 4 files

Files

• CHANGES.md +4/−0
• examples/Example/Monad/ParserInterface.hs +27/−0
• src/Z3/Opts.hs +15/−1
• z3.cabal +4/−2

@@ -1,6 +1,10 @@  # Release Notes +## 4.3.1++* Fix compatibility with base 4.11 due to SMP (M Farkas-Dyck)+ ## 4.3  ### Fixes

@@ -0,0 +1,27 @@+-- | Parse AST from SMTLIB string+module Example.Monad.ParserInterface+  ( run )+  where++import Z3.Monad++run :: IO ()+run = evalZ3 script >>= print++-- Toy example SMTLIB string+smtStr1 :: String+smtStr1 = "(declare-const x Int)\n(assert (< x 5))"++smtStr2 :: String+smtStr2 = "(declare-const x Int)\n(assert (> x 5))"+++script :: Z3 Result+script = do+  l <- parseSMTLib2String smtStr1 [] [] [] []+  r <- parseSMTLib2String smtStr2 [] [] [] []+  eq <- mkEq l r+  assert l+  assert r+  assert eq+  check

@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-}  -- | -- Module    : Z3.Opts@@ -52,15 +53,28 @@ import qualified Data.Fixed as Fixed import           Data.Monoid ( Monoid(..) ) +#if MIN_VERSION_base(4,9,0)+import           Data.Semigroup ( Semigroup (..) )+#endif+ --------------------------------------------------------------------- -- Configuration  -- | Z3 configuration. newtype Opts = Opts [Opt] +#if MIN_VERSION_base(4,9,0)+instance Semigroup Opts where+  Opts ps1 <> Opts ps2 = Opts (ps1 ++ ps2)+#endif+ instance Monoid Opts where   mempty = Opts []-  mappend (Opts ps1) (Opts ps2) = Opts (ps1++ps2)+#if MIN_VERSION_base(4,9,0)+  mappend = (<>)+#else+  Opts ps1 `mappend` Opts ps2 = Opts (ps1 ++ ps2)+#endif  singleton :: Opt -> Opts singleton o = Opts [o]

@@ -1,5 +1,5 @@ Name:                z3-Version:             4.3+Version:             4.3.1 Synopsis:            Bindings for the Z3 Theorem Prover Description:     Bindings for the Z3 4./x/ Theorem Prover (<https://github.com/Z3Prover/z3>).@@ -67,7 +67,8 @@                          ForeignFunctionInterface                          MultiParamTypeClasses -    Other-extensions:    DeriveDataTypeable+    Other-extensions:    CPP+                         DeriveDataTypeable                          EmptyDataDecls                          GeneralizedNewtypeDeriving                          PatternGuards@@ -105,6 +106,7 @@                        Example.Monad.FuncModel                        Example.Monad.Interpolation                        Example.Monad.MutuallyRecursive+                       Example.Monad.ParserInterface                        Example.Monad.Quantifiers                        Example.Monad.QuantifierElimination                        Example.Monad.ToSMTLib