3956 branching on complete conditions in Booster

booster/library/Booster/JsonRpc.hs

@@ -22,7 +22,7 @@ import Control.Monad
 import Control.Monad.IO.Class
 import Control.Monad.Trans.Except (catchE, except, runExcept, runExceptT, throwE, withExceptT)
 import Crypto.Hash (SHA256 (..), hashWith)
-import Data.Bifunctor (second)
+import Data.Bifunctor (first, second)
 import Data.Foldable
 import Data.List (singleton)
 import Data.Map.Strict (Map)
@@ -44,11 +44,12 @@ 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))
+import Booster.Pattern.Base (Pattern (..), Predicate, Sort (SortApp), Term, Variable)
 import Booster.Pattern.Base qualified as Pattern
 import Booster.Pattern.Implies (runImplies)
 import Booster.Pattern.Pretty
 import Booster.Pattern.Rewrite (
+    RewriteBranchNextState (..),
     RewriteConfig (..),
     RewriteFailed (..),
     RewriteResult (..),
@@ -57,7 +58,9 @@ import Booster.Pattern.Rewrite (
  )
 import Booster.Pattern.Substitution qualified as Substitution
 import Booster.Pattern.Util (
+    externaliseRuleMarker,
     freeVariables,
+    modifyVarName,
     sortOfPattern,
     sortOfTerm,
  )
@@ -479,11 +482,13 @@ execResponse req (d, traces, rr) unsupported = case rr of
                     { reason = RpcTypes.Branching
                     , depth
                     , logs
-                    , state = toExecState p unsupported Nothing
+                    , state = toExecState p unsupported Nothing Nothing Nothing
                     , nextStates =
-                        Just $
-                            map (\(_, muid, p') -> toExecState p' unsupported (Just muid)) $
-                                toList nexts
+                        Just
+                            $ map
+                                ( \(RewriteBranchNextState{ruleUniqueId, rewrittenPat, mRulePredicate, ruleSubstitution}) -> toExecState rewrittenPat unsupported (Just ruleUniqueId) mRulePredicate (Just ruleSubstitution)
+                                )
+                            $ toList nexts
                     , rule = Nothing
                     , unknownPredicate = Nothing
                     }
@@ -494,7 +499,7 @@ execResponse req (d, traces, rr) unsupported = case rr of
                     { reason = RpcTypes.Stuck
                     , depth
                     , logs
-                    , state = toExecState p unsupported Nothing
+                    , state = toExecState p unsupported Nothing Nothing Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -506,7 +511,7 @@ execResponse req (d, traces, rr) unsupported = case rr of
                     { reason = RpcTypes.Vacuous
                     , depth
                     , logs
-                    , state = toExecState p unsupported Nothing
+                    , state = toExecState p unsupported Nothing Nothing Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -518,8 +523,8 @@ execResponse req (d, traces, rr) unsupported = case rr of
                     { reason = RpcTypes.CutPointRule
                     , depth
                     , logs
-                    , state = toExecState p unsupported Nothing
-                    , nextStates = Just [toExecState next unsupported Nothing]
+                    , state = toExecState p unsupported Nothing Nothing Nothing
+                    , nextStates = Just [toExecState next unsupported Nothing Nothing Nothing]
                     , rule = Just lbl
                     , unknownPredicate = Nothing
                     }
@@ -530,7 +535,7 @@ execResponse req (d, traces, rr) unsupported = case rr of
                     { reason = RpcTypes.TerminalRule
                     , depth
                     , logs
-                    , state = toExecState p unsupported Nothing
+                    , state = toExecState p unsupported Nothing Nothing Nothing
                     , nextStates = Nothing
                     , rule = Just lbl
                     , unknownPredicate = Nothing
@@ -542,7 +547,7 @@ execResponse req (d, traces, rr) unsupported = case rr of
                     { reason = RpcTypes.DepthBound
                     , depth
                     , logs
-                    , state = toExecState p unsupported Nothing
+                    , state = toExecState p unsupported Nothing Nothing Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -559,7 +564,7 @@ execResponse req (d, traces, rr) unsupported = case rr of
                                     (logSuccessfulRewrites, logFailedRewrites)
                                     (RewriteStepFailed failure)
                          in logs <|> abortRewriteLog
-                    , state = toExecState p unsupported Nothing
+                    , state = toExecState p unsupported Nothing Nothing Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -582,19 +587,31 @@ execResponse req (d, traces, rr) unsupported = case rr of
                 xs@(_ : _) -> Just xs
 
 toExecState ::
-    Pattern -> [Syntax.KorePattern] -> Maybe UniqueId -> RpcTypes.ExecuteState
-toExecState pat unsupported muid =
+    Pattern ->
+    [Syntax.KorePattern] ->
+    Maybe UniqueId ->
+    Maybe Predicate ->
+    Maybe (Map Variable Term) ->
+    RpcTypes.ExecuteState
+toExecState pat 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) . first (modifyVarName externaliseRuleMarker))
+            . Map.toList
+            <$> mruleSubst
     (t, p, s) = externalisePattern pat
     termSort = externaliseSort $ sortOfPattern pat
+    predicateSort = externaliseSort Pattern.SortBool
     allUnsupported = Syntax.KJAnd termSort unsupported
     addUnsupported
         | null unsupported = id
@@ -639,6 +656,11 @@ mkLogRewriteTrace
                                             { reason = "Uncertain about a condition in rule"
                                             , _ruleId = Just $ getUniqueId (uniqueId $ Definition.attributes r)
                                             }
+                                    RewriteRemainderPredicate rs _ _ ->
+                                        Failure
+                                            { reason = "Uncertain about a condition in rule"
+                                            , _ruleId = Just $ getUniqueId (uniqueId $ Definition.attributes (head rs))
+                                            }
                                     DefinednessUnclear r _ undefReasons ->
                                         Failure
                                             { reason = "Uncertain about definedness of rule because of: " <> pack (show undefReasons)

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,
@@ -188,6 +190,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
 -}
@@ -205,3 +212,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)