Always output fully-simplified states (#2303)

* executionStrategy: Simplify always appears after Rewrite

* limitedExecutionStrategy: Add missing documentation

Co-authored-by: Thomas Tuegel <[email protected]>

Author: emarzion

kore/src/Kore/Step.hs

@@ -102,13 +102,27 @@ retractRemaining _ = Nothing
 -}
 executionStrategy :: Stream (Strategy Prim)
 executionStrategy =
-    (Strategy.sequence . fmap Strategy.apply)
-        [ Begin
-        , Simplify
-        , Rewrite
-        ]
-    & Stream.iterate id
+    step1 Stream.:> Stream.iterate id stepN
+  where
+    step1 =
+        (Strategy.sequence . fmap Strategy.apply)
+            [ Begin
+            , Simplify
+            , Rewrite
+            , Simplify
+            ]
+    stepN =
+        (Strategy.sequence . fmap Strategy.apply)
+            [ Begin
+            , Rewrite
+            , Simplify
+            ]
+
+{- | The sequence of transitions under the specified depth limit.
+
+See also: 'executionStrategy'
 
+ -}
 limitedExecutionStrategy :: Limit Natural -> [Strategy Prim]
 limitedExecutionStrategy depthLimit =
     Limit.takeWithin depthLimit (toList executionStrategy)
@@ -119,7 +133,7 @@ data Prim
     = Begin
     | Simplify
     | Rewrite
-    deriving (Show)
+    deriving (Eq, Show)
 
 {- The two modes of symbolic execution. Each mode determines the way
     rewrite rules are applied during a rewrite step.

kore/test/Test/Kore/Step.hs

@@ -1,10 +1,18 @@
 module Test.Kore.Step
     ( test_stepStrategy
+    , test_executionStrategy
     ) where
 
 import Prelude.Kore
 
+import Hedgehog
+    ( Gen
+    )
+import qualified Hedgehog
+import qualified Hedgehog.Gen
+import qualified Hedgehog.Range
 import Test.Tasty
+import Test.Tasty.Hedgehog
 
 import qualified Control.Exception as Exception
 import qualified Control.Lens as Lens
@@ -298,6 +306,47 @@ test_stepStrategy =
             Right _ ->
                 assertFailure "Expected exception LimitExceeded"
 
+test_executionStrategy :: [TestTree]
+test_executionStrategy =
+    [ testProperty "every step contains Rewrite" $ Hedgehog.property $ do
+        strategies <- Hedgehog.forAll genStrategies
+        for_ strategies $ \strategy -> do
+            Hedgehog.annotateShow strategy
+            Hedgehog.assert (hasRewrite strategy)
+
+    , testProperty "Simplify is the last sub-step" $ Hedgehog.property $ do
+        strategies <- Hedgehog.forAll genStrategies
+        let strategy = last strategies
+        Hedgehog.annotateShow strategy
+        Hedgehog.assert (isLastSimplify strategy)
+    ]
+  where
+    genStrategies :: Gen [Strategy Prim]
+    genStrategies = do
+        let range = Hedgehog.Gen.integral (Hedgehog.Range.linear 1 16)
+        depthLimit <- Limit <$> range
+        pure (limitedExecutionStrategy depthLimit)
+
+    hasRewrite :: Strategy Prim -> Bool
+    hasRewrite = \case
+        Strategy.Seq s1 s2 -> hasRewrite s1 || hasRewrite s2
+        Strategy.And s1 s2 -> hasRewrite s1 || hasRewrite s2
+        Strategy.Or s1 s2 -> hasRewrite s1 || hasRewrite s2
+        Strategy.Apply p -> p == Rewrite
+        Strategy.Stuck -> False
+        Strategy.Continue -> False
+
+    isLastSimplify :: Strategy Prim -> Bool
+    isLastSimplify = \case
+        Strategy.Seq s Strategy.Continue -> isLastSimplify s
+        Strategy.Seq s Strategy.Stuck -> isLastSimplify s
+        Strategy.Seq _ s -> isLastSimplify s
+        Strategy.And s1 s2 -> isLastSimplify s1 && isLastSimplify s2
+        Strategy.Or s1 s2 -> isLastSimplify s1 && isLastSimplify s2
+        Strategy.Apply p -> p == Simplify
+        Strategy.Stuck -> False
+        Strategy.Continue -> False
+
 simpleRewrite
     :: TermLike VariableName
     -> TermLike VariableName