boolector 0.0.0.4 → 0.0.0.5

raw patch · 5 files changed

+74/−3 lines, 5 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

boolector.cabal +11/−1
src/Boolector.hs +2/−2
test/Arith_Example3.hs +50/−0
test/Array_Example.hs +6/−0
test/UF_Example.hs +5/−0

boolector.cabal view

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

src/Boolector.hs view

@@ -1018,13 +1018,13 @@ -- | Determine if @sort@ is an array sort. isArraySort :: Sort -> Bool isArraySort srt = case sortTy srt of-                    BitVecSort _ -> True+                    ArraySort _ _ -> True                     _ -> False  -- | Determine if @sort@ is a bit-vector sort. isBitvecSort :: Sort -> Bool isBitvecSort srt = case sortTy srt of-                    ArraySort _ _ -> True+                    BitVecSort _ -> True                     _ -> False  -- | Determine if @sort@ is a function sort.

+ test/Arith_Example3.hs view

@@ -0,0 +1,50 @@+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 sort:+    u64   <- B.bitvecSort 64++    -- Test isBitvecSort:+    assert (B.isBitvecSort u64) $ return ()++    -- Create variables x and y+    x <- B.var u64 "x"+    y <- B.var u64 "y"++    -- Create constants:+    big   <- B.unsignedInt _BIG u64+    small <- B.unsignedInt _SMALL u64+    +    -- Create action to print model+    let printModel = do mx <- B.unsignedBvAssignment x+                        my <- B.unsignedBvAssignment y+                        assert (mx == _BIG) $ return ()+                        assert (my == _BIG) $ return ()+                        liftIO $ putStrLn $ show [mx, my]+  +    -- (assert (= x y))+    B.assert =<< B.eq x y+    -- (assert (= x big))+    B.assert =<< B.eq x big+    -- (assert (= small big))+    B.assert =<< B.ne small big++    -- Print SMT2 file+    smt <- B.dumpToString B.DumpSMT2+    liftIO $ putStrLn smt++    -- Check satisfiability:+    B.Sat <- B.sat++    -- Print model:+    printModel++  where _BIG   = 18446744073709551615+        _SMALL = 4294967295

test/Array_Example.hs view

@@ -12,6 +12,12 @@      arr8x32 <- B.arraySort u8 u32 +    -- Test isBitvecSort:+    assert (B.isBitvecSort u8) $ return ()+    assert (B.isBitvecSort u32) $ return ()+    -- Test isArraySort:+    assert (B.isArraySort arr8x32) $ return ()+     arr <- B.array arr8x32 "a"      x <- B.var u8 "x"

test/UF_Example.hs view

@@ -12,6 +12,11 @@     u32 <- B.bitvecSort 32     fSort <- B.funSort [u32] u32 +    -- Test isBitvecSort:+    assert (B.isBitvecSort u32) $ return ()+    -- Test isFunSort:+    assert (B.isFunSort fSort) $ return ()+     -- Create variables f, a, and b:     f <- B.uf fSort "f"     a <- B.var u32 "a"