summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDeianStefan <>2018-09-06 22:49:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2018-09-06 22:49:00 (GMT)
commit18c70bf17fb7f917fd3cfa39ca8fb63f037bb7d9 (patch)
treee9e31deff869d7457699086c713f4c0ef545ab33
parent3ae623410175a2efa0af4a19cc86660d817b45be (diff)
version 0.0.0.50.0.0.5
-rw-r--r--boolector.cabal12
-rw-r--r--src/Boolector.hs4
-rw-r--r--test/Arith_Example3.hs50
-rw-r--r--test/Array_Example.hs6
-rw-r--r--test/UF_Example.hs5
5 files changed, 74 insertions, 3 deletions
diff --git a/boolector.cabal b/boolector.cabal
index 6ccfd35..09947ca 100644
--- a/boolector.cabal
+++ b/boolector.cabal
@@ -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:
@@ -88,6 +88,16 @@ Test-Suite Arith_Example2
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
Build-Depends: base >= 4.7 && < 5
diff --git a/src/Boolector.hs b/src/Boolector.hs
index 4963ebf..5c650e3 100644
--- a/src/Boolector.hs
+++ b/src/Boolector.hs
@@ -1018,13 +1018,13 @@ isEqualSort n1 n2 = liftBoolector2 B.isEqualSort (_node n1) (_node n2)
-- | 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.
diff --git a/test/Arith_Example3.hs b/test/Arith_Example3.hs
new file mode 100644
index 0000000..eb8b657
--- /dev/null
+++ b/test/Arith_Example3.hs
@@ -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
diff --git a/test/Array_Example.hs b/test/Array_Example.hs
index 501f820..0390e6a 100644
--- a/test/Array_Example.hs
+++ b/test/Array_Example.hs
@@ -12,6 +12,12 @@ main = do
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"
diff --git a/test/UF_Example.hs b/test/UF_Example.hs
index fc9fabf..86b36c4 100644
--- a/test/UF_Example.hs
+++ b/test/UF_Example.hs
@@ -12,6 +12,11 @@ main = do
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"