boolector 0.0.0.8 → 0.0.0.9

raw patch · 2 files changed

+6/−3 lines, 2 filesdep +failPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: fail

API changes (from Hackage documentation)

+ Boolector: instance Control.Monad.Fail.MonadFail Boolector.Boolector

- Boolector.Foreign: add :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: add :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: and :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: and :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: array :: (Btor) -> (Sort) -> (String) -> IO ((Node))

+ Boolector.Foreign: array :: Btor -> Sort -> String -> IO Node

- Boolector.Foreign: arraySort :: (Btor) -> (Sort) -> (Sort) -> IO ((Sort))

+ Boolector.Foreign: arraySort :: Btor -> Sort -> Sort -> IO Sort

- Boolector.Foreign: assert :: (Btor) -> (Node) -> IO ()

+ Boolector.Foreign: assert :: Btor -> Node -> IO ()

- Boolector.Foreign: assume :: (Btor) -> (Node) -> IO ()

+ Boolector.Foreign: assume :: Btor -> Node -> IO ()

- Boolector.Foreign: bitvecSort :: (Btor) -> (CUInt) -> IO ((Sort))

+ Boolector.Foreign: bitvecSort :: Btor -> CUInt -> IO Sort

- Boolector.Foreign: boolSort :: (Btor) -> IO ((Sort))

+ Boolector.Foreign: boolSort :: Btor -> IO Sort

- Boolector.Foreign: bvAssignment :: (Btor) -> (Node) -> IO ((String))

+ Boolector.Foreign: bvAssignment :: Btor -> Node -> IO String

- Boolector.Foreign: concat :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: concat :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: cond :: (Btor) -> (Node) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: cond :: Btor -> Node -> Node -> Node -> IO Node

- Boolector.Foreign: const :: (Btor) -> (String) -> IO ((Node))

+ Boolector.Foreign: const :: Btor -> String -> IO Node

- Boolector.Foreign: constd :: (Btor) -> (Sort) -> (String) -> IO ((Node))

+ Boolector.Foreign: constd :: Btor -> Sort -> String -> IO Node

- Boolector.Foreign: consth :: (Btor) -> (Sort) -> (String) -> IO ((Node))

+ Boolector.Foreign: consth :: Btor -> Sort -> String -> IO Node

- Boolector.Foreign: dec :: (Btor) -> (Node) -> IO ((Node))

+ Boolector.Foreign: dec :: Btor -> Node -> IO Node

- Boolector.Foreign: dumpBtor :: (Btor) -> (File) -> IO ()

+ Boolector.Foreign: dumpBtor :: Btor -> File -> IO ()

- Boolector.Foreign: dumpBtorNode :: (Btor) -> (File) -> (Node) -> IO ()

+ Boolector.Foreign: dumpBtorNode :: Btor -> File -> Node -> IO ()

- Boolector.Foreign: dumpSmt2 :: (Btor) -> (File) -> IO ()

+ Boolector.Foreign: dumpSmt2 :: Btor -> File -> IO ()

- Boolector.Foreign: dumpSmt2Node :: (Btor) -> (File) -> (Node) -> IO ()

+ Boolector.Foreign: dumpSmt2Node :: Btor -> File -> Node -> IO ()

- Boolector.Foreign: eq :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: eq :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: failed :: (Btor) -> (Node) -> IO ((Bool))

+ Boolector.Foreign: failed :: Btor -> Node -> IO Bool

- Boolector.Foreign: false :: (Btor) -> IO ((Node))

+ Boolector.Foreign: false :: Btor -> IO Node

- Boolector.Foreign: fixateAssumptions :: (Btor) -> IO ()

+ Boolector.Foreign: fixateAssumptions :: Btor -> IO ()

- Boolector.Foreign: funGetCodomainSort :: (Btor) -> (Node) -> IO ((Sort))

+ Boolector.Foreign: funGetCodomainSort :: Btor -> Node -> IO Sort

- Boolector.Foreign: funGetDomainSort :: (Btor) -> (Node) -> IO ((Sort))

+ Boolector.Foreign: funGetDomainSort :: Btor -> Node -> IO Sort

- Boolector.Foreign: getBits :: (Btor) -> (Node) -> IO ((String))

+ Boolector.Foreign: getBits :: Btor -> Node -> IO String

- Boolector.Foreign: getFunArity :: (Btor) -> (Node) -> IO ((CUInt))

+ Boolector.Foreign: getFunArity :: Btor -> Node -> IO CUInt

- Boolector.Foreign: getIndexWidth :: (Btor) -> (Node) -> IO ((CUInt))

+ Boolector.Foreign: getIndexWidth :: Btor -> Node -> IO CUInt

- Boolector.Foreign: getOpt :: (Btor) -> (Option) -> IO ((CUInt))

+ Boolector.Foreign: getOpt :: Btor -> Option -> IO CUInt

- Boolector.Foreign: getSort :: (Btor) -> (Node) -> IO ((Sort))

+ Boolector.Foreign: getSort :: Btor -> Node -> IO Sort

- Boolector.Foreign: getWidth :: (Btor) -> (Node) -> IO ((CUInt))

+ Boolector.Foreign: getWidth :: Btor -> Node -> IO CUInt

- Boolector.Foreign: iff :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: iff :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: implies :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: implies :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: inc :: (Btor) -> (Node) -> IO ((Node))

+ Boolector.Foreign: inc :: Btor -> Node -> IO Node

- Boolector.Foreign: int :: (Btor) -> (CInt) -> (Sort) -> IO ((Node))

+ Boolector.Foreign: int :: Btor -> CInt -> Sort -> IO Node

- Boolector.Foreign: isArray :: (Btor) -> (Node) -> IO ((Bool))

+ Boolector.Foreign: isArray :: Btor -> Node -> IO Bool

- Boolector.Foreign: isArraySort :: (Btor) -> (Sort) -> IO ((Bool))

+ Boolector.Foreign: isArraySort :: Btor -> Sort -> IO Bool

- Boolector.Foreign: isArrayVar :: (Btor) -> (Node) -> IO ((Bool))

+ Boolector.Foreign: isArrayVar :: Btor -> Node -> IO Bool

- Boolector.Foreign: isBitvecSort :: (Btor) -> (Sort) -> IO ((Bool))

+ Boolector.Foreign: isBitvecSort :: Btor -> Sort -> IO Bool

- Boolector.Foreign: isBoundParam :: (Btor) -> (Node) -> IO ((Bool))

+ Boolector.Foreign: isBoundParam :: Btor -> Node -> IO Bool

- Boolector.Foreign: isConst :: (Btor) -> (Node) -> IO ((Bool))

+ Boolector.Foreign: isConst :: Btor -> Node -> IO Bool

- Boolector.Foreign: isEqualSort :: (Btor) -> (Node) -> (Node) -> IO ((Bool))

+ Boolector.Foreign: isEqualSort :: Btor -> Node -> Node -> IO Bool

- Boolector.Foreign: isFun :: (Btor) -> (Node) -> IO ((Bool))

+ Boolector.Foreign: isFun :: Btor -> Node -> IO Bool

- Boolector.Foreign: isFunSort :: (Btor) -> (Sort) -> IO ((Bool))

+ Boolector.Foreign: isFunSort :: Btor -> Sort -> IO Bool

- Boolector.Foreign: isParam :: (Btor) -> (Node) -> IO ((Bool))

+ Boolector.Foreign: isParam :: Btor -> Node -> IO Bool

- Boolector.Foreign: isUf :: (Btor) -> (Node) -> IO ((Bool))

+ Boolector.Foreign: isUf :: Btor -> Node -> IO Bool

- Boolector.Foreign: isVar :: (Btor) -> (Node) -> IO ((Bool))

+ Boolector.Foreign: isVar :: Btor -> Node -> IO Bool

- Boolector.Foreign: limitedSat :: (Btor) -> (Int) -> (Int) -> IO ((Status))

+ Boolector.Foreign: limitedSat :: Btor -> Int -> Int -> IO Status

- Boolector.Foreign: mul :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: mul :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: nand :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: nand :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: ne :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: ne :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: neg :: (Btor) -> (Node) -> IO ((Node))

+ Boolector.Foreign: neg :: Btor -> Node -> IO Node

- Boolector.Foreign: new :: IO (Btor)

+ Boolector.Foreign: new :: IO Btor

- Boolector.Foreign: nor :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: nor :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: not :: (Btor) -> (Node) -> IO ((Node))

+ Boolector.Foreign: not :: Btor -> Node -> IO Node

- Boolector.Foreign: one :: (Btor) -> (Sort) -> IO ((Node))

+ Boolector.Foreign: one :: Btor -> Sort -> IO Node

- Boolector.Foreign: ones :: (Btor) -> (Sort) -> IO ((Node))

+ Boolector.Foreign: ones :: Btor -> Sort -> IO Node

- Boolector.Foreign: or :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: or :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: param :: (Btor) -> (Sort) -> (String) -> IO ((Node))

+ Boolector.Foreign: param :: Btor -> Sort -> String -> IO Node

- Boolector.Foreign: pop :: (Btor) -> (CUInt) -> IO ()

+ Boolector.Foreign: pop :: Btor -> CUInt -> IO ()

- Boolector.Foreign: push :: (Btor) -> (CUInt) -> IO ()

+ Boolector.Foreign: push :: Btor -> CUInt -> IO ()

- Boolector.Foreign: read :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: read :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: redand :: (Btor) -> (Node) -> IO ((Node))

+ Boolector.Foreign: redand :: Btor -> Node -> IO Node

- Boolector.Foreign: redor :: (Btor) -> (Node) -> IO ((Node))

+ Boolector.Foreign: redor :: Btor -> Node -> IO Node

- Boolector.Foreign: redxor :: (Btor) -> (Node) -> IO ((Node))

+ Boolector.Foreign: redxor :: Btor -> Node -> IO Node

- Boolector.Foreign: repeat :: (Btor) -> (Node) -> (CUInt) -> IO ((Node))

+ Boolector.Foreign: repeat :: Btor -> Node -> CUInt -> IO Node

- Boolector.Foreign: resetAssumptions :: (Btor) -> IO ()

+ Boolector.Foreign: resetAssumptions :: Btor -> IO ()

- Boolector.Foreign: rol :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: rol :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: ror :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: ror :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: saddo :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: saddo :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: sat :: (Btor) -> IO ((Status))

+ Boolector.Foreign: sat :: Btor -> IO Status

- Boolector.Foreign: sdiv :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: sdiv :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: sdivo :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: sdivo :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: setOpt :: (Btor) -> (Option) -> (CUInt) -> IO ()

+ Boolector.Foreign: setOpt :: Btor -> Option -> CUInt -> IO ()

- Boolector.Foreign: setSatSolver :: (Btor) -> (String) -> IO ()

+ Boolector.Foreign: setSatSolver :: Btor -> String -> IO ()

- Boolector.Foreign: setSymbol :: (Btor) -> (Node) -> (String) -> IO ()

+ Boolector.Foreign: setSymbol :: Btor -> Node -> String -> IO ()

- Boolector.Foreign: sext :: (Btor) -> (Node) -> (CUInt) -> IO ((Node))

+ Boolector.Foreign: sext :: Btor -> Node -> CUInt -> IO Node

- Boolector.Foreign: sgt :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: sgt :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: sgte :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: sgte :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: simplify :: (Btor) -> IO ((Status))

+ Boolector.Foreign: simplify :: Btor -> IO Status

- Boolector.Foreign: slice :: (Btor) -> (Node) -> (CUInt) -> (CUInt) -> IO ((Node))

+ Boolector.Foreign: slice :: Btor -> Node -> CUInt -> CUInt -> IO Node

- Boolector.Foreign: sll :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: sll :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: slt :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: slt :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: slte :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: slte :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: smod :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: smod :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: smulo :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: smulo :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: sra :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: sra :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: srem :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: srem :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: srl :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: srl :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: ssubo :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: ssubo :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: sub :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: sub :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: true :: (Btor) -> IO ((Node))

+ Boolector.Foreign: true :: Btor -> IO Node

- Boolector.Foreign: uaddo :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: uaddo :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: udiv :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: udiv :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: uext :: (Btor) -> (Node) -> (CUInt) -> IO ((Node))

+ Boolector.Foreign: uext :: Btor -> Node -> CUInt -> IO Node

- Boolector.Foreign: uf :: (Btor) -> (Sort) -> (String) -> IO ((Node))

+ Boolector.Foreign: uf :: Btor -> Sort -> String -> IO Node

- Boolector.Foreign: ugt :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: ugt :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: ugte :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: ugte :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: ult :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: ult :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: ulte :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: ulte :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: umulo :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: umulo :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: unsignedInt :: (Btor) -> (CUInt) -> (Sort) -> IO ((Node))

+ Boolector.Foreign: unsignedInt :: Btor -> CUInt -> Sort -> IO Node

- Boolector.Foreign: urem :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: urem :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: usubo :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: usubo :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: var :: (Btor) -> (Sort) -> (String) -> IO ((Node))

+ Boolector.Foreign: var :: Btor -> Sort -> String -> IO Node

- Boolector.Foreign: write :: (Btor) -> (Node) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: write :: Btor -> Node -> Node -> Node -> IO Node

- Boolector.Foreign: xnor :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: xnor :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: xor :: (Btor) -> (Node) -> (Node) -> IO ((Node))

+ Boolector.Foreign: xor :: Btor -> Node -> Node -> IO Node

- Boolector.Foreign: zero :: (Btor) -> (Sort) -> IO ((Node))

+ Boolector.Foreign: zero :: Btor -> Sort -> IO Node

Files

boolector.cabal +4/−2
src/Boolector.hs +2/−1

boolector.cabal view

@@ -1,5 +1,5 @@ name:                boolector-version:             0.0.0.8+version:             0.0.0.9 synopsis:            Haskell bindings for the Boolector SMT solver description: @@ -12,7 +12,7 @@  license:             MIT license-file:        LICENSE-author:              Dein Stefan, Johannes Waldmann, Armin Biere+author:              Deian Stefan, Johannes Waldmann, Armin Biere maintainer:          Deian Stefan <deian@cs.ucsd.edu> category:            Math, SMT, Theorem Provers, Formal Methods, Bit vectors build-type:          Simple@@ -37,6 +37,8 @@         temporary,         directory,         time+  if impl(ghc < 8.0)+    build-depends: fail == 4.9.0.0    ghc-options: -Wall -fno-warn-orphans   build-tools:      c2hs

src/Boolector.hs view

@@ -238,6 +238,7 @@ import Boolector.Foreign (Option(..), Status(..)) import qualified Boolector.Foreign as B +import qualified Control.Monad.Fail as Fail import Data.Char (isDigit) import Data.Maybe (listToMaybe) import Data.Map (Map)@@ -278,7 +279,7 @@  -- | Bolector monad, keeping track of underlying solver state. newtype Boolector a = Boolector { unBoolector :: StateT BoolectorState IO a }-    deriving (Functor, Applicative, Monad, MonadState BoolectorState, MonadIO)+    deriving (Functor, Applicative, Monad, MonadState BoolectorState, MonadIO, Fail.MonadFail)  -- | Evaluate a Boolector action with a given configurations. evalBoolector :: BoolectorState -> Boolector a -> IO a