summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDeianStefan <>2018-07-03 06:20:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2018-07-03 06:20:00 (GMT)
commitb8ec3a18a186daa33a3a76e564ae67469607e6ec (patch)
tree3e9b16258f5ad19e59dae1b4f6c990abed5f7c41
parent8f3319cf747a8c006388ff53afc431cca048a8cc (diff)
version 0.0.0.20.0.0.2
-rw-r--r--boolector.cabal19
-rw-r--r--src/Boolector.hs30
-rw-r--r--src/Boolector/Foreign.chs186
-rw-r--r--test/API_Usage_Example.hs2
-rw-r--r--test/GetSetSymbol_Example.hs56
5 files changed, 265 insertions, 28 deletions
diff --git a/boolector.cabal b/boolector.cabal
index b800536..2375c30 100644
--- 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,10 +13,16 @@ description:
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
@@ -70,3 +76,12 @@ Test-Suite Arith_Example
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
index af35306..725ffc2 100644
--- a/src/Boolector.hs
+++ b/src/Boolector.hs
@@ -139,6 +139,7 @@ module Boolector ( -- * Boolector monadic computations
, uext
, sext
, concat
+ , repeat
-- *** Bit-wise operations
, xor
, xnor
@@ -189,6 +190,7 @@ module Boolector ( -- * Boolector monadic computations
, funGetCodomainSort
, funGetArity
, getSymbol
+ , setSymbol
, getWidth
, getIndexWidth
, isConst
@@ -237,7 +239,7 @@ import Control.Monad.State.Strict
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 @@ newBoolectorState (Just time) = do
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 :: MonadBoolector m => m Status
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 @@ redand = liftBoolector1 B.redand
-- | 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,9 +806,13 @@ funGetArity :: MonadBoolector m => Node -> m Word
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.
--
-- If the expression is an array, it returns the bit width of the array
diff --git a/src/Boolector/Foreign.chs b/src/Boolector/Foreign.chs
index 1c702a9..a7b9143 100644
--- a/src/Boolector/Foreign.chs
+++ b/src/Boolector/Foreign.chs
@@ -6,9 +6,159 @@
-}
{-# LANGUAGE StandaloneDeriving #-}
-module Boolector.Foreign where
-
-import Foreign
+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 Prelude hiding (read, not, and, or, const, concat, repeat)
+
+import Foreign hiding (xor, new)
import Foreign.C
import Control.Monad
@@ -198,9 +348,6 @@ foreign import ccall "boolector_set_term"
-- | 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 @@ foreign import ccall "boolector_set_term"
-- 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 @@ foreign import ccall "boolector_set_term"
-- 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,7 +770,17 @@ withNodes (hx:hxs) f = withNode hx $ \cx -> withNodes hxs $ \cxs -> f (cx:cxs)
{#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 @@ foreign import ccall "boolector_fun_sort_check"
-- 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 @@ withSorts (hx:hxs) f = withSort hx $ \cx -> withSorts hxs $ \cxs -> f (cx:cxs)
-- 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
index bffd007..3c80705 100644
--- a/test/API_Usage_Example.hs
+++ b/test/API_Usage_Example.hs
@@ -17,7 +17,7 @@ main = do
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
index 0000000..fe5cd23
--- /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 ()