Merge branch 'main' into feature/bdd-sat

msakai · Nov 20, 2021 · b23aa35 · b23aa35
2 parents 044872e + 25ebf46
commit b23aa35
Show file tree

Hide file tree

Showing 4 changed files with 61 additions and 8 deletions.
diff --git a/src/Data/DecisionDiagram/BDD.hs b/src/Data/DecisionDiagram/BDD.hs
@@ -594,10 +594,10 @@ fold ff tt br bdd = runST $ do
         case m of
           Just ret -> return ret
           Nothing -> do
-            r0 <- f lo
-            r1 <- f hi
+            r0 <- unsafeInterleaveST $ f lo
+            r1 <- unsafeInterleaveST $ f hi
             let ret = br top r0 r1
-            H.insert h p ret
+            H.insert h p ret  -- Note that H.insert is value-strict
             return ret
   f bdd
 
@@ -620,7 +620,7 @@ mkFold'Op !ff !tt br = do
             r0 <- f lo
             r1 <- f hi
             let ret = br top r0 r1
-            seq ret $ H.insert h p ret
+            H.insert h p ret  -- Note that H.insert is value-strict
             return ret
   return f
 

diff --git a/src/Data/DecisionDiagram/ZDD.hs b/src/Data/DecisionDiagram/ZDD.hs
@@ -134,6 +134,7 @@ import Control.Monad
 import Control.Monad.Primitive
 #endif
 import Control.Monad.ST
+import Control.Monad.ST.Unsafe
 import qualified Data.Foldable as Foldable
 import Data.Function (on)
 import Data.Functor.Identity
@@ -826,10 +827,10 @@ fold ff tt br zdd = runST $ do
         case m of
           Just ret -> return ret
           Nothing -> do
-            r0 <- f p0
-            r1 <- f p1
+            r0 <- unsafeInterleaveST $ f p0
+            r1 <- unsafeInterleaveST $ f p1
             let ret = br top r0 r1
-            H.insert h p ret
+            H.insert h p ret  -- Note that H.insert is value-strict
             return ret
   f zdd
 
@@ -847,7 +848,7 @@ fold' !ff !tt br zdd = runST $ do
             r0 <- f p0
             r1 <- f p1
             let ret = br top r0 r1
-            seq ret $ H.insert h p ret
+            H.insert h p ret  -- Note that H.insert is value-strict
             return ret
   f zdd
 

diff --git a/test/TestBDD.hs b/test/TestBDD.hs
@@ -8,9 +8,11 @@ import Data.IntMap.Lazy (IntMap)
 import qualified Data.IntMap.Lazy as IntMap
 import Data.IntSet (IntSet)
 import qualified Data.IntSet as IntSet
+import Data.IORef
 import Data.List
 import Data.Proxy
 import qualified Data.Set as Set
+import System.IO.Unsafe
 import Test.QuickCheck.Function (apply)
 import Test.Tasty
 import Test.Tasty.HUnit
@@ -513,6 +515,31 @@ prop_existsUniqueSet_union =
 
 -- ------------------------------------------------------------------------
 
+case_fold_laziness :: Assertion
+case_fold_laziness = do
+  let bdd :: BDD BDD.AscOrder
+      bdd = BDD.Branch 0 (BDD.Branch 1 (BDD.Leaf False) (BDD.Leaf True)) (BDD.Branch 2 (BDD.Leaf False) (BDD.Leaf True))
+      f x lo _hi =
+        if x == 2 then
+          error "unused value should not be evaluated"
+        else
+          lo
+  seq (BDD.fold False True f bdd) $ return ()
+
+case_fold'_strictness :: Assertion
+case_fold'_strictness = do
+  ref <- newIORef False
+  let bdd :: BDD BDD.AscOrder
+      bdd = BDD.Branch 0 (BDD.Branch 1 (BDD.Leaf False) (BDD.Leaf True)) (BDD.Branch 2 (BDD.Leaf False) (BDD.Leaf True))
+      f x lo _hi = unsafePerformIO $ do
+        when (x==2) $ writeIORef ref True
+        return lo
+  seq (BDD.fold' False True f bdd) $ do
+    flag <- readIORef ref
+    assertBool "unused value should be evaluated" flag
+
+-- ------------------------------------------------------------------------
+
 case_support_false :: Assertion
 case_support_false = BDD.support BDD.false @?= IntSet.empty
 

diff --git a/test/TestZDD.hs b/test/TestZDD.hs
@@ -10,6 +10,7 @@ import Data.IntMap (IntMap)
 import qualified Data.IntMap as IntMap
 import Data.IntSet (IntSet)
 import qualified Data.IntSet as IntSet
+import Data.IORef
 import Data.List
 import qualified Data.Map.Strict as Map
 import Data.Proxy
@@ -20,6 +21,7 @@ import Data.Word
 import qualified GHC.Exts as Exts
 import Statistics.Distribution
 import Statistics.Distribution.ChiSquared (chiSquared)
+import System.IO.Unsafe
 import qualified System.Random.MWC as Rand
 import Test.QuickCheck.Function (apply)
 import Test.QuickCheck.Instances.Vector ()
@@ -678,6 +680,29 @@ prop_findMaxSum =
               .&&.
               conjoin [counterexample (show (s, setWeight s)) $ obj0 >= setWeight s | s <- ZDD.toListOfIntSets a]
 
+case_fold_laziness :: Assertion
+case_fold_laziness = do
+  let bdd :: ZDD ZDD.AscOrder
+      bdd = ZDD.Branch 0 (ZDD.Branch 1 ZDD.Empty ZDD.Base) (ZDD.Branch 2 ZDD.Empty ZDD.Base)
+      f x lo _hi =
+        if x == 2 then
+          error "unused value should not be evaluated"
+        else
+          lo
+  seq (ZDD.fold False True f bdd) $ return ()
+
+case_fold'_strictness :: Assertion
+case_fold'_strictness = do
+  ref <- newIORef False
+  let bdd :: ZDD ZDD.AscOrder
+      bdd = ZDD.Branch 0 (ZDD.Branch 1 ZDD.Empty ZDD.Base) (ZDD.Branch 2 ZDD.Empty ZDD.Base)
+      f x lo _hi = unsafePerformIO $ do
+        when (x==2) $ writeIORef ref True
+        return lo
+  seq (ZDD.fold' False True f bdd) $ do
+    flag <- readIORef ref
+    assertBool "unused value should be evaluated" flag
+
 -- ------------------------------------------------------------------------
 
 prop_toGraph_fromGraph :: Property