Extract strategy from class Goal

The strategy belongs to and is common to all reachability proofs.

Author: ttuegel

kore/src/Kore/Strategies/Goal.hs

@@ -4,6 +4,7 @@ License     : NCSA
 -}
 module Kore.Strategies.Goal
     ( Goal (..)
+    , strategy
     , TransitionRule
     , Prim
     , FromRulePattern (..)
@@ -13,10 +14,8 @@ module Kore.Strategies.Goal
     , extractClaims
     , unprovenNodes
     , proven
-    , onePathFirstStep
-    , onePathFollowupStep
-    , allPathFirstStep
-    , allPathFollowupStep
+    , reachabilityFirstStep
+    , reachabilityNextStep
     , getConfiguration
     , getDestination
     , transitionRule
@@ -196,12 +195,8 @@ class Goal goal where
         => goal -> Rule goal
     goalToRule = coerce
 
-    strategy
-        :: goal
-        -> [goal]
-        -> [Rule goal]
-        -> Stream (Strategy Prim)
-
+    -- TODO (thomas.tuegel): isTriviallyValid should be part of
+    -- checkImplication. why is this so slow?
     isTriviallyValid :: goal -> Bool
 
     checkImplication
@@ -309,8 +304,6 @@ instance Goal OnePathRule where
 
     isTriviallyValid = isTriviallyValid' _Unwrapped
 
-    strategy _ _ _ = onePathFirstStep :> Stream.iterate id onePathFollowupStep
-
 deriveSeqOnePath
     ::  MonadSimplify simplifier
     =>  [Rule OnePathRule]
@@ -364,8 +357,6 @@ instance Goal AllPathRule where
           | all isTriviallyValid proofState = pure Proven
           | otherwise = pure proofState
 
-    strategy _ _ _ = allPathFirstStep :> Stream.iterate id allPathFollowupStep
-
 deriveParAllPath
     ::  MonadSimplify simplifier
     =>  [Rule AllPathRule]
@@ -433,24 +424,6 @@ instance Goal ReachabilityRule where
         & fmap (fmap OnePath)
         & onePathTransition
 
-    strategy
-        :: ReachabilityRule
-        -> [ReachabilityRule]
-        -> [Rule ReachabilityRule]
-        -> Stream (Strategy Prim)
-    strategy goal claims axioms =
-        case goal of
-            OnePath rule ->
-                strategy
-                    rule
-                    (mapMaybe maybeOnePath claims)
-                    (fmap ruleReachabilityToRuleOnePath axioms)
-            AllPath rule ->
-                strategy
-                    rule
-                    (mapMaybe maybeAllPath claims)
-                    (fmap ruleReachabilityToRuleAllPath axioms)
-
 instance ClaimExtractor ReachabilityRule where
     extractClaim (attrs, sentence) =
         case fromSentenceAxiom (attrs, Syntax.getSentenceClaim sentence) of
@@ -478,19 +451,6 @@ maybeAllPath :: ReachabilityRule -> Maybe AllPathRule
 maybeAllPath (AllPath rule) = Just rule
 maybeAllPath _ = Nothing
 
--- The functions below are easier to read coercions between
--- the newtypes over 'RewriteRule VariableName' defined in the
--- instances of 'Goal' as 'Rule's.
-ruleReachabilityToRuleAllPath
-    :: Rule ReachabilityRule
-    -> Rule AllPathRule
-ruleReachabilityToRuleAllPath = coerce
-
-ruleReachabilityToRuleOnePath
-    :: Rule ReachabilityRule
-    -> Rule OnePathRule
-ruleReachabilityToRuleOnePath = coerce
-
 ruleAllPathToRuleReachability
     :: Rule AllPathRule
     -> Rule ReachabilityRule
@@ -592,8 +552,8 @@ transitionRule claims axiomGroups = transitionRuleWorker
 
     transitionRuleWorker _ state = return state
 
-onePathFirstStep :: Strategy Prim
-onePathFirstStep =
+reachabilityFirstStep :: Strategy Prim
+reachabilityFirstStep =
     (Strategy.sequence . map Strategy.apply)
         [ CheckProven
         , CheckGoalStuck
@@ -607,8 +567,8 @@ onePathFirstStep =
         , TriviallyValid
         ]
 
-onePathFollowupStep :: Strategy Prim
-onePathFollowupStep =
+reachabilityNextStep :: Strategy Prim
+reachabilityNextStep =
     (Strategy.sequence . map Strategy.apply)
         [ CheckProven
         , CheckGoalStuck
@@ -623,36 +583,9 @@ onePathFollowupStep =
         , TriviallyValid
         ]
 
-allPathFirstStep :: Strategy Prim
-allPathFirstStep =
-    (Strategy.sequence . map Strategy.apply)
-        [ CheckProven
-        , CheckGoalStuck
-        , CheckGoalRemainder
-        , Simplify
-        , TriviallyValid
-        , CheckImplication
-        , ApplyAxioms
-        , ResetGoal
-        , Simplify
-        , TriviallyValid
-        ]
-
-allPathFollowupStep :: Strategy Prim
-allPathFollowupStep =
-    (Strategy.sequence . map Strategy.apply)
-        [ CheckProven
-        , CheckGoalStuck
-        , CheckGoalRemainder
-        , Simplify
-        , TriviallyValid
-        , CheckImplication
-        , ApplyClaims
-        , ApplyAxioms
-        , ResetGoal
-        , Simplify
-        , TriviallyValid
-        ]
+strategy :: Stream (Strategy Prim)
+strategy =
+    reachabilityFirstStep :> Stream.iterate id reachabilityNextStep
 
 {- | The result of checking the direct implication of a proof goal.
 

kore/src/Kore/Strategies/Verification.hs

@@ -45,7 +45,6 @@ import qualified Data.Graph.Inductive.Graph as Graph
 import Data.List.Extra
     ( groupSortOn
     )
-import qualified Data.Stream.Infinite as Stream
 import Data.Text
     ( Text
     )
@@ -248,7 +247,7 @@ verifyClaim
     let
         startPattern = ProofState.Goal $ getConfiguration goal
         limitedStrategy =
-            strategy goal claims axioms
+            strategy
             & Foldable.toList
             & Limit.takeWithin depthLimit
     Strategy.leavesM
@@ -344,10 +343,10 @@ verifyClaimStep target claims axioms executionGraph node =
         | otherwise = followupStep
 
     firstStep :: Strategy Prim
-    firstStep = strategy target claims axioms Stream.!! 0
+    firstStep = reachabilityFirstStep
 
     followupStep :: Strategy Prim
-    followupStep = strategy target claims axioms Stream.!! 1
+    followupStep = reachabilityNextStep
 
     ExecutionGraph { root } = executionGraph
 

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

@@ -27,10 +27,6 @@ import Data.Sequence
     ( Seq
     )
 import qualified Data.Sequence as Seq
-import Data.Stream.Infinite
-    ( Stream (..)
-    )
-import qualified Data.Stream.Infinite as Stream
 import qualified Generics.SOP as SOP
 import qualified GHC.Generics as GHC
 
@@ -152,7 +148,7 @@ test_transitionRule_CheckImplication :: [TestTree]
 test_transitionRule_CheckImplication =
     [ unmodified ProofState.Proven
     , unmodified (ProofState.GoalRemainder (A, B))
-    , ProofState.Goal (B, B) `becomes` (ProofState.Goal (Bot, B), mempty)
+    , ProofState.Goal (B, B) `becomes` (ProofState.Proven, mempty)
     ]
   where
     run = runTransitionRule [] [] ProofState.CheckImplication
@@ -180,12 +176,12 @@ test_transitionRule_ApplyClaims =
     , unmodified (ProofState.GoalRewritten    (A, B))
     , [Rule (A, C)]
         `derives`
-        [ (ProofState.Goal    (C,   C), Seq.singleton $ Rule (A, C))
+        [ (ProofState.GoalRewritten (C,   C), Seq.singleton $ Rule (A, C))
         , (ProofState.GoalRemainder (Bot, C), mempty)
         ]
     , fmap Rule [(A, B), (B, C)]
         `derives`
-        [ (ProofState.Goal    (B  , C), Seq.singleton $ Rule (A, B))
+        [ (ProofState.GoalRewritten (B  , C), Seq.singleton $ Rule (A, B))
         , (ProofState.GoalRemainder (Bot, C), mempty)
         ]
     ]
@@ -208,12 +204,12 @@ test_transitionRule_ApplyAxioms =
     , unmodified (ProofState.GoalRewritten    (A, B))
     , [Rule (A, C)]
         `derives`
-        [ (ProofState.Goal    (C,   C), Seq.singleton $ Rule (A, C))
+        [ (ProofState.GoalRewritten (C,   C), Seq.singleton $ Rule (A, C))
         , (ProofState.GoalRemainder (Bot, C), mempty)
         ]
     , fmap Rule [(A, B), (B, C)]
         `derives`
-        [ (ProofState.Goal    (B  , C), Seq.singleton $ Rule (A, B))
+        [ (ProofState.GoalRewritten (B  , C), Seq.singleton $ Rule (A, B))
         , (ProofState.GoalRemainder (Bot, C), mempty)
         ]
     ]
@@ -244,6 +240,7 @@ test_runStrategy =
 
     , [Rule (A, A)] `proves` (A, B)
     , [Rule (A, A)] `proves` (A, C)
+    , [Rule (A, A)] `disproves` (A, C) $ []
 
     , fmap Rule [(A, B), (A, C)] `proves`    (A, BorC)
     , fmap Rule [(A, B), (A, C)] `disproves` (A, B   ) $ [(C, B)]
@@ -261,7 +258,7 @@ test_runStrategy =
         $ Strategy.runStrategy
             Unlimited
             (Goal.transitionRule [unRule goal] [axioms])
-            (Foldable.toList $ Goal.strategy (unRule goal) [unRule goal] axioms)
+            (Foldable.toList Goal.strategy)
             (ProofState.Goal . unRule $ goal)
     disproves
         :: HasCallStack
@@ -347,41 +344,11 @@ newtype instance Goal.Rule Goal =
     deriving (Eq, GHC.Generic, Show)
 
 instance Goal.Goal Goal where
-    strategy _ _ _ =
-        firstStep :> Stream.iterate id nextStep
+    checkImplication (src, dst)
+      | src' == Bot = return Goal.Implied
+      | otherwise = return $ Goal.NotImplied (src', dst)
       where
-        firstStep =
-            (Strategy.sequence . map Strategy.apply)
-                [ ProofState.CheckProven
-                , ProofState.CheckGoalRemainder
-                , ProofState.CheckImplication
-                , ProofState.TriviallyValid
-                , ProofState.ApplyAxioms
-                , ProofState.Simplify
-                , ProofState.TriviallyValid
-                , ProofState.ResetGoal
-                , ProofState.TriviallyValid
-                ]
-        nextStep =
-            (Strategy.sequence . map Strategy.apply)
-                [ ProofState.CheckProven
-                , ProofState.CheckGoalRemainder
-                , ProofState.CheckImplication
-                , ProofState.TriviallyValid
-                , ProofState.ApplyClaims
-                , ProofState.CheckImplication
-                , ProofState.Simplify
-                , ProofState.TriviallyValid
-                , ProofState.ApplyAxioms
-                , ProofState.CheckImplication
-                , ProofState.Simplify
-                , ProofState.TriviallyValid
-                , ProofState.ResetGoal
-                , ProofState.TriviallyValid
-                ]
-
-    checkImplication (src, dst) =
-        return . Goal.NotImplied $ (difference src dst, dst)
+        src' = difference src dst
 
     -- | The goal is trivially valid when the members are equal.
     isTriviallyValid :: Goal -> Bool
@@ -402,7 +369,7 @@ derivePar rules (src, dst) =
   where
     goal rule@(Rule (_, to)) = do
         Transition.addRule rule
-        (pure . ProofState.Goal) (to, dst)
+        (pure . ProofState.GoalRewritten) (to, dst)
     goalRemainder = do
         let r = Foldable.foldl' difference src (fst . unRule <$> applied)
         (pure . ProofState.GoalRemainder) (r, dst)

kore/test/Test/Kore/Strategies/OnePath/Step.hs

@@ -892,10 +892,7 @@ runOnePathSteps
         coinductiveRewrites
         (groupSortOn Attribute.Axiom.getPriorityOfAxiom rewrites)
         goal
-        (Limit.takeWithin
-            depthLimit
-            (Foldable.toList $ strategy goal coinductiveRewrites rewrites)
-        )
+        (Limit.takeWithin depthLimit (Foldable.toList strategy))
     return (sort $ nub result)
 
 assertStuck