Added simplification by subsumption with smt solver

src/Main.hs

@@ -31,6 +31,7 @@ import Solver.SubnetEmptyTrap
 import Solver.LivenessInvariant
 import Solver.SafetyInvariant
 import Solver.SComponent
+import Solver.Simplifier
 --import Solver.CommFreeReachability
 
 
@@ -288,12 +289,31 @@ getLivenessInvariant net f cuts = do
         simp <- opt optSimpFormula
         let dnfCuts = generateCuts f cuts
         verbosePut 2 $ "Number of disjuncts: " ++ show (length dnfCuts)
+--        let simpCuts = if simp then simplifyCuts dnfCuts else dnfCuts
         let simpCuts = if simp then simplifyCuts dnfCuts else dnfCuts
-        verbosePut 2 $ "Number of simplified disjuncts: " ++ show (length simpCuts)
-        rs <- mapM (checkSat . checkLivenessInvariantSat net) simpCuts
+        verbosePut 2 $ "Number of simplified disjuncts (1): " ++ show (length simpCuts)
+        simpCuts' <- if simp then simplifyBySubsumption net [] simpCuts else return simpCuts
+        verbosePut 2 $ "Number of simplified disjuncts (2): " ++ show (length simpCuts')
+        rs <- mapM (checkSat . checkLivenessInvariantSat net) simpCuts'
         let added = map (Just . cutToLivenessInvariant) cuts
         return $ sequence (rs ++ added)
 
+simplifyBySubsumption :: PetriNet -> [SimpleCut] -> [SimpleCut] -> OptIO [SimpleCut]
+simplifyBySubsumption _ acc [] = return $ reverse acc
+simplifyBySubsumption net acc (c0:cs) = do
+        r <- checkSat $ checkSubsumptionSat net c0 (acc ++ cs)
+        let acc' = case r of
+                    Nothing -> acc
+                    Just _ -> c0:acc
+        simplifyBySubsumption net acc' cs
+
+removeWith :: (a -> a -> Bool) -> [a] -> [a]
+removeWith f = removeCuts' []
+        where
+            removeCuts' acc [] = reverse acc
+            removeCuts' acc (x:xs) = removeCuts' (x : cutFilter x acc) (cutFilter x xs)
+            cutFilter cut = filter (not . f cut)
+
 checkLivenessProperty' :: PetriNet ->
         Formula Transition -> [Cut] -> OptIO (Maybe FiringVector, [Cut])
 checkLivenessProperty' net f cuts = do

src/Solver/LivenessInvariant.hs

@@ -4,17 +4,18 @@ module Solver.LivenessInvariant (
   , generateCuts
   , simplifyCuts
   , cutToLivenessInvariant
+  , SimpleCut
 ) where
 
 import Data.SBV
 import Data.List (intercalate)
 import qualified Data.Map as M
+import qualified Data.Set as S
 
 import Util
 import Solver
 import Property
 import PetriNet
-import qualified Data.Set as S
 
 data LivenessInvariant =
             RankingFunction (SimpleCut, Vector Place)
@@ -160,5 +161,3 @@ getLivenessInvariant net cut y =
         RankingFunction
                 (toSimpleCut cut,
                  buildVector (map (\p -> (p, val y (placeName p))) (places net)))
-
-

src/Solver/Simplifier.hs

+module Solver.Simplifier (
+    checkSubsumptionSat
+) where
+
+import Data.SBV
+import qualified Data.Map as M
+import qualified Data.Set as S
+
+import Util
+import Solver
+import Solver.LivenessInvariant
+import PetriNet
+
+checkTransPositive :: SBMap Transition -> S.Set Transition -> SBool
+checkTransPositive m ts = bOr $ map (val m) $ S.elems ts
+
+checkTransNegative :: SBMap Transition -> S.Set Transition -> SBool
+checkTransNegative m ts = bAnd $ map (bnot . val m) $ S.elems ts
+
+checkCutPositive :: SBMap Transition -> SimpleCut -> SBool
+checkCutPositive m (c0, cs) =
+        checkTransNegative m c0 &&& bAnd (map (checkTransPositive m) cs)
+
+checkCutNegative :: SBMap Transition -> SimpleCut -> SBool
+checkCutNegative m (c0, cs) =
+        checkTransPositive m c0 ||| bOr (map (checkTransNegative m) cs)
+
+checkCuts :: SimpleCut -> [SimpleCut] -> SBMap Transition -> SBool
+checkCuts c0 cs m = checkCutPositive m c0 &&& bAnd (map (checkCutNegative m) cs)
+
+getSubsumption :: BMap Transition -> [Transition]
+getSubsumption m = M.keys (M.filter id m)
+
+checkSubsumptionSat :: PetriNet -> SimpleCut -> [SimpleCut] -> ConstraintProblem Bool [Transition]
+checkSubsumptionSat net c0 cs =
+        let m = makeVarMap $ transitions net
+        in  ("constraint subsumption", "subsumption",
+            getNames m,
+            \fm -> checkCuts c0 cs (fmap fm m),
+            \fm -> getSubsumption (fmap fm m))

src/Util.hs

@@ -15,6 +15,7 @@ import Data.List
 import Data.Ord
 import Data.Function
 import Control.Monad.Reader
+import System.IO
 
 import Options
 
@@ -109,6 +110,7 @@ verbosePut ::  Int -> String -> OptIO ()
 verbosePut level str = do
         verbosity <- opt optVerbosity
         when (verbosity >= level) (putLine str)
+        liftIO $ hFlush stdout -- TODO: remove again
 
 putLine :: String -> OptIO ()
 putLine = liftIO . putStrLn