boolector 0.0.0.2 → 0.0.0.3

raw patch · 7 files changed

+80/−33 lines, 7 filesdep +directorydep +temporaryPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: directory, temporary

API changes (from Hackage documentation)

Files

• boolector.cabal +4/−2
• src/Boolector.hs +43/−24
• src/Boolector/Foreign.chs +27/−3
• test/API_Usage_Example.hs +1/−1
• test/Arith_Example.hs +2/−0
• test/Array_Example.hs +1/−1
• test/GetSetSymbol_Example.hs +2/−2

@@ -1,5 +1,5 @@ name:                boolector-version:             0.0.0.2+version:             0.0.0.3 synopsis:            Haskell bindings for the Boolector SMT solver description: @@ -33,7 +33,9 @@   build-depends:         base >= 4.7 && < 5,         containers,-        mtl+        mtl,+        temporary,+        directory    ghc-options: -Wall -fno-warn-orphans   build-tools:      c2hs

@@ -219,10 +219,11 @@                  , isFunSort                  , funSortCheck                  -- * Debug dumping-                 , dumpBtorNode-                 , dumpSmt2Node-                 , dumpBtor-                 , dumpSmt2+                 , dump+                 , dumpNode+                 , dumpToString+                 , dumpNodeToString+                 , DumpFormat(..)                  ) where  import Boolector.Foreign (Option(..), Status(..), Node, Sort)@@ -975,29 +976,47 @@ -- Dumping -- --- | Recursively dump @node@ to file in BTOR_ format.-dumpBtorNode :: MonadBoolector m => FilePath -> Node -> m ()-dumpBtorNode path node = do-  file <- liftIO $ B.fopen path "w"-  liftBoolector2 B.dumpBtorNode file node+-- | Output dump format.+data DumpFormat = DumpBtor | DumpSMT2+      deriving (Eq, Show) --- | Recursively dump @node@ to file in SMT-LIB v2 format.-dumpSmt2Node :: MonadBoolector m => FilePath -> Node -> m ()-dumpSmt2Node path node = do-  file <- liftIO $ B.fopen path "w"-  liftBoolector2 B.dumpSmt2Node file node+-- | Recursively dump @node@ to file in BTOR or SMT-LIB v2 format.+dumpNode :: MonadBoolector m => DumpFormat -> FilePath -> Node -> m ()+dumpNode fmt path node = do+  btor <- unBoolectorState `liftM` getBoolectorState+  liftIO $ B.withDumpFile path $ \file -> dumper btor file node+  where dumper = case fmt of+                  DumpBtor -> B.dumpBtorNode+                  _        -> B.dumpSmt2Node --- | Dump formula to file in BTOR_ format.-dumpBtor :: MonadBoolector m => FilePath -> m ()-dumpBtor path = do-  file <- liftIO $ B.fopen path "w"-  liftBoolector1 B.dumpBtor file+-- | Dump formula to file in BTOR or SMT-LIB v2 format.+dump :: MonadBoolector m => DumpFormat -> FilePath -> m ()+dump fmt path = do+  btor <- unBoolectorState `liftM` getBoolectorState+  liftIO $ B.withDumpFile path (dumper btor)+  where dumper = case fmt of+                  DumpBtor -> B.dumpBtor+                  _        -> B.dumpSmt2 --- | Dumps formula to file in SMT-LIB v2 format.-dumpSmt2 :: MonadBoolector m => FilePath -> m ()-dumpSmt2 path = do-  file <- liftIO $ B.fopen path "w"-  liftBoolector1 B.dumpSmt2 file+-- | Same as 'dumpNode', but returns string.+-- TODO: this is super slow, we should request feature from boolector.+dumpNodeToString :: MonadBoolector m => DumpFormat -> Node -> m String+dumpNodeToString fmt node = do+  btor <- unBoolectorState `liftM` getBoolectorState+  liftIO $ B.withTempDumpFile (\file -> dumper btor file node)+  where dumper = case fmt of+                  DumpBtor -> B.dumpBtorNode+                  _        -> B.dumpSmt2Node++-- | Same as 'dump', but returns string.+-- TODO: this is super slow, we should request feature from boolector.+dumpToString :: MonadBoolector m => DumpFormat -> m String+dumpToString fmt = do+  btor <- unBoolectorState `liftM` getBoolectorState+  liftIO $ B.withTempDumpFile (dumper btor)+  where dumper = case fmt of+                  DumpBtor -> B.dumpBtor+                  _        -> B.dumpSmt2  -- -- Helpers

@@ -152,7 +152,7 @@   , dumpBtor   , dumpSmt2   -- * Helpers-  , fopen+  , withDumpFile, withTempDumpFile    , setTerm   ) where @@ -162,6 +162,9 @@ import Foreign.C  import Control.Monad+import Control.Exception (bracket, finally, onException)+import System.IO.Temp+import System.Directory (removeFile)  {#context lib = "boolector" prefix = "boolector_" #} @@ -900,10 +903,31 @@ --  -- | POSIX files-{#pointer *FILE as File foreign finalizer fclose newtype#}+{#pointer *FILE as File foreign newtype#} --- | Expose POSIX file open.+-- | POSIX fopen. {#fun fopen as ^ {`String', `String'} -> `File' #}++-- | POSIX fclose.+{#fun fclose as ^ {`File'} -> `()' #}++-- | POSIX fflush.+{#fun fflush as ^ {`File'} -> `()' #}++-- | Helper for writing to dump file.+withDumpFile :: String+             -> (File -> IO ())+             -> IO ()+withDumpFile path act = bracket+  (fopen path "w") fclose+  (\fileHandle -> act fileHandle >> fflush fileHandle)++-- | Helper for writing to dump file.+withTempDumpFile :: (File -> IO ()) -> IO String+withTempDumpFile act = do+  path <- emptySystemTempFile "haskell-boolector"+  withDumpFile path act `onException` removeFile path+  readFile path `finally` removeFile path  -- | Recursively dump @node@ to file in BTOR_ format. {#fun dump_btor_node as ^ { `Btor' , `File', `Node' } -> `()' #}

@@ -30,7 +30,7 @@     B.assert =<< B.ugt y one      -- Dump the corresponding SMT Lib 2 to a file-    B.dumpSmt2 "dump_example.smt2"+    B.dump B.DumpSMT2 "dump_example.smt2"      -- Check satisfiability     B.Sat <- B.sat

@@ -32,6 +32,8 @@     -- (assert (>= (* 2 x) (+ y z)))     do tmp1 <- B.mul two x        tmp2 <- B.add y z+       tmp2Str <- B.dumpNodeToString B.DumpSMT2 tmp2+       liftIO $ putStrLn $ "tmp2Str = " ++ tmp2Str        B.assert =<< B.sgte tmp1 tmp2      -- (assert (< (f x) (g x x)))

@@ -24,7 +24,7 @@     y' <- B.read arr x     w <- B.var u8 "w" -    B.dumpSmt2 "dump_example.smt2"+    B.dump B.DumpSMT2 "dump_example.smt2"     B.sat     mx  <- B.unsignedBvAssignment x     my <- B.unsignedBvAssignment y

@@ -41,8 +41,8 @@     B.assert =<< B.ugt x one     B.assert =<< B.ugt y one -    -- Dump the corresponding SMT Lib 2 to a file-    B.dumpSmt2 "dump_example.smt2"+    -- Dump the corresponding SMT Lib 2+    B.dumpToString B.DumpSMT2 >>= liftIO . putStrLn      -- Check satisfiability     B.Sat <- B.sat