Change the representation of reachability claims, part 2

kore/app/exec/Main.hs

@@ -134,12 +134,12 @@ import Kore.Parser
     )
 import Kore.Rewriting.RewritingVariable
 import Kore.Step
-import Kore.Step.RulePattern
+import Kore.Step.ClaimPattern
     ( ReachabilityRule
-    , RewriteRule
+    , toSentence
     )
-import qualified Kore.Step.RulePattern as Rule
-    ( toSentence
+import Kore.Step.RulePattern
+    ( RewriteRule
     )
 import Kore.Step.Search
     ( SearchType (..)
@@ -757,7 +757,7 @@ koreProve execOptions proveOptions = do
             Module
                 { moduleName = savedProofsModuleName
                 , moduleSentences =
-                    specModuleDefinitions ++ map Rule.toSentence provenClaims
+                    specModuleDefinitions <> fmap toSentence provenClaims
                 , moduleAttributes = def
                 }
         provenDefinition = Definition

kore/src/Kore/ASTVerifier/SentenceVerifier.hs

@@ -75,26 +75,22 @@ import qualified Kore.Builtin as Builtin
 import Kore.Error
 import Kore.IndexedModule.IndexedModule
 import Kore.IndexedModule.Resolvers as Resolvers
-import Kore.Internal.Predicate
-    ( unwrapPredicate
-    )
 import qualified Kore.Internal.Symbol as Internal.Symbol
 import Kore.Internal.TermLike.TermLike
     ( freeVariables
     )
 import Kore.Sort
-import qualified Kore.Step.AntiLeft as AntiLeft
-    ( toTermLike
+import Kore.Step.ClaimPattern
+    ( AllPathRule (..)
+    , ClaimPattern
+    , OnePathRule (..)
+    , freeVariablesLeft
+    , freeVariablesRight
     )
 import Kore.Step.Rule
     ( QualifiedAxiomPattern (..)
     , fromSentenceAxiom
     )
-import Kore.Step.RulePattern
-    ( AllPathRule (..)
-    , OnePathRule (..)
-    , RulePattern (..)
-    )
 import Kore.Syntax.Definition
 import Kore.Syntax.Variable
 import qualified Kore.Verified as Verified
@@ -411,27 +407,19 @@ verifyClaimSentence sentence =
             ((attrs, verified) :)
     rejectClaim attrs verified =
         case fromSentenceAxiom (attrs, verified) of
-            Right (OnePathClaimPattern (OnePathRule rulePattern))
-              | rejectRulePattern rulePattern -> True
-            Right (AllPathClaimPattern (AllPathRule rulePattern))
-              | rejectRulePattern rulePattern -> True
+            Right (OnePathClaimPattern (OnePathRule claimPattern))
+              | rejectClaimPattern claimPattern -> True
+            Right (AllPathClaimPattern (AllPathRule claimPattern))
+              | rejectClaimPattern claimPattern -> True
             _ -> False
-    rejectRulePattern :: RulePattern VariableName -> Bool
-    rejectRulePattern
-        RulePattern
-            { left
-            , antiLeft
-            , requires
-            , rhs
-            }
-      =
-        not $ Set.isSubsetOf rightVars leftVars
+    rejectClaimPattern :: ClaimPattern -> Bool
+    rejectClaimPattern claimPattern =
+        not $ Set.isSubsetOf freeRightVars freeLeftVars
           where
-            rightVars, leftVars :: Set (SomeVariable VariableName)
-            rightVars = freeVariables rhs & FreeVariables.toSet
-            lhs = Foldable.toList (AntiLeft.toTermLike <$> antiLeft)
-                <> [left, unwrapPredicate requires]
-            leftVars = foldMap freeVariables lhs & FreeVariables.toSet
+            freeRightVars =
+                freeVariablesRight claimPattern & FreeVariables.toSet
+            freeLeftVars =
+                freeVariablesLeft claimPattern & FreeVariables.toSet
 
 verifySorts :: [ParsedSentence] -> SentenceVerifier ()
 verifySorts = Foldable.traverse_ verifySortSentence . mapMaybe project

kore/src/Kore/Exec.hs

@@ -31,6 +31,7 @@ import Control.Error
     ( note
     , runMaybeT
     )
+import qualified Control.Lens as Lens
 import Control.Monad
     ( (>=>)
     )
@@ -108,6 +109,10 @@ import qualified Kore.Repl as Repl
 import qualified Kore.Repl.Data as Repl.Data
 import Kore.Rewriting.RewritingVariable
 import Kore.Step
+import Kore.Step.ClaimPattern
+    ( ReachabilityRule (..)
+    , lensClaimPattern
+    )
 import Kore.Step.Rule
     ( extractImplicationClaims
     , extractRewriteAxioms
@@ -124,11 +129,11 @@ import Kore.Step.Rule.Simplify
     )
 import Kore.Step.RulePattern
     ( ImplicationRule (..)
-    , ReachabilityRule (..)
     , RewriteRule (RewriteRule)
-    , ToRulePattern (..)
     , getRewriteRule
     , lhsEqualsRhs
+    , mkRewritingRule
+    , unRewritingRule
     )
 import Kore.Step.RulePattern as RulePattern
     ( RulePattern (..)
@@ -233,10 +238,13 @@ exec breadthLimit verifiedModule strategy initialTerm =
                 Strategy.leavesM
                     updateQueue
                     (Strategy.unfoldTransition transit)
-                    (strategy rewriteRules, (ExecDepth 0, initialConfig))
+                    ( strategy rewriteRules
+                    , (ExecDepth 0, mkRewritingPattern initialConfig)
+                    )
         infoExecDepth execDepth
-        exitCode <- getExitCode verifiedModule finalConfig
-        let finalTerm = forceSort initialSort $ Pattern.toTermLike finalConfig
+        let finalConfig' = getRewritingPattern finalConfig
+        exitCode <- getExitCode verifiedModule finalConfig'
+        let finalTerm = forceSort initialSort $ Pattern.toTermLike finalConfig'
         return (exitCode, finalTerm)
   where
     dropStrategy = snd
@@ -247,7 +255,7 @@ exec breadthLimit verifiedModule strategy initialTerm =
         takeFirstResult act =
             Logic.observeT (takeResult <$> lift act) & runMaybeT
         orElseBottom =
-            pure . fromMaybe (ExecDepth 0, Pattern.bottomOf initialSort)
+            pure . fromMaybe (ExecDepth 0, mkRewritingPattern (Pattern.bottomOf initialSort))
     verifiedModule' =
         IndexedModule.mapPatterns
             -- TODO (thomas.tuegel): Move this into Kore.Builtin
@@ -339,19 +347,23 @@ search breadthLimit verifiedModule strategy termLike searchPattern searchConfig
                     (config : _) -> config
             runStrategy' =
                 runStrategy breadthLimit transitionRule (strategy rewriteRules)
-        executionGraph <- runStrategy' initialPattern
+        executionGraph <- runStrategy' (mkRewritingPattern initialPattern)
         let
             match target config = Search.matchWith target config
         solutionsLists <-
             searchGraph
                 searchConfig
-                (match SideCondition.topTODO searchPattern)
+                (match SideCondition.topTODO (mkRewritingPattern searchPattern))
                 executionGraph
         let
             solutions = concatMap MultiOr.extractPatterns solutionsLists
             orPredicate =
                 makeMultipleOrPredicate (Condition.toPredicate <$> solutions)
-        return (forceSort patternSort $ unwrapPredicate orPredicate)
+        return
+            . forceSort patternSort
+            . getRewritingTerm
+            . unwrapPredicate
+            $ orPredicate
   where
     patternSort = termLikeSort termLike
 
@@ -643,8 +655,9 @@ simplifyReachabilityRule
     => ReachabilityRule
     -> simplifier ReachabilityRule
 simplifyReachabilityRule rule = do
-    rule' <- Rule.simplifyRewriteRule (RewriteRule . toRulePattern $ rule)
-    return (Goal.fromRulePattern rule . getRewriteRule $ rule')
+    let claim = Lens.view lensClaimPattern rule
+    claim' <- Rule.simplifyClaimPattern claim
+    return $ Lens.set lensClaimPattern claim' rule
 
 -- | Collect various rules and simplifiers in preparation to execute.
 initialize

kore/src/Kore/IndexedModule/SortGraph.hs

@@ -72,8 +72,6 @@ fromSubsorts relations =
 
         nodeMap :: Map Sort Int
         nodeMap = Map.fromList (map swap lnodes)
-          where
-            swap (x, y) = (y, x)
 
         edges :: [Graph.LEdge ()]
         edges =

kore/src/Kore/Internal/Conditional.hs

@@ -20,6 +20,7 @@ module Kore.Internal.Conditional
     , isPredicate
     , Kore.Internal.Conditional.mapVariables
     , isNormalized
+    , assertNormalized
     , markPredicateSimplified
     , markPredicateSimplifiedConditional
     , setPredicateSimplified
@@ -463,6 +464,21 @@ isNormalized Conditional { predicate, substitution } =
     Substitution.isNormalized substitution
     && Predicate.isFreeOf predicate (Substitution.variables substitution)
 
+{- | See also: 'isNormalized'
+ -}
+assertNormalized
+    :: HasCallStack
+    => Ord variable
+    => Conditional variable term
+    -> a
+    -> a
+assertNormalized Conditional { predicate, substitution } a =
+    a
+    & assert (Substitution.isNormalized substitution)
+    & assert (Predicate.isFreeOf predicate variables)
+  where
+    variables = Substitution.variables substitution
+
 {-| Marks the condition's predicate as being simplified.
 
 Since the substitution is usually simplified, this usually marks the entire

kore/src/Kore/Internal/MultiAnd.hs

@@ -17,9 +17,13 @@ module Kore.Internal.MultiAnd
     , make
     , toPredicate
     , singleton
+    , toPattern
+    , map
     ) where
 
-import Prelude.Kore
+import Prelude.Kore hiding
+    ( map
+    )
 
 import Control.DeepSeq
     ( NFData
@@ -30,11 +34,18 @@ import qualified GHC.Exts as GHC
 import qualified GHC.Generics as GHC
 
 import Debug
+import Kore.Internal.Pattern
+    ( Pattern
+    )
+import qualified Kore.Internal.Pattern as Pattern
 import Kore.Internal.Predicate
     ( Predicate
     , makeAndPredicate
     , makeTruePredicate_
     )
+import Kore.Internal.TermLike
+    ( mkAnd
+    )
 import Kore.Internal.Variable
 import Kore.TopBottom
     ( TopBottom (..)
@@ -172,3 +183,20 @@ toPredicate (MultiAnd predicates) =
     case predicates of
         [] -> makeTruePredicate_
         _  -> foldr1 makeAndPredicate predicates
+
+toPattern
+    :: InternalVariable variable
+    => MultiAnd (Pattern variable)
+    -> Pattern variable
+toPattern (MultiAnd patterns) =
+    case patterns of
+       [] -> Pattern.top
+       _ -> foldr1 (\pat1 pat2 -> pure mkAnd <*> pat1 <*> pat2) patterns
+
+map
+    :: Ord child2
+    => TopBottom child2
+    => (child1 -> child2)
+    -> MultiAnd child1
+    -> MultiAnd child2
+map f = make . fmap f . extractPatterns

kore/src/Kore/Internal/MultiOr.hs

@@ -26,11 +26,14 @@ module Kore.Internal.MultiOr
     , merge
     , mergeAll
     , singleton
+    , map
     -- * Re-exports
     , Alternative (..)
     ) where
 
-import Prelude.Kore
+import Prelude.Kore hiding
+    ( map
+    )
 
 import Control.DeepSeq
     ( NFData
@@ -355,3 +358,11 @@ gather act = make <$> Logic.gather act
 
 observeAllT :: (Ord a, TopBottom a, Monad m) => LogicT m a -> m (MultiOr a)
 observeAllT act = make <$> Logic.observeAllT act
+
+map
+    :: Ord child2
+    => TopBottom child2
+    => (child1 -> child2)
+    -> MultiOr child1
+    -> MultiOr child2
+map f = make . fmap f . extractPatterns

kore/src/Kore/Internal/OrPattern.hs

@@ -21,11 +21,11 @@ module Kore.Internal.OrPattern
     , toTermLike
     , targetBinder
     , substitute
-    , parseFromTermLike
     , MultiOr.flatten
     , MultiOr.filterOr
     , MultiOr.gather
     , MultiOr.observeAllT
+    , MultiOr.map
     ) where
 
 import Prelude.Kore
@@ -57,7 +57,6 @@ import qualified Kore.Internal.SideCondition.SideCondition as SideCondition
     )
 import Kore.Internal.TermLike
     ( InternalVariable
-    , pattern Or_
     , Sort
     , TermLike
     , mkBottom_
@@ -233,11 +232,3 @@ substitute
     -> OrPattern variable
 substitute subst =
     fromPatterns . fmap (Pattern.substitute subst) . toPatterns
-
-parseFromTermLike
-    :: InternalVariable variable
-    => TermLike variable
-    -> OrPattern variable
-parseFromTermLike (Or_ _ term1 term2) =
-    parseFromTermLike term1 <> parseFromTermLike term2
-parseFromTermLike term = fromTermLike term

kore/src/Kore/Internal/SideCondition.hs

@@ -156,8 +156,8 @@ andCondition
     => SideCondition variable
     -> Condition variable
     -> SideCondition variable
-andCondition SideCondition {assumedTrue} newCondition =
-    assert (isNormalized result) result
+andCondition SideCondition { assumedTrue } newCondition =
+    assertNormalized result result
   where
     result = SideCondition
         { representation = toRepresentationCondition merged
@@ -214,3 +214,11 @@ toRepresentationCondition =
 
 isNormalized :: forall variable. Ord variable => SideCondition variable -> Bool
 isNormalized = Conditional.isNormalized . from @_ @(Condition variable)
+
+assertNormalized
+    :: forall variable a
+    .  HasCallStack
+    => Ord variable
+    => SideCondition variable
+    -> a -> a
+assertNormalized = Conditional.assertNormalized . from @_ @(Condition variable)