Skip to content

Attempt no. 2 at fixing rule-substitution #3939

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Jun 17, 2024
Merged

Attempt no. 2 at fixing rule-substitution #3939

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
9cde223
Attempt no. 2 at fixing rule-substitution
goodlyrottenapple Jun 14, 2024
954a301
fix test
goodlyrottenapple Jun 14, 2024
e1e261e
update golden
goodlyrottenapple Jun 14, 2024
21fb083
modify rpc test to check he case when VarX appears in rule and config…
goodlyrottenapple Jun 17, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 10 additions & 2 deletions kore/src/Kore/JsonRpc.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,11 +81,12 @@ import Kore.Rewrite (
import Kore.Rewrite.ClaimPattern qualified as ClaimPattern
import Kore.Rewrite.RewriteStep (EnableAssumeInitialDefined (..))
import Kore.Rewrite.RewritingVariable (
RewritingVariableName,
RewritingVariableName (..),
getRewritingPattern,
getRewritingVariable,
isSomeConfigVariable,
isSomeEquationVariable,
isSomeRuleVariable,
mkRewritingPattern,
mkRewritingTerm,
)
Expand Down Expand Up @@ -386,7 +387,14 @@ respond serverState moduleName runSMT =
else Just $ Kore.Syntax.Json.fromTermLike $ foldl TermLike.mkAnd pr' $ map toEquals predsFromSub
in ( getRewritingPattern p'
, finalPr
, PatternJson.fromSubstitution sort $ Substitution.mapVariables getRewritingVariable sub
, PatternJson.fromSubstitution sort
$ Substitution.mapVariables
( pure $ \case
ConfigVariableName v -> v
RuleVariableName [email protected]{base = TermLike.Id{getId = nm, idLocation = loc}} -> v{SomeVariable.base = TermLike.Id{getId = "Rule" <> nm, idLocation = loc}}
EquationVariableName [email protected]{base = TermLike.Id{getId = nm, idLocation = loc}} -> v{SomeVariable.base = TermLike.Id{getId = "Eq" <> nm, idLocation = loc}}
)
$ Substitution.filter isSomeRuleVariable sub
, rid
)

Expand Down
28 changes: 19 additions & 9 deletions kore/src/Kore/Rewrite/RewriteStep.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,12 @@ finalizeAppliedRule ::
RulePattern RewritingVariableName ->
-- | Conditions of applied rule
Condition RewritingVariableName ->
LogicT Simplifier (Pattern RewritingVariableName)
LogicT
Simplifier
( Substitution.Substitution
RewritingVariableName
, Pattern RewritingVariableName
)
finalizeAppliedRule
sideCondition
renamedRule
Expand All @@ -133,7 +138,7 @@ finalizeAppliedRule
ruleRHS = Rule.rhs renamedRule

catchSimplifiesToBottom srt = \case
[] -> return $ pure $ mkBottom srt
[] -> return (mempty, pure $ mkBottom srt)
xs -> Logic.scatter xs

{- | Combine all the conditions to apply rule and construct the result.
Expand All @@ -153,7 +158,12 @@ constructConfiguration ::
Condition RewritingVariableName ->
-- | Final configuration
Pattern RewritingVariableName ->
LogicT Simplifier (Pattern RewritingVariableName)
LogicT
Simplifier
( Substitution.Substitution
RewritingVariableName
, Pattern RewritingVariableName
)
constructConfiguration
sideCondition
appliedCondition
Expand Down Expand Up @@ -181,7 +191,7 @@ constructConfiguration
-- TODO (thomas.tuegel): Should the final term be simplified after
-- substitution?
debugCreatedSubstitution substitution (termLikeSort finalTerm)
return (finalTerm' `Pattern.withCondition` finalCondition)
return (substitution, finalTerm' `Pattern.withCondition` finalCondition)

finalizeAppliedClaim ::
-- | SideCondition containing metadata
Expand All @@ -190,7 +200,7 @@ finalizeAppliedClaim ::
ClaimPattern ->
-- | Conditions of applied rule
Condition RewritingVariableName ->
LogicT Simplifier (Pattern RewritingVariableName)
LogicT Simplifier (Substitution.Substitution RewritingVariableName, Pattern RewritingVariableName)
finalizeAppliedClaim sideCondition renamedRule appliedCondition =
-- `constructConfiguration` may simplify the configuration to bottom
-- we want to "catch" this and return a #bottom Pattern
Expand All @@ -210,7 +220,7 @@ finalizeAppliedClaim sideCondition renamedRule appliedCondition =
ClaimPattern{right} = renamedRule

catchSimplifiesToBottom srt = \case
[] -> return $ pure $ mkBottom srt
[] -> return (mempty, pure $ mkBottom srt)
xs -> Logic.scatter xs

type UnifyingRuleWithRepresentation representation rule =
Expand All @@ -226,7 +236,7 @@ type UnifyingRuleWithRepresentation representation rule =
type FinalizeApplied rule =
rule ->
Condition RewritingVariableName ->
LogicT Simplifier (Pattern RewritingVariableName)
LogicT Simplifier (Substitution.Substitution RewritingVariableName, Pattern RewritingVariableName)

finalizeRule ::
UnifyingRuleWithRepresentation representation rule =>
Expand Down Expand Up @@ -256,9 +266,9 @@ finalizeRule
unificationCondition
checkSubstitutionCoverage initial (toRule <$> unifiedRule)
let renamedRule = Conditional.term unifiedRule
final <- finalizeApplied renamedRule applied
(subst, final) <- finalizeApplied renamedRule applied
let result = resetResultPattern initialVariables final
return Step.Result{appliedRule = unifiedRule, result}
return Step.Result{appliedRule = unifiedRule{substitution = subst}, result}

-- | Finalizes a list of applied rules into 'Results'.
type Finalizer rule =
Expand Down
2 changes: 1 addition & 1 deletion kore/src/Kore/Rewrite/RewritingVariable.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ Copyright : (c) Runtime Verification, 2020-2021
License : BSD-3-Clause
-}
module Kore.Rewrite.RewritingVariable (
RewritingVariableName,
RewritingVariableName (..),
RewritingVariable,
isEquationVariable,
isConfigVariable,
Expand Down
2 changes: 1 addition & 1 deletion test/rpc-server/execute/branching-prune-unsat-remainder/response.golden
View file
Open in desktop

Large diffs are not rendered by default.

12 changes: 6 additions & 6 deletions test/rpc-server/execute/branching/definition.kore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -715,23 +715,23 @@ module TEST
\top{SortK{}}())))
[UNIQUE'Unds'ID{}("651bff3fa53d464ac7dd7aa77e1ef6071e14c959eb6df97baa325e2ad300daaa"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2305,8,2305,67)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/nix/store/j993pnk64sgpw2qm7408ixnagfkknjzd-k-6.0.181-af105e4141030abe25055854fc02205be4ed223c-maven/include/kframework/builtin/domains.md)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody \"requires\" Bool [klabel(#ruleRequires), symbol]")]

// rule `<generatedTop>`(`<T>`(`<k>`(inj{State,KItem}(#token("a","State"))~>_DotVar2),`<val>`(V) #as _Gen5),_DotVar0)=>`<generatedTop>`(`<T>`(`<k>`(inj{State,KItem}(#token("b","State"))~>_DotVar2),_Gen5),_DotVar0) requires `_==Int_`(V,#token("0","Int")) ensures #token("true","Bool") [UNIQUE_ID(79cf50846fb75eb486ff134a1a00f1546aee170ae548228b79d8898c12c93d2b), label(TEST.AB), org.kframework.attributes.Location(Location(17,14,17,67)), org.kframework.attributes.Source(Source(/home/sam/git/haskell-backend/test/rpc-server/resources/a-to-f/test.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])]
// rule `<generatedTop>`(`<T>`(`<k>`(inj{State,KItem}(#token("a","State"))~>_DotVar2),`<val>`(X) #as _Gen5),_DotVar0)=>`<generatedTop>`(`<T>`(`<k>`(inj{State,KItem}(#token("b","State"))~>_DotVar2),_Gen5),_DotVar0) requires `_==Int_`(X,#token("0","Int")) ensures #token("true","Bool") [UNIQUE_ID(79cf50846fb75eb486ff134a1a00f1546aee170ae548228b79d8898c12c93d2b), label(TEST.AB), org.kframework.attributes.Location(Location(17,14,17,67)), org.kframework.attributes.Source(Source(/home/sam/git/haskell-backend/test/rpc-server/resources/a-to-f/test.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])]
axiom{} \rewrites{SortGeneratedTopCell{}} (
\and{SortGeneratedTopCell{}} (
Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\dv{SortState{}}("a")),Var'Unds'DotVar2:SortK{})),\and{SortValCell{}}(Lbl'-LT-'val'-GT-'{}(VarV:SortInt{}),Var'Unds'Gen5:SortValCell{})),Var'Unds'DotVar0:SortGeneratedCounterCell{}),
Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\dv{SortState{}}("a")),Var'Unds'DotVar2:SortK{})),\and{SortValCell{}}(Lbl'-LT-'val'-GT-'{}(VarX:SortInt{}),Var'Unds'Gen5:SortValCell{})),Var'Unds'DotVar0:SortGeneratedCounterCell{}),
\equals{SortBool{},SortGeneratedTopCell{}}(
Lbl'UndsEqlsEqls'Int'Unds'{}(VarV:SortInt{},\dv{SortInt{}}("0")),
Lbl'UndsEqlsEqls'Int'Unds'{}(VarX:SortInt{},\dv{SortInt{}}("0")),
\dv{SortBool{}}("true"))),
\and{SortGeneratedTopCell{}} (
Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\dv{SortState{}}("b")),Var'Unds'DotVar2:SortK{})),Var'Unds'Gen5:SortValCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{}), \top{SortGeneratedTopCell{}}()))
[UNIQUE'Unds'ID{}("79cf50846fb75eb486ff134a1a00f1546aee170ae548228b79d8898c12c93d2b"), label{}("TEST.AB"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(17,14,17,67)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/sam/git/haskell-backend/test/rpc-server/resources/a-to-f/test.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}("syntax #RuleContent ::= #RuleBody \"requires\" Bool [klabel(#ruleRequires), symbol]")]

// rule `<generatedTop>`(`<T>`(`<k>`(inj{State,KItem}(#token("a","State"))~>_DotVar2),`<val>`(V) #as _Gen5),_DotVar0)=>`<generatedTop>`(`<T>`(`<k>`(inj{State,KItem}(#token("c","State"))~>_DotVar2),_Gen5),_DotVar0) requires `notBool_`(`_==Int_`(V,#token("0","Int"))) ensures #token("true","Bool") [UNIQUE_ID(6974170fb1496dc2cae5b77afce0c12386d66ce73a4b2344c6512681ba06c70d), label(TEST.AC), org.kframework.attributes.Location(Location(18,14,18,77)), org.kframework.attributes.Source(Source(/home/sam/git/haskell-backend/test/rpc-server/resources/a-to-f/test.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])]
// rule `<generatedTop>`(`<T>`(`<k>`(inj{State,KItem}(#token("a","State"))~>_DotVar2),`<val>`(X) #as _Gen5),_DotVar0)=>`<generatedTop>`(`<T>`(`<k>`(inj{State,KItem}(#token("c","State"))~>_DotVar2),_Gen5),_DotVar0) requires `notBool_`(`_==Int_`(X,#token("0","Int"))) ensures #token("true","Bool") [UNIQUE_ID(6974170fb1496dc2cae5b77afce0c12386d66ce73a4b2344c6512681ba06c70d), label(TEST.AC), org.kframework.attributes.Location(Location(18,14,18,77)), org.kframework.attributes.Source(Source(/home/sam/git/haskell-backend/test/rpc-server/resources/a-to-f/test.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])]
axiom{} \rewrites{SortGeneratedTopCell{}} (
\and{SortGeneratedTopCell{}} (
Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\dv{SortState{}}("a")),Var'Unds'DotVar2:SortK{})),\and{SortValCell{}}(Lbl'-LT-'val'-GT-'{}(VarV:SortInt{}),Var'Unds'Gen5:SortValCell{})),Var'Unds'DotVar0:SortGeneratedCounterCell{}),
Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\dv{SortState{}}("a")),Var'Unds'DotVar2:SortK{})),\and{SortValCell{}}(Lbl'-LT-'val'-GT-'{}(VarX:SortInt{}),Var'Unds'Gen5:SortValCell{})),Var'Unds'DotVar0:SortGeneratedCounterCell{}),
\equals{SortBool{},SortGeneratedTopCell{}}(
LblnotBool'Unds'{}(Lbl'UndsEqlsEqls'Int'Unds'{}(VarV:SortInt{},\dv{SortInt{}}("0"))),
LblnotBool'Unds'{}(Lbl'UndsEqlsEqls'Int'Unds'{}(VarX:SortInt{},\dv{SortInt{}}("0"))),
\dv{SortBool{}}("true"))),
\and{SortGeneratedTopCell{}} (
Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortState{}, SortKItem{}}(\dv{SortState{}}("c")),Var'Unds'DotVar2:SortK{})),Var'Unds'Gen5:SortValCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{}), \top{SortGeneratedTopCell{}}()))
Expand Down
Loading
Loading