boolector 0.0.0.7 → 0.0.0.8

raw patch · 6 files changed

+110/−19 lines, 6 filesdep +timePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: time

API changes (from Hackage documentation)

Files

• boolector.cabal +12/−2
• src/Boolector.hs +65/−13
• src/Boolector/Foreign.chs +5/−0
• test/API_Usage_Example.hs +2/−2
• test/Const_Example.hs +24/−0
• test/GetSetSymbol_Example.hs +2/−2

@@ -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 @@         containers,         mtl,         temporary,-        directory+        directory,+        time    ghc-options: -Wall -fno-warn-orphans   build-tools:      c2hs@@ -113,5 +114,14 @@                , boolector   Type: exitcode-stdio-1.0   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

@@ -209,6 +209,10 @@                  , unsignedBvAssignment                  , signedBvAssignment                  , boolAssignment+                 -- ** Constant nodes+                 , boolConst+                 , signedBvConst+                 , unsignedBvConst                  -- ** Sorts                  , Sort                  , SortTy, sortTy@@ -245,8 +249,11 @@ 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 @@  -- | 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 @@   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 @@  -- | 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 @@ 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 @@ -- 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 @@ 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 @@ 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

@@ -122,6 +122,7 @@   , getFunArity   , getSymbol   , setSymbol+  , getBits   , getWidth   , getIndexWidth   , isConst@@ -787,6 +788,10 @@  -- | 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. --

@@ -6,8 +6,8 @@  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

@@ -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 ()+

@@ -10,8 +10,8 @@  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