Handle input substitution as part of Pattern

booster/library/Booster/JsonRpc.hs

@@ -44,7 +44,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 (..), Sort (SortApp))
 import Booster.Pattern.Base qualified as Pattern
 import Booster.Pattern.Implies (runImplies)
 import Booster.Pattern.Pretty
@@ -166,7 +166,7 @@ respond stateVar request =
                         result <-
                             performRewrite rewriteConfig substPat
                         SMT.finaliseSolver solver
-                        pure $ execResponse req result substitution unsupported
+                        pure $ execResponse req result unsupported
             RpcTypes.AddModule RpcTypes.AddModuleRequest{_module, nameAsId = nameAsId'} -> Booster.Log.withContext CtxAddModule $ runExceptT $ do
                 -- block other request executions while modifying the server state
                 state <- liftIO $ takeMVar stateVar
@@ -244,21 +244,21 @@ respond stateVar request =
                                     RpcError.CouldNotVerifyPattern $
                                         map patternErrorToRpcError patternErrors
                     -- term and predicate (pattern)
-                    Right (TermAndPredicates pat substitution unsupported) -> do
+                    Right (TermAndPredicates pat unsupported) -> do
                         unless (null unsupported) $ do
                             withKorePatternContext (KoreJson.KJAnd (externaliseSort $ sortOfPattern pat) unsupported) $ do
                                 logMessage ("ignoring unsupported predicate parts" :: Text)
                         -- apply the given substitution before doing anything else
                         let substPat =
                                 Pattern
-                                    { term = Substitution.substituteInTerm substitution pat.term
-                                    , constraints = Set.map (Substitution.substituteInPredicate substitution) pat.constraints
+                                    { term = Substitution.substituteInTerm pat.substitution pat.term
+                                    , constraints = Set.map (Substitution.substituteInPredicate pat.substitution) pat.constraints
                                     , ceilConditions = pat.ceilConditions
-                                    , substitution
+                                    , substitution = pat.substitution
                                     }
                         ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPat >>= \case
                             (Right newPattern, _) -> do
-                                let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern substitution
+                                let (term, mbPredicate, mbSubstitution) = externalisePattern newPattern
                                     tSort = externaliseSort (sortOfPattern newPattern)
                                     result = case catMaybes (mbPredicate : mbSubstitution : map Just unsupported) of
                                         [] -> term
@@ -333,7 +333,7 @@ respond stateVar request =
                             -- term and predicates were sent. Only work on predicates
                             (boolPs, suppliedSubst) <-
                                 case things of
-                                    TermAndPredicates pat substitution unsupported -> do
+                                    TermAndPredicates pat unsupported -> do
                                         withContext CtxGetModel $
                                             logMessage' ("ignoring supplied terms and only checking predicates" :: Text)
 
@@ -342,7 +342,7 @@ respond stateVar request =
                                                 logMessage' ("ignoring unsupported predicates" :: Text)
                                                 withContext CtxDetail $
                                                     logMessage (Text.unwords $ map prettyPattern unsupported)
-                                        pure (Set.toList pat.constraints, substitution)
+                                        pure (Set.toList pat.constraints, pat.substitution)
                                     Predicates ps -> do
                                         unless (null ps.ceilPredicates && null ps.unsupported) $ do
                                             withContext CtxGetModel $ do
@@ -473,21 +473,20 @@ execStateToKoreJson RpcTypes.ExecuteState{term = t, substitution, predicate} =
 execResponse ::
     RpcTypes.ExecuteRequest ->
     (Natural, Seq (RewriteTrace ()), RewriteResult Pattern) ->
-    Map Variable Term ->
     [Syntax.KorePattern] ->
     Either ErrorObj (RpcTypes.API 'RpcTypes.Res)
-execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
+execResponse req (d, traces, rr) unsupported = case rr of
     RewriteBranch p nexts ->
         Right $
             RpcTypes.Execute
                 RpcTypes.ExecuteResult
                     { reason = RpcTypes.Branching
                     , depth
                     , logs
-                    , state = toExecState p originalSubstitution unsupported Nothing
+                    , state = toExecState p unsupported Nothing
                     , nextStates =
                         Just $
-                            map (\(_, muid, p') -> toExecState p' originalSubstitution unsupported (Just muid)) $
+                            map (\(_, muid, p') -> toExecState p' unsupported (Just muid)) $
                                 toList nexts
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -499,7 +498,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 unsupported Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -511,7 +510,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 unsupported Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -523,8 +522,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 unsupported Nothing
+                    , nextStates = Just [toExecState next unsupported Nothing]
                     , rule = Just lbl
                     , unknownPredicate = Nothing
                     }
@@ -535,7 +534,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 unsupported Nothing
                     , nextStates = Nothing
                     , rule = Just lbl
                     , unknownPredicate = Nothing
@@ -547,7 +546,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 unsupported Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -564,7 +563,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 unsupported Nothing
                     , nextStates = Nothing
                     , rule = Nothing
                     , unknownPredicate = Nothing
@@ -587,8 +586,8 @@ 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 -> [Syntax.KorePattern] -> Maybe UniqueId -> RpcTypes.ExecuteState
+toExecState pat unsupported muid =
     RpcTypes.ExecuteState
         { term = addHeader t
         , predicate = addHeader <$> addUnsupported p
@@ -598,7 +597,7 @@ toExecState pat sub unsupported muid =
         , ruleId = getUniqueId <$> muid
         }
   where
-    (t, p, s) = externalisePattern pat sub
+    (t, p, s) = externalisePattern pat
     termSort = externaliseSort $ sortOfPattern pat
     allUnsupported = Syntax.KJAnd termSort unsupported
     addUnsupported

booster/library/Booster/JsonRpc/Utils.hs

@@ -279,18 +279,9 @@ diffBy def pat1 pat2 =
             <> if null ps.unsupported
                 then ""
                 else BS.unlines ("Unsupported parts:" : map Json.encode ps.unsupported)
-    renderBS (TermAndPredicates p m u) =
+    renderBS (TermAndPredicates p u) =
         ( BS.pack . renderDefault $
             pretty (PrettyWithModifiers @['Decoded, 'Truncated] p)
-                <+> vsep
-                    ( map
-                        ( \(k, v) ->
-                            pretty (PrettyWithModifiers @['Decoded, 'Truncated] k)
-                                <+> "="
-                                <+> pretty (PrettyWithModifiers @['Decoded, 'Truncated] v)
-                        )
-                        (Map.toList m)
-                    )
         )
             <> if null u then "" else BS.unlines ("Unsupported parts: " : map Json.encode u)
     internalise =

booster/library/Booster/Pattern/Implies.hs

@@ -69,8 +69,10 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
                      in runExcept $
                             internalisePatternOrTopOrBottom DisallowAlias CheckSubsorts Nothing def existentials korePat
 
-                checkImplies patL substitutionL unsupportedL existsL patR substitutionR unsupportedR existsR = do
-                    let freeVarsL =
+                checkImplies patL unsupportedL existsL patR unsupportedR existsR = do
+                    let substitutionL = patL.substitution
+                        substitutionR = patR.substitution
+                        freeVarsL =
                             ( freeVariables patL.term
                                 <> (Set.unions $ Set.map (freeVariables . coerce) patL.constraints)
                                 <> (Set.fromList $ Map.keys substitutionL)
@@ -210,10 +212,10 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
                 (Right IsTop{}, _) ->
                     pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly $
                         "The check implication step expects the antecedent term to be function-like."
-                ( Right (IsPattern (existsL, patL, substitutionL, unsupportedL))
-                    , Right (IsPattern (existsR, patR, substitutionR, unsupportedR))
+                ( Right (IsPattern (existsL, patL, unsupportedL))
+                    , Right (IsPattern (existsR, patR, unsupportedR))
                     ) ->
-                        checkImplies patL substitutionL unsupportedL existsL patR substitutionR unsupportedR existsR
+                        checkImplies patL unsupportedL existsL patR unsupportedR existsR
                 (Right IsPattern{}, Right (IsTop sort)) ->
                     implies' (Kore.Syntax.KJTop sort) sort antecedent.term consequent.term mempty
                 (Right IsPattern{}, Right (IsBottom sort)) ->

booster/library/Booster/Syntax/Json/Externalise.hs

@@ -19,9 +19,7 @@ import Data.Text.Encoding qualified as Text
 import Booster.Pattern.Base (externaliseKmapUnsafe)
 import Booster.Pattern.Base qualified as Internal
 import Booster.Pattern.Bool qualified as Internal
-import Booster.Pattern.Substitution qualified as Substitution
 import Booster.Pattern.Util (sortOfTerm)
-import Data.Map (Map)
 import Data.Map qualified as Map
 import Kore.Syntax.Json.Types qualified as Syntax
 
@@ -31,17 +29,15 @@ import Kore.Syntax.Json.Types qualified as Syntax
 -}
 externalisePattern ::
     Internal.Pattern ->
-    Map Internal.Variable Internal.Term ->
     (Syntax.KorePattern, Maybe Syntax.KorePattern, Maybe Syntax.KorePattern)
-externalisePattern Internal.Pattern{term = term, constraints, ceilConditions, substitution = ensuredSubstitution} inputSubstitution =
+externalisePattern Internal.Pattern{term = term, constraints, ceilConditions, substitution} =
     -- need a sort for the predicates in external format
     let sort = externaliseSort $ sortOfTerm term
         -- inputSubstitution is probably not needed here at all
-        substitutions = ensuredSubstitution `Substitution.compose` inputSubstitution
         externalisedSubstitution =
-            if null substitutions
+            if null substitution
                 then Nothing
-                else Just . multiAnd sort . map (uncurry $ externaliseSubstitution sort) . Map.toList $ substitutions
+                else Just . multiAnd sort . map (uncurry $ externaliseSubstitution sort) . Map.toList $ substitution
         externalisedPredicate =
             if null constraints && null ceilConditions
                 then Nothing

booster/library/Booster/Syntax/Json/Internalise.hs

@@ -133,12 +133,11 @@ data TermOrPredicates -- = Either Predicate Pattern
     = Predicates InternalisedPredicates
     | TermAndPredicates
         Internal.Pattern
-        (Map Internal.Variable Internal.Term)
         [Syntax.KorePattern]
     deriving stock (Eq, Show)
 
 retractPattern :: TermOrPredicates -> Maybe Internal.Pattern
-retractPattern (TermAndPredicates patt _ _) = Just patt
+retractPattern (TermAndPredicates patt _) = Just patt
 retractPattern _ = Nothing
 
 -- main interface functions
@@ -204,7 +203,7 @@ internalisePatternOrTopOrBottom ::
     Except
         PatternError
         ( PatternOrTopOrBottom
-            ([Internal.Variable], Internal.Pattern, Map Internal.Variable Internal.Term, [Syntax.KorePattern])
+            ([Internal.Variable], Internal.Pattern, [Syntax.KorePattern])
         )
 internalisePatternOrTopOrBottom allowAlias checkSubsorts sortVars definition existentials p = do
     let exploded = explodeAnd p
@@ -223,8 +222,7 @@ internalisePatternOrTopOrBottom allowAlias checkSubsorts sortVars definition exi
                 pure $
                     IsPattern
                         ( existentialVars
-                        , Internal.Pattern{term, constraints = Set.fromList preds, ceilConditions, substitution = mempty} -- this is the ensures-substitution, leave empty
-                        , subst
+                        , Internal.Pattern{term, constraints = Set.fromList preds, ceilConditions, substitution = subst}
                         , unknown
                         )
   where
@@ -258,9 +256,8 @@ internaliseTermOrPredicate allowAlias checkSubsorts sortVars definition syntaxPa
                             { term
                             , constraints = Set.fromList constrs
                             , ceilConditions
-                            , substitution = mempty -- this is the ensures-substitution, leave empty
+                            , substitution = substitution
                             }
-                        substitution
                         unsupported
             )
 

booster/tools/booster/Proxy.hs

@@ -524,7 +524,6 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of
                                     Right
                                         ( ( Booster.toExecState
                                                 Pattern{term, ceilConditions, constraints = Set.fromList preds, substitution = sub}
-                                                sub
                                                 unsup
                                                 Nothing
                                           )