diff --git a/boolector.cabal b/boolector.cabal --- a/boolector.cabal +++ b/boolector.cabal @@ -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 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 diff --git a/src/Boolector.hs b/src/Boolector.hs --- a/src/Boolector.hs +++ b/src/Boolector.hs @@ -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. -- diff --git a/src/Boolector/Foreign.chs b/src/Boolector/Foreign.chs --- a/src/Boolector/Foreign.chs +++ b/src/Boolector/Foreign.chs @@ -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. diff --git a/test/API_Usage_Example.hs b/test/API_Usage_Example.hs --- a/test/API_Usage_Example.hs +++ b/test/API_Usage_Example.hs @@ -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 diff --git a/test/GetSetSymbol_Example.hs b/test/GetSetSymbol_Example.hs new file mode 100644 --- /dev/null +++ b/test/GetSetSymbol_Example.hs @@ -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 ()