summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDeianStefan <>2018-07-07 03:43:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2018-07-07 03:43:00 (GMT)
commitbdad9c7c1fab44586abef9add8879c629017daa3 (patch)
treef9930ec34646d20fb41557612c5c49a0d964184c
parentb8ec3a18a186daa33a3a76e564ae67469607e6ec (diff)
version 0.0.0.30.0.0.3
-rw-r--r--boolector.cabal6
-rw-r--r--src/Boolector.hs73
-rw-r--r--src/Boolector/Foreign.chs30
-rw-r--r--test/API_Usage_Example.hs2
-rw-r--r--test/Arith_Example.hs2
-rw-r--r--test/Array_Example.hs2
-rw-r--r--test/GetSetSymbol_Example.hs4
7 files changed, 83 insertions, 36 deletions
diff --git a/boolector.cabal b/boolector.cabal
index 2375c30..c640636 100644
--- a/boolector.cabal
+++ b/boolector.cabal
@@ -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 @@ library
build-depends:
base >= 4.7 && < 5,
containers,
- mtl
+ mtl,
+ temporary,
+ directory
ghc-options: -Wall -fno-warn-orphans
build-tools: c2hs
diff --git a/src/Boolector.hs b/src/Boolector.hs
index 725ffc2..ccd8cc2 100644
--- a/src/Boolector.hs
+++ b/src/Boolector.hs
@@ -219,10 +219,11 @@ module Boolector ( -- * Boolector monadic computations
, 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 @@ funSortCheck = liftBoolector2 B.funSortCheck
-- 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
-
--- | 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
-
--- | 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
-
--- | 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
+-- | Output dump format.
+data DumpFormat = DumpBtor | DumpSMT2
+ deriving (Eq, Show)
+
+-- | 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 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
+
+-- | 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
diff --git a/src/Boolector/Foreign.chs b/src/Boolector/Foreign.chs
index a7b9143..0d4d3dc 100644
--- a/src/Boolector/Foreign.chs
+++ b/src/Boolector/Foreign.chs
@@ -152,7 +152,7 @@ module Boolector.Foreign (
, dumpBtor
, dumpSmt2
-- * Helpers
- , fopen
+ , withDumpFile, withTempDumpFile
, setTerm
) where
@@ -162,6 +162,9 @@ import Foreign hiding (xor, new)
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,11 +903,32 @@ withSorts (hx:hxs) f = withSort hx $ \cx -> withSorts hxs $ \cxs -> f (cx:cxs)
--
-- | 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' } -> `()' #}
diff --git a/test/API_Usage_Example.hs b/test/API_Usage_Example.hs
index 3c80705..665fe59 100644
--- a/test/API_Usage_Example.hs
+++ b/test/API_Usage_Example.hs
@@ -30,7 +30,7 @@ main = do
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
diff --git a/test/Arith_Example.hs b/test/Arith_Example.hs
index 4fff224..3c59faa 100644
--- a/test/Arith_Example.hs
+++ b/test/Arith_Example.hs
@@ -32,6 +32,8 @@ main = do
-- (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)))
diff --git a/test/Array_Example.hs b/test/Array_Example.hs
index ab84699..501f820 100644
--- a/test/Array_Example.hs
+++ b/test/Array_Example.hs
@@ -24,7 +24,7 @@ main = do
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
diff --git a/test/GetSetSymbol_Example.hs b/test/GetSetSymbol_Example.hs
index fe5cd23..305bf77 100644
--- a/test/GetSetSymbol_Example.hs
+++ b/test/GetSetSymbol_Example.hs
@@ -41,8 +41,8 @@ main = do
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