Log the combined rewrite rule remainder

Add negative info to DebugAppliedRewriteRules log entry

Debug remainder

Debug remainders more

Make kore-rpc-booster aware of DebugRewriteRulesRemainder

Revert "Debug remainders more"

This reverts commit 0c56365.

Revert "Debug remainder"

This reverts commit cab0016.

Add json log for DebugRewriteRulesRemainder

Add default implementation of oneLineContextJson

Add entry type to json of DebugRewriteRulesRemainder

Ask forDebugEvaluateCondition

Fix typo

Accept rule count in DebugRewriteRulesRemainder

Author: geo2a

booster/tools/booster/Server.hs

@@ -394,6 +394,7 @@ logLevelToKoreLogEntryMap =
             )
         , (LevelOther "SimplifySuccess", ["DebugTerm"])
         , (LevelOther "RewriteSuccess", ["DebugAppliedRewriteRules", "DebugTerm"])
+        , (LevelOther "Unconditional", ["DebugRewriteRulesRemainder", "DebugEvaluateCondition"])
         ]
 
 data CLProxyOptions = CLProxyOptions

kore/kore.cabal

@@ -352,6 +352,7 @@ library
     Kore.Log.DebugRewriteTrace
     Kore.Log.DebugSolver
     Kore.Log.DebugSubstitutionSimplifier
+    Kore.Log.DebugRewriteRulesRemainder
     Kore.Log.DebugTransition
     Kore.Log.DebugUnification
     Kore.Log.DebugUnifyBottom

kore/src/Kore/Log/DebugAppliedRewriteRules.hs

@@ -67,7 +67,8 @@ instance Entry DebugAppliedRewriteRules where
         | null appliedRewriteRules = True
         | otherwise = False
     oneLineDoc DebugAppliedRewriteRules{appliedRewriteRules}
-        | null appliedRewriteRules = mempty
+        | null appliedRewriteRules =
+            "failed to apply " <> pretty (length appliedRewriteRules) <> " rewrite rules"
         | otherwise =
             "applied " <> pretty (length appliedRewriteRules) <> " rewrite rules"
     oneLineJson DebugAppliedRewriteRules{appliedRewriteRules}

kore/src/Kore/Log/DebugRewriteRulesRemainder.hs

@@ -0,0 +1,108 @@
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE NoStrict #-}
+{-# LANGUAGE NoStrictData #-}
+
+{- |
+Copyright   : (c) Runtime Verification, 2020-2021
+License     : BSD-3-Clause
+-}
+module Kore.Log.DebugRewriteRulesRemainder (
+    DebugRewriteRulesRemainder (..),
+    debugRewriteRulesRemainder,
+) where
+
+import Data.Aeson (Value (Array), object, toJSON, (.=))
+import Data.Text qualified as Text
+import Data.Vector (fromList)
+import Kore.Internal.Conditional qualified as Conditional
+import Kore.Internal.Pattern (
+    Pattern,
+ )
+import Kore.Internal.Predicate (
+    Predicate,
+ )
+import Kore.Internal.Predicate qualified as Predicate
+import Kore.Internal.TermLike qualified as TermLike
+import Kore.Internal.Variable (
+    VariableName,
+    toVariableName,
+ )
+import Kore.Rewrite.RewritingVariable
+import Kore.Syntax.Json qualified as PatternJson
+import Kore.Unparser
+import Kore.Util (showHashHex)
+import Log
+import Prelude.Kore
+import Pretty (
+    Pretty (..),
+ )
+import Pretty qualified
+
+data DebugRewriteRulesRemainder = DebugRewriteRulesRemainder
+    { configuration :: !(Pattern VariableName)
+    , rulesCount :: !Int
+    , remainder :: !(Predicate RewritingVariableName)
+    }
+    deriving stock (Show)
+
+instance Pretty DebugRewriteRulesRemainder where
+    pretty DebugRewriteRulesRemainder{..} =
+        Pretty.vsep
+            [ (Pretty.hsep . catMaybes)
+                [ Just "The rules"
+                , Just "produced a remainder"
+                , Just . pretty $ remainder
+                ]
+            , "On configuration:"
+            , Pretty.indent 2 . unparse $ configuration
+            ]
+
+instance Entry DebugRewriteRulesRemainder where
+    entrySeverity _ = Debug
+    helpDoc _ = "log rewrite rules remainder"
+
+    oneLineContextJson
+        entry@DebugRewriteRulesRemainder{configuration, rulesCount} =
+            Array $
+                fromList
+                    [ object ["entry" .= entryTypeText (toEntry entry)]
+                    , object
+                        [ "term" .= showHashHex (hash configuration)
+                        ]
+                    , object
+                        [ "rules-count" .= Text.pack (show rulesCount)
+                        ]
+                    ]
+
+    oneLineDoc entry@(DebugRewriteRulesRemainder{rulesCount, remainder}) =
+        let context = map Pretty.brackets (pretty <$> oneLineContextDoc entry <> ["detail"])
+            logMsg =
+                ( Pretty.hsep . concat $
+                    [ ["After applying ", pretty rulesCount, " rewrite rules"]
+                    , ["there is a remainder condition: ", Pretty.group . pretty $ remainder]
+                    ]
+                )
+         in mconcat context <> logMsg
+
+    oneLineJson DebugRewriteRulesRemainder{remainder} =
+        toJSON
+            . PatternJson.fromPredicate sortBool
+            . Predicate.mapVariables (pure toVariableName)
+            $ remainder
+
+sortBool :: TermLike.Sort
+sortBool =
+    (TermLike.SortActualSort $ TermLike.SortActual (TermLike.Id "SortBool" TermLike.AstLocationNone) [])
+
+debugRewriteRulesRemainder ::
+    MonadLog log =>
+    Pattern RewritingVariableName ->
+    Int ->
+    Predicate RewritingVariableName ->
+    log ()
+debugRewriteRulesRemainder pat rulesCount remainder =
+    logEntry DebugRewriteRulesRemainder{..}
+  where
+    configuration = mapConditionalVariables TermLike.mapVariables pat
+    mapConditionalVariables mapTermVariables =
+        Conditional.mapVariables mapTermVariables (pure toVariableName)

kore/src/Kore/Log/Registry.hs

@@ -63,6 +63,9 @@ import Kore.Log.DebugProven (
 import Kore.Log.DebugRetrySolverQuery (
     DebugRetrySolverQuery,
  )
+import Kore.Log.DebugRewriteRulesRemainder (
+    DebugRewriteRulesRemainder,
+ )
 import Kore.Log.DebugRewriteTrace (
     DebugFinalPatterns,
     DebugInitialClaim,
@@ -229,6 +232,7 @@ entryHelpDocsErr, entryHelpDocsNoErr :: [Pretty.Doc ()]
             , mk $ Proxy @DebugTransition
             , mk $ Proxy @DebugAppliedRewriteRules
             , mk $ Proxy @DebugAppliedLabeledRewriteRule
+            , mk $ Proxy @DebugRewriteRulesRemainder
             , mk $ Proxy @DebugAttemptedRewriteRules
             , mk $ Proxy @DebugSubstitutionSimplifier
             , mk $ Proxy @WarnFunctionWithoutEvaluators

kore/src/Kore/Rewrite/RewriteStep.hs

@@ -43,6 +43,7 @@ import Kore.Log.DebugAppliedRewriteRules (
     debugAppliedRewriteRules,
  )
 import Kore.Log.DebugCreatedSubstitution (debugCreatedSubstitution)
+import Kore.Log.DebugRewriteRulesRemainder (debugRewriteRulesRemainder)
 import Kore.Log.DebugRewriteTrace (
     debugRewriteTrace,
  )
@@ -305,6 +306,7 @@ finalizeRulesParallel
                     & fmap fold
             let unifications = MultiOr.make (Conditional.withoutTerm <$> unifiedRules)
                 remainderPredicate = Remainder.remainder' unifications
+            debugRewriteRulesRemainder initial (length unifiedRules) remainderPredicate
             -- evaluate the remainder predicate to make sure it is actually satisfiable
             SMT.evalPredicate
                 (ErrorDecidePredicateUnknown $srcLoc Nothing)

kore/src/Log/Entry.hs

@@ -66,7 +66,7 @@ class (Show entry, Typeable entry) => Entry entry where
 
     oneLineContextJson :: entry -> JSON.Value
     default oneLineContextJson :: entry -> JSON.Value
-    oneLineContextJson _ = JSON.Array mempty
+    oneLineContextJson entry = JSON.object ["entry" JSON..= entryTypeText (toEntry entry)]
 
     oneLineContextDoc :: entry -> [Text]
     default oneLineContextDoc :: entry -> [Text]