summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDeianStefan <>2018-12-21 08:29:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2018-12-21 08:29:00 (GMT)
commit9d1ee7aae9359b71a1ae3fd5241ae4321033e342 (patch)
treeff302f8999bef5462f5f7e490c130b613e9a1e94
parentc86e5117b0f64456eb21e3b1c6dff60234b4dfa4 (diff)
version 0.0.0.80.0.0.8
-rw-r--r--boolector.cabal14
-rw-r--r--src/Boolector.hs78
-rw-r--r--src/Boolector/Foreign.chs5
-rw-r--r--test/API_Usage_Example.hs4
-rw-r--r--test/Const_Example.hs24
-rw-r--r--test/GetSetSymbol_Example.hs4
6 files changed, 110 insertions, 19 deletions
diff --git a/boolector.cabal b/boolector.cabal
index 3267fbe..bd96c72 100644
--- a/boolector.cabal
+++ b/boolector.cabal
@@ -1,5 +1,5 @@
name: boolector
-version: 0.0.0.7
+version: 0.0.0.8
synopsis: Haskell bindings for the Boolector SMT solver
description:
@@ -35,7 +35,8 @@ library
containers,
mtl,
temporary,
- directory
+ directory,
+ time
ghc-options: -Wall -fno-warn-orphans
build-tools: c2hs
@@ -115,3 +116,12 @@ Test-Suite UF_Example2
main-is: UF_Example2.hs
extra-libraries: boolector
hs-source-dirs: test
+
+Test-Suite Const_Example
+ default-language: Haskell2010
+ Build-Depends: base >= 4.7 && < 5
+ , boolector
+ Type: exitcode-stdio-1.0
+ main-is: Const_Example.hs
+ extra-libraries: boolector
+ hs-source-dirs: test
diff --git a/src/Boolector.hs b/src/Boolector.hs
index 0d02020..70016ed 100644
--- a/src/Boolector.hs
+++ b/src/Boolector.hs
@@ -209,6 +209,10 @@ module Boolector ( -- * Boolector monadic computations
, unsignedBvAssignment
, signedBvAssignment
, boolAssignment
+ -- ** Constant nodes
+ , boolConst
+ , signedBvConst
+ , unsignedBvConst
-- ** Sorts
, Sort
, SortTy, sortTy
@@ -245,7 +249,10 @@ import Data.Word
import Control.Applicative ((<$>))
import Control.Monad.State.Strict
import Control.Exception hiding (assert)
-import Control.Concurrent
+
+import Data.Time.Clock
+import Data.Time.Clock.TAI
+import Data.Time.Clock.System
import Prelude hiding (read, not, and, or, const, concat, repeat)
import qualified Prelude as Prelude
@@ -284,7 +291,7 @@ runBoolector bState act = runStateT (unBoolector $ createDefaultSorts >> act) bS
-- | Create new Boolector state with optional timeout. By default, we enable
-- support for model generation and incremental solving.
-newBoolectorState :: Maybe Int -> IO BoolectorState
+newBoolectorState :: Maybe Integer -> IO BoolectorState
newBoolectorState Nothing = do
b <- B.new
B.setOpt b OPT_MODEL_GEN 2
@@ -292,12 +299,12 @@ newBoolectorState Nothing = do
B.setOpt b OPT_INCREMENTAL 1
return $ BoolectorState b emptyBoolectorCache
newBoolectorState (Just time) = do
- term <- newMVar 0
btorState@(BoolectorState b _) <- newBoolectorState Nothing
+ t0 <- systemToTAITime `liftM` getSystemTime
B.setTerm b $ \_ -> do
- readMVar term
- void $ forkIO $ do threadDelay $ time * 1000
- putMVar term 1 -- this will cause boolector eval to fail if not done
+ t1 <- systemToTAITime `liftM` getSystemTime
+ let shouldTerminate = diffAbsoluteTime t1 t0 > secondsToDiffTime time
+ return $ if shouldTerminate then 1 else 0
return btorState
-- | Set option.
@@ -406,7 +413,7 @@ zero = mkNode "zero" . liftBoolector1 B.zero . _sort
-- | Create bit vector constant of sort @sort@, where each bit is set to one.
ones :: MonadBoolector m => Sort -> m Node
-ones srt = mkNode onesStr $ liftBoolector1 B.one $ _sort srt
+ones srt = mkNode onesStr $ liftBoolector1 B.ones $ _sort srt
where onesStr = "0b" ++ replicate nr '1'
nr = case sortTy srt of
BoolSort -> 1
@@ -887,6 +894,10 @@ getSymbol = liftBoolector1 B.getSymbol . _node
setSymbol :: MonadBoolector m => Node -> String -> m ()
setSymbol n str = liftBoolector2 B.setSymbol (_node n) str
+-- | Get the bit vector of a constant node as a bit string.
+getBits :: MonadBoolector m => Node -> m String
+getBits = liftBoolector1 B.getBits . _node
+
-- | Get the bit width of an expression.
--
-- If the expression is an array, it returns the bit width of the array
@@ -937,6 +948,51 @@ isFun = liftBoolector1 B.isFun . _node
-- Models.
--
+-- | Get the bool value of a constant node if it is constant.
+boolConst :: MonadBoolector m => Node -> m (Maybe Bool)
+boolConst node = do
+ cnst <- isConst node
+ if cnst
+ then do str <- getBits node
+ Just `liftM` bitsToBool str
+ else return Nothing
+
+-- | Get the unsigned integer value of a constant node if it is constant.
+unsignedBvConst :: MonadBoolector m => Node -> m (Maybe Integer)
+unsignedBvConst node = do
+ cnst <- isConst node
+ if cnst
+ then do str <- getBits node
+ Just `liftM` bitsToUnsignedInteger str
+ else return Nothing
+
+-- | Get the signed integer value of a constant node if it is constant.
+signedBvConst :: MonadBoolector m => Node -> m (Maybe Integer)
+signedBvConst node = do
+ cnst <- isConst node
+ if cnst
+ then do str <- getBits node
+ val <- bitsToUnsignedInteger str
+ w <- getWidth node
+ let max_signed_w = 2 ^ pred w
+ return . Just $ if val >= max_signed_w
+ then val - (2*max_signed_w)
+ else val
+ else return Nothing
+
+-- | Helper for converting bit-string to an unsigned integer.
+bitsToUnsignedInteger :: MonadBoolector m => String -> m Integer
+bitsToUnsignedInteger str = do
+ when (Prelude.not $ all isDigit str) $ error $ "getModelVal: not numeric: " ++ str
+ liftIO $ evaluate $ foldl (\ n c -> 2 * n + Prelude.read [c]) 0 str
+
+-- | Helper for converting bit-string to a boolean.
+bitsToBool :: MonadBoolector m => String -> m Bool
+bitsToBool str = liftIO $ evaluate $ case str of
+ "0" -> False
+ "1" -> True
+ _ -> error $ "bitsToBool: not boolean: " ++ str
+
-- | Generate an assignment string for bit vector expression if
-- boolector_sat has returned BOOLECTOR_SAT and model generation has been
-- enabled.
@@ -951,8 +1007,7 @@ bvAssignment = liftBoolector1 B.bvAssignment . _node
unsignedBvAssignment :: MonadBoolector m => Node -> m Integer
unsignedBvAssignment node = do
str <- bvAssignment node
- when (Prelude.not $ all isDigit str) $ error $ "getModelVal: not numeric: " ++ str
- liftIO $ evaluate $ foldl (\ n c -> 2 * n + Prelude.read [c]) 0 str
+ bitsToUnsignedInteger str
-- | Get signed integer value from model.
signedBvAssignment :: MonadBoolector m => Node -> m Integer
@@ -968,10 +1023,7 @@ signedBvAssignment node = do
boolAssignment :: MonadBoolector m => Node -> m Bool
boolAssignment node = do
str <- bvAssignment node
- liftIO $ evaluate $ case str of
- "0" -> False
- "1" -> True
- _ -> error $ "boolAssignment: not boolean: " ++ str
+ bitsToBool str
--
-- Sorts
diff --git a/src/Boolector/Foreign.chs b/src/Boolector/Foreign.chs
index 0d4d3dc..30c0575 100644
--- a/src/Boolector/Foreign.chs
+++ b/src/Boolector/Foreign.chs
@@ -122,6 +122,7 @@ module Boolector.Foreign (
, getFunArity
, getSymbol
, setSymbol
+ , getBits
, getWidth
, getIndexWidth
, isConst
@@ -788,6 +789,10 @@ getSymbol hbtor hnode = withBtor hbtor $ \cbtor ->
-- | Set the symbol of an expression.
{#fun set_symbol as ^ { `Btor' , `Node', `String' } -> `()' #}
+-- | Get the bit vector of a constant node as a bit string.
+{#fun get_bits as ^ { `Btor' , `Node' } -> `String' #}
+
+
-- | Get the bit width of an expression.
--
-- If the expression is an array, it returns the bit width of the array
diff --git a/test/API_Usage_Example.hs b/test/API_Usage_Example.hs
index dcbaa56..4b51505 100644
--- a/test/API_Usage_Example.hs
+++ b/test/API_Usage_Example.hs
@@ -6,8 +6,8 @@ import Control.Concurrent
main :: IO ()
main = do
- -- Create new Boolector state with a 1000ms timeout
- bs <- B.newBoolectorState (Just 1000)
+ -- Create new Boolector state with a 1s timeout
+ bs <- B.newBoolectorState (Just 1)
B.evalBoolector bs $ do
-- Create a 8-bit bit-vector
u8 <- B.bitvecSort 8
diff --git a/test/Const_Example.hs b/test/Const_Example.hs
new file mode 100644
index 0000000..6a77f37
--- /dev/null
+++ b/test/Const_Example.hs
@@ -0,0 +1,24 @@
+import qualified Boolector as B
+
+import Control.Monad.IO.Class
+import Control.Exception (assert)
+import Control.Concurrent
+
+main :: IO ()
+main = do
+ -- Create new Boolector state with a 1s timeout
+ bs <- B.newBoolectorState (Just 1)
+ B.evalBoolector bs $ do
+ -- Create a 8-bit bit-vector
+ u8 <- B.bitvecSort 8
+
+ -- Create a constant value and two variables of sort u8
+ c <- B.unsignedInt 35 u8
+ x <- B.var u8 "x"
+
+ -- Get model
+ mc <- B.signedBvConst c
+ mx <- B.signedBvConst x
+ assert (mc == Just 35) $ return ()
+ assert (mx == Nothing) $ return ()
+
diff --git a/test/GetSetSymbol_Example.hs b/test/GetSetSymbol_Example.hs
index 305bf77..95454a8 100644
--- a/test/GetSetSymbol_Example.hs
+++ b/test/GetSetSymbol_Example.hs
@@ -10,8 +10,8 @@ import Control.Concurrent
main :: IO ()
main = do
- -- Create new Boolector state with a 1000ms timeout
- bs <- B.newBoolectorState (Just 1000)
+ -- Create new Boolector state with a 1s timeout
+ bs <- B.newBoolectorState (Just 1)
B.evalBoolector bs $ do
-- Create a 8-bit bit-vector
u8 <- B.bitvecSort 8