summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDeianStefan <>2018-09-15 21:17:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2018-09-15 21:17:00 (GMT)
commita4f5cd58c9698e26453f056e26a2aedd92eb948b (patch)
tree9d632017897df59d3f608f3b4551a0f77cf99033
parent18c70bf17fb7f917fd3cfa39ca8fb63f037bb7d9 (diff)
version 0.0.0.60.0.0.6
-rw-r--r--boolector.cabal2
-rw-r--r--src/Boolector.hs63
2 files changed, 52 insertions, 13 deletions
diff --git a/boolector.cabal b/boolector.cabal
index 09947ca..27e4605 100644
--- a/boolector.cabal
+++ b/boolector.cabal
@@ -1,5 +1,5 @@
name: boolector
-version: 0.0.0.5
+version: 0.0.0.6
synopsis: Haskell bindings for the Boolector SMT solver
description:
diff --git a/src/Boolector.hs b/src/Boolector.hs
index 5c650e3..c5d3a0e 100644
--- a/src/Boolector.hs
+++ b/src/Boolector.hs
@@ -77,6 +77,7 @@ module Boolector ( -- * Boolector monadic computations
-- ** Boolector state
, BoolectorState
, newBoolectorState
+ , createDefaultSorts
-- ** Options and configurations
, Option(..)
, setOpt
@@ -273,12 +274,12 @@ newtype Boolector a = Boolector { unBoolector :: StateT BoolectorState IO a }
-- | Evaluate a Boolector action with a given configurations.
evalBoolector :: BoolectorState -> Boolector a -> IO a
-evalBoolector bState act = evalStateT (unBoolector act) bState
+evalBoolector bState act = evalStateT (unBoolector $ createDefaultSorts >> act) bState
-- | Like 'evalBoolector', but take an explicit starting BoolectorState, and
-- return the final BoolectorState
runBoolector :: BoolectorState -> Boolector a -> IO (a, BoolectorState)
-runBoolector bState act = runStateT (unBoolector act) bState
+runBoolector bState act = runStateT (unBoolector $ createDefaultSorts >> act) bState
-- | Create new Boolector state with optional timeout. By default, we enable
-- support for model generation and incremental solving.
@@ -468,33 +469,58 @@ slice :: MonadBoolector m
-> Word32 -- ^ Upper index which must be greater than or equal to zero, and less than the bit width of @node@.
-> Word32 -- ^ Lower index which must be greater than or equal to zero, and less than or equal to @upper@.
-> m Node
-slice n u l = mkNode ["slice", show n, show u, show l] $
- liftBoolector3 B.slice (_node n) (fromIntegral u) (fromIntegral l)
+slice n u l = do
+ -- Create sort if not already in cache
+ void $ bitvecSort (fromIntegral $ u - l + 1)
+ --
+ mkNode ["slice", show n, show u, show l] $
+ liftBoolector3 B.slice (_node n) (fromIntegral u) (fromIntegral l)
-- | Create unsigned extension.
--
-- The bit vector @node@ is padded with @width@ * zeroes.
uext :: MonadBoolector m => Node -> Word32 -> m Node
-uext n w = mkNode ["uext", show n, show w] $
- liftBoolector2 B.uext (_node n) (fromIntegral w)
+uext n w = do
+ -- Create sort if not already in cache
+ nw <- getWidth n
+ void $ bitvecSort (fromIntegral $ nw + w)
+ --
+ mkNode ["uext", show n, show w] $
+ liftBoolector2 B.uext (_node n) (fromIntegral w)
-- | Create signed extension.
--
-- The bit vector @node@ is padded with @width@ bits where the value
-- depends on the value of the most significant bit of node @n@.
sext :: MonadBoolector m => Node -> Word32 -> m Node
-sext n w = mkNode ["sext", show n, show w] $
- liftBoolector2 B.sext (_node n) (fromIntegral w)
+sext n w = do
+ -- Create sort if not already in cache
+ nw <- getWidth n
+ void $ bitvecSort (fromIntegral $ nw + w)
+ --
+ mkNode ["sext", show n, show w] $
+ liftBoolector2 B.sext (_node n) (fromIntegral w)
-- | Create the concatenation of two bit vectors.
concat :: MonadBoolector m => Node -> Node -> m Node
-concat n1 n2 = mkNode ["concat", show n1, show n2] $
- liftBoolector2 B.concat (_node n1) (_node n2)
+concat n1 n2 = do
+ -- Create sort if not already in cache
+ nw1 <- getWidth n1
+ nw2 <- getWidth n2
+ void $ bitvecSort (fromIntegral $ nw1 + nw2)
+ --
+ mkNode ["concat", show n1, show n2] $
+ liftBoolector2 B.concat (_node n1) (_node n2)
-- | Create @n@ concatenations of a given node @node@.
repeat :: MonadBoolector m => Node -> Word32 -> m Node
-repeat n w = mkNode ["repeat", show n, show w] $
- liftBoolector2 B.repeat (_node n) (fromIntegral w)
+repeat n w = do
+ -- Create sort if not already in cache
+ nw <- getWidth n
+ void $ bitvecSort (fromIntegral $ nw * w)
+ --
+ mkNode ["repeat", show n, show w] $
+ liftBoolector2 B.repeat (_node n) (fromIntegral w)
-- | Create boolean implication.
implies :: MonadBoolector m => Node -> Node -> m Node
@@ -965,6 +991,19 @@ data Sort = Sort { sortTy :: SortTy -- ^ Get sort type
instance Show Sort where
show = show . sortTy
+-- | Create some default, sane sorts.
+createDefaultSorts :: Boolector ()
+createDefaultSorts = do
+ void $ boolSort
+ void $ bitvecSort 1
+ void $ bitvecSort 2
+ void $ bitvecSort 4
+ void $ bitvecSort 8
+ void $ bitvecSort 16
+ void $ bitvecSort 32
+ void $ bitvecSort 64
+ void $ bitvecSort 128
+
-- | Create Boolean sort.
boolSort :: Boolector Sort
boolSort = do