Explore the remainder branch when Booster is uncertain about rewrite rule conditions

booster/library/Booster/JsonRpc.hs

@@ -47,7 +47,7 @@ import Booster.Definition.Base qualified as Definition (RewriteRule (..))
 import Booster.LLVM as LLVM (API)
 import Booster.Log
 import Booster.Pattern.ApplyEquations qualified as ApplyEquations
-import Booster.Pattern.Base (Pattern (..), Sort (SortApp), Term, Variable)
+import Booster.Pattern.Base (Pattern (..), Predicate (..), Sort (SortApp), Term, Variable)
 import Booster.Pattern.Base qualified as Pattern
 import Booster.Pattern.Bool (pattern TrueBool)
 import Booster.Pattern.Match (FailReason (..), MatchResult (..), MatchType (..), matchTerms)
@@ -609,11 +609,14 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                     { reason = RpcTypes.Branching
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported Nothing
+                    , state = toExecState p originalSubstitution unsupported Nothing Nothing Nothing
                     , nextStates =
-                        Just $
-                            map (\(_, muid, p') -> toExecState p' originalSubstitution unsupported (Just muid)) $
-                                toList nexts
+                        -- FIXME return _ruleSubst in the response, removing '#'s from the variable names to make pyk happy
+                        Just
+                            $ map
+                                ( \(_, muid, p', mrulePred, _ruleSubst) -> toExecState p' originalSubstitution unsupported (Just muid) mrulePred Nothing
+                                )
+                            $ toList nexts
                     , rule = Nothing
                     , unknownPredicate = Nothing
                     }
@@ -624,7 +627,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                     { reason = RpcTypes.Stuck
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported Nothing
+                    , state = toExecState p originalSubstitution unsupported Nothing Nothing Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -636,7 +639,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                     { reason = RpcTypes.Vacuous
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported Nothing
+                    , state = toExecState p originalSubstitution unsupported Nothing Nothing Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -648,8 +651,8 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                     { reason = RpcTypes.CutPointRule
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported Nothing
-                    , nextStates = Just [toExecState next originalSubstitution unsupported Nothing]
+                    , state = toExecState p originalSubstitution unsupported Nothing Nothing Nothing
+                    , nextStates = Just [toExecState next originalSubstitution unsupported Nothing Nothing Nothing]
                     , rule = Just lbl
                     , unknownPredicate = Nothing
                     }
@@ -660,7 +663,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                     { reason = RpcTypes.TerminalRule
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported Nothing
+                    , state = toExecState p originalSubstitution unsupported Nothing Nothing Nothing
                     , nextStates = Nothing
                     , rule = Just lbl
                     , unknownPredicate = Nothing
@@ -672,7 +675,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                     { reason = RpcTypes.DepthBound
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported Nothing
+                    , state = toExecState p originalSubstitution unsupported Nothing Nothing Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -689,7 +692,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                                     (logSuccessfulRewrites, logFailedRewrites)
                                     (RewriteStepFailed failure)
                          in logs <|> abortRewriteLog
-                    , state = toExecState p originalSubstitution unsupported Nothing
+                    , state = toExecState p originalSubstitution unsupported Nothing Nothing Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -712,19 +715,32 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
                 xs@(_ : _) -> Just xs
 
 toExecState ::
-    Pattern -> Map Variable Term -> [Syntax.KorePattern] -> Maybe UniqueId -> RpcTypes.ExecuteState
-toExecState pat sub unsupported muid =
+    Pattern ->
+    Map Variable Term ->
+    [Syntax.KorePattern] ->
+    Maybe UniqueId ->
+    Maybe Predicate ->
+    Maybe (Map Variable Term) ->
+    RpcTypes.ExecuteState
+toExecState pat sub unsupported muid mrulePredicate mruleSubst =
     RpcTypes.ExecuteState
         { term = addHeader t
         , predicate = addHeader <$> addUnsupported p
         , substitution = addHeader <$> s
-        , ruleSubstitution = Nothing
-        , rulePredicate = Nothing
+        , ruleSubstitution = addHeader <$> mruleSubstExt
+        , rulePredicate = addHeader <$> mrulePredExt
         , ruleId = getUniqueId <$> muid
         }
   where
+    mrulePredExt = externalisePredicate termSort <$> mrulePredicate
+    mruleSubstExt =
+        Syntax.KJAnd predicateSort
+            . map (uncurry $ externaliseSubstitution predicateSort)
+            . Map.toList
+            <$> mruleSubst
     (t, p, s) = externalisePattern pat sub
     termSort = externaliseSort $ sortOfPattern pat
+    predicateSort = externaliseSort Pattern.SortBool
     allUnsupported = Syntax.KJAnd termSort unsupported
     addUnsupported
         | null unsupported = id

booster/library/Booster/JsonRpc/Utils.hs

@@ -70,15 +70,19 @@ diffJson file1 file2 =
     -- \| Branching execution results are considered equivalent if
     -- \* they both have two branches
     -- \* branches are syntactically the same, but may be in different order
+    -- \* the "rule-substitution" field is ignored
     sameModuloBranchOrder :: ExecuteResult -> ExecuteResult -> Bool
     sameModuloBranchOrder res1 res2
         | res1.reason == Branching && res1.reason == res2.reason =
-            case (res1.nextStates, res2.nextStates) of
+            case (map ignoreRuleSubstituiton <$> res1.nextStates, map ignoreRuleSubstituiton <$> res2.nextStates) of
                 (Just xs, Just ys) ->
                     length xs == 2 && length ys == 2 && (xs == ys || xs == reverse ys)
                 _ -> False
         | otherwise = False
 
+    ignoreRuleSubstituiton :: ExecuteState -> ExecuteState
+    ignoreRuleSubstituiton state = state{ruleSubstitution = Nothing}
+
 data DiffResult
     = Identical KoreRpcType
     | DifferentType KoreRpcType KoreRpcType

booster/library/Booster/Pattern/Bool.hs

@@ -7,9 +7,11 @@ License     : BSD-3-Clause
 module Booster.Pattern.Bool (
     foldAndBool,
     isBottom,
+    isFalse,
     negateBool,
     splitBoolPredicates,
     splitAndBools,
+    collapseAndBools,
     -- patterns
     pattern TrueBool,
     pattern FalseBool,
@@ -189,6 +191,11 @@ foldAndBool (x : xs) = AndBool x $ foldAndBool xs
 isBottom :: Pattern -> Bool
 isBottom = (Predicate FalseBool `elem`) . constraints
 
+isFalse :: Predicate -> Bool
+isFalse = \case
+    (Predicate FalseBool) -> True
+    _ -> False
+
 {- | We want to break apart predicates of type `Y1 andBool ... Yn` apart, in case some of the `Y`s are abstract
 which prevents the original expression from being fed to the LLVM simplifyBool function
 -}
@@ -206,3 +213,7 @@ splitAndBools :: Predicate -> [Predicate]
 splitAndBools p@(Predicate t)
     | AndBool l r <- t = concatMap (splitAndBools . Predicate) [l, r]
     | otherwise = [p]
+
+-- | Inverse of splitAndBools
+collapseAndBools :: [Predicate] -> Predicate
+collapseAndBools = Predicate . foldAndBool . map (\(Predicate p) -> p)