boolector 0.0.0.3 → 0.0.0.4

raw patch · 5 files changed

+414/−147 lines, 5 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• boolector.cabal +19/−1
• src/Boolector.hs +257/−145
• test/API_Usage_Example.hs +5/−1
• test/Arith_Example2.hs +93/−0
• test/UF_Example2.hs +40/−0

@@ -1,5 +1,5 @@ name:                boolector-version:             0.0.0.3+version:             0.0.0.4 synopsis:            Haskell bindings for the Boolector SMT solver description: @@ -79,11 +79,29 @@   extra-libraries:  boolector   hs-source-dirs: test +Test-Suite Arith_Example2+  default-language: Haskell2010+  Build-Depends: base >= 4.7 && < 5+               , boolector+  Type: exitcode-stdio-1.0+  main-is: Arith_Example2.hs+  extra-libraries:  boolector+  hs-source-dirs: test+ Test-Suite GetSetSymbol_Example   default-language: Haskell2010   Build-Depends: base >= 4.7 && < 5                , boolector   Type: exitcode-stdio-1.0   main-is: GetSetSymbol_Example.hs+  extra-libraries:  boolector+  hs-source-dirs: test++Test-Suite UF_Example2+  default-language: Haskell2010+  Build-Depends: base >= 4.7 && < 5+               , boolector+  Type: exitcode-stdio-1.0+  main-is: UF_Example2.hs   extra-libraries:  boolector   hs-source-dirs: test

@@ -1,3 +1,4 @@+{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-} {-|  This module exposes a DSL for writing symbolic computations atop the Boolector@@ -154,22 +155,23 @@                  , ror                  -- *** Arithmetic operations                  , add-                 , uaddo-                 , saddo                  , inc                  , sub-                 , usubo-                 , ssubo                  , dec                  , mul-                 , umulo-                 , smulo                  , udiv                  , sdiv-                 , sdivo                  , urem                  , srem                  , smod+                 -- **** Overflow detection+                 , uaddo+                 , saddo+                 , usubo+                 , ssubo+                 , umulo+                 , smulo+                 , sdivo                  -- *** Comparison operations                  , ult                  , slt@@ -208,6 +210,7 @@                  , boolAssignment                  -- ** Sorts                  , Sort+                 , SortTy, sortTy                  , boolSort                  , bitvecSort                  , funSort@@ -226,16 +229,18 @@                  , DumpFormat(..)                  ) where -import Boolector.Foreign (Option(..), Status(..), Node, Sort)+import Boolector.Foreign (Option(..), Status(..)) import qualified Boolector.Foreign as B  import Data.Char (isDigit)+import Data.Maybe (listToMaybe) import Data.Map (Map) import qualified Data.Map as Map import Data.IntMap (IntMap) import qualified Data.IntMap as IntMap import Data.Word +import Control.Applicative ((<$>)) import Control.Monad.State.Strict import Control.Exception hiding (assert) import Control.Concurrent@@ -313,15 +318,15 @@  -- | Add a constraint. assert :: MonadBoolector m => Node -> m ()-assert = liftBoolector1 B.assert+assert = liftBoolector1 B.assert . _node  -- | Add an assumption. assume :: MonadBoolector m => Node -> m ()-assume = liftBoolector1 B.assume+assume = liftBoolector1 B.assume . _node  -- | Determine if assumption node is a failed assumption. failed :: MonadBoolector m => Node -> m Bool-failed = liftBoolector1 B.failed+failed = liftBoolector1 B.failed . _node  -- | Add all assumptions as assertions. fixateAssumptions :: MonadBoolector m => m ()@@ -360,6 +365,13 @@ -- Expressions -- +-- | Node data type wrapping the underlying Boolector node with a show string.+data Node = Node { _node     :: B.Node+                 , _showNode :: String } deriving (Eq, Ord)++instance Show Node where+  show = _showNode+ -- | Like true and false bool :: MonadBoolector m => Bool -> m Node bool True  = true@@ -368,35 +380,40 @@ -- | Create constant true. This is represented by the bit vector constant one -- with bit width one. true :: MonadBoolector m => m Node-true = liftBoolector0 B.true+true = mkNode "true" $ liftBoolector0 B.true  -- | Create bit vector constant zero with bit width one. false :: MonadBoolector m => m Node-false = liftBoolector0 B.false+false = mkNode "false" $ liftBoolector0 B.false  -- | Create bit vector constant representing the bit vector @bits@. const :: MonadBoolector m => String -> m Node-const = liftBoolector1 B.const+const str = mkNode ("0b" ++ str) $ liftBoolector1 B.const str  -- | Create bit vector constant representing the decimal number @str@. constd :: MonadBoolector m => Sort -> String -> m Node-constd = liftBoolector2 B.constd+constd srt str = mkNode str $ liftBoolector2 B.constd (_sort srt) str  -- | Create bit vector constant representing the hexadecimal number @str@. consth :: MonadBoolector m => Sort -> String -> m Node-consth = liftBoolector2 B.consth+consth srt str = mkNode ("0x" ++ str) $ liftBoolector2 B.consth (_sort srt) str  -- | Create bit vector constant zero of sort @sort@. zero :: MonadBoolector m => Sort -> m Node-zero = liftBoolector1 B.zero+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 = liftBoolector1 B.ones+ones srt = mkNode onesStr $ liftBoolector1 B.one $ _sort srt+  where onesStr = "0b" ++ replicate nr '1'+        nr = case sortTy srt of+              BoolSort -> 1+              BitVecSort wNr -> fromIntegral wNr+              _ -> error "invalid sort"  -- | Create bit vector constant one of sort @sort@. one :: MonadBoolector m => Sort -> m Node-one = liftBoolector1 B.one+one = mkNode "1" . liftBoolector1 B.one . _sort  -- |  Create bit vector constant representing the unsigned integer @u@ of -- sort @sort@.@@ -404,7 +421,7 @@ -- The constant is obtained by either truncating bits or by unsigned extension -- (padding with zeroes). unsignedInt :: MonadBoolector m => Integer -> Sort -> m Node-unsignedInt i sort = liftBoolector2 B.unsignedInt (fromIntegral i) sort+unsignedInt i srt = constd srt (show i)  -- | Create bit vector constant representing the signed integer @i@ of sort -- @sort@.@@ -412,37 +429,38 @@ -- The constant is obtained by either truncating bits or by -- signed extension (padding with ones). signedInt :: MonadBoolector m => Integer -> Sort -> m Node-signedInt i sort = liftBoolector2 B.int (fromIntegral i) sort+signedInt i srt = constd srt (show i) + -- | Create a bit vector variable of sort @sort@. var :: MonadBoolector m => Sort -> String -> m Node-var = createNamedNode B.var+var srt str = mkNamedNode "var" B.var srt str  -- | Create the one's complement of bit vector @node@. not :: MonadBoolector m => Node -> m Node-not = liftBoolector1 B.not+not n1 = mkNode ["not", show n1] $ liftBoolector1 B.not (_node n1)  -- | Create the two's complement of bit vector @node@. neg :: MonadBoolector m => Node -> m Node-neg = liftBoolector1 B.neg+neg n1 = mkNode ["neg", show n1] $ liftBoolector1 B.neg (_node n1)  -- | Create *or* reduction of node @node@. -- -- All bits of node @node@ are combined by a Boolean *or*. redor :: MonadBoolector m => Node -> m Node-redor = liftBoolector1 B.redor+redor n1 = mkNode ["redor", show n1] $ liftBoolector1 B.redor (_node n1)  -- | Create *xor* reduction of node @node@. -- -- All bits of @node@ are combined by a Boolean *xor*. redxor :: MonadBoolector m => Node -> m Node-redxor = liftBoolector1 B.redxor+redxor n1 = mkNode ["redxor", show n1] $ liftBoolector1 B.redxor (_node n1)  -- | Create *and* reduction of node @node@. -- -- All bits of @node@ are combined by a Boolean *and*. redand :: MonadBoolector m => Node -> m Node-redand = liftBoolector1 B.redand+redand n = mkNode ["redand", show n] $ liftBoolector1 B.redand (_node n)  -- | Create a bit vector slice of @node@ from index @upper@ to index @lower@. slice :: MonadBoolector m@@ -450,50 +468,59 @@       -> 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 = (liftBoolector3 B.slice) n (fromIntegral u) (fromIntegral l)+slice n u l = 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 = (liftBoolector2 B.uext) n $ fromIntegral w+uext n 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 = liftBoolector2 B.sext n (fromIntegral w)+sext n 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 = liftBoolector2 B.concat+concat n1 n2 = 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 = liftBoolector2 B.repeat n (fromIntegral w)+repeat n w = mkNode ["repeat", show n, show w] $+             liftBoolector2 B.repeat (_node n) (fromIntegral w)  -- | Create boolean implication. implies :: MonadBoolector m => Node -> Node -> m Node-implies = liftBoolector2 B.implies+implies n1 n2 = mkNode ["implies", show n1, show n2] $+                liftBoolector2 B.implies (_node n1) (_node n2)  -- | Create Boolean equivalence. iff :: MonadBoolector m => Node -> Node -> m Node-iff = liftBoolector2 B.iff+iff n1 n2 = mkNode ["iff", show n1, show n2] $+            liftBoolector2 B.iff (_node n1) (_node n2)  -- | Create bit vector or array equality. -- -- Both operands are either bit vectors with the same bit width or arrays -- of the same type. eq :: MonadBoolector m => Node -> Node -> m Node-eq = liftBoolector2 B.eq+eq n1 n2 = mkNode ["eq", show n1, show n2] $+           liftBoolector2 B.eq (_node n1) (_node n2)  -- | Create bit vector or array inequality. -- -- Both operands are either bit vectors with the same bit width or arrays -- of the same type. ne :: MonadBoolector m => Node -> Node -> m Node-ne = liftBoolector2 B.ne+ne n1 n2 = mkNode ["ne", show n1, show n2] $+           liftBoolector2 B.ne (_node n1) (_node n2)  -- | Create an if-then-else. --@@ -505,7 +532,8 @@      -> Node -- ^ Then node      -> Node -- ^ Else node      -> m Node-cond = liftBoolector3 B.cond+cond n1 n2 n3 = mkNode ["cond", show n1, show n2, show n3] $+                liftBoolector3 B.cond (_node n1) (_node n2) (_node n3)  -- -- Bit-wise operations.@@ -513,27 +541,27 @@  -- | Create a bit vector *xor*. xor :: MonadBoolector m => Node -> Node -> m Node-xor = liftBoolector2 B.xor+xor n1 n2 = mkNode ["xor", show n1, show n2] $ liftBoolector2 B.xor (_node n1) (_node n2)  -- | Create a bit vector *xnor*. xnor :: MonadBoolector m => Node -> Node -> m Node-xnor = liftBoolector2 B.xnor+xnor n1 n2 = mkNode ["xnor", show n1, show n2] $ liftBoolector2 B.xnor (_node n1) (_node n2)  -- | Create a bit vector *and*. and  :: MonadBoolector m => Node -> Node -> m Node-and  = liftBoolector2 B.and+and n1 n2 = mkNode ["and", show n1, show n2] $ liftBoolector2 B.and (_node n1) (_node n2)  -- | Create a bit vector *nand*. nand :: MonadBoolector m => Node -> Node -> m Node-nand = liftBoolector2 B.nand+nand n1 n2 = mkNode ["nand", show n1, show n2] $ liftBoolector2 B.nand (_node n1) (_node n2)  -- | Create a bit vector *or*. or :: MonadBoolector m => Node -> Node -> m Node-or = liftBoolector2 B.or+or n1 n2 = mkNode ["or", show n1, show n2] $ liftBoolector2 B.or (_node n1) (_node n2)  -- | Create a bit vector *nor*. nor :: MonadBoolector m => Node -> Node -> m Node-nor = liftBoolector2 B.nor+nor n1 n2 = mkNode ["nor", show n1, show n2] $ liftBoolector2 B.nor (_node n1) (_node n2)  -- | Create a logical shift left. --@@ -543,7 +571,7 @@     => Node -- ^ First bit vector operand where the bit width is a power of two and greater than 1.     -> Node -- ^ Second bit vector operand with bit width log2 of the bit width of @n0@.     -> m Node-sll = liftBoolector2 B.sll+sll n1 n2 = mkNode ["sll", show n1, show n2] $ liftBoolector2 B.sll (_node n1) (_node n2)  -- | Create a logical shift right. --@@ -553,7 +581,7 @@     => Node -- ^ First bit vector operand where the bit width is a power of two and greater than 1.     -> Node -- ^ Second bit vector operand with bit width log2 of the bit width of @n0@.     -> m Node-srl = liftBoolector2 B.srl+srl n1 n2 = mkNode ["srl", show n1, show n2] $ liftBoolector2 B.srl (_node n1) (_node n2)  -- | Create an arithmetic shift right. --@@ -563,7 +591,7 @@     => Node -- ^ First bit vector operand where the bit width is a power of two and greater than 1.     -> Node -- ^ Second bit vector operand with bit width log2 of the bit width of @n0@.     -> m Node-sra = liftBoolector2 B.sra+sra n1 n2 = mkNode ["sra", show n1, show n2] $ liftBoolector2 B.sra (_node n1) (_node n2)  -- | Create a rotate left. --@@ -573,7 +601,7 @@     => Node -- ^ First bit vector operand where the bit width is a power of two and greater than 1.     -> Node -- ^ Second bit vector operand with bit width log2 of the bit width of @n0@.     -> m Node-rol = liftBoolector2 B.rol+rol n1 n2 = mkNode ["rol", show n1, show n2] $ liftBoolector2 B.rol (_node n1) (_node n2)  -- | Create a rotate right. --@@ -583,7 +611,7 @@     => Node -- ^ First bit vector operand where the bit width is a power of two and greater than 1.     -> Node -- ^ Second bit vector operand with bit width log2 of the bit width of @n0@.     -> m Node-ror = liftBoolector2 B.ror+ror n1 n2 = mkNode ["ror", show n1, show n2] $ liftBoolector2 B.ror (_node n1) (_node n2)  -- -- Arithmetic operations.@@ -591,107 +619,125 @@  -- | Create bit vector addition. add :: MonadBoolector m => Node -> Node -> m Node-add = liftBoolector2 B.add---- | Create an unsigned bit vector addition overflow detection.-uaddo :: MonadBoolector m => Node -> Node -> m Node-uaddo = liftBoolector2 B.uaddo---- | Create a signed bit vector addition overflow detection.-saddo :: MonadBoolector m => Node -> Node -> m Node-saddo = liftBoolector2 B.saddo+add n1 n2 = mkNode ["add", show n1, show n2] $ liftBoolector2 B.add (_node n1) (_node n2)  -- | Create bit vector expression that increments bit vector @node@ by one. inc :: Node ->  Boolector Node-inc = liftBoolector1 B.inc+inc n = mkNode ["inc", show n] $ liftBoolector1 B.inc (_node n)  -- | Create a bit vector subtraction. sub :: MonadBoolector m => Node -> Node -> m Node-sub = liftBoolector2 B.sub---- | Create an unsigned bit vector subtraction overflow detection.-usubo :: MonadBoolector m => Node -> Node -> m Node-usubo = liftBoolector2 B.usubo---- | Create a signed bit vector subtraction overflow detection.-ssubo :: MonadBoolector m => Node -> Node -> m Node-ssubo = liftBoolector2 B.ssubo+sub n1 n2 = mkNode ["sub", show n1, show n2] $ liftBoolector2 B.sub (_node n1) (_node n2)  -- | Create bit vector expression that decrements bit vector @node@ by one. dec :: MonadBoolector m => Node -> m Node-dec = liftBoolector1 B.dec+dec n = mkNode ["dec", show n] $ liftBoolector1 B.dec (_node n)  -- | Create a bitvector multiplication. mul :: MonadBoolector m => Node -> Node -> m Node-mul = liftBoolector2 B.mul---- | Create an unsigned bit vector multiplication overflow detection.-umulo :: MonadBoolector m => Node -> Node -> m Node-umulo = liftBoolector2 B.umulo---- | Create signed multiplication overflow detection.-smulo :: MonadBoolector m => Node -> Node -> m Node-smulo = liftBoolector2 B.smulo+mul n1 n2 = mkNode ["mul", show n1, show n2] $ liftBoolector2 B.mul (_node n1) (_node n2)  -- | Create unsigned division. udiv :: MonadBoolector m => Node -> Node -> m Node-udiv = liftBoolector2 B.udiv+udiv n1 n2 = mkNode ["udiv", show n1, show n2] $ liftBoolector2 B.udiv (_node n1) (_node n2)  -- | Create signed division. sdiv :: MonadBoolector m => Node -> Node -> m Node-sdiv = liftBoolector2 B.sdiv---- | Create a signed bit vector division overflow detection.-sdivo :: MonadBoolector m => Node -> Node -> m Node-sdivo = liftBoolector2 B.sdivo+sdiv n1 n2 = mkNode ["sdiv", show n1, show n2] $ liftBoolector2 B.sdiv (_node n1) (_node n2)  -- | Create an unsigned remainder. urem :: MonadBoolector m => Node -> Node -> m Node-urem = liftBoolector2 B.urem+urem n1 n2 = mkNode ["urem", show n1, show n2] $ liftBoolector2 B.urem (_node n1) (_node n2)  -- | Create a signed remainder. srem :: MonadBoolector m => Node -> Node -> m Node-srem = liftBoolector2 B.srem+srem n1 n2 = mkNode ["srem", show n1, show n2] $ liftBoolector2 B.srem (_node n1) (_node n2)  -- | Create a, signed remainder where its sign matches the sign of the divisor. smod :: MonadBoolector m => Node -> Node -> m Node-smod = liftBoolector2 B.smod+smod n1 n2 = mkNode ["smod", show n1, show n2] $ liftBoolector2 B.smod (_node n1) (_node n2)  --+-- Overflow detection+--++-- | Create an unsigned bit vector subtraction overflow detection.+-- Returns bit vector with bit-width one, which indicates if the operation+-- overflows.+usubo :: MonadBoolector m => Node -> Node -> m Node+usubo n1 n2 = mkNode ["usubo", show n1, show n2] $ liftBoolector2 B.usubo (_node n1) (_node n2)++-- | Create a signed bit vector subtraction overflow detection.+-- Returns bit vector with bit-width one, which indicates if the operation+-- overflows.+ssubo :: MonadBoolector m => Node -> Node -> m Node+ssubo n1 n2 = mkNode ["ssubo", show n1, show n2] $ liftBoolector2 B.ssubo (_node n1) (_node n2)++-- | Create an unsigned bit vector addition overflow detection.+-- Returns bit vector with bit-width one, which indicates if the operation+-- overflows.+uaddo :: MonadBoolector m => Node -> Node -> m Node+uaddo n1 n2 = mkNode ["uaddo", show n1, show n2] $ liftBoolector2 B.uaddo (_node n1) (_node n2)++-- | Create a signed bit vector addition overflow detection.+-- Returns bit vector with bit-width one, which indicates if the operation+-- overflows.+saddo :: MonadBoolector m => Node -> Node -> m Node+saddo n1 n2 = mkNode ["saddo", show n1, show n2] $ liftBoolector2 B.saddo (_node n1) (_node n2)++-- | Create an unsigned bit vector multiplication overflow detection.+-- Returns bit vector with bit-width one, which indicates if the operation+-- overflows.+umulo :: MonadBoolector m => Node -> Node -> m Node+umulo n1 n2 = mkNode ["umulo", show n1, show n2] $ liftBoolector2 B.umulo (_node n1) (_node n2)++-- | Create signed multiplication overflow detection.+-- Returns bit vector with bit-width one, which indicates if the operation+-- overflows.+smulo :: MonadBoolector m => Node -> Node -> m Node+smulo n1 n2 = mkNode ["smulo", show n1, show n2] $ liftBoolector2 B.smulo (_node n1) (_node n2)++-- | Create a signed bit vector division overflow detection.+-- Returns bit vector with bit-width one, which indicates if the operation+-- overflows.+sdivo :: MonadBoolector m => Node -> Node -> m Node+sdivo n1 n2 = mkNode ["sdivo", show n1, show n2] $ liftBoolector2 B.sdivo (_node n1) (_node n2)++-- -- Comparison operations. --  -- | Create an unsigned less than. ult :: MonadBoolector m => Node -> Node -> m Node-ult = liftBoolector2 B.ult+ult n1 n2 = mkNode ["ult", show n1, show n2] $ liftBoolector2 B.ult (_node n1) (_node n2)  -- | Create a signed less than. slt :: MonadBoolector m => Node -> Node -> m Node-slt = liftBoolector2 B.slt+slt n1 n2 = mkNode ["slt", show n1, show n2] $ liftBoolector2 B.slt (_node n1) (_node n2)  -- | Create an unsigned less than or equal. ulte :: MonadBoolector m => Node -> Node -> m Node-ulte = liftBoolector2 B.ulte+ulte n1 n2 = mkNode ["ulte", show n1, show n2] $ liftBoolector2 B.ulte (_node n1) (_node n2)  -- | Create a signed less than or equal. slte :: MonadBoolector m => Node -> Node -> m Node-slte = liftBoolector2 B.slte+slte n1 n2 = mkNode ["slte", show n1, show n2] $ liftBoolector2 B.slte (_node n1) (_node n2)  -- | Create an unsigned greater than. ugt :: MonadBoolector m => Node -> Node -> m Node-ugt = liftBoolector2 B.ugt+ugt n1 n2 = mkNode ["ugt", show n1, show n2] $ liftBoolector2 B.ugt (_node n1) (_node n2)  -- | Create a signed greater than. sgt :: MonadBoolector m => Node -> Node -> m Node-sgt = liftBoolector2 B.sgt+sgt n1 n2 = mkNode ["sgt", show n1, show n2] $ liftBoolector2 B.sgt (_node n1) (_node n2)  -- | Create an unsigned greater than or equal. ugte :: MonadBoolector m => Node -> Node -> m Node-ugte = liftBoolector2 B.ugte+ugte n1 n2 = mkNode ["ugte", show n1, show n2] $ liftBoolector2 B.ugte (_node n1) (_node n2)  -- | Create a signed greater than or equal. sgte :: MonadBoolector m => Node -> Node -> m Node-sgte = liftBoolector2 B.sgte+sgte n1 n2 = mkNode ["sgte", show n1, show n2] $ liftBoolector2 B.sgte (_node n1) (_node n2)  -- -- Array operations@@ -701,14 +747,14 @@ -- -- The name must be unique. array :: MonadBoolector m => Sort -> String -> m Node-array = createNamedNode B.array+array srt str = mkNamedNode "array" B.array srt str  -- | Create a read on array @n_array@ at position @n_index@. read :: MonadBoolector m      => Node -- ^ Array operand.      -> Node -- ^ Bit vector index. The bit width of @n_index@ must have the same bit width as the indices of @n_array@.      -> m Node-read = liftBoolector2 B.read+read n1 n2 = mkNode ["read", show n1, show n2] $ liftBoolector2 B.read (_node n1) (_node n2)  -- | Create a write on array @n_array@ at position @n_index@ with value -- @n_value@.@@ -722,7 +768,7 @@       -> Node -- ^ Bit vector index.       -> Node -- ^ Bit vector value.       -> m Node-write = liftBoolector3 B.write+write n1 n2 n3 = mkNode ["write", show n1, show n2, show n3] $ liftBoolector3 B.write (_node n1) (_node n2) (_node n3)  -- -- Functions@@ -732,7 +778,7 @@ -- -- The name must be unique. uf :: MonadBoolector m => Sort -> String -> m Node-uf = createNamedNode B.uf+uf srt str = mkNamedNode "uf" B.uf srt str  -- | Create function parameter of sort @sort@. --@@ -740,7 +786,7 @@ -- used to create functions. Once a parameter is bound to a function, it -- cannot be re-used in other functions. param :: MonadBoolector m => Sort -> String -> m Node-param = liftBoolector2 B.param+param srt str = mkNode ["param", show srt, str] $ liftBoolector2 B.param (_sort srt) str  -- | Create a function with body @node@ parameterized over parameters -- @param_nodes@.@@ -753,7 +799,7 @@     => [Node] -- ^ Parameters of function.     -> Node   -- ^ Function body parameterized over @param_nodes@.     -> m Node-fun = liftBoolector2 B.fun+fun n1 n2 = mkNode ["fun", show n1, show n2] $ liftBoolector2 B.fun (map _node n1) (_node n2)  -- | Create a function application on function @n_fun@ with arguments -- @arg_nodes@.@@ -761,7 +807,7 @@       => [Node] -- ^ Arguments to be applied.       -> Node   -- ^ Number of arguments to be applied.       -> m Node-apply = liftBoolector2 B.apply+apply n1 n2 = mkNode ["apply", show n1, show n2] $  liftBoolector2 B.apply (map _node n1) (_node n2)   --@@ -770,17 +816,17 @@  -- | Create a universally quantified term. forall :: MonadBoolector m-       => [Node] -- ^ Quantified variables-       -> Node   -- ^ Term where variables may occur+       => [Node] -- ^ Quantified variables (create with 'param')+       -> Node   -- ^ Term where variables may occur. (Cannot contain functions.)        -> m Node-forall = liftBoolector2 B.forall+forall n1 n2 = mkNode ["forall", show n1, show n2] $  liftBoolector2 B.forall (map _node n1) (_node n2)  -- | Create an existentially quantifed term. exists :: MonadBoolector m-       => [Node] -- ^ Quantified variables-       -> Node   -- ^ Term where variables may occur+       => [Node] -- ^ Quantified variables (create with 'param')+       -> Node   -- ^ Term where variables may occur. (Cannot contain functions.)        -> m Node-exists = liftBoolector2 B.exists+exists n1 n2 = mkNode ["exists", show n1, show n2] $  liftBoolector2 B.exists (map _node n1) (_node n2)  -- -- Accessors@@ -788,31 +834,31 @@  -- | Get the sort of given @node@. The result does not have to be released. getSort :: MonadBoolector m => Node -> m Sort-getSort = liftBoolector1 B.getSort+getSort n = liftBoolector1 B.getSort (_node n) >>= lookupSort  -- | Get the domain sort of given function node @node@. -- -- The result does not have to be released. funGetDomainSort :: MonadBoolector m => Node -> m Sort-funGetDomainSort = liftBoolector1 B.funGetDomainSort+funGetDomainSort n = liftBoolector1 B.funGetDomainSort (_node n) >>= lookupSort  -- | Get the codomain sort of given function node @node@. -- -- The result does not have to be released. funGetCodomainSort :: MonadBoolector m => Node -> m Sort-funGetCodomainSort = liftBoolector1 B.funGetCodomainSort+funGetCodomainSort n = liftBoolector1 B.funGetCodomainSort (_node n) >>= lookupSort  -- | Get the arity of function node. funGetArity :: MonadBoolector m => Node -> m Word-funGetArity n = fromIntegral `liftM` liftBoolector1 B.getFunArity n+funGetArity n = fromIntegral `liftM` liftBoolector1 B.getFunArity (_node n)  -- | Get the symbol of an expression. getSymbol :: MonadBoolector m => Node -> m (Maybe String)-getSymbol = liftBoolector1 B.getSymbol+getSymbol = liftBoolector1 B.getSymbol . _node  -- | Set the symbol of an expression. setSymbol :: MonadBoolector m => Node -> String -> m ()-setSymbol = liftBoolector2 B.setSymbol+setSymbol n str = liftBoolector2 B.setSymbol (_node n) str  -- | Get the bit width of an expression. --@@ -820,44 +866,44 @@ -- elements. -- If the expression is a function, it returns the bit width of the function's -- return value.-getWidth :: MonadBoolector m => Node -> m Word-getWidth n = fromIntegral `liftM` liftBoolector1 B.getWidth n+getWidth :: MonadBoolector m => Node -> m Word32+getWidth n = fromIntegral `liftM` liftBoolector1 B.getWidth (_node n)  -- | Get the bit width of indices of @n_array@.-getIndexWidth :: MonadBoolector m => Node -> m Word-getIndexWidth n = fromIntegral `liftM` liftBoolector1 B.getIndexWidth n+getIndexWidth :: MonadBoolector m => Node -> m Word32+getIndexWidth n = fromIntegral `liftM` liftBoolector1 B.getIndexWidth (_node n)  -- | Determine if given node is a constant node. isConst :: MonadBoolector m => Node -> m Bool-isConst = liftBoolector1 B.isConst+isConst = liftBoolector1 B.isConst . _node  -- | Determine if given node is a bit vector variable. isVar :: MonadBoolector m => Node -> m Bool-isVar = liftBoolector1 B.isVar+isVar = liftBoolector1 B.isVar . _node  -- | Determine if given node is an array node. isArray :: MonadBoolector m => Node -> m Bool-isArray = liftBoolector1 B.isArray+isArray = liftBoolector1 B.isArray . _node  -- | Determine if given node is an array node. isArrayVar :: MonadBoolector m => Node -> m Bool-isArrayVar = liftBoolector1 B.isArrayVar+isArrayVar = liftBoolector1 B.isArrayVar . _node  -- | Determine if given node is a parameter node. isParam :: MonadBoolector m => Node -> m Bool-isParam = liftBoolector1 B.isParam+isParam = liftBoolector1 B.isParam . _node  -- | Determine if given parameter node is bound by a function. isBoundParam :: MonadBoolector m => Node -> m Bool-isBoundParam = liftBoolector1 B.isBoundParam+isBoundParam = liftBoolector1 B.isBoundParam . _node  -- | Determine if given node is an uninterpreted function node. isUf :: MonadBoolector m => Node -> m Bool-isUf = liftBoolector1 B.isUf+isUf = liftBoolector1 B.isUf . _node  -- | Determine if given node is a function node. isFun :: MonadBoolector m => Node -> m Bool-isFun = liftBoolector1 B.isFun+isFun = liftBoolector1 B.isFun . _node   --@@ -872,7 +918,7 @@ -- occurs in an assertion or current assumption. The assignment string has to -- be freed by 'freeBvAssignment'. bvAssignment :: MonadBoolector m => Node -> m String-bvAssignment = liftBoolector1 B.bvAssignment+bvAssignment = liftBoolector1 B.bvAssignment . _node  -- | Get unsigned integer value from model. unsignedBvAssignment :: MonadBoolector m => Node -> m Integer@@ -904,14 +950,28 @@ -- Sorts -- +-- | Type of sorts, used to keep track of sorts without having to go back into C-land.+data SortTy = BoolSort+            | BitVecSort Word+            | FunSort [SortTy] SortTy+            | ArraySort SortTy SortTy+            deriving (Eq, Ord, Show) +-- | Sort wraps the udnerlying Boolector sort with a showable type.+data Sort = Sort { sortTy :: SortTy -- ^ Get sort type+                 , _sort  :: B.Sort+                 } deriving (Eq, Ord)++instance Show Sort where+  show = show . sortTy+ -- | Create Boolean sort. boolSort :: Boolector Sort boolSort = do   sc <- getSortCache   case scBool sc of     Just srt -> return srt-    _ -> do srt <- liftBoolector0 B.boolSort+    _ -> do srt <- Sort BoolSort <$> liftBoolector0 B.boolSort             setSortCache $ sc { scBool = Just srt }             return srt @@ -922,7 +982,7 @@   let bvMap = scBitVec sc   case IntMap.lookup nr bvMap of     Just srt -> return srt-    _ -> do srt <- liftBoolector1 B.bitvecSort nr+    _ -> do srt <- Sort (BitVecSort nr) <$> liftBoolector1 B.bitvecSort nr             setSortCache $ sc { scBitVec = IntMap.insert nr srt bvMap }             return srt   where nr = fromIntegral wnr@@ -934,7 +994,8 @@   let funMap = scFun sc   case Map.lookup (ret, args) funMap of     Just srt -> return srt-    _ -> do srt <- liftBoolector2 B.funSort args ret+    _ -> do srt <- Sort (FunSort (map sortTy args) (sortTy ret))+                       <$> liftBoolector2 B.funSort (map _sort args) (_sort ret)             setSortCache $ sc { scFun = Map.insert (ret, args) srt funMap }             return srt @@ -945,31 +1006,38 @@   let arrMap = scArray sc   case Map.lookup (dom, rng) arrMap of     Just srt -> return srt-    _ -> do srt <- liftBoolector2 B.arraySort dom rng+    _ -> do srt <- Sort (ArraySort (sortTy dom) (sortTy rng))+                      <$> liftBoolector2 B.arraySort (_sort dom) (_sort rng)             setSortCache $ sc { scArray = Map.insert (dom, rng) srt arrMap }             return srt  -- | Determine if @n0@ and @n1@ have the same sort or not. isEqualSort :: MonadBoolector m => Node -> Node -> m Bool-isEqualSort = liftBoolector2 B.isEqualSort+isEqualSort n1 n2 = liftBoolector2 B.isEqualSort (_node n1) (_node n2)  -- | Determine if @sort@ is an array sort.-isArraySort :: MonadBoolector m => Sort -> m Bool-isArraySort = liftBoolector1 B.isArraySort+isArraySort :: Sort -> Bool+isArraySort srt = case sortTy srt of+                    BitVecSort _ -> True+                    _ -> False  -- | Determine if @sort@ is a bit-vector sort.-isBitvecSort :: MonadBoolector m => Sort -> m Bool-isBitvecSort = liftBoolector1 B.isBitvecSort+isBitvecSort :: Sort -> Bool+isBitvecSort srt = case sortTy srt of+                    ArraySort _ _ -> True+                    _ -> False  -- | Determine if @sort@ is a function sort.-isFunSort :: MonadBoolector m => Sort -> m Bool-isFunSort = liftBoolector1 B.isFunSort+isFunSort :: Sort -> Bool+isFunSort srt = case sortTy srt of+                    FunSort _ _ -> True+                    _ -> False  -- | Check if sorts of given arguments matches the function signature. -- Returns 'Nothing' if all sorts are correct; otherwise it returns the -- position of the incorrect argument. funSortCheck :: MonadBoolector m => [Node] -> Node -> m (Maybe Int)-funSortCheck = liftBoolector2 B.funSortCheck+funSortCheck n1 n2 = liftBoolector2 B.funSortCheck (map _node n1) (_node n2)   --@@ -984,7 +1052,7 @@ 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+  liftIO $ B.withDumpFile path $ \file -> dumper btor file (_node node)   where dumper = case fmt of                   DumpBtor -> B.dumpBtorNode                   _        -> B.dumpSmt2Node@@ -1003,7 +1071,7 @@ dumpNodeToString :: MonadBoolector m => DumpFormat -> Node -> m String dumpNodeToString fmt node = do   btor <- unBoolectorState `liftM` getBoolectorState-  liftIO $ B.withTempDumpFile (\file -> dumper btor file node)+  liftIO $ B.withTempDumpFile (\file -> dumper btor file (_node node))   where dumper = case fmt of                   DumpBtor -> B.dumpBtorNode                   _        -> B.dumpSmt2Node@@ -1091,15 +1159,59 @@   s0 <- getBoolectorState   putBoolectorState $ s0 { unBoolectorCache = (unBoolectorCache s0) { varCache = vc } } ++--+-- Internal helpers+--++-- | Class used to create nodes from boolector nodes, given a stringification+class Show s => MkNode s where+  mkNode :: MonadBoolector m => s -> m B.Node -> m Node++instance MkNode String where+  mkNode str act = do+    node <- act+    return $ Node node str++instance MkNode [String] where+  mkNode str act = do+    node <- act+    return $ Node node $ "(" ++ unwords str ++ ")"++ -- | Create a new named node given a constructor or return it from variable -- cache. The name must be unique.-createNamedNode :: MonadBoolector m-                => (B.Btor -> Sort -> String -> IO Node)-                -> Sort -> String -> m Node-createNamedNode ctor sort name = do+mkNamedNode :: MonadBoolector m+            => String                                    -- ^ Kind of node+            -> (B.Btor -> B.Sort -> String -> IO B.Node) -- ^ Underlying constructor+            -> Sort                                      -- ^ Sort of node+            -> String                                    -- ^ Name of node+            -> m Node+mkNamedNode kind ctor sort name = do   vc <- getVarCache   case Map.lookup (name, sort) vc of     Just srt -> return srt-    _ -> do node <- liftBoolector2 ctor sort name+    _ -> do node <- mkNode [kind, name, "::", show sort] $+                      liftBoolector2 ctor (_sort sort) name             setVarCache $ Map.insert (name, sort) node vc             return node++-- | Get the high level sort from cache that corresponds to boolector sort+lookupSort :: MonadBoolector m => B.Sort -> m Sort+lookupSort bSort = do+  sc <- getSortCache+  case () of+    _ | Just srt <- lookupBoolSort sc   -> return srt+    _ | Just srt <- lookupBitVecSort sc -> return srt+    _ | Just srt <- lookupFunSort sc    -> return srt+    _ | Just srt <- lookupArraySort sc  -> return srt+    _ -> fail "BUG: should really have the sort in the cache"+  where lookupBoolSort sc = case scBool sc of+                              Just srt | _sort srt == bSort -> Just srt+                              _ -> Nothing+        lookupBitVecSort sc = listToMaybe $ IntMap.elems $+                                IntMap.filter (\s -> _sort s == bSort) $ scBitVec sc+        lookupFunSort sc = listToMaybe $ Map.elems $+                                Map.filter (\s -> _sort s == bSort) $ scFun sc+        lookupArraySort sc = listToMaybe $ Map.elems $+                                Map.filter (\s -> _sort s == bSort) $ scArray sc

@@ -24,10 +24,14 @@     e  <- B.eq c p      -- Make some assertions-    B.assert =<< B.and no e+    B.and no e >>= \node -> do+      liftIO $ putStrLn (show node)+      B.assert node+     one <- B.one u8     B.assert =<< B.ugt x one     B.assert =<< B.ugt y one+      -- Dump the corresponding SMT Lib 2 to a file     B.dump B.DumpSMT2 "dump_example.smt2"

@@ -0,0 +1,93 @@+import qualified Boolector as B++import Control.Monad.IO.Class+import Control.Exception (assert)+++main :: IO ()+main = do+  bs <- B.newBoolectorState Nothing+  B.evalBoolector bs $ do+    -- Create sorts:+    i64   <- B.bitvecSort 64+    fSort <- B.funSort [i64] i64+    gSort <- B.funSort [i64, i64] i64++    -- Create variables x, y, z, f, g+    x <- B.var i64 "x"+    y <- B.var i64 "y"+    z <- B.var i64 "z"+    f <- B.uf fSort "f"+    g <- B.uf gSort "g"++    -- Create constant:+    two <- B.signedInt (-2^60) i64+    +    -- Create action to print model+    let printModel = do mx <- B.signedBvAssignment x+                        my <- B.signedBvAssignment y+                        mz <- B.signedBvAssignment z+                        liftIO $ putStrLn $ show [mx, my, mz]+  +    -- (assert (>= (* -2^60 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)))+    do tmp1 <- B.apply [x] f+       tmp2 <- B.apply [x, x] g+       B.assert =<< B.slt tmp1 tmp2++    -- (assert (> (f y) (g x x)))+    do tmp1 <- B.apply [y] f+       tmp2 <- B.apply [x, x] g+       B.assert =<< B.sgt tmp1 tmp2++    -- Check satisfiability:+    B.Sat <- B.sat++    -- Print model:+    printModel++    -- Push context+    B.push 1++    -- Add (false) assertion:+    B.assert =<< B.eq x y++    -- Check satisfiability:+    B.Unsat <- B.sat++    -- Pop context+    B.pop 1++    -- Can check sat again and pirnt model+    B.Sat <- B.sat+    printModel++++{- This example is from https://rise4fun.com/Z3/smtc_arith:++; This example illustrates basic arithmetic and uninterpreted functions+(declare-fun x () Int)+(declare-fun y () Int)+(declare-fun z () Int)+(assert (>= (* 2 x) (+ y z)))+(declare-fun f (Int) Int)+(declare-fun g (Int Int) Int)+(assert (< (f x) (g x x)))+(assert (> (f y) (g x x)))+(check-sat)+(get-model)+(push)+(assert (= x y))+(check-sat)+(pop)+(exit)++-}+

@@ -0,0 +1,40 @@+import qualified Boolector as B+import Control.Monad.IO.Class++main :: IO ()+main = do+  bs <- B.newBoolectorState Nothing+  B.evalBoolector bs $ do+    -- Create sorts:+    i32   <- B.bitvecSort 32+    fSort <- B.funSort [i32] i32+    +    -- Create constants:+    one   <- B.signedInt 1 i32+    two   <- B.signedInt 2 i32+    five  <- B.signedInt 5 i32+    fifty <- B.signedInt 50 i32++    -- Create variable and function:+    x <- B.var i32 "x"+    f <- B.uf fSort "f"++    -- f(x) >= 5 && f(x) < 50+    do tmp1 <- B.apply [x] f +       B.assert =<< B.sgte tmp1 five+       B.assert =<< B.slt tmp1 fifty++    -- f(2) + 1 > 5 && f(2) <= 50+    do tmp1 <- B.apply [two] f+       tmp2 <- B.add tmp1 one+       B.assert =<< B.sgte tmp2 five+       B.assert =<< B.slte tmp2 fifty++    -- x >= 2+    B.assert =<< B.sgte x two++    -- Check satisfiability:+    B.Sat <- B.sat++    return ()+