boolector 0.0.0.1 → 0.0.0.2

raw patch · 5 files changed

+264/−27 lines, 5 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• boolector.cabal +17/−2
• src/Boolector.hs +20/−10
• src/Boolector/Foreign.chs +170/−14
• test/API_Usage_Example.hs +1/−1
• test/GetSetSymbol_Example.hs +56/−0

@@ -1,5 +1,5 @@ name:                boolector-version:             0.0.0.1+version:             0.0.0.2 synopsis:            Haskell bindings for the Boolector SMT solver description: @@ -13,11 +13,17 @@ license:             MIT license-file:        LICENSE author:              Dein Stefan, Johannes Waldmann, Armin Biere-maintainer:          deian@cs.ucsd.edu+maintainer:          Deian Stefan <deian@cs.ucsd.edu> category:            Math, SMT, Theorem Provers, Formal Methods, Bit vectors build-type:          Simple cabal-version:       >= 1.10+homepage:       https://github.com/plsyssec/haskell-boolector+bug-reports:    https://github.com/plsyssec/haskell-boolector/issues +source-repository head+  type:     git+  location: https://github.com/PLSysSec/haskell-boolector.git+ library   hs-source-dirs: src   default-language: Haskell2010@@ -68,5 +74,14 @@                , boolector   Type: exitcode-stdio-1.0   main-is: Arith_Example.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

@@ -139,6 +139,7 @@                  , uext                  , sext                  , concat+                 , repeat                  -- *** Bit-wise operations                  , xor                  , xnor@@ -189,6 +190,7 @@                  , funGetCodomainSort                  , funGetArity                  , getSymbol+                 , setSymbol                  , getWidth                  , getIndexWidth                  , isConst@@ -237,7 +239,7 @@ import Control.Exception hiding (assert) import Control.Concurrent -import Prelude hiding (read, not, and, or, const, concat)+import Prelude hiding (read, not, and, or, const, concat, repeat) import qualified Prelude as Prelude  --@@ -291,11 +293,11 @@   return btorState  -- | Set option.-setOpt :: MonadBoolector m => Option -> Word -> m ()+setOpt :: MonadBoolector m => Option -> Word32 -> m () setOpt o w = liftBoolector2 B.setOpt o (fromIntegral w)  -- | Get option.-getOpt :: MonadBoolector m => Option -> m Word+getOpt :: MonadBoolector m => Option -> m Word32 getOpt o = fromIntegral `liftM` liftBoolector1 B.getOpt o  -- | Which sat solver to use.@@ -333,11 +335,11 @@ sat = liftBoolector0 B.sat  -- | Push new context levels.-push :: MonadBoolector m => Word -> m ()+push :: MonadBoolector m => Word32 -> m () push w = liftBoolector1 B.push (fromIntegral w)  -- | Pop context levels.-pop :: MonadBoolector m => Word -> m ()+pop :: MonadBoolector m => Word32 -> m () pop w = liftBoolector1 B.pop (fromIntegral w)  -- | Solve an input formula and limit the search by the number of lemmas@@ -444,28 +446,32 @@ -- | Create a bit vector slice of @node@ from index @upper@ to index @lower@. slice :: MonadBoolector m       => Node -- ^ Bit vector node.-      -> Word -- ^ Upper index which must be greater than or equal to zero, and less than the bit width of @node@.-      -> Word -- ^ Lower index which must be greater than or equal to zero, and less than or equal to @upper@.+      -> 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)  -- | Create unsigned extension. -- -- The bit vector @node@ is padded with @width@ * zeroes.-uext :: MonadBoolector m => Node -> Word -> m Node+uext :: MonadBoolector m => Node -> Word32 -> m Node uext n w = (liftBoolector2 B.uext) 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 -> Word -> m Node+sext :: MonadBoolector m => Node -> Word32 -> m Node sext n w = liftBoolector2 B.sext n (fromIntegral w)  -- | Create the concatenation of two bit vectors. concat :: MonadBoolector m => Node -> Node -> m Node concat = liftBoolector2 B.concat +-- | Create @n@ concatenations of a given node @node@.+repeat :: MonadBoolector m => Node -> Word32 -> m Node+repeat n w = liftBoolector2 B.repeat n (fromIntegral w)+ -- | Create boolean implication. implies :: MonadBoolector m => Node -> Node -> m Node implies = liftBoolector2 B.implies@@ -800,8 +806,12 @@ funGetArity n = fromIntegral `liftM` liftBoolector1 B.getFunArity n  -- | Get the symbol of an expression.-getSymbol :: MonadBoolector m => Node -> m String+getSymbol :: MonadBoolector m => Node -> m (Maybe String) getSymbol = liftBoolector1 B.getSymbol++-- | Set the symbol of an expression.+setSymbol :: MonadBoolector m => Node -> String -> m ()+setSymbol = liftBoolector2 B.setSymbol  -- | Get the bit width of an expression. --

@@ -6,9 +6,159 @@  -} {-# LANGUAGE StandaloneDeriving #-}-module Boolector.Foreign where+module Boolector.Foreign (+   -- ** Boolector state, options and configurations+    Btor+  , new+  , Option(..)+  , setOpt+  , getOpt+  , setSatSolver+  -- * SAT/SMT queries+  , Node+  , sat+  , limitedSat+  , simplify+  , Status(..)+  -- ** Assert and assume+  , assert+  , assume+  , failed+  , fixateAssumptions+  , resetAssumptions+  , push+  , pop+  -- ** Variables and constants+  , var+  , const+  , constd+  , consth+  -- *** Booleans+  , true+  , false+  -- *** Bit-vectors+  , zero+  , one+  , ones+  , unsignedInt+  , int+  -- *** Arrays+  , array+  -- *** Functions+  , fun+  , uf+  -- **** Parameters+  , param+  -- *** Quantified terms+  , forall+  , exists+  -- ** Operations+  -- *** Implications and conditionals+  , implies+  , iff+  , cond+  -- *** Equality checking+  , eq+  , ne+  -- *** Bit flipping, extraction, extension, and reduction+  , not+  , neg+  , redor+  , redxor+  , redand+  , slice+  , uext+  , sext+  , concat+  , repeat+  -- *** Bit-wise operations+  , xor+  , xnor+  , and+  , nand+  , or+  , nor+  , sll+  , srl+  , sra+  , rol+  , ror+  -- *** Arithmetic operations+  , add+  , uaddo+  , saddo+  , inc+  , sub+  , usubo+  , ssubo+  , dec+  , mul+  , umulo+  , smulo+  , udiv+  , sdiv+  , sdivo+  , urem+  , srem+  , smod+  -- *** Comparison operations+  , ult+  , slt+  , ulte+  , slte+  , ugt+  , sgt+  , ugte+  , sgte+  -- *** Array operations+  , read+  , write+  -- *** Function operations+  , apply+  -- ** Accessors+  , getSort+  , funGetDomainSort+  , funGetCodomainSort+  , getFunArity+  , getSymbol+  , setSymbol+  , getWidth+  , getIndexWidth+  , isConst+  , isVar+  , isArray+  , isArrayVar+  , isParam+  , isBoundParam+  , isUf+  , isFun+  -- ** Models+  , bvAssignment+  -- ** Sorts+  , Sort+  , boolSort+  , bitvecSort+  , funSort+  , arraySort+  -- *** Accessors+  , isEqualSort+  , isArraySort+  , isBitvecSort+  , isFunSort+  , funSortCheck+  -- * Debug dumping+  , dumpBtorNode+  , dumpSmt2Node+  , dumpBtor+  , dumpSmt2+  -- * Helpers+  , fopen+  , setTerm+  ) where -import Foreign+import Prelude hiding (read, not, and, or, const, concat, repeat)++import Foreign hiding (xor, new) import Foreign.C  import Control.Monad@@ -198,9 +348,6 @@ -- | Get the current value of an option. {#fun get_opt as ^ { `Btor', `Option' } -> `CUInt' #} --- | Check if Boolector has a given option.-{#fun has_opt as ^ { `Btor', `Option' } -> `Bool' #}- -- -- Solving --@@ -250,9 +397,6 @@ -- Expressions -- --- | Copy expression (increments reference counter).-{#fun copy as ^ { `Btor' , `Node' } -> `Node' #}- -- | Create bit vector constant representing the bit vector @bits@. {#fun const as ^ { `Btor' , `String' } -> `Node' #} @@ -420,6 +564,7 @@ -- Given bit vector node @n1@, the value it represents is the number of bits -- by which node @n0@ is rotated to the left. {#fun rol as ^ { `Btor' , `Node', `Node'} -> `Node' #}+ -- | Create a rotate right. -- -- Given bit vector node @n1@, the value it represents is the number of bits by@@ -625,8 +770,18 @@ {#fun get_fun_arity as ^ { `Btor' , `Node' } -> `CUInt' #}  -- | Get the symbol of an expression.-{#fun get_symbol as ^ { `Btor' , `Node' } -> `String' #}+foreign import ccall safe "Boolector/Foreign.chs.h boolector_get_symbol"+  getSymbol'_ :: Ptr Btor -> Ptr Node -> IO CString +-- | Get the symbol of an expression.+getSymbol :: Btor -> Node -> IO (Maybe String)+getSymbol hbtor hnode = withBtor hbtor $ \cbtor -> +  withNode hnode $ \cnode -> do+    cstrPtr <- getSymbol'_ cbtor cnode+    if cstrPtr == nullPtr +      then return Nothing+      else Just `liftM` peekCString cstrPtr+ -- | Set the symbol of an expression. {#fun set_symbol as ^ { `Btor' , `Node', `String' } -> `()' #} @@ -691,12 +846,12 @@ -- The expression can be an arbitrary bit vector expression which -- occurs in an assertion or current assumption. The assignment string has to -- be freed by 'free_bv_assignment'.+--+-- TODO: we should change this function to return a ModelString and use+-- free_bv_assignment to actually free the assignments. We're very leaky right+--now. {#fun bv_assignment as ^ { `Btor' , `Node' } -> `String' #} --- | Free an assignment string for bit vectors.  TODO: we should change--- bv_assignment to return a ModelString and  use free to actually free the--- assignments. We're very leaky right now.-{#fun free_bv_assignment as ^ { `Btor' , `String' } -> `()' #}  -- -- Sorts.@@ -744,9 +899,10 @@ -- Dumping -- +-- | POSIX files {#pointer *FILE as File foreign finalizer fclose newtype#} --- | libc's fopen+-- | Expose POSIX file open. {#fun fopen as ^ {`String', `String'} -> `File' #}  -- | Recursively dump @node@ to file in BTOR_ format.

@@ -17,7 +17,7 @@     x <- B.var u8 "x"     y <- B.var u8 "y" -    -- Perofmr some operations on the values+    -- Perform some operations on the values     p  <- B.mul x y     o  <- B.umulo x y     no <- B.not o

@@ -0,0 +1,56 @@++import qualified Boolector as B++import Control.Monad.IO.Class+import Control.Exception (assert)+import Control.Concurrent++-- This example is same as the API_Usage_Example, but additionally tests+-- symbols getters and setters++main :: IO ()+main = do+  -- Create new Boolector state with a 1000ms timeout+  bs <- B.newBoolectorState (Just 1000)+  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"+    y <- B.var u8 "y"++    B.getSymbol x >>= \xname -> assert (xname == Just "x") $ return ()+    B.getSymbol y >>= \yname -> assert (yname == Just "y") $ return ()++    -- Perform some operations on the values+    p  <- B.mul x y+    o  <- B.umulo x y+    no <- B.not o+    e  <- B.eq c p++    B.getSymbol p >>= \pname -> assert (pname == Nothing) $ return ()+    B.setSymbol p "p"+    B.getSymbol p >>= \pname -> assert (pname == Just "p") $ return ()+++    -- Make some assertions+    B.assert =<< B.and no e+    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.dumpSmt2 "dump_example.smt2"++    -- Check satisfiability+    B.Sat <- B.sat++    -- Get model+    mx <- B.unsignedBvAssignment x+    my <- B.unsignedBvAssignment y+    mp <- B.unsignedBvAssignment p+    assert (mx == 7) $ return ()+    assert (my == 5) $ return ()+    assert (mp == 35) $ return ()