From 4347105296d121d9a6871d745791565fdc76effe Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 16 Oct 2024 22:38:39 +1100 Subject: [PATCH] Recognise ==Int and ==K equations as substitutions when internalising (#4061) Booster now recognises predicates of shape `true #Equals (VAR ==Int )` and `true #Equals (VAR ==K )` as substitutions (given the global scope does not contradict that, i.e., no cycles or multiple substitutions for the same VAR...). Currently only matches ==Int and ==K. We could also match notBool (_ =/=Int _) and notBool (_ =/=K _) (more magic). When internalising rules and equations, the substitution must be turned back into predicates for the `requires` clause. Currently we also turn back the ensures clause substitutions into predicates (might want to change that). Part of #4059 --- .../Booster/Syntax/Json/Internalise.hs | 38 +++- .../Booster/Syntax/ParsedKore/Internalise.hs | 26 +-- .../rpc-integration/test-vacuous/README.md | 2 + .../response-vacuous-but-rewritten.json | 167 +++++++----------- .../response-vacuous-without-rewrite.json | 167 +++++++----------- 5 files changed, 173 insertions(+), 227 deletions(-) diff --git a/booster/library/Booster/Syntax/Json/Internalise.hs b/booster/library/Booster/Syntax/Json/Internalise.hs index e5db8e344f..dbca5fb972 100644 --- a/booster/library/Booster/Syntax/Json/Internalise.hs +++ b/booster/library/Booster/Syntax/Json/Internalise.hs @@ -24,6 +24,7 @@ module Booster.Syntax.Json.Internalise ( textToBS, trm, handleBS, + asEquations, TermOrPredicates (..), InternalisedPredicates (..), PatternOrTopOrBottom (..), @@ -481,6 +482,10 @@ mkEq x t = Internal.Predicate $ case sortOfTerm t of Internal.SortBool -> Internal.EqualsBool (Internal.Var x) t otherSort -> Internal.EqualsK (Internal.KSeq otherSort (Internal.Var x)) (Internal.KSeq otherSort t) +-- | turns a substitution into a list of equations +asEquations :: Map Internal.Variable Internal.Term -> [Internal.Predicate] +asEquations = map (uncurry mkEq) . Map.assocs + internalisePred :: Flag "alias" -> Flag "subsorts" -> @@ -540,10 +545,12 @@ internalisePred allowAlias checkSubsorts sortVars definition@KoreDefinition{sort ensureEqualSorts (sortOfTerm a) argS ensureEqualSorts (sortOfTerm b) argS case (argS, a, b) of + -- for "true" #Equals P, check whether P is in fact a substitution (Internal.SortBool, Internal.TrueBool, x) -> - pure [BoolPred $ Internal.Predicate x] + mapM mbSubstitution [x] (Internal.SortBool, x, Internal.TrueBool) -> - pure [BoolPred $ Internal.Predicate x] + mapM mbSubstitution [x] + -- we could also detect NotBool (NEquals _) in "false" #Equals P (Internal.SortBool, Internal.FalseBool, x) -> pure [BoolPred $ Internal.Predicate $ Internal.NotBool x] (Internal.SortBool, x, Internal.FalseBool) -> @@ -600,6 +607,33 @@ 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 6a1acbd6f5..5c258cba73 100644 --- a/booster/library/Booster/Syntax/ParsedKore/Internalise.hs +++ b/booster/library/Booster/Syntax/ParsedKore/Internalise.hs @@ -765,6 +765,10 @@ 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. +-} internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported :: KoreDefinition -> SourceRef -> @@ -776,16 +780,16 @@ internalisePatternEnsureNoSubstitutionOrCeilOrUnsupported partialDefinition ref (term, preds, ceilConditions, substitution, unsupported) <- withExcept (DefinitionPatternError ref) $ internalisePattern AllowAlias IgnoreSubsorts maybeVars partialDefinition t - unless (null substitution) $ - throwE $ - DefinitionPatternError ref SubstitutionNotAllowed unless (null ceilConditions) $ throwE $ DefinitionPatternError ref CeilNotAllowed unless (null unsupported) $ throwE $ DefinitionPatternError ref (NotSupported (head unsupported)) - pure (Util.modifyVariablesInT f term, map (Util.modifyVariablesInP f) preds) + pure + ( Util.modifyVariablesInT f term + , map (Util.modifyVariablesInP f) (preds <> asEquations substitution) + ) internaliseRewriteRuleNoAlias :: KoreDefinition -> @@ -964,12 +968,10 @@ internaliseCeil partialDef left right sortVars attrs = do internalPs <- withExcept (DefinitionPatternError (sourceRef attrs)) $ internalisePredicates AllowAlias IgnoreSubsorts (Just sortVars) partialDef [p] - let constraints = internalPs.boolPredicates - substitutions = internalPs.substitution + let + -- turn substitution-like predicates back into equations + constraints = internalPs.boolPredicates <> asEquations internalPs.substitution unsupported = internalPs.unsupported - unless (null substitutions) $ - throwE $ - DefinitionPatternError (sourceRef attrs) SubstitutionNotAllowed unless (null unsupported) $ throwE $ DefinitionPatternError (sourceRef attrs) $ @@ -1005,9 +1007,6 @@ internaliseFunctionEquation partialDef requires args leftTerm right sortVars att withExcept (DefinitionPatternError (sourceRef attrs)) $ internalisePattern AllowAlias IgnoreSubsorts (Just sortVars) partialDef $ Syntax.KJAnd leftTerm.sort [leftTerm, requires] - unless (null substitution) $ - throwE $ - DefinitionPatternError (sourceRef attrs) SubstitutionNotAllowed unless (null ceils) $ throwE $ DefinitionPatternError (sourceRef attrs) CeilNotAllowed @@ -1049,7 +1048,8 @@ internaliseFunctionEquation partialDef requires args leftTerm right sortVars att RewriteRule { lhs , rhs - , requires = map (Util.modifyVariablesInP $ Util.modifyVarName ("Eq#" <>)) preds + , requires = + map (Util.modifyVariablesInP $ Util.modifyVarName ("Eq#" <>)) (preds <> asEquations substitution) , ensures , attributes , computedAttributes diff --git a/booster/test/rpc-integration/test-vacuous/README.md b/booster/test/rpc-integration/test-vacuous/README.md index 00c6823dc4..80b71a94c7 100644 --- a/booster/test/rpc-integration/test-vacuous/README.md +++ b/booster/test/rpc-integration/test-vacuous/README.md @@ -37,6 +37,7 @@ Rules `init` and `AC` introduce constraints on this variable: _Expected:_ - The rewrite is stuck with `dN \and...(contradiction)` + - The `N` is substituted by value `1` in the final result (booster). - The result is simplified and discovered to be `vacuous` (with state `d`). 1) _vacuous-but-rewritten_ @@ -47,6 +48,7 @@ Rules `init` and `AC` introduce constraints on this variable: _Expected:_ - Rewrite with `BD` (despite the contradiction) - The rewrite is stuck with `dN \and...(contradiction)` + - The `N` is substituted by value `1` in the final result (booster). - The result is simplified and discovered to be `vacuous` (with state `d`). With `kore-rpc-dev`, some contradictions will be discovered before or while diff --git a/booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json b/booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json index b7cf387833..c604e9284f 100644 --- a/booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json +++ b/booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json @@ -66,13 +66,13 @@ "sorts": [], "args": [ { - "tag": "EVar", - "name": "N", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "0" } ] }, @@ -95,119 +95,74 @@ ] } }, + "substitution": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "N", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + "second": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + } + }, "predicate": { "format": "KORE", "version": 1, "term": { - "tag": "And", + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, "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": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "N", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "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": "LblnotBool'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "N", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - } - ] + "value": "true" + }, + "second": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "false" + } } } } diff --git a/booster/test/rpc-integration/test-vacuous/response-vacuous-without-rewrite.json b/booster/test/rpc-integration/test-vacuous/response-vacuous-without-rewrite.json index d3b14044a8..9bb9e7c837 100644 --- a/booster/test/rpc-integration/test-vacuous/response-vacuous-without-rewrite.json +++ b/booster/test/rpc-integration/test-vacuous/response-vacuous-without-rewrite.json @@ -66,13 +66,13 @@ "sorts": [], "args": [ { - "tag": "EVar", - "name": "N", + "tag": "DV", "sort": { "tag": "SortApp", "name": "SortInt", "args": [] - } + }, + "value": "0" } ] }, @@ -95,119 +95,74 @@ ] } }, + "substitution": { + "format": "KORE", + "version": 1, + "term": { + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "sort": { + "tag": "SortApp", + "name": "SortGeneratedTopCell", + "args": [] + }, + "first": { + "tag": "EVar", + "name": "N", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + } + }, + "second": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortInt", + "args": [] + }, + "value": "0" + } + } + }, "predicate": { "format": "KORE", "version": 1, "term": { - "tag": "And", + "tag": "Equals", + "argSort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, "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": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "N", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } + "first": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "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": "LblnotBool'Unds'", - "sorts": [], - "args": [ - { - "tag": "App", - "name": "Lbl'UndsEqlsEqls'Int'Unds'", - "sorts": [], - "args": [ - { - "tag": "EVar", - "name": "N", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - } - }, - { - "tag": "DV", - "sort": { - "tag": "SortApp", - "name": "SortInt", - "args": [] - }, - "value": "0" - } - ] - } - ] - } - } - ] + "value": "true" + }, + "second": { + "tag": "DV", + "sort": { + "tag": "SortApp", + "name": "SortBool", + "args": [] + }, + "value": "false" + } } } }