Merge remote-tracking branch 'origin/master' into _update-deps/runtim…

…everification/k

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
@@ -55,12 +55,11 @@ import Booster.Pattern.Rewrite (
     RewriteTrace (..),
     performRewrite,
  )
+import Booster.Pattern.Substitution qualified as Substitution
 import Booster.Pattern.Util (
     freeVariables,
     sortOfPattern,
     sortOfTerm,
-    substituteInPredicate,
-    substituteInTerm,
  )
 import Booster.Prettyprinter (renderText)
 import Booster.SMT.Interface qualified as SMT
@@ -69,6 +68,7 @@ import Booster.Syntax.Json.Externalise
 import Booster.Syntax.Json.Internalise (
     InternalisedPredicates (..),
     TermOrPredicates (..),
+    extractSubstitution,
     internalisePattern,
     internaliseTermOrPredicate,
     logPatternError,
@@ -131,12 +131,14 @@ respond stateVar request =
                                         [ req.logSuccessfulRewrites
                                         , req.logFailedRewrites
                                         ]
-                        -- apply the given substitution before doing anything else
+                        -- apply the given substitution before doing anything else,
+                        -- as internalisePattern does not substitute
                         let substPat =
                                 Pattern
-                                    { term = substituteInTerm substitution term
-                                    , constraints = Set.fromList $ map (substituteInPredicate substitution) preds
+                                    { term = Substitution.substituteInTerm substitution term
+                                    , constraints = Set.fromList $ map (Substitution.substituteInPredicate substitution) preds
                                     , ceilConditions = ceils
+                                    , substitution
                                     }
                             -- remember all variables used in the substitutions
                             substVars =
@@ -166,7 +168,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,20 +246,14 @@ respond stateVar request =
                                     RpcError.CouldNotVerifyPattern $
                                         map patternErrorToRpcError patternErrors
                     -- term and predicate (pattern)
-                    Right (TermAndPredicates pat substitution unsupported) -> do
+                    -- NOTE: the input substitution will have already been applied by internaliseTermOrPredicate
+                    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 = substituteInTerm substitution pat.term
-                                    , constraints = Set.map (substituteInPredicate substitution) pat.constraints
-                                    , ceilConditions = pat.ceilConditions
-                                    }
-                        ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPat >>= \case
+                        ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty pat >>= \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
@@ -281,23 +277,24 @@ respond stateVar request =
                                 withKorePatternContext (KoreJson.KJAnd (externaliseSort $ SortApp "SortBool" []) ps.unsupported) $ do
                                     logMessage ("ignoring unsupported predicate parts" :: Text)
                             -- apply the given substitution before doing anything else
-                            let predicates = map (substituteInPredicate ps.substitution) ps.boolPredicates
+                            let predicates = map (Substitution.substituteInPredicate ps.substitution) ps.boolPredicates
                             withContext CtxConstraint $
                                 ApplyEquations.simplifyConstraints
                                     def
                                     mLlvmLibrary
                                     solver
                                     mempty
-                                    predicates
+                                    (predicates <> Substitution.asEquations ps.substitution)
                                     >>= \case
-                                        (Right newPreds, _) -> do
+                                        (Right simplified, _) -> do
                                             let predicateSort =
                                                     fromMaybe (error "not a predicate") $
                                                         sortOfJson req.state.term
+                                                (simplifiedSubstitution, simplifiedPredicates) = extractSubstitution simplified
                                                 result =
-                                                    map (externalisePredicate predicateSort) newPreds
+                                                    map (externalisePredicate predicateSort) (Set.toList simplifiedPredicates)
                                                         <> map (externaliseCeil predicateSort) ps.ceilPredicates
-                                                        <> map (uncurry $ externaliseSubstitution predicateSort) (Map.toList ps.substitution)
+                                                        <> map (uncurry $ externaliseSubstitution predicateSort) (Map.assocs simplifiedSubstitution)
                                                         <> ps.unsupported
 
                                             pure $ Right (addHeader $ Syntax.KJAnd predicateSort result)
@@ -332,7 +329,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)
 
@@ -341,7 +338,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
@@ -472,21 +469,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
@@ -498,7 +494,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
@@ -510,7 +506,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
@@ -522,8 +518,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
                     }
@@ -534,7 +530,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
@@ -546,7 +542,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
@@ -563,7 +559,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
@@ -586,8 +582,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
@@ -597,7 +593,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/Log.hs

@@ -69,6 +69,7 @@ import Booster.Pattern.Base (
     pattern AndTerm,
  )
 import Booster.Pattern.Pretty
+import Booster.Pattern.Substitution (asEquations)
 import Booster.Prettyprinter (renderOneLineText)
 import Booster.Syntax.Json (KorePattern, addHeader, prettyPattern)
 import Booster.Syntax.Json.Externalise (externaliseTerm)
@@ -185,8 +186,8 @@ withTermContext t@(Term attrs _) m =
         m
 
 withPatternContext :: LoggerMIO m => Pattern -> m a -> m a
-withPatternContext Pattern{term, constraints} m =
-    let t' = foldl' AndTerm term $ Set.toList $ Set.map coerce constraints -- FIXME
+withPatternContext Pattern{term, constraints, substitution} m =
+    let t' = foldl' AndTerm term . map coerce $ Set.toList constraints <> asEquations substitution
      in withTermContext t' m
 
 instance ToLogFormat KorePattern where

booster/library/Booster/Pattern/ApplyEquations.hs

@@ -66,10 +66,12 @@ import Booster.Pattern.Bool
 import Booster.Pattern.Index qualified as Idx
 import Booster.Pattern.Match
 import Booster.Pattern.Pretty
+import Booster.Pattern.Substitution
 import Booster.Pattern.Util
 import Booster.Prettyprinter (renderOneLineText)
 import Booster.SMT.Interface qualified as SMT
 import Booster.Syntax.Json.Externalise (externaliseTerm)
+import Booster.Syntax.Json.Internalise (extractSubstitution)
 import Booster.Util (Bound (..))
 import Kore.JsonRpc.Types.ContextLog (CLContext (CLWithId), IdContext (CtxCached))
 import Kore.Util (showHashHex)
@@ -455,7 +457,15 @@ evaluatePattern ::
     Pattern ->
     io (Either EquationFailure Pattern, SimplifierCache)
 evaluatePattern def mLlvmLibrary smtSolver cache pat =
-    runEquationT def mLlvmLibrary smtSolver cache pat.constraints . evaluatePattern' $ pat
+    runEquationT
+        def
+        mLlvmLibrary
+        smtSolver
+        cache
+        -- interpret substitution as additional known constraints
+        (pat.constraints <> (Set.fromList . asEquations $ pat.substitution))
+        . evaluatePattern'
+        $ pat
 
 -- version for internal nested evaluation
 evaluatePattern' ::
@@ -469,7 +479,20 @@ evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do
     traverse_ simplifyAssumedPredicate . predicates =<< getState
     -- this may yield additional new constraints, left unevaluated
     evaluatedConstraints <- predicates <$> getState
-    pure Pattern{constraints = evaluatedConstraints, term = newTerm, ceilConditions}
+    -- The interface-level evaluatePattern puts pat.substitution together with pat.constraints
+    -- into the simplifier state as known truth. Here the substitution will bubble-up as part of
+    -- evaluatedConstraints. To avoid duplicating constraints (i.e. having equivalent entities
+    -- in pat.predicate and pat.substitution), we discard the old substitution here
+    -- and extract a possible simplified one from evaluatedConstraints.
+    let (simplifiedSubsitution, simplifiedConstraints) = extractSubstitution (Set.toList evaluatedConstraints)
+
+    pure
+        Pattern
+            { constraints = simplifiedConstraints
+            , term = newTerm
+            , ceilConditions
+            , substitution = simplifiedSubsitution
+            }
   where
     -- when TooManyIterations exception occurred while evaluating the top-level term,
     -- i.e. not in a recursive evaluation of a side-condition,

booster/library/Booster/Pattern/Base.hs

@@ -36,6 +36,7 @@ import Data.Functor.Foldable
 import Data.Hashable (Hashable)
 import Data.Hashable qualified as Hashable
 import Data.List as List (foldl', foldl1', sort)
+import Data.Map.Strict (Map)
 import Data.Set (Set)
 import Data.Set qualified as Set
 import GHC.Generics (Generic)
@@ -761,19 +762,22 @@ pattern KSeq sort a =
 
 --------------------
 
+type Substitution = Map Variable Term
+
 -- | A term (configuration) constrained by a number of predicates.
 data Pattern = Pattern
     { term :: Term
     , constraints :: !(Set Predicate)
+    , substitution :: Substitution
     , ceilConditions :: ![Ceil]
     }
     deriving stock (Eq, Ord, Show, Generic, Data)
     deriving anyclass (NFData)
 
 pattern Pattern_ :: Term -> Pattern
-pattern Pattern_ t <- Pattern t _ _
+pattern Pattern_ t <- Pattern t _ _ _
     where
-        Pattern_ t = Pattern t mempty mempty
+        Pattern_ t = Pattern t mempty mempty mempty
 
 pattern ConsApplication :: Symbol -> [Sort] -> [Term] -> Term
 pattern ConsApplication sym sorts args <-

booster/library/Booster/Pattern/Binary.hs

@@ -564,7 +564,7 @@ decodePattern mDef = do
                 preds <- forM preds' $ \case
                     BPredicate pIdx -> Predicate <$> getTerm pIdx
                     _ -> fail "Expecting a predicate"
-                pure $ Pattern trm (Set.fromList preds) mempty
+                pure $ Pattern trm (Set.fromList preds) mempty mempty
             _ -> fail "Expecting a term on the top of the stack"
 
 encodeMagicHeaderAndVersion :: Version -> Put

booster/library/Booster/Pattern/Bool.hs

@@ -36,11 +36,10 @@ import Booster.Definition.Attributes.Base (
     pattern IsNotMacroOrAlias,
  )
 import Booster.Pattern.Base (
-    Pattern,
+    Pattern (..),
     Predicate (..),
     Symbol (Symbol),
     Term,
-    constraints,
     pattern DomainValue,
     pattern SortBool,
     pattern SortInt,