Fix breadth limit bug; implementation for prove

kore/app/exec/Main.hs

@@ -89,11 +89,11 @@ import Kore.IndexedModule.IndexedModule
 import qualified Kore.IndexedModule.MetadataToolsBuilder as MetadataTools
     ( build
     )
+import qualified Kore.Internal.OrPattern as OrPattern
 import Kore.Internal.Pattern
     ( Conditional (..)
     , Pattern
     )
-import qualified Kore.Internal.Pattern as Pattern
 import Kore.Internal.Predicate
     ( makePredicate
     )
@@ -678,12 +678,15 @@ koreProve execOptions proveOptions = do
             maybeAlreadyProvenModule
 
     (exitCode, final) <- case proveResult of
-        Left Stuck { stuckPattern, provenClaims } -> do
+        Left Stuck { stuckPatterns, provenClaims } -> do
             maybe
                 (return ())
                 (lift . saveProven specModule provenClaims)
                 saveProofs
-            return (failure $ Pattern.toTermLike stuckPattern)
+            stuckPatterns
+                & OrPattern.toTermLike
+                & failure
+                & return
         Right () -> return success
 
     lift $ renderResult execOptions (unparse final)

kore/src/Kore/Exec.hs

@@ -224,7 +224,10 @@ exec breadthLimit verifiedModule strategy initialTerm =
                 let
                     updateQueue = \as ->
                         Strategy.unfoldDepthFirst as
-                        >=> lift . Strategy.applyBreadthLimit breadthLimit
+                        >=> lift
+                            . Strategy.applyBreadthLimit
+                                breadthLimit
+                                dropStrategy
                     transit instr config =
                         Strategy.transitionRule transitionRule instr config
                         & runTransitionT
@@ -238,6 +241,7 @@ exec breadthLimit verifiedModule strategy initialTerm =
         let finalTerm = forceSort initialSort $ Pattern.toTermLike finalConfig
         return (exitCode, finalTerm)
   where
+    dropStrategy = snd
     -- Get the first final configuration of an execution graph.
     getFinalConfigOf = takeFirstResult >=> orElseBottom
       where

kore/src/Kore/Step/Strategy.hs

@@ -451,8 +451,6 @@ See also: 'pickLongest', 'pickFinal', 'pickOne', 'pickStar', 'pickPlus'
 constructExecutionGraph
     :: forall m config rule instr
     .  (MonadProfiler m, MonadThrow m)
-    => Show instr
-    => Typeable instr
     => Limit Natural
     -> (instr -> config -> TransitionT rule m config)
     -> [instr]
@@ -464,10 +462,11 @@ constructExecutionGraph breadthLimit transit instrs0 searchOrder0 config0 =
     & flip State.execStateT execGraph
   where
     execGraph = emptyExecutionGraph config0
+    dropStrategy = snd
 
     mkQueue = \as ->
         unfoldSearchOrder searchOrder0 as
-        >=> applyBreadthLimit breadthLimit
+        >=> applyBreadthLimit breadthLimit dropStrategy
         >=> profileQueueLength
 
     profileQueueLength queue = do
@@ -546,14 +545,15 @@ unfoldSearchOrder DepthFirst = unfoldDepthFirst
 unfoldSearchOrder BreadthFirst = unfoldBreadthFirst
 
 applyBreadthLimit
-    :: Exception (LimitExceeded a)
+    :: Exception (LimitExceeded b)
     => MonadThrow m
     => Limit Natural
+    -> (a -> b)
     -> Seq a
     -> m (Seq a)
-applyBreadthLimit breadthLimit as
-  | _ Seq.:<| as' <- as, exceedsLimit as' =
-    Exception.throwM (LimitExceeded as)
+applyBreadthLimit breadthLimit transf as
+  | exceedsLimit as =
+    Exception.throwM (LimitExceeded (transf <$> as))
   | otherwise = pure as
   where
     exceedsLimit = not . withinLimit breadthLimit . fromIntegral . Seq.length
@@ -637,8 +637,6 @@ See also: 'pickLongest', 'pickFinal', 'pickOne', 'pickStar', 'pickPlus'
 runStrategy
     :: forall m prim rule config
     .  (MonadProfiler m, MonadThrow m)
-    => Show prim
-    => Typeable prim
     => Limit Natural
     -> (prim -> config -> TransitionT rule m config)
     -- ^ Primitive strategy rule
@@ -653,8 +651,6 @@ runStrategy breadthLimit applyPrim instrs0 config0 =
 runStrategyWithSearchOrder
     :: forall m prim rule config
     .  (MonadProfiler m, MonadThrow m)
-    => Show prim
-    => Typeable prim
     => Limit Natural
     -> (prim -> config -> TransitionT rule m config)
     -- ^ Primitive strategy rule

kore/src/Kore/Strategies/Verification.hs

@@ -29,6 +29,7 @@ import qualified Control.Monad as Monad
     )
 import Control.Monad.Catch
     ( MonadCatch
+    , handle
     )
 import Control.Monad.Except
     ( ExceptT
@@ -52,6 +53,10 @@ import Data.Limit
     )
 import qualified Data.Limit as Limit
 import Kore.Debug
+import Kore.Internal.OrPattern
+    ( OrPattern
+    )
+import qualified Kore.Internal.OrPattern as OrPattern
 import Kore.Internal.Pattern
     ( Pattern
     )
@@ -92,7 +97,10 @@ import qualified Logic
 -- TODO (thomas.tuegel): (Pattern VariableName) should be ReachabilityRule.
 type CommonProofState = ProofState.ProofState (Pattern VariableName)
 
-commonProofStateTransformer :: ProofStateTransformer (Pattern VariableName) (Pattern VariableName)
+commonProofStateTransformer
+    :: ProofStateTransformer
+        (Pattern VariableName)
+        (Pattern VariableName)
 commonProofStateTransformer =
     ProofStateTransformer
         { goalTransformer = id
@@ -108,7 +116,7 @@ The action may throw an exception if the proof fails; the exception is a single
 @'Pattern' 'VariableName'@, the first unprovable configuration.
 
  -}
-type Verifier m = ExceptT (Pattern VariableName) m
+type Verifier m = ExceptT (OrPattern VariableName) m
 
 {- | Verifies a set of claims. When it verifies a certain claim, after the
 first step, it also uses the claims as axioms (i.e. it does coinductive proofs).
@@ -121,7 +129,7 @@ If the verification succeeds, it returns ().
 -}
 data Stuck =
     Stuck
-    { stuckPattern :: !(Pattern VariableName)
+    { stuckPatterns :: !(OrPattern VariableName)
     , provenClaims :: ![ReachabilityRule]
     }
     deriving (Eq, GHC.Generic, Show)
@@ -204,8 +212,8 @@ verifyHelper breadthLimit searchOrder claims axioms (ToProve toProve) =
             verifyClaim breadthLimit searchOrder claims axioms unprovenClaim
             return (claim : provenClaims)
       where
-        wrapStuckPattern :: Pattern VariableName -> Stuck
-        wrapStuckPattern stuckPattern = Stuck { stuckPattern, provenClaims }
+        wrapStuckPattern :: OrPattern VariableName -> Stuck
+        wrapStuckPattern stuckPatterns = Stuck { stuckPatterns, provenClaims }
 
 verifyClaim
     :: forall simplifier
@@ -215,7 +223,7 @@ verifyClaim
     -> AllClaims ReachabilityRule
     -> Axioms ReachabilityRule
     -> (ReachabilityRule, Limit Natural)
-    -> ExceptT (Pattern VariableName) simplifier ()
+    -> ExceptT (OrPattern VariableName) simplifier ()
 verifyClaim
     breadthLimit
     searchOrder
@@ -230,19 +238,31 @@ verifyClaim
             strategy goal claims axioms
             & Foldable.toList
             & Limit.takeWithin depthLimit
-    Strategy.leavesM
-        updateQueue
-        (Strategy.unfoldTransition transit)
-        (limitedStrategy, startPattern)
-        & fmap discardStrategy
-        & throwUnproven
+    handle
+        handleLimitExceeded
+        $ Strategy.leavesM
+            updateQueue
+            (Strategy.unfoldTransition transit)
+            (limitedStrategy, startPattern)
+            & fmap discardStrategy
+            & throwUnproven
   where
     destination = getDestination goal
     discardStrategy = snd
 
+    handleLimitExceeded
+        :: Strategy.LimitExceeded CommonProofState
+        -> ExceptT (OrPattern VariableName) simplifier ()
+    handleLimitExceeded (Strategy.LimitExceeded patterns) =
+        Monad.Except.throwError
+        . OrPattern.fromPatterns
+        $ fmap
+            (ProofState.proofState commonProofStateTransformer)
+            patterns
+
     updateQueue = \as ->
         Strategy.unfoldSearchOrder searchOrder as
-        >=> lift . Strategy.applyBreadthLimit breadthLimit
+        >=> lift . Strategy.applyBreadthLimit breadthLimit snd
         >=> profileQueueLength
 
     profileQueueLength queue = do
@@ -263,7 +283,7 @@ verifyClaim
         -> Verifier simplifier ()
     throwUnprovenOrElse proofState acts = do
         ProofState.extractUnproven proofState
-            & Foldable.traverse_ Monad.Except.throwError
+            & Foldable.traverse_ (Monad.Except.throwError . OrPattern.fromPattern)
         acts
 
     transit instr config =

kore/test/Test/Kore/Exec.hs

@@ -55,10 +55,8 @@ import Kore.Internal.Predicate
     )
 import Kore.Internal.TermLike
 import qualified Kore.Internal.TermLike as TermLike
-import Kore.Rewriting.RewritingVariable
 import Kore.Step
-    ( Prim (..)
-    , priorityAllStrategy
+    ( priorityAllStrategy
     , priorityAnyStrategy
     )
 import Kore.Step.Rule
@@ -74,7 +72,6 @@ import Kore.Step.Search
 import qualified Kore.Step.Search as Search
 import Kore.Step.Strategy
     ( LimitExceeded (..)
-    , Strategy (..)
     )
 import Kore.Syntax.Definition hiding
     ( Symbol
@@ -227,7 +224,7 @@ test_searchExceedingBreadthLimit =
 
     assertion searchType =
         catch (shouldExceedBreadthLimit searchType)
-        $ \(_ :: LimitExceeded ([Strategy (Prim (RewriteRule RewritingVariableName))], Graph.Node)) ->
+        $ \(_ :: LimitExceeded Graph.Node) ->
             pure ()
 
     shouldExceedBreadthLimit :: SearchType -> IO ()

kore/test/Test/Kore/Strategies/AllPath/Verification.hs

@@ -14,13 +14,13 @@ import Data.Limit
     )
 
 import qualified Kore.Attribute.Axiom as Attribute
+import qualified Kore.Internal.OrPattern as OrPattern
 import Kore.Internal.Pattern
     ( Conditional (Conditional)
     )
 import Kore.Internal.Pattern as Conditional
     ( Conditional (..)
     )
-import Kore.Internal.Pattern as Pattern
 import Kore.Internal.Predicate
     ( makeEqualsPredicate
     , makeNotPredicate
@@ -67,7 +67,7 @@ test_allPathVerification =
             [ simpleClaim Mock.a Mock.b ]
             []
         assertEqual ""
-            (Left $ Pattern.fromTermLike Mock.a)
+            (Left $ OrPattern.fromTermLike Mock.a)
             actual
     -- TODO(Ana): this should be uncommented if we decide
     --            that the destination doesn't need to be
@@ -133,7 +133,7 @@ test_allPathVerification =
             [ simpleClaim Mock.a Mock.b ]
             []
         assertEqual ""
-            (Left $ Pattern.fromTermLike Mock.c)
+            (Left $ OrPattern.fromTermLike Mock.c)
             actual
     , testCase "Verifies one claim with branching" $ do
         -- Axiom: constr11(a) => b
@@ -169,7 +169,8 @@ test_allPathVerification =
             [simpleClaim (Mock.functionalConstr10 (mkElemVar Mock.x)) Mock.b]
             []
         assertEqual ""
-            (Left Conditional
+            ( Left . OrPattern.fromPattern
+            $ Conditional
                 { term = Mock.functionalConstr11 (mkElemVar Mock.x)
                 , predicate =
                     makeNotPredicate
@@ -221,7 +222,7 @@ test_allPathVerification =
             ]
             []
         assertEqual ""
-            (Left $ Pattern.fromTermLike Mock.c)
+            (Left $ OrPattern.fromTermLike Mock.c)
             actual
     , testCase "fails second of two claims" $ do
         -- Axiom: a => b
@@ -242,7 +243,7 @@ test_allPathVerification =
             ]
             []
         assertEqual ""
-            (Left $ Pattern.fromTermLike Mock.e)
+            (Left $ OrPattern.fromTermLike Mock.e)
             actual
     , testCase "second proves first but fails" $ do
         -- Axiom: a => b
@@ -261,7 +262,7 @@ test_allPathVerification =
             ]
             []
         assertEqual ""
-            (Left $ Pattern.fromTermLike Mock.b)
+            (Left $ OrPattern.fromTermLike Mock.b)
             actual
     , testCase "first proves second but fails" $ do
         -- Axiom: a => b
@@ -280,7 +281,7 @@ test_allPathVerification =
             ]
             []
         assertEqual ""
-            (Left $ Pattern.fromTermLike Mock.b)
+            (Left $ OrPattern.fromTermLike Mock.b)
             actual
     , testCase "trusted first proves second" $ do
         -- Axiom: a => b
@@ -323,7 +324,7 @@ test_allPathVerification =
             ]
             []
         assertEqual ""
-            (Left $ Pattern.fromTermLike Mock.e)
+            (Left $ OrPattern.fromTermLike Mock.e)
             actual
     , testCase "Priority: should get stuck because of second axiom" $ do
         -- Axioms:
@@ -343,7 +344,7 @@ test_allPathVerification =
             ]
             []
         assertEqual ""
-            (Left $ Pattern.fromTermLike Mock.c)
+            (Left $ OrPattern.fromTermLike Mock.c)
             actual
     , testCase "Priority: should succeed, prefering axiom with priority 1" $ do
         -- Axioms:

kore/test/Test/Kore/Strategies/Common.hs

@@ -17,8 +17,8 @@ import Numeric.Natural
     ( Natural
     )
 
-import Kore.Internal.Pattern
-    ( Pattern
+import Kore.Internal.OrPattern
+    ( OrPattern
     )
 import Kore.Internal.TermLike
 import Kore.Rewriting.RewritingVariable
@@ -59,7 +59,7 @@ runVerificationToPattern
     -> [Rule ReachabilityRule]
     -> [ReachabilityRule]
     -> [ReachabilityRule]
-    -> IO (Either (Pattern VariableName) ())
+    -> IO (Either (OrPattern VariableName) ())
 runVerificationToPattern breadthLimit depthLimit axioms claims alreadyProven =
     do
         stuck <- runVerification
@@ -70,7 +70,8 @@ runVerificationToPattern breadthLimit depthLimit axioms claims alreadyProven =
             alreadyProven
         return (toPattern stuck)
   where
-    toPattern = Bifunctor.first stuckPattern
+    toPattern =
+        Bifunctor.first stuckPatterns
 
 runVerification
     :: Limit Natural