From 302b8488cb3d5de1a0053911ba5d47796a619ddc Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Tue, 7 Jan 2020 16:07:12 +0100 Subject: [PATCH 1/2] add missing rules --- prover/lang/kore-lang.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/prover/lang/kore-lang.md b/prover/lang/kore-lang.md index 374e8fb0d..b3a6df3a4 100644 --- a/prover/lang/kore-lang.md +++ b/prover/lang/kore-lang.md @@ -246,6 +246,7 @@ module KORE-HELPERS syntax Sort ::= getReturnSort(Pattern) [function] rule getReturnSort( I:Int ) => Int rule getReturnSort( _ { S } ) => S + rule getReturnSort( plus ( ARGS ) ) => Int rule getReturnSort( minus ( ARGS ) ) => Int rule getReturnSort( select ( ARGS ) ) => Int rule getReturnSort( union ( ARGS ) ) => SetInt @@ -285,6 +286,10 @@ module KORE-HELPERS => .Patterns rule getGroundTerms(\and(P, Ps), VARs) => getGroundTerms(P, VARs) ++Patterns getGroundTerms(\and(Ps), VARs) + rule getGroundTerms(\or(.Patterns), VARs) + => .Patterns + rule getGroundTerms(\or(P, Ps), VARs) + => getGroundTerms(P, VARs) ++Patterns getGroundTerms(\or(Ps), VARs) rule getGroundTerms(\not(P), VARs) => getGroundTerms(P, VARs) rule getGroundTerms(S:Symbol(ARGS:Patterns) #as APPLY, VARs) @@ -483,6 +488,7 @@ Alpha renaming: Rename all bound variables. Free variables are left unchanged. rule alphaRename(\not(Ps)) => \not(alphaRename(Ps)) rule alphaRename(\and(Ps)) => \and(alphaRenamePs(Ps)) rule alphaRename(\or(Ps)) => \or(alphaRenamePs(Ps)) + rule alphaRename(\implies(L,R)) => \implies(alphaRename(L), alphaRename(R)) rule alphaRename(S:Symbol(ARGs)) => S(alphaRenamePs(ARGs)) rule alphaRename(S:Symbol) => S rule alphaRename(V:Variable) => V From 4eed6226768a47ffd0629977681e151b0353060d Mon Sep 17 00:00:00 2001 From: Jan Tusil Date: Wed, 22 Jan 2020 15:55:46 +0100 Subject: [PATCH 2/2] getUnfoldables should look into symbol arguments --- prover/strategies/unfolding.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/prover/strategies/unfolding.md b/prover/strategies/unfolding.md index 543a12faa..4e4a027e7 100644 --- a/prover/strategies/unfolding.md +++ b/prover/strategies/unfolding.md @@ -27,13 +27,14 @@ module STRATEGY-UNFOLDING syntax Patterns ::= getUnfoldables(Patterns) [function] rule getUnfoldables(.Patterns) => .Patterns rule getUnfoldables(R(ARGS), REST) - => R(ARGS), getUnfoldables(REST) + => R(ARGS), (getUnfoldables(ARGS) + ++Patterns getUnfoldables(REST)) requires isUnfoldable(R) rule getUnfoldables(S:Symbol, REST) => getUnfoldables(REST) requires notBool isUnfoldable(S) rule getUnfoldables(S:Symbol(ARGS), REST) - => getUnfoldables(REST) + => getUnfoldables(ARGS) ++Patterns getUnfoldables(REST) requires notBool isUnfoldable(S) andBool S =/=K sep rule getUnfoldables(I:Int, REST)