diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs index 979da2e731..48dafb6cf2 100644 --- a/booster/library/Booster/JsonRpc.hs +++ b/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,10 +469,9 @@ 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 @@ -483,10 +479,10 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of { 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 diff --git a/booster/library/Booster/JsonRpc/Utils.hs b/booster/library/Booster/JsonRpc/Utils.hs index f27e3e7909..1a319cfd47 100644 --- a/booster/library/Booster/JsonRpc/Utils.hs +++ b/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 = diff --git a/booster/library/Booster/Log.hs b/booster/library/Booster/Log.hs index 5e862f8345..8cf4e9b36d 100644 --- a/booster/library/Booster/Log.hs +++ b/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 diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs index a410afebe0..53b801fcc2 100644 --- a/booster/library/Booster/Pattern/ApplyEquations.hs +++ b/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, diff --git a/booster/library/Booster/Pattern/Base.hs b/booster/library/Booster/Pattern/Base.hs index a2b4661614..f8991bc259 100644 --- a/booster/library/Booster/Pattern/Base.hs +++ b/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 <- diff --git a/booster/library/Booster/Pattern/Binary.hs b/booster/library/Booster/Pattern/Binary.hs index c398e33878..9f8f9d2ac7 100644 --- a/booster/library/Booster/Pattern/Binary.hs +++ b/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 diff --git a/booster/library/Booster/Pattern/Bool.hs b/booster/library/Booster/Pattern/Bool.hs index 39dd2cacc3..a232a86239 100644 --- a/booster/library/Booster/Pattern/Bool.hs +++ b/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, diff --git a/booster/library/Booster/Pattern/Implies.hs b/booster/library/Booster/Pattern/Implies.hs index 0dd5a33f0e..92ec8d9cfb 100644 --- a/booster/library/Booster/Pattern/Implies.hs +++ b/booster/library/Booster/Pattern/Implies.hs @@ -26,7 +26,8 @@ import Booster.Pattern.Base (Pattern (..), Predicate (..)) import Booster.Pattern.Bool (pattern TrueBool) import Booster.Pattern.Match (FailReason (..), MatchResult (..), MatchType (Implies), matchTerms) import Booster.Pattern.Pretty (FromModifiersT, ModifiersRep (..), pretty') -import Booster.Pattern.Util (freeVariables, sortOfPattern, substituteInPredicate, substituteInTerm) +import Booster.Pattern.Substitution (asEquations) +import Booster.Pattern.Util (freeVariables, sortOfPattern) import Booster.Prettyprinter (renderDefault) import Booster.SMT.Interface qualified as SMT import Booster.Syntax.Json (addHeader, prettyPattern) @@ -68,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) @@ -104,41 +107,26 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = map (pack . show) $ unsupportedL <> unsupportedR | otherwise -> do - let - -- apply the given substitution before doing anything else - substPatL = - Pattern - { term = substituteInTerm substitutionL patL.term - , constraints = Set.map (substituteInPredicate substitutionL) patL.constraints - , ceilConditions = patL.ceilConditions - } - substPatR = - Pattern - { term = substituteInTerm substitutionR patR.term - , constraints = Set.map (substituteInPredicate substitutionR) patR.constraints - , ceilConditions = patR.ceilConditions - } - - SMT.isSat solver (Set.toList substPatL.constraints) >>= \case + SMT.isSat solver (Set.toList patL.constraints) patL.substitution >>= \case SMT.IsUnsat -> - let sort = externaliseSort $ sortOfPattern substPatL + let sort = externaliseSort $ sortOfPattern patL in implies' (Kore.Syntax.KJBottom sort) sort antecedent.term consequent.term mempty - _ -> checkImpliesMatchTerms existsL substPatL existsR substPatR + _ -> checkImpliesMatchTerms existsL patL existsR patR - checkImpliesMatchTerms existsL substPatL existsR substPatR = - case matchTerms Booster.Pattern.Match.Implies def substPatR.term substPatL.term of + checkImpliesMatchTerms existsL patL existsR patR = + case matchTerms Booster.Pattern.Match.Implies def patR.term patL.term of MatchFailed (SubsortingError sortError) -> pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $ show sortError MatchFailed{} -> doesNotImply - (sortOfPattern substPatL) - (externaliseExistTerm existsL substPatL.term) - (externaliseExistTerm existsR substPatR.term) + (sortOfPattern patL) + (externaliseExistTerm existsL patL.term) + (externaliseExistTerm existsR patR.term) MatchIndeterminate remainder -> - ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPatL >>= \case + ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty patL >>= \case (Right simplifedSubstPatL, _) -> - if substPatL == simplifedSubstPatL + if patL == simplifedSubstPatL then -- we are being conservative here for now and returning an error. -- since we have already simplified the LHS, we may want to eventually return implise, but the condition -- will contain the remainder as an equality contraint, predicating the implication on that equality being true. @@ -151,19 +139,20 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $ NonEmpty.toList remainder ) - else checkImpliesMatchTerms existsL simplifedSubstPatL existsR substPatR + else checkImpliesMatchTerms existsL simplifedSubstPatL existsR patR (Left err, _) -> pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ err) MatchSuccess subst -> do let filteredConsequentPreds = - Set.map (substituteInPredicate subst) substPatR.constraints `Set.difference` substPatL.constraints + (patR.constraints <> (Set.fromList $ asEquations patR.substitution)) + `Set.difference` (patL.constraints <> (Set.fromList $ asEquations patL.substitution)) if null filteredConsequentPreds then implies - (sortOfPattern substPatL) - (externaliseExistTerm existsL substPatL.term) - (externaliseExistTerm existsR substPatR.term) + (sortOfPattern patL) + (externaliseExistTerm existsL patL.term) + (externaliseExistTerm existsR patR.term) subst else ApplyEquations.evaluateConstraints def mLlvmLibrary solver mempty filteredConsequentPreds >>= \case @@ -171,9 +160,9 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent = if all (== Predicate TrueBool) newPreds then implies - (sortOfPattern substPatL) - (externaliseExistTerm existsL substPatL.term) - (externaliseExistTerm existsR substPatR.term) + (sortOfPattern patL) + (externaliseExistTerm existsL patL.term) + (externaliseExistTerm existsR patR.term) subst else -- here we conservatively abort -- an anlternative would be to return valid, putting the unknown constraints into the @@ -204,10 +193,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)) -> diff --git a/booster/library/Booster/Pattern/Match.hs b/booster/library/Booster/Pattern/Match.hs index dd8d82caa0..b85985f7eb 100644 --- a/booster/library/Booster/Pattern/Match.hs +++ b/booster/library/Booster/Pattern/Match.hs @@ -8,7 +8,6 @@ module Booster.Pattern.Match ( MatchResult (..), MatchType (..), FailReason (..), - Substitution, matchTerms, checkSubsort, SortError (..), @@ -37,12 +36,12 @@ import Booster.Definition.Attributes.Base (KListDefinition, KMapDefinition, KSet import Booster.Definition.Base import Booster.Pattern.Base import Booster.Pattern.Pretty +import Booster.Pattern.Substitution qualified as Substitution import Booster.Pattern.Util ( checkSymbolIsAc, freeVariables, isConstructorSymbol, sortOfTerm, - substituteInTerm, ) -- | Result of matching a pattern to a subject (a substitution or an indication of what went wrong) @@ -119,8 +118,6 @@ instance FromModifiersT mods => Pretty (PrettyWithModifiers mods FailReason) whe SubjectVariableMatch t v -> hsep ["Cannot match variable in subject:", pretty' @mods v, pretty' @mods t] -type Substitution = Map Variable Term - {- | Attempts to find a simple unifying substitution for the given terms. @@ -668,7 +665,7 @@ matchMaps -- before matching map keys. enqueueMapProblem (KMap def patKeyVals patRest) (KMap def subjKeyVals subjRest) else do - let patternKeyVals = map (first (substituteInTerm st.mSubstitution)) patKeyVals + let patternKeyVals = map (first (Substitution.substituteInTerm st.mSubstitution)) patKeyVals -- check for duplicate keys checkDuplicateKeys patternKeyVals patRest checkDuplicateKeys subjKeyVals subjRest @@ -785,13 +782,13 @@ bindVariable matchType var term@(Term termAttrs _) = do Nothing -> do let -- apply existing substitutions to term - term' = substituteInTerm currentSubst term + term' = Substitution.substituteInTerm currentSubst term when (var `Set.member` freeVariables term') $ failWith (VariableRecursion var term) let -- substitute in existing substitution terms currentSubst' = - Map.map (substituteInTerm $ Map.singleton var term') currentSubst + Map.map (Substitution.substituteInTerm $ Map.singleton var term') currentSubst newSubst = Map.insert var term' currentSubst' modify $ \s -> s{mSubstitution = newSubst} diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs index 39d6f71c2f..47c16b6321 100644 --- a/booster/library/Booster/Pattern/Rewrite.hs +++ b/booster/library/Booster/Pattern/Rewrite.hs @@ -63,14 +63,15 @@ import Booster.Pattern.Match ( MatchResult (MatchFailed, MatchIndeterminate, MatchSuccess), MatchType (Rewrite), SortError, - Substitution, matchTerms, ) import Booster.Pattern.Pretty +import Booster.Pattern.Substitution import Booster.Pattern.Util import Booster.Prettyprinter import Booster.SMT.Interface qualified as SMT import Booster.Syntax.Json.Externalise (externaliseTerm) +import Booster.Syntax.Json.Internalise (extractSubstitution) import Booster.Util (Flag (..)) newtype RewriteT io a = RewriteT @@ -279,8 +280,8 @@ applyRule pat@Pattern{ceilConditions} rule = getPrettyModifiers >>= \case ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> do def <- lift getDefinition - -- unify terms - subst <- withContext CtxMatch $ case matchTerms Rewrite def rule.lhs pat.term of + -- match term with rule's left-hand side + ruleSubstitution <- withContext CtxMatch $ case matchTerms Rewrite def rule.lhs pat.term of MatchFailed (SubsortingError sortError) -> do withContext CtxError $ logPretty' @mods sortError failRewrite $ RewriteSortError rule pat.term sortError @@ -303,23 +304,38 @@ applyRule pat@Pattern{ceilConditions} rule = NE.toList remainder ) failRewrite $ RuleApplicationUnclear rule pat.term remainder - MatchSuccess substitution -> do + MatchSuccess matchingSubstitution -> do + -- existential variables may be present in rule.rhs and rule.ensures, + -- need to strip prefixes and freshen their names with respect to variables already + -- present in the input pattern and in the matching substitution + varsFromInput <- lift . RewriteT $ asks (.varsToAvoid) + let varsFromPattern = freeVariables pat.term <> (Set.unions $ Set.map (freeVariables . coerce) pat.constraints) + varsFromSubst = Set.unions . map freeVariables . Map.elems $ matchingSubstitution + forbiddenVars = varsFromInput <> varsFromPattern <> varsFromSubst + existentialSubst = + Map.fromSet + (\v -> Var $ freshenVar v{variableName = stripMarker v.variableName} forbiddenVars) + rule.existentials + ruleSubstitution = matchingSubstitution <> existentialSubst + withContext CtxSuccess $ do logMessage rule withContext CtxSubstitution $ logMessage $ WithJsonMessage ( object - ["substitution" .= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList substitution)] + [ "substitution" + .= (bimap (externaliseTerm . Var) externaliseTerm <$> Map.toList ruleSubstitution) + ] ) $ renderOneLineText $ "Substitution:" <+> ( hsep $ intersperse "," $ map (\(k, v) -> pretty' @mods k <+> "->" <+> pretty' @mods v) $ - Map.toList substitution + Map.toList ruleSubstitution ) - pure substitution + pure ruleSubstitution -- Also fail the whole rewrite if a rule applies but may introduce -- an undefined term. @@ -336,40 +352,35 @@ applyRule pat@Pattern{ceilConditions} rule = rule.computedAttributes.notPreservesDefinednessReasons -- check required constraints from lhs: Stop if any is false, abort rewrite if indeterminate. - checkRequires subst + checkRequires ruleSubstitution -- check ensures constraints (new) from rhs: stop and return `Trivial` if -- any are false, remove all that are trivially true, return the rest - newConstraints <- checkEnsures subst + ensuredConditions <- checkEnsures ruleSubstitution -- if a new constraint is going to be added, the equation cache is invalid - unless (null newConstraints) $ do + unless (null ensuredConditions) $ do withContextFor Equations . logMessage $ ("New path condition ensured, invalidating cache" :: Text) lift . RewriteT . lift . modify $ \s -> s{equations = mempty} - -- existential variables may be present in rule.rhs and rule.ensures, - -- need to strip prefixes and freshen their names with respect to variables already - -- present in the input pattern and in the unification substitution - varsFromInput <- lift . RewriteT $ asks (.varsToAvoid) - let varsFromPattern = freeVariables pat.term <> (Set.unions $ Set.map (freeVariables . coerce) pat.constraints) - varsFromSubst = Set.unions . map freeVariables . Map.elems $ subst - forbiddenVars = varsFromInput <> varsFromPattern <> varsFromSubst - existentialSubst = - Map.fromSet - (\v -> Var $ freshenVar v{variableName = stripMarker v.variableName} forbiddenVars) - rule.existentials - - -- modify the substitution to include the existentials - let substWithExistentials = subst `Map.union` existentialSubst + -- partition ensured constrains into substitution and predicates + let (newSubsitution, newConstraints) = extractSubstitution ensuredConditions + + -- compose the existing substitution pattern and the newly acquired one + let (modifiedPatternSubst, leftoverConstraints) = extractSubstitution . asEquations $ newSubsitution `compose` pat.substitution + let rewrittenTerm = substituteInTerm (modifiedPatternSubst `compose` ruleSubstitution) rule.rhs + substitutedNewConstraints = + Set.map + (coerce . substituteInTerm (modifiedPatternSubst `compose` ruleSubstitution) . coerce) + newConstraints let rewritten = Pattern - (substituteInTerm substWithExistentials rule.rhs) + rewrittenTerm -- adding new constraints that have not been trivially `Top`, substituting the Ex# variables - ( pat.constraints - <> (Set.fromList $ map (coerce . substituteInTerm existentialSubst . coerce) newConstraints) - ) + (pat.constraints <> substitutedNewConstraints <> leftoverConstraints) + modifiedPatternSubst -- ruleSubstitution is not needed, do not attach it to the result ceilConditions withContext CtxSuccess $ withPatternContext rewritten $ @@ -424,21 +435,37 @@ applyRule pat@Pattern{ceilConditions} rule = -- apply substitution to rule requires let ruleRequires = concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) rule.requires + knownConstraints = pat.constraints <> (Set.fromList . asEquations $ pat.substitution) -- filter out any predicates known to be _syntactically_ present in the known prior - toCheck <- lift $ filterOutKnownConstraints pat.constraints ruleRequires + toCheck <- + lift $ + filterOutKnownConstraints + knownConstraints + ruleRequires -- simplify the constraints (one by one in isolation). Stop if false, abort rewrite if indeterminate. unclearRequires <- - catMaybes <$> mapM (checkConstraint id notAppliedIfBottom pat.constraints) toCheck + catMaybes + <$> mapM + ( checkConstraint + id + notAppliedIfBottom + knownConstraints + ) + toCheck -- unclear conditions may have been simplified and -- could now be syntactically present in the path constraints, filter again - stillUnclear <- lift $ filterOutKnownConstraints pat.constraints unclearRequires + stillUnclear <- + lift $ + filterOutKnownConstraints + knownConstraints + unclearRequires -- check unclear requires-clauses in the context of known constraints (priorKnowledge) solver <- lift $ RewriteT $ (.smtSolver) <$> ask - SMT.checkPredicates solver pat.constraints mempty (Set.fromList stillUnclear) >>= \case + SMT.checkPredicates solver pat.constraints pat.substitution (Set.fromList stillUnclear) >>= \case SMT.IsUnknown reason -> do -- abort rewrite if a solver result was Unknown withContext CtxAbort $ logMessage reason @@ -452,17 +479,25 @@ applyRule pat@Pattern{ceilConditions} rule = checkEnsures :: Substitution -> RewriteRuleAppT (RewriteT io) [Predicate] checkEnsures matchingSubst = do - -- apply substitution to rule requires + -- apply substitution to rule ensures let ruleEnsures = concatMap (splitBoolPredicates . coerce . substituteInTerm matchingSubst . coerce) rule.ensures + knownConstraints = pat.constraints <> (Set.fromList . asEquations $ pat.substitution) newConstraints <- - catMaybes <$> mapM (checkConstraint id trivialIfBottom pat.constraints) ruleEnsures + catMaybes + <$> mapM + ( checkConstraint + id + trivialIfBottom + knownConstraints + ) + ruleEnsures -- check all new constraints together with the known side constraints solver <- lift $ RewriteT $ (.smtSolver) <$> ask -- TODO it is probably enough to establish satisfiablity (rather than validity) of the ensured conditions. -- For now, we check validity to be safe and admit indeterminate result (i.e. (P, not P) is (Sat, Sat)). - (lift $ SMT.checkPredicates solver pat.constraints mempty (Set.fromList newConstraints)) >>= \case + (lift $ SMT.checkPredicates solver pat.constraints pat.substitution (Set.fromList newConstraints)) >>= \case SMT.IsInvalid -> do withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text) RewriteRuleAppT $ pure Trivial @@ -480,12 +515,6 @@ applyRule pat@Pattern{ceilConditions} rule = _other -> pure () - -- if a new constraint is going to be added, the equation cache is invalid - unless (null newConstraints) $ do - withContextFor Equations . logMessage $ - ("New path condition ensured, invalidating cache" :: Text) - - lift . RewriteT . lift . modify $ \s -> s{equations = mempty} pure newConstraints smtUnclear :: [Predicate] -> RewriteRuleAppT (RewriteT io) () @@ -669,7 +698,7 @@ mkDiffTerms = \case * RewriteStuck: config could not be re-written by any rule, return current * RewriteFailed: rewriter cannot handle the case, return current - The actions are logged at the custom log level '"Rewrite"'. + The result also includes a @'Substitution'@ accumulated from the rules ensures clauses. This flow chart should represent the actions of this function: diff --git a/booster/library/Booster/Pattern/Substitution.hs b/booster/library/Booster/Pattern/Substitution.hs new file mode 100644 index 0000000000..f2299ccf37 --- /dev/null +++ b/booster/library/Booster/Pattern/Substitution.hs @@ -0,0 +1,68 @@ +{- | +Copyright : (c) Runtime Verification, 2024 +License : BSD-3-Clause + +Function to manipulate @'Substitution'@s and convert to/from @'Predicate'@s + +This module is intended to be imported qualified. +-} +module Booster.Pattern.Substitution ( + mkEq, + asEquations, + compose, + substituteInPredicate, + substituteInTerm, +) where + +import Data.Bifunctor (bimap) +import Data.Coerce (coerce) +import Data.Map.Strict (Map) +import Data.Map.Strict qualified as Map +import Data.Maybe (fromMaybe) +import Data.Set qualified as Set + +import Booster.Pattern.Base +import Booster.Pattern.Bool +import Booster.Pattern.Util (sortOfTerm) + +{- | Compose substitutions: + - apply the left one to the assignments in the right one + - merge left with the result of above, left takes priority +-} +compose :: Substitution -> Substitution -> Substitution +compose newSubst oldSubst = + let substitutedOldSubst = Map.map (substituteInTerm newSubst) oldSubst + in (newSubst `Map.union` substitutedOldSubst) -- new bindings take priority + +-- | Build an equality predicate form a variable assignment +mkEq :: Variable -> Term -> Predicate +mkEq x t = Predicate $ case sortOfTerm t of + SortInt -> EqualsInt (Var x) t + SortBool -> EqualsBool (Var x) t + otherSort -> EqualsK (KSeq otherSort (Var x)) (KSeq otherSort t) + +-- | turns a substitution into a list of equations +asEquations :: Map Variable Term -> [Predicate] +asEquations = map (uncurry mkEq) . Map.assocs + +substituteInTerm :: Substitution -> Term -> Term +substituteInTerm substitution = goSubst + where + targetSet = Map.keysSet substitution + goSubst t + | Set.null (targetSet `Set.intersection` (getAttributes t).variables) = t + | otherwise = case t of + Var v -> fromMaybe t (Map.lookup v substitution) + DomainValue{} -> t + SymbolApplication sym sorts args -> + SymbolApplication sym sorts $ map goSubst args + AndTerm t1 t2 -> AndTerm (goSubst t1) (goSubst t2) + Injection ss s sub -> Injection ss s (goSubst sub) + KMap attrs keyVals rest -> KMap attrs (bimap goSubst goSubst <$> keyVals) (goSubst <$> rest) + KList def heads rest -> + KList def (map goSubst heads) (bimap goSubst (map goSubst) <$> rest) + KSet def elements rest -> + KSet def (map goSubst elements) (goSubst <$> rest) + +substituteInPredicate :: Substitution -> Predicate -> Predicate +substituteInPredicate substitution = coerce . substituteInTerm substitution . coerce diff --git a/booster/library/Booster/Pattern/Util.hs b/booster/library/Booster/Pattern/Util.hs index c819db8758..7f249d58ed 100644 --- a/booster/library/Booster/Pattern/Util.hs +++ b/booster/library/Booster/Pattern/Util.hs @@ -6,9 +6,6 @@ module Booster.Pattern.Util ( substituteInSort, sortOfTerm, sortOfPattern, - substituteInTerm, - substituteInPredicate, - modifyVariables, modifyVariablesInT, modifyVariablesInP, modifyVarName, @@ -82,36 +79,6 @@ substituteInSort subst (SortApp n args) = sortOfPattern :: Pattern -> Sort sortOfPattern pat = sortOfTerm pat.term -substituteInTerm :: Map Variable Term -> Term -> Term -substituteInTerm substitution = goSubst - where - targetSet = Map.keysSet substitution - goSubst t - | Set.null (targetSet `Set.intersection` (getAttributes t).variables) = t - | otherwise = case t of - Var v -> fromMaybe t (Map.lookup v substitution) - DomainValue{} -> t - SymbolApplication sym sorts args -> - SymbolApplication sym sorts $ map goSubst args - AndTerm t1 t2 -> AndTerm (goSubst t1) (goSubst t2) - Injection ss s sub -> Injection ss s (goSubst sub) - KMap attrs keyVals rest -> KMap attrs (bimap goSubst goSubst <$> keyVals) (goSubst <$> rest) - KList def heads rest -> - KList def (map goSubst heads) (bimap goSubst (map goSubst) <$> rest) - KSet def elements rest -> - KSet def (map goSubst elements) (goSubst <$> rest) - -substituteInPredicate :: Map Variable Term -> Predicate -> Predicate -substituteInPredicate substitution = coerce . substituteInTerm substitution . coerce - -modifyVariables :: (Variable -> Variable) -> Pattern -> Pattern -modifyVariables f p = - Pattern - { term = modifyVariablesInT f p.term - , constraints = Set.map (modifyVariablesInP f) p.constraints - , ceilConditions = map (coerce $ modifyVariablesInT f) p.ceilConditions - } - modifyVariablesInT :: (Variable -> Variable) -> Term -> Term modifyVariablesInT f = cata $ \case VarF v -> Var (f v) diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs index 731562f2d4..962f3e5a1f 100644 --- a/booster/library/Booster/SMT/Interface.hs +++ b/booster/library/Booster/SMT/Interface.hs @@ -280,8 +280,9 @@ isSat :: Log.LoggerMIO io => SMT.SMTContext -> [Predicate] -> + Map Variable Term -> -- supplied substitution io (IsSatResult ()) -isSat ctxt ps = fmap void <$> (isSatReturnTransState ctxt ps mempty) +isSat ctxt ps subst = fmap void <$> (isSatReturnTransState ctxt ps subst) {- | Implementation of get-model request diff --git a/booster/library/Booster/Syntax/Json/Externalise.hs b/booster/library/Booster/Syntax/Json/Externalise.hs index 4c0ba5e8eb..2b7bf2494e 100644 --- a/booster/library/Booster/Syntax/Json/Externalise.hs +++ b/booster/library/Booster/Syntax/Json/Externalise.hs @@ -20,7 +20,6 @@ import Booster.Pattern.Base (externaliseKmapUnsafe) import Booster.Pattern.Base qualified as Internal import Booster.Pattern.Bool qualified as Internal import Booster.Pattern.Util (sortOfTerm) -import Data.Map (Map) import Data.Map qualified as Map import Kore.Syntax.Json.Types qualified as Syntax @@ -30,16 +29,16 @@ 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} substitutions = +externalisePattern Internal.Pattern{term = term, constraints, ceilConditions, substitution} = -- need a sort for the predicates in external format let sort = externaliseSort $ sortOfTerm term - substitution = - if null substitutions + -- inputSubstitution is probably not needed here at all + externalisedSubstitution = + if null substitution then Nothing - else Just . multiAnd sort . map (uncurry $ externaliseSubstitution sort) . Map.toList $ substitutions - predicate = + else Just . multiAnd sort . map (uncurry $ externaliseSubstitution sort) . Map.toList $ substitution + externalisedPredicate = if null constraints && null ceilConditions then Nothing else @@ -47,7 +46,7 @@ externalisePattern Internal.Pattern{term = term, constraints, ceilConditions} su multiAnd sort $ map (externalisePredicate sort) (Set.toList constraints) ++ map (externaliseCeil sort) ceilConditions - in (externaliseTerm term, predicate, substitution) + in (externaliseTerm term, externalisedPredicate, externalisedSubstitution) where multiAnd :: Syntax.Sort -> [Syntax.KorePattern] -> Syntax.KorePattern multiAnd _ [] = error "multiAnd: empty" diff --git a/booster/library/Booster/Syntax/Json/Internalise.hs b/booster/library/Booster/Syntax/Json/Internalise.hs index dbca5fb972..591895b18d 100644 --- a/booster/library/Booster/Syntax/Json/Internalise.hs +++ b/booster/library/Booster/Syntax/Json/Internalise.hs @@ -24,7 +24,6 @@ module Booster.Syntax.Json.Internalise ( textToBS, trm, handleBS, - asEquations, TermOrPredicates (..), InternalisedPredicates (..), PatternOrTopOrBottom (..), @@ -36,6 +35,8 @@ module Booster.Syntax.Json.Internalise ( pattern CheckSubsorts, pattern IgnoreSubsorts, logPatternError, + -- substitution mining + extractSubstitution, -- for test only InternalisedPredicate (..), ) where @@ -50,6 +51,7 @@ import Data.ByteString.Char8 (ByteString, isPrefixOf) import Data.ByteString.Char8 qualified as BS import Data.Char (isLower) import Data.Coerce (coerce) +import Data.Either (partitionEithers) import Data.Foldable () import Data.Generics (extQ) import Data.Graph (SCC (..), stronglyConnComp) @@ -72,6 +74,7 @@ import Booster.Log (LoggerMIO, logMessage, withKorePatternContext) import Booster.Pattern.Base qualified as Internal import Booster.Pattern.Bool qualified as Internal import Booster.Pattern.Pretty +import Booster.Pattern.Substitution qualified as Internal import Booster.Pattern.Util (freeVariables, sortOfTerm, substituteInSort) import Booster.Prettyprinter (renderDefault) import Booster.Syntax.Json (addHeader) @@ -131,15 +134,20 @@ 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 +{- | Internalise a @'Syntax.KorePattern'@ into the components constituting a @'Internal.Pattern'@ + + Note: This function will NOT apply the internalised @'Internal.Substitution'@ to the other components. + The callers of this function must decide if it is necessary to substitute. + Use @'internalisePatternOrTopOrBottom'@ or @'internaliseTermOrPredicate'@ that return an already + substituted @'Internal.Pattern'@. +-} internalisePattern :: Flag "alias" -> Flag "subsorts" -> @@ -151,7 +159,7 @@ internalisePattern :: ( Internal.Term , [Internal.Predicate] , [Internal.Ceil] - , Map Internal.Variable Internal.Term + , Internal.Substitution , [Syntax.KorePattern] ) internalisePattern allowAlias checkSubsorts sortVars definition p = do @@ -191,7 +199,11 @@ data PatternOrTopOrBottom a | IsPattern a deriving (Functor) --- main interface functions +{- | Internalise a @'Syntax.KorePattern'@ into @'Internal.Pattern'@, detecting and reporting trivial cases. + + Note: This function will apply the internalised @'Internal.Substitution'@ part of the pattern's constraints + to the term and constraints (but not the ceils). +-} internalisePatternOrTopOrBottom :: Flag "alias" -> Flag "subsorts" -> @@ -202,7 +214,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 @@ -221,8 +233,12 @@ internalisePatternOrTopOrBottom allowAlias checkSubsorts sortVars definition exi pure $ IsPattern ( existentialVars - , Internal.Pattern{term, constraints = Set.fromList preds, ceilConditions} - , subst + , Internal.Pattern + { term = Internal.substituteInTerm subst term + , constraints = Set.map (Internal.substituteInPredicate subst) . Set.fromList $ preds + , ceilConditions + , substitution = subst + } , unknown ) where @@ -236,6 +252,15 @@ internalisePatternOrTopOrBottom allowAlias checkSubsorts sortVars definition exi Syntax.KJBottom{sort} : _ -> Just $ IsBottom sort _ : xs -> isBottom xs +{- | Internalise a @'Syntax.KorePattern'@ into either @'Internal.Pattern'@ + or @'[InternalisedPredicates]'@ if only terms of sort bool are present. + + Note: If this function successfully internalises a @'Internal.Pattern'@, it will apply the + @'Internal.Substitution'@ part to the term and constraints (but not the ceils). + + Otherwise, when we get predicates only, the substitution part + is not applied to the rest of the predicates. +-} internaliseTermOrPredicate :: Flag "alias" -> Flag "subsorts" -> @@ -252,8 +277,12 @@ internaliseTermOrPredicate allowAlias checkSubsorts sortVars definition syntaxPa internalisePattern allowAlias checkSubsorts sortVars definition syntaxPatt pure $ TermAndPredicates - Internal.Pattern{term, constraints = Set.fromList constrs, ceilConditions} - substitution + Internal.Pattern + { term = Internal.substituteInTerm substitution term + , constraints = Set.map (Internal.substituteInPredicate substitution) . Set.fromList $ constrs + , ceilConditions + , substitution + } unsupported ) @@ -458,7 +487,7 @@ mkSubstitution initialSubst = Map.partition ((== 1) . length) $ Map.fromListWith (<>) [(v, [t]) | SubstitutionPred v t <- initialSubst] equations = - [mkEq v t | (v, ts) <- Map.assocs duplicates, t <- ts] + [Internal.mkEq v t | (v, ts) <- Map.assocs duplicates, t <- ts] in execState breakCycles (Map.map head substMap, equations) where breakCycles :: State (Map Internal.Variable Internal.Term, [Internal.Predicate]) () @@ -472,19 +501,53 @@ mkSubstitution initialSubst = else do modify $ \(m, eqs) -> ( m `Map.withoutKeys` cycleNodes - , eqs <> (map (uncurry mkEq) $ Map.assocs $ m `Map.restrictKeys` cycleNodes) + , eqs <> (map (uncurry Internal.mkEq) $ Map.assocs $ m `Map.restrictKeys` cycleNodes) ) breakCycles -mkEq :: Internal.Variable -> Internal.Term -> Internal.Predicate -mkEq x t = Internal.Predicate $ case sortOfTerm t of - Internal.SortInt -> Internal.EqualsInt (Internal.Var x) t - Internal.SortBool -> Internal.EqualsBool (Internal.Var x) t - otherSort -> Internal.EqualsK (Internal.KSeq otherSort (Internal.Var x)) (Internal.KSeq otherSort t) +-- | Given a equality @'Term'@, decide if it can be interpreted as substitution. +mbSubstitution :: + Internal.Term -> InternalisedPredicate +mbSubstitution = \case + eq@(Internal.EqualsInt (Internal.Var x) e) + | x `Set.member` freeVariables e -> boolPred eq + | otherwise -> SubstitutionPred x e + eq@(Internal.EqualsInt e (Internal.Var x)) + | x `Set.member` freeVariables e -> boolPred eq + | otherwise -> SubstitutionPred x e + eq@(Internal.EqualsK (Internal.KSeq _sortL (Internal.Var x)) (Internal.KSeq _sortR e)) -> + do + -- NB sorts do not have to agree! (could be subsorts) + if (x `Set.member` freeVariables e) + then boolPred eq + else SubstitutionPred x e + eq@(Internal.EqualsK (Internal.KSeq _sortL e) (Internal.KSeq _sortR (Internal.Var x))) -> + do + -- NB sorts do not have to agree! (could be subsorts) + if (x `Set.member` freeVariables e) + then boolPred eq + else SubstitutionPred x e + other -> + boolPred other + where + boolPred = BoolPred . Internal.Predicate --- | turns a substitution into a list of equations -asEquations :: Map Internal.Variable Internal.Term -> [Internal.Predicate] -asEquations = map (uncurry mkEq) . Map.assocs +extractSubstitution :: + [Internal.Predicate] -> (Map Internal.Variable Internal.Term, Set Internal.Predicate) +extractSubstitution ps = + let (potentialSubstitution, otherPreds) = partitionSubstitutionPreds . map mbSubstitution . coerce $ ps + (newSubstitution, leftoverPreds) = mkSubstitution potentialSubstitution + in (newSubstitution, Set.fromList $ leftoverPreds <> otherPreds) + where + partitionSubstitutionPreds = partitionEithers . map unpackBoolPred + where + unpackBoolPred :: InternalisedPredicate -> Either InternalisedPredicate Internal.Predicate + unpackBoolPred = \case + pSubst@SubstitutionPred{} -> Left pSubst + BoolPred p -> Right p + other -> + -- this case is impossible the input is a valid Internal.Predicate + error $ "extractSubstitution: unsupported predicate " <> show other internalisePred :: Flag "alias" -> @@ -547,9 +610,9 @@ internalisePred allowAlias checkSubsorts sortVars definition@KoreDefinition{sort case (argS, a, b) of -- for "true" #Equals P, check whether P is in fact a substitution (Internal.SortBool, Internal.TrueBool, x) -> - mapM mbSubstitution [x] + pure [mbSubstitution x] (Internal.SortBool, x, Internal.TrueBool) -> - mapM mbSubstitution [x] + pure [mbSubstitution x] -- we could also detect NotBool (NEquals _) in "false" #Equals P (Internal.SortBool, Internal.FalseBool, x) -> pure [BoolPred $ Internal.Predicate $ Internal.NotBool x] @@ -557,12 +620,12 @@ internalisePred allowAlias checkSubsorts sortVars definition@KoreDefinition{sort pure [BoolPred $ Internal.Predicate $ Internal.NotBool x] (_, Internal.Var x, t) | x `Set.member` freeVariables t -> - pure [BoolPred $ mkEq x t] + pure [BoolPred $ Internal.mkEq x t] | otherwise -> pure [SubstitutionPred x t] (_, t, Internal.Var x) | x `Set.member` freeVariables t -> - pure [BoolPred $ mkEq x t] + pure [BoolPred $ Internal.mkEq x t] | otherwise -> pure [SubstitutionPred x t] (Internal.SortInt, _, _) -> @@ -607,33 +670,6 @@ internalisePred allowAlias checkSubsorts sortVars definition@KoreDefinition{sort throwE (IncompatibleSorts (map externaliseSort [s1, s2])) zipWithM_ go args1 args2 - mbSubstitution :: Internal.Term -> Except PatternError InternalisedPredicate - mbSubstitution = \case - eq@(Internal.EqualsInt (Internal.Var x) e) - | x `Set.member` freeVariables e -> pure $ boolPred eq - | otherwise -> pure $ SubstitutionPred x e - eq@(Internal.EqualsInt e (Internal.Var x)) - | x `Set.member` freeVariables e -> pure $ boolPred eq - | otherwise -> pure $ SubstitutionPred x e - eq@(Internal.EqualsK (Internal.KSeq _sortL (Internal.Var x)) (Internal.KSeq _sortR e)) -> - do - -- NB sorts do not have to agree! (could be subsorts) - pure $ - if (x `Set.member` freeVariables e) - then boolPred eq - else SubstitutionPred x e - eq@(Internal.EqualsK (Internal.KSeq _sortL e) (Internal.KSeq _sortR (Internal.Var x))) -> - do - -- NB sorts do not have to agree! (could be subsorts) - pure $ - if (x `Set.member` freeVariables e) - then boolPred eq - else SubstitutionPred x e - other -> - pure $ boolPred other - - boolPred = BoolPred . Internal.Predicate - ---------------------------------------- -- for use with withAssoc diff --git a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs index 5c258cba73..4031315d62 100644 --- a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs +++ b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs @@ -57,6 +57,7 @@ import Booster.Pattern.Base qualified as Def.Symbol (Symbol (..)) import Booster.Pattern.Bool (foldAndBool, pattern TrueBool) import Booster.Pattern.Index as Idx import Booster.Pattern.Pretty +import Booster.Pattern.Substitution qualified as Substitution import Booster.Pattern.Util qualified as Util import Booster.Prettyprinter hiding (attributes) import Booster.Syntax.Json.Internalise @@ -765,18 +766,20 @@ internaliseAxiom (Partial partialDefinition) parsedAxiom = sortVars attribs -{- | internalises a pattern and turns its contained substitution into - equations (predicates). Errors if any ceil conditions or - unsupported predicates are found. +{- | Internalises a pattern to be used as a rule left/right-hand side. + + Turns its contained substitution into predicates. + + Errors if any ceil conditions or unsupported predicates are found. -} -internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported :: +internaliseRulePattern :: KoreDefinition -> SourceRef -> Maybe [Id] -> (Variable -> Variable) -> Syntax.KorePattern -> Except DefinitionError (Def.Term, [Predicate]) -internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported partialDefinition ref maybeVars f t = do +internaliseRulePattern partialDefinition ref maybeVars f t = do (term, preds, ceilConditions, substitution, unsupported) <- withExcept (DefinitionPatternError ref) $ internalisePattern AllowAlias IgnoreSubsorts maybeVars partialDefinition t @@ -788,7 +791,7 @@ internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported partialDefinition ref DefinitionPatternError ref (NotSupported (head unsupported)) pure ( Util.modifyVariablesInT f term - , map (Util.modifyVariablesInP f) (preds <> asEquations substitution) + , map (Util.modifyVariablesInP f) (preds <> Substitution.asEquations substitution) ) internaliseRewriteRuleNoAlias :: @@ -805,7 +808,7 @@ internaliseRewriteRuleNoAlias partialDefinition exs left right axAttributes = do -- to avoid name clashes with patterns from the user; -- filter out literal `Top` constraints (lhs, requires) <- - internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported + internaliseRulePattern partialDefinition ref Nothing @@ -816,7 +819,7 @@ internaliseRewriteRuleNoAlias partialDefinition exs left right axAttributes = do | v `Set.member` existentials' = Util.modifyVarName Util.markAsExVar v | otherwise = Util.modifyVarName Util.markAsRuleVar v (rhs, ensures) <- - internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported + internaliseRulePattern partialDefinition ref Nothing @@ -872,14 +875,14 @@ internaliseSimpleEquation partialDef precond left right sortVars attrs | Syntax.KJApp{} <- left = do -- this ensures that `left` is a _term_ (invariant guarded by classifyAxiom) (lhs, requires) <- - internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported + internaliseRulePattern partialDef (sourceRef attrs) (Just sortVars) (Util.modifyVarName ("Eq#" <>)) $ Syntax.KJAnd left.sort [left, precond] (rhs, ensures) <- - internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported + internaliseRulePattern partialDef (sourceRef attrs) (Just sortVars) @@ -931,7 +934,7 @@ internaliseCeil :: internaliseCeil partialDef left right sortVars attrs = do -- this ensures that `left` is a _term_ (invariant guarded by classifyAxiom) (lhs, _) <- - internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported + internaliseRulePattern partialDef (sourceRef attrs) (Just sortVars) @@ -970,7 +973,7 @@ internaliseCeil partialDef left right sortVars attrs = do internalisePredicates AllowAlias IgnoreSubsorts (Just sortVars) partialDef [p] let -- turn substitution-like predicates back into equations - constraints = internalPs.boolPredicates <> asEquations internalPs.substitution + constraints = internalPs.boolPredicates <> Substitution.asEquations internalPs.substitution unsupported = internalPs.unsupported unless (null unsupported) $ throwE $ @@ -1017,9 +1020,9 @@ internaliseFunctionEquation partialDef requires args leftTerm right sortVars att argPairs <- mapM internaliseArg args let lhs = Util.modifyVariablesInT (Util.modifyVarName ("Eq#" <>)) $ - Util.substituteInTerm (Map.fromList argPairs) left + Substitution.substituteInTerm (Map.fromList argPairs) left (rhs, ensures) <- - internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported + internaliseRulePattern partialDef (sourceRef attrs) (Just sortVars) @@ -1049,7 +1052,9 @@ internaliseFunctionEquation partialDef requires args leftTerm right sortVars att { lhs , rhs , requires = - map (Util.modifyVariablesInP $ Util.modifyVarName ("Eq#" <>)) (preds <> asEquations substitution) + map + (Util.modifyVariablesInP $ Util.modifyVarName ("Eq#" <>)) + (preds <> Substitution.asEquations substitution) , ensures , attributes , computedAttributes diff --git a/booster/test/rpc-integration/test-a-to-f/response-branching.kore-rpc-dev b/booster/test/rpc-integration/test-a-to-f/response-branching.kore-rpc-dev deleted file mode 100644 index 0d2f7baef6..0000000000 --- a/booster/test/rpc-integration/test-a-to-f/response-branching.kore-rpc-dev +++ /dev/null @@ -1,400 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "branching", - "depth": 0, - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "a" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - } - }, - "next-states": [ - { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "c" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "rule-id": "3cfae148c63f879628626da1753b07d517f6ac9b414543f7dd8f7b3e8e19329e", - "rule-substitution": { - "format": "KORE", - "version": 1, - "term": { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortGeneratedCounterCell", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "RuleVar'Unds'DotVar0", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedCounterCell", - "args": [] - } - }, - "second": { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortK", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "RuleVar'Unds'DotVar1", - "sort": { - "tag": "SortApp", - "name": "SortK", - "args": [] - } - }, - "second": { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - } - ] - } - } - }, - { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "b" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "rule-id": "aba8479fef763c749fa1a1837f2591f85d8541ca8837c738cf586de790c6f8b8", - "rule-substitution": { - "format": "KORE", - "version": 1, - "term": { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortGeneratedCounterCell", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "RuleVar'Unds'DotVar0", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedCounterCell", - "args": [] - } - }, - "second": { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortK", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "RuleVar'Unds'DotVar1", - "sort": { - "tag": "SortApp", - "name": "SortK", - "args": [] - } - }, - "second": { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - } - ] - } - } - } - ] - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-diamond/response-infeasible-branching.booster-dev b/booster/test/rpc-integration/test-diamond/response-infeasible-branching.booster-dev index ce99ad8ff6..c96f33b892 100644 --- a/booster/test/rpc-integration/test-diamond/response-infeasible-branching.booster-dev +++ b/booster/test/rpc-integration/test-diamond/response-infeasible-branching.booster-dev @@ -67,13 +67,13 @@ "sorts": [], "args": [ { - "tag": "EVar", - "name": "X", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "42" } ] }, @@ -96,14 +96,14 @@ ] } }, - "predicate": { + "substitution": { "format": "KORE", "version": 1, "term": { "tag": "Equals", "argSort": { "tag": "SortApp", - "name": "SortBool", + "name": "SortInt", "args": [] }, "sort": { @@ -112,38 +112,22 @@ "args": [] }, "first": { - "tag": "DV", + "tag": "EVar", + "name": "X", "sort": { "tag": "SortApp", - "name": "SortBool", + "name": "SortInt", "args": [] - }, - "value": "true" + } }, "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "42" - } - ] + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "42" } } } diff --git a/booster/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.booster-dev b/booster/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.booster-dev deleted file mode 100644 index 12b421e0d0..0000000000 --- a/booster/test/rpc-integration/test-diamond/response-mutual-constraints-stuck.booster-dev +++ /dev/null @@ -1,134 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "stuck", - "depth": 2, - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "g" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - } - }, - "logs": [ - { - "tag": "rewrite", - "origin": "booster", - "result": { - "tag": "success", - "rule-id": "928fbc2c9e62487c0fdc40fb4eeff63c14c06f9cd3e4bdde5c62be73b318d352" - } - }, - { - "tag": "rewrite", - "origin": "booster", - "result": { - "tag": "success", - "rule-id": "51a4003346d710ea028036ee9bdeaf964113e46e843a8c8f15a8f0f886be1fcf" - } - }, - { - "tag": "rewrite", - "origin": "booster", - "result": { - "tag": "failure", - "reason": "No applicable rules found" - } - }, - { - "tag": "rewrite", - "origin": "booster", - "result": { - "tag": "failure", - "reason": "No applicable rules found" - } - } - ] - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.booster-dev b/booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.booster-dev deleted file mode 100644 index 92827d7008..0000000000 --- a/booster/test/rpc-integration/test-diamond/response-mutual-constraints-terminal.booster-dev +++ /dev/null @@ -1,119 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "terminal-rule", - "depth": 2, - "rule": "TEST.FG", - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "g" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - } - }, - "logs": [ - { - "tag": "rewrite", - "origin": "booster", - "result": { - "tag": "success", - "rule-id": "928fbc2c9e62487c0fdc40fb4eeff63c14c06f9cd3e4bdde5c62be73b318d352" - } - }, - { - "tag": "rewrite", - "origin": "booster", - "result": { - "tag": "success", - "rule-id": "51a4003346d710ea028036ee9bdeaf964113e46e843a8c8f15a8f0f886be1fcf" - } - } - ] - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.json b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.json index 44aefb1934..812dbd3a09 100644 --- a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.json +++ b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.json @@ -86,73 +86,63 @@ }, "patterns": [ { - "tag": "And", + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + }, "sort": { "tag": "SortApp", "name": "SortGeneratedTopCell", "args": [] }, - "patterns": [ - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - }, - "second": { - "tag": "App", - "name": "Lblb'Unds'QUESTIONMARK-VARS'Unds'State", - "sorts": [], - "args": [] - } - }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "Var'Ques'X0", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - }, - "second": { - "tag": "EVar", - "name": "Var'Ques'X1", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } + "first": { + "tag": "EVar", + "name": "Var'Ques'X", + "sort": { + "tag": "SortApp", + "name": "SortState", + "args": [] } - ] + }, + "second": { + "tag": "App", + "name": "Lblb'Unds'QUESTIONMARK-VARS'Unds'State", + "sorts": [], + "args": [] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "Var'Ques'X0", + "sort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + } + }, + "second": { + "tag": "EVar", + "name": "Var'Ques'X1", + "sort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + } + } }, { "tag": "Equals", diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.booster-dev b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.kore-rpc-dev similarity index 67% rename from booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.booster-dev rename to booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.kore-rpc-dev index 812dbd3a09..44aefb1934 100644 --- a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.booster-dev +++ b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.kore-rpc-dev @@ -86,63 +86,73 @@ }, "patterns": [ { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, + "tag": "And", "sort": { "tag": "SortApp", "name": "SortGeneratedTopCell", "args": [] }, - "first": { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - }, - "second": { - "tag": "App", - "name": "Lblb'Unds'QUESTIONMARK-VARS'Unds'State", - "sorts": [], - "args": [] - } - }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "Var'Ques'X0", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - }, - "second": { - "tag": "EVar", - "name": "Var'Ques'X1", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] + "patterns": [ + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "Var'Ques'X", + "sort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + } + }, + "second": { + "tag": "App", + "name": "Lblb'Unds'QUESTIONMARK-VARS'Unds'State", + "sorts": [], + "args": [] + } + }, + { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "Var'Ques'X0", + "sort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + } + }, + "second": { + "tag": "EVar", + "name": "Var'Ques'X1", + "sort": { + "tag": "SortApp", + "name": "SortState", + "args": [] + } + } } - } + ] }, { "tag": "Equals", diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques.booster-dev b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques.json similarity index 100% rename from booster/test/rpc-integration/test-questionmark-vars/response-one-ques.booster-dev rename to booster/test/rpc-integration/test-questionmark-vars/response-one-ques.json diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques.kore-rpc-dev b/booster/test/rpc-integration/test-questionmark-vars/response-one-ques.kore-rpc-dev deleted file mode 100644 index 8852423b90..0000000000 --- a/booster/test/rpc-integration/test-questionmark-vars/response-one-ques.kore-rpc-dev +++ /dev/null @@ -1,121 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "stuck", - "depth": 1, - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'a-state'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'b-state'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'Stop'State'Unds'QUESTIONMARK-VARS'Unds'State", - "sorts": [], - "args": [] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "predicate": { - "format": "KORE", - "version": 1, - "term": { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lblcondition'LParUndsRParUnds'QUESTIONMARK-VARS'Unds'Bool'Unds'State", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - } - } - } - } - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.booster-dev b/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.json similarity index 100% rename from booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.booster-dev rename to booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.json diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.kore-rpc-dev b/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.kore-rpc-dev deleted file mode 100644 index eb9ba3ab36..0000000000 --- a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-external.kore-rpc-dev +++ /dev/null @@ -1,124 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "stuck", - "depth": 1, - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'a-state'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'b-state'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X0", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "predicate": { - "format": "KORE", - "version": 1, - "term": { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lblcondition'LParUndsRParUnds'QUESTIONMARK-VARS'Unds'Bool'Unds'State", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X0", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - } - } - } - } - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal-with-counter.booster-dev b/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal-with-counter.json similarity index 100% rename from booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal-with-counter.booster-dev rename to booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal-with-counter.json diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.booster-dev b/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.json similarity index 100% rename from booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.booster-dev rename to booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.json diff --git a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.kore-rpc-dev b/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.kore-rpc-dev deleted file mode 100644 index a450b120fc..0000000000 --- a/booster/test/rpc-integration/test-questionmark-vars/response-two-ques-internal.kore-rpc-dev +++ /dev/null @@ -1,172 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "stuck", - "depth": 2, - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'a-state'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'b-state'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X0", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "predicate": { - "format": "KORE", - "version": 1, - "term": { - "tag": "And", - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "patterns": [ - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lblcondition'LParUndsRParUnds'QUESTIONMARK-VARS'Unds'Bool'Unds'State", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - } - }, - { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lblcondition'LParUndsRParUnds'QUESTIONMARK-VARS'Unds'Bool'Unds'State", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X0", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - } - } - ] - } - } - ] - } - } - } - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-substitutions/README.md b/booster/test/rpc-integration/test-substitutions/README.md index f6bf9f83bb..6180c4c7af 100644 --- a/booster/test/rpc-integration/test-substitutions/README.md +++ b/booster/test/rpc-integration/test-substitutions/README.md @@ -39,6 +39,7 @@ NB: Booster applies the given substitution before performing any action. - starts from `concrete-subst` - with two equations that have circular dependencies: `Y = 1 +Int X`, `X = Y -Int 1` - leading to end state with `X == 42` from the `ensures`-clause + - `booster-dev` return a trivial circular constraint `X ==Int X` * `state-symbolic-bottom-predicate.execute` - starts from `symbolic-subst` - with an equation that is instantly false: `X = 1 +Int X` diff --git a/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev b/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev index 259a441aeb..337751c9c3 100644 --- a/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev +++ b/booster/test/rpc-integration/test-substitutions/response-circular-equations.booster-dev @@ -66,13 +66,13 @@ "sorts": [], "args": [ { - "tag": "EVar", - "name": "X", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "42" } ] }, @@ -82,29 +82,13 @@ "sorts": [], "args": [ { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "1" - } - ] + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "43" } ] }, @@ -128,57 +112,6 @@ } }, "substitution": { - "format": "KORE", - "version": 1, - "term": { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "EVar", - "name": "Y", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - "second": { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "1" - }, - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - } - } - }, - "predicate": { "format": "KORE", "version": 1, "term": { @@ -193,7 +126,7 @@ "tag": "Equals", "argSort": { "tag": "SortApp", - "name": "SortBool", + "name": "SortInt", "args": [] }, "sort": { @@ -202,45 +135,29 @@ "args": [] }, "first": { - "tag": "DV", + "tag": "EVar", + "name": "X", "sort": { "tag": "SortApp", - "name": "SortBool", + "name": "SortInt", "args": [] - }, - "value": "true" + } }, "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "42" } }, { "tag": "Equals", "argSort": { "tag": "SortApp", - "name": "SortBool", + "name": "SortInt", "args": [] }, "sort": { @@ -249,42 +166,77 @@ "args": [] }, "first": { - "tag": "DV", + "tag": "EVar", + "name": "Y", "sort": { "tag": "SortApp", - "name": "SortBool", + "name": "SortInt", "args": [] - }, - "value": "true" + } }, "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "42" - } - ] + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "43" } } ] } + }, + "predicate": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "true" + }, + "second": { + "tag": "App", + "name": "Lbl'UndsEqlsEqls'Int'Unds'", + "sorts": [], + "args": [ + { + "tag": "EVar", + "name": "X", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + { + "tag": "EVar", + "name": "X", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + } + ] + } + } } } } diff --git a/booster/test/rpc-integration/test-substitutions/response-concrete-substitution.booster-dev b/booster/test/rpc-integration/test-substitutions/response-concrete-substitution.booster-dev deleted file mode 100644 index 379ed33ccc..0000000000 --- a/booster/test/rpc-integration/test-substitutions/response-concrete-substitution.booster-dev +++ /dev/null @@ -1,168 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "terminal-rule", - "depth": 1, - "rule": "TEST.concrete-subst", - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "a" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'jnt'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Y", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "predicate": { - "format": "KORE", - "version": 1, - "term": { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "42" - } - ] - } - } - } - } - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev deleted file mode 100644 index 8196839aaa..0000000000 --- a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.booster-dev +++ /dev/null @@ -1,183 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "vacuous", - "depth": 0, - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "symbolic-subst" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'jnt'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Y", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "predicate": { - "format": "KORE", - "version": 1, - "term": { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "App", - "name": "Lbl'UndsPlus'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "1" - }, - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - } - ] - } - } - } - } - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json index 8196839aaa..8dd09608d8 100644 --- a/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json +++ b/booster/test/rpc-integration/test-substitutions/response-symbolic-bottom-predicate.json @@ -180,4 +180,4 @@ } } } -} \ No newline at end of file +} diff --git a/booster/test/rpc-integration/test-substitutions/response-symbolic-substitution.booster-dev b/booster/test/rpc-integration/test-substitutions/response-symbolic-substitution.booster-dev deleted file mode 100644 index 5cf51a99bb..0000000000 --- a/booster/test/rpc-integration/test-substitutions/response-symbolic-substitution.booster-dev +++ /dev/null @@ -1,168 +0,0 @@ -{ - "jsonrpc": "2.0", - "id": 1, - "result": { - "reason": "terminal-rule", - "depth": 1, - "rule": "TEST.symbolic-subst", - "state": { - "term": { - "format": "KORE", - "version": 1, - "term": { - "tag": "App", - "name": "Lbl'-LT-'generatedTop'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'-LT-'k'-GT-'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "kseq", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "inj", - "sorts": [ - { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - { - "tag": "SortApp", - "name": "SortKItem", - "args": [] - } - ], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortState", - "args": [] - }, - "value": "a" - } - ] - }, - { - "tag": "App", - "name": "dotk", - "sorts": [], - "args": [] - } - ] - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'int'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'jnt'-GT-'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Y", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - }, - { - "tag": "App", - "name": "Lbl'-LT-'generatedCounter'-GT-'", - "sorts": [], - "args": [ - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - }, - "predicate": { - "format": "KORE", - "version": 1, - "term": { - "tag": "Equals", - "argSort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "sort": { - "tag": "SortApp", - "name": "SortGeneratedTopCell", - "args": [] - }, - "first": { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortBool", - "args": [] - }, - "value": "true" - }, - "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "EVar", - "name": "Y", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - } - ] - } - } - } - } - } -} \ No newline at end of file diff --git a/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test1.json b/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test1.json index caf1cf3ac9..f0938023a3 100644 --- a/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test1.json +++ b/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test1.json @@ -63,13 +63,13 @@ "sorts": [], "args": [ { - "tag": "EVar", - "name": "Var'Ques'X", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "42" } ] }, @@ -92,14 +92,14 @@ ] } }, - "predicate": { + "substitution": { "format": "KORE", "version": 1, "term": { "tag": "Equals", "argSort": { "tag": "SortApp", - "name": "SortBool", + "name": "SortInt", "args": [] }, "sort": { @@ -108,38 +108,22 @@ "args": [] }, "first": { - "tag": "DV", + "tag": "EVar", + "name": "Var'Ques'X", "sort": { "tag": "SortApp", - "name": "SortBool", + "name": "SortInt", "args": [] - }, - "value": "true" + } }, "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "42" - } - ] + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "42" } } } diff --git a/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test2.json b/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test2.json index 9d24d95c64..8b9792046d 100644 --- a/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test2.json +++ b/booster/test/rpc-integration/test-use-path-condition-in-equations/response-test2.json @@ -63,13 +63,13 @@ "sorts": [], "args": [ { - "tag": "EVar", - "name": "Var'Ques'X", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "42" } ] }, @@ -92,14 +92,14 @@ ] } }, - "predicate": { + "substitution": { "format": "KORE", "version": 1, "term": { "tag": "Equals", "argSort": { "tag": "SortApp", - "name": "SortBool", + "name": "SortInt", "args": [] }, "sort": { @@ -108,41 +108,25 @@ "args": [] }, "first": { - "tag": "DV", + "tag": "EVar", + "name": "Var'Ques'X", "sort": { "tag": "SortApp", - "name": "SortBool", + "name": "SortInt", "args": [] - }, - "value": "true" + } }, "second": { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "Var'Ques'X", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "42" - } - ] + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "42" } } } } } -} +} \ No newline at end of file diff --git a/booster/tools/booster/Proxy.hs b/booster/tools/booster/Proxy.hs index edadbd7e0f..251728085b 100644 --- a/booster/tools/booster/Proxy.hs +++ b/booster/tools/booster/Proxy.hs @@ -523,8 +523,7 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of pure $ Right ( ( Booster.toExecState - Pattern{term, ceilConditions, constraints = Set.fromList preds} - sub + Pattern{term, ceilConditions, constraints = Set.fromList preds, substitution = sub} unsup Nothing ) diff --git a/booster/unit-tests/Test/Booster/Pattern/Binary.hs b/booster/unit-tests/Test/Booster/Pattern/Binary.hs index 931d803707..e5588fda77 100644 --- a/booster/unit-tests/Test/Booster/Pattern/Binary.hs +++ b/booster/unit-tests/Test/Booster/Pattern/Binary.hs @@ -67,7 +67,7 @@ genPredicate = <$> Gen.choice [pure TrueBool, pure FalseBool, genTerm] genPattern :: Gen Pattern -genPattern = (\t cs -> Pattern t cs mempty) <$> genTerm <*> (Set.fromList <$> upTo 10 genPredicate) +genPattern = (\t cs -> Pattern t cs mempty mempty) <$> genTerm <*> (Set.fromList <$> upTo 10 genPredicate) test_BinaryRoundTrips :: [TestTree] test_BinaryRoundTrips = diff --git a/booster/unit-tests/Test/Booster/Pattern/Substitution.hs b/booster/unit-tests/Test/Booster/Pattern/Substitution.hs new file mode 100644 index 0000000000..663bdd2a54 --- /dev/null +++ b/booster/unit-tests/Test/Booster/Pattern/Substitution.hs @@ -0,0 +1,84 @@ +{-# LANGUAGE QuasiQuotes #-} + +module Test.Booster.Pattern.Substitution ( + test_subst, +) where + +import Data.Map qualified as Map +import Test.Tasty +import Test.Tasty.HUnit + +import Booster.Definition.Attributes.Base +import Booster.Pattern.Base +import Booster.Pattern.Substitution +import Booster.Syntax.Json.Internalise (trm) + +test_subst :: TestTree +test_subst = + testGroup + "Substitution" + [ testGroup + "Application" + [ test + "con1(X)[con1(Y)/X]" + ("X" |-> [trm| con1{}(Y:SomeSort{}) |]) + ([trm| con1{}(X:SomeSort{}) |]) + ([trm| con1{}(con1{}(Y:SomeSort{})) |]) + , test + "con1(X)/\\con1(X)[con1(Y)/X]" + ("X" |-> [trm| con1{}(Y:SomeSort{}) |]) + (AndTerm ([trm| con1{}(X:SomeSort{}) |]) ([trm| con1{}(X:SomeSort{}) |])) + (AndTerm ([trm| con1{}(con1{}(Y:SomeSort{})) |]) ([trm| con1{}(con1{}(Y:SomeSort{})) |])) + , test + "con1(X)/\\con1(Y)[con1(Y)/X]" + ("X" |-> [trm| con1{}(Y:SomeSort{}) |]) + (AndTerm ([trm| con1{}(X:SomeSort{}) |]) ([trm| con1{}(Y:SomeSort{}) |])) + (AndTerm ([trm| con1{}(con1{}(Y:SomeSort{})) |]) ([trm| con1{}(Y:SomeSort{}) |])) + ] + , testGroup + "Composition" + [ testCase + "compose is idempotent" + $ (("X" |-> [trm| con1{}(Y:SomeSort{}) |]) `compose` ("X" |-> [trm| con1{}(Y:SomeSort{}) |])) + @?= ("X" |-> [trm| con1{}(Y:SomeSort{}) |]) + , testCase + "compose is transitive and saturating" + $ (("X" |-> [trm| Z:SomeSort{} |]) `compose` ("Y" |-> [trm| X:SomeSort{} |])) + @?= ("X" |-> [trm| Z:SomeSort{} |]) + <> ("Y" |-> [trm| Z:SomeSort{} |]) + ] + ] + +---------------------------------------- +-- Test fixture +test :: String -> Map.Map Variable Term -> Term -> Term -> TestTree +test name substitutions term expected = + testCase name $ substituteInTerm substitutions term @?= expected + +someSort :: Sort +someSort = SortApp "SomeSort" [] + +(|->) :: VarName -> Term -> Substitution +(|->) v t = Map.fromList [(Variable someSort v, t)] + +asConstructor :: SymbolAttributes +asConstructor = + SymbolAttributes + Constructor + IsNotIdem + IsNotAssoc + IsNotMacroOrAlias + CanBeEvaluated + Nothing + Nothing + Nothing + +con1 :: Symbol +con1 = + Symbol + { name = "con1" + , sortVars = [] + , resultSort = someSort + , argSorts = [someSort] + , attributes = asConstructor + } diff --git a/booster/unit-tests/Test/Booster/Pattern/Util.hs b/booster/unit-tests/Test/Booster/Pattern/Util.hs index 110c542898..11f021c5dd 100644 --- a/booster/unit-tests/Test/Booster/Pattern/Util.hs +++ b/booster/unit-tests/Test/Booster/Pattern/Util.hs @@ -1,38 +1,14 @@ module Test.Booster.Pattern.Util ( - test_subst, test_freshen, ) where -import Data.Map qualified as Map import Data.Set qualified as Set import Test.Tasty import Test.Tasty.HUnit -import Booster.Definition.Attributes.Base import Booster.Pattern.Base import Booster.Pattern.Util -test_subst :: TestTree -test_subst = - testGroup - "Substitution" - [ test - "con1(X)[con1(Y)/X]" - (Map.fromList [(Variable someSort "X", app con1 [var "Y" someSort])]) - (app con1 [var "X" someSort]) - (app con1 [app con1 [var "Y" someSort]]) - , test - "con1(X)/\\con1(X)[con1(Y)/X]" - (Map.fromList [(Variable someSort "X", app con1 [var "Y" someSort])]) - (AndTerm (app con1 [var "X" someSort]) (app con1 [var "X" someSort])) - (AndTerm (app con1 [app con1 [var "Y" someSort]]) (app con1 [app con1 [var "Y" someSort]])) - , test - "con1(X)/\\con1(Y)[con1(Y)/X]" - (Map.fromList [(Variable someSort "X", app con1 [var "Y" someSort])]) - (AndTerm (app con1 [var "X" someSort]) (app con1 [var "Y" someSort])) - (AndTerm (app con1 [app con1 [var "Y" someSort]]) (app con1 [var "Y" someSort])) - ] - test_freshen :: TestTree test_freshen = testGroup @@ -53,38 +29,6 @@ test_freshen = ] ---------------------------------------- --- Test fixture -test :: String -> Map.Map Variable Term -> Term -> Term -> TestTree -test name substitutions term expected = - testCase name $ substituteInTerm substitutions term @?= expected someSort :: Sort someSort = SortApp "SomeSort" [] - -var :: VarName -> Sort -> Term -var variableName variableSort = Var $ Variable{variableSort, variableName} - -app :: Symbol -> [Term] -> Term -app s = SymbolApplication s [] - -asConstructor :: SymbolAttributes -asConstructor = - SymbolAttributes - Constructor - IsNotIdem - IsNotAssoc - IsNotMacroOrAlias - CanBeEvaluated - Nothing - Nothing - Nothing - -con1 :: Symbol -con1 = - Symbol - { name = "con1" - , sortVars = [] - , resultSort = someSort - , argSorts = [someSort] - , attributes = asConstructor - }