Testing different simplifications in parallel

slapnet.cabal

@@ -22,7 +22,7 @@ executable slapnet
   other-modules:
   -- other-extensions:
   build-depends:       base >=4 && <5, sbv, parsec, containers, transformers,
-                       bytestring, mtl
+                       bytestring, mtl, stm, async, parallel-io
   hs-source-dirs:      src
   default-language:    Haskell2010
-  ghc-options:         -fsimpl-tick-factor=1000
+  ghc-options:         -fsimpl-tick-factor=1000 -threaded -rtsopts -with-rtsopts=-N 

src/Main.hs

@@ -3,6 +3,7 @@ module Main where
 import System.Exit
 import System.IO
 import Control.Monad
+import Control.Concurrent.ParallelIO
 import Control.Arrow (first)
 import Data.List (partition)
 import Data.Maybe
@@ -405,14 +406,19 @@ main = do
 exitSuccessWith :: String -> IO ()
 exitSuccessWith msg = do
         putStrLn msg
-        exitSuccess
+        cleanupAndExitWith ExitSuccess
 
 exitFailureWith :: String -> IO ()
 exitFailureWith msg = do
         putStrLn msg
-        exitWith $ ExitFailure 2
+        cleanupAndExitWith $ ExitFailure 2
 
 exitErrorWith :: String -> IO ()
 exitErrorWith msg = do
         hPutStrLn stderr msg
-        exitWith $ ExitFailure 3
+        cleanupAndExitWith $ ExitFailure 3
+
+cleanupAndExitWith :: ExitCode -> IO ()
+cleanupAndExitWith code = do
+        stopGlobalPool
+        exitWith code

src/Options.hs

@@ -59,7 +59,7 @@ startOptions = Options { inputFormat = PNET
                        , optShowVersion = False
                        , optProperties = []
                        , optTransformations = []
-                       , optSimpFormula = 6
+                       , optSimpFormula = 100
                        , optRefinementType = Just SComponentWithCutRefinement
                        , optMinimizeRefinement = 0
                        , optInvariant = False

src/Solver/Simplifier.hs

@@ -7,6 +7,9 @@ module Solver.Simplifier (
 
 import Data.SBV
 import Data.Maybe
+import Data.Ord (comparing)
+import Data.List (minimumBy)
+import Control.Arrow (second)
 import Control.Monad
 import Control.Monad.Identity
 import qualified Data.Map as M
@@ -50,47 +53,66 @@ checkSubsumptionSat c0 cs =
 cutTransitions :: SimpleCut -> S.Set Transition
 cutTransitions (c0, cs) = S.unions (c0:cs)
 
-generateCuts :: PetriNet -> Formula Transition -> [Cut] -> OptIO [SimpleCut]
-generateCuts net f cuts = do
+type SimpConfig = ([[SimpleCut] -> OptIO [SimpleCut]], SimpleCut, SimpleCut, Int)
+
+simpWithoutFormula :: PetriNet -> Formula Transition -> SimpConfig
+simpWithoutFormula net f =
+        (
+        [ return . simplifyCuts
+        , return . removeImplicants
+        , greedySimplify net f
+        , return . combineCuts
+        , simplifyBySubsumption
+        ]
+        , (S.empty, [])
+        , second (S.fromList (transitions net) :) (formulaToCut f)
+        , 2
+        )
+
+simpWithFormula :: PetriNet -> Formula Transition -> SimpConfig
+simpWithFormula net f =
+        (
+        [ return . simplifyCuts
+        , return . removeImplicants
+        , return . filterInvariantTransitions net
+        , greedySimplify net FTrue
+        , return . combineCuts
+        , simplifyBySubsumption
+        ]
+        , second (S.fromList (transitions net) :) (formulaToCut f)
+        , (S.empty, [])
+        , 2
+        )
+
+applySimpConfig :: SimpConfig -> [Cut] -> OptIO [SimpleCut]
+applySimpConfig (simpFunctions, initialCut, afterCut, otfIndex) cuts = do
             simp <- opt optSimpFormula
-
-            let simpFunctions =
-                    [ return . simplifyCuts
-                    , return . removeImplicants
-                    , simplifyBySubsumption
-                    , greedySimplify net f
-                    , simplifyBySubsumption
-                    ]
-            let (otfSimps, afterSimps) = splitAt 2 $ take simp simpFunctions
+            let (otfSimps, afterSimps) = splitAt otfIndex $ take simp simpFunctions
             let simpFunction = foldl (>=>) return afterSimps
             let otfFunction = foldl (>=>) return otfSimps
             let cnfCuts = map cutToSimpleDNFCuts cuts
-            dnfCuts <- foldM (combine otfFunction) [(S.empty, [])] cnfCuts
+            dnfCuts <- foldM (combine otfFunction) [initialCut] cnfCuts
             simpCuts <- simpFunction dnfCuts
-
-            let simpFunctions' =
-                    [ return . simplifyCuts
-                    , return . removeImplicants
-                    , return . filterInvariantTransitions net
-                    , simplifyBySubsumption
-                    , greedySimplify net FTrue
-                    , simplifyBySubsumption
-                    ]
-            let (otfSimps', afterSimps') = splitAt 2 $ take simp simpFunctions'
-            let simpFunction' = foldl (>=>) return afterSimps'
-            let otfFunction' = foldl (>=>) return otfSimps'
- 
-            let (fc0, fcs) = formulaToCut f
-            let addedTransitions = S.fromList (transitions net)
-            let addedCut = (fc0, addedTransitions : fcs)
-            simpCutsWithFormula <- combine otfFunction' [addedCut] simpCuts
-            simpCuts' <- simpFunction' simpCutsWithFormula
-            return simpCuts'
+            combine otfFunction [afterCut] simpCuts
         where
             combine simpFunction cs1 cs2 =
                 simpFunction [ (c1c0 `S.union` c2c0, c1cs ++ c2cs)
                              | (c1c0, c1cs) <- cs1, (c2c0, c2cs) <- cs2 ]
 
+generateCuts :: PetriNet -> Formula Transition -> [Cut] -> OptIO [SimpleCut]
+generateCuts net f cuts = do
+        let configs = [simpWithFormula, simpWithoutFormula]
+        let tasks = map (\c -> applySimpConfig (c net f) cuts) configs
+        rs <- parallelIO tasks
+        return $ minimumBy (comparing length) rs
+
+combineCuts :: [SimpleCut] -> [SimpleCut]
+combineCuts cuts =
+            M.toList $ M.fromListWith combineFunc cuts
+        where
+            combineFunc cs cs' =
+                simplifyPositiveCut [ c `S.union` c' | c <- cs, c' <- cs' ]
+
 filterInvariantTransitions :: PetriNet -> [SimpleCut] -> [SimpleCut]
 filterInvariantTransitions net =
         let ts = S.fromList $ invariantTransitions net
@@ -115,12 +137,15 @@ simplifyCuts = mapMaybe simplifyCut
 simplifyCut :: SimpleCut -> Maybe SimpleCut
 simplifyCut (c0, cs) =
         let remove b a = a `S.difference` b
-            cs' = removeWith S.isSubsetOf $ map (remove c0) cs
+            cs' = simplifyPositiveCut $ map (remove c0) cs
         in  if any S.null cs' then
                 Nothing
             else
                 Just (c0, cs')
 
+simplifyPositiveCut :: [S.Set Transition] -> [S.Set Transition]
+simplifyPositiveCut = removeWith S.isSubsetOf 
+
 simplifyBySubsumption :: [SimpleCut] -> OptIO [SimpleCut]
 simplifyBySubsumption = simplifyBySubsumption' []
 

src/Util.hs

@@ -5,15 +5,16 @@ module Util
      listSet,listMap,val,vals,mval,zeroVal,positiveVal,sumVal,
      makeVarMap,makeVarMapWith,buildVector,makeVector,getNames,
      Vector,Model,VarMap,SIMap,SBMap,IMap,BMap,showWeighted,
-     OptIO,verbosePut,opt,putLine)
+     OptIO,verbosePut,opt,putLine,parallelIO)
 where
 
 import Data.SBV
 import qualified Data.Map as M
-import Control.Monad
 import Data.List
 import Data.Ord
 import Data.Function
+import Control.Concurrent.ParallelIO
+import Control.Monad
 import Control.Monad.Reader
 import System.IO
 
@@ -115,6 +116,11 @@ verbosePut level str = do
 putLine :: String -> OptIO ()
 putLine = liftIO . putStrLn
 
+parallelIO :: [OptIO a] -> OptIO [a]
+parallelIO tasks = do
+        opts <- ask
+        liftIO $ parallel $ map (`runReaderT` opts) tasks
+
 {-
 - String functions
 -}