diff --git a/prover/lang/kore-lang.md b/prover/lang/kore-lang.md
index 851a24f7f..bd345020a 100644
--- a/prover/lang/kore-lang.md
+++ b/prover/lang/kore-lang.md
@@ -324,6 +324,8 @@ module KORE-HELPERS
rule getReturnSort(\and(.Patterns)) => TopSort
rule getReturnSort(_:SetVariable) => TopSort
+ rule getReturnSort(\exists{Vs} P) => getReturnSort(P)
+
syntax Sort ::= "TopSort" [token]
| "BottomSort" [token]
@@ -397,6 +399,7 @@ module KORE-HELPERS
rule getFreeVariables(N:Int, .Patterns) => .Patterns
rule getFreeVariables(X:Variable, .Patterns) => X, .Patterns
+ rule getFreeVariables(X:SetVariable, .Patterns) => X, .Patterns
rule getFreeVariables(S:Symbol, .Patterns) => .Patterns
rule getFreeVariables(S:Symbol(ARGS) , .Patterns) => getFreeVariables(ARGS)
@@ -415,12 +418,20 @@ module KORE-HELPERS
=> getFreeVariables(P, .Patterns) -Patterns Vs
rule getFreeVariables(\forall { Vs } P, .Patterns)
=> getFreeVariables(P, .Patterns) -Patterns Vs
+ rule getFreeVariables(\mu X . P, .Patterns)
+ => getFreeVariables(P, .Patterns) -Patterns (X, .Patterns)
+
rule getFreeVariables(implicationContext(CONTEXT, P), .Patterns)
=> (getFreeVariables(CONTEXT, .Patterns) ++Patterns getFreeVariables(P, .Patterns))
- -Patterns #hole { Heap }, #hole { Bool }
+ -Patterns #hole { Heap }, #hole { Bool }, #hole { TopSort }
rule getFreeVariables(\typeof(P, _))
=> getFreeVariables(P)
+ syntax Patterns ::= filterSetVariables(Patterns) [function]
+ rule filterSetVariables(.Patterns) => .Patterns
+ rule filterSetVariables(V:Variable, Vs) => V, filterSetVariables(Vs)
+ rule filterSetVariables(X:SetVariable, Vs) => filterSetVariables(Vs)
+
// TODO: These seem specific to implication. Perhaps they need better names?
syntax Patterns ::= getUniversalVariables(Pattern) [function]
rule getUniversalVariables(GOAL) => getFreeVariables(GOAL, .Patterns)
@@ -605,6 +616,7 @@ Alpha renaming: Rename all bound variables. Free variables are left unchanged.
=> #fun(RENAMING => \forall { Fs[RENAMING] } alphaRename(substMap(P,RENAMING))) ( makeFreshSubstitution(Fs) )
rule alphaRename(\exists { Fs:Patterns } P:Pattern)
=> #fun(RENAMING => \exists { Fs[RENAMING] } alphaRename(substMap(P,RENAMING))) ( makeFreshSubstitution(Fs) )
+ rule alphaRename(\mu X . P:Pattern) => \mu !X . alphaRename(subst(P, X, !X))
rule alphaRename(\equals(L, R)) => \equals(alphaRename(L), alphaRename(R))
rule alphaRename(\not(Ps)) => \not(alphaRename(Ps))
rule alphaRename(\functionalPattern(Ps)) => \functionalPattern(alphaRename(Ps))
@@ -614,6 +626,7 @@ Alpha renaming: Rename all bound variables. Free variables are left unchanged.
rule alphaRename(S:Symbol(ARGs)) => S(alphaRenamePs(ARGs))
rule alphaRename(S:Symbol) => S
rule alphaRename(V:Variable) => V
+ rule alphaRename(X:SetVariable) => X
rule alphaRename(I:Int) => I
rule alphaRename(implicationContext(P, Qs))
=> implicationContext(alphaRename(P), alphaRename(Qs))
@@ -754,16 +767,18 @@ Simplifications
rule isPredicatePattern(#hole { Bool }) => true
rule isPredicatePattern(#hole { Heap }) => false
rule isPredicatePattern(V:VariableName { Heap }) => false
+ rule isPredicatePattern(V:SetVariable) => false
// TODO: This should use an axiom, similar to `functional` instead: `axiom predicate(P)`
rule isPredicatePattern(S:Symbol(ARGS)) => true
- requires getReturnSort(S(ARGS)) ==K Bool
+ requires getReturnSort(S(ARGS)) =/=K Heap
rule isPredicatePattern(S:Symbol(ARGS)) => false
requires getReturnSort(S(ARGS)) ==K Heap
rule isPredicatePattern(emp(.Patterns)) => false
rule isPredicatePattern(\exists{Vs} P) => isPredicatePattern(P)
rule isPredicatePattern(\forall{Vs} P) => isPredicatePattern(P)
+ rule isPredicatePattern(\mu X . P) => false
rule isPredicatePattern(implicationContext(\and(sep(_),_),_)) => false
rule isPredicatePattern(\typeof(_,_)) => true
rule isPredicatePattern(implicationContext(_,_)) => true
@@ -783,6 +798,8 @@ Simplifications
rule isSpatialPattern(#hole { Bool }) => false
rule isSpatialPattern(#hole { Heap }) => true
rule isSpatialPattern(V:VariableName { Heap }) => true
+ rule isSpatialPattern(V:SetVariable) => false
+ rule isSpatialPattern(\mu X . P) => false
// TODO: Perhaps normalization should get rid of this?
rule isSpatialPattern(\exists{_} implicationContext(\and(sep(_),_),_)) => true
@@ -825,6 +842,7 @@ Simplifications
syntax Bool ::= hasImplicationContext(Pattern) [function]
syntax Bool ::= hasImplicationContextPs(Patterns) [function]
rule hasImplicationContext(X:Variable) => false
+ rule hasImplicationContext(X:SetVariable) => false
rule hasImplicationContext(X:Int) => false
rule hasImplicationContext(S:Symbol) => false
rule hasImplicationContext(\implies(LHS, RHS))
diff --git a/prover/prover.md b/prover/prover.md
index 4ff55c132..d842a0837 100644
--- a/prover/prover.md
+++ b/prover/prover.md
@@ -60,7 +60,7 @@ module STRATEGIES-EXPORTED-SYNTAX
| "kt-solve-implications" "(" Strategy ")"
| "instantiate-universals-with-ground-terms"
| "instantiate-separation-logic-axioms" | "pto-is-injective"
- | "spatial-patterns-equal"
+ | "spatial-patterns-equal" | "patterns-equal"
| "spatial-patterns-match"
| "match" | "match-debug" | "match-pto"
| "frame"
diff --git a/prover/strategies/core.md b/prover/strategies/core.md
index 81c1a88f2..14756dac7 100644
--- a/prover/strategies/core.md
+++ b/prover/strategies/core.md
@@ -26,6 +26,7 @@ module PROVER-CORE-SYNTAX
| Strategy "&" Strategy [right, format(%1%n%2 %3)]
| Strategy "|" Strategy [right, format(%1%n%2 %3)]
syntax Strategy ::= "or-split" | "and-split" | "or-split-rhs" | "and-split-rhs"
+ syntax Strategy ::= "rhs-top"
syntax Strategy ::= "prune" "(" Patterns ")"
syntax Strategy ::= Strategy "{" Int "}"
@@ -286,6 +287,13 @@ Internal strategy used to implement `or-split` and `and-split`.
rule #andSplitImplication(P1, Vs, (P2, Ps)) => replace-goal(\implies(P1, \exists{Vs} \and(P2, .Patterns))) & #andSplitImplication(P1, Vs, Ps) [owise]
```
+`rhs-top` evaluates to success if the right hand side is top
+
+```k
+ rule \implies(LHS, \exists{.Patterns} \and(.Patterns))
+ rhs-top => success ...
+```
+
If-then-else-fi strategy is useful for implementing other strategies:
```k
diff --git a/prover/strategies/knaster-tarski.md b/prover/strategies/knaster-tarski.md
index a63a32ca3..54908449d 100644
--- a/prover/strategies/knaster-tarski.md
+++ b/prover/strategies/knaster-tarski.md
@@ -82,7 +82,7 @@ for guessing an instantiation of the inductive hypothesis.
=> ( kt-wrap(LRP) . kt-forall-intro
. kt-unfold . remove-lhs-existential
. kt-unwrap
- . simplify . normalize . or-split-rhs. lift-constraints
+ . simplify . normalize . or-split-rhs . lift-constraints
. ( with-each-implication-context( simplify . normalize . or-split-rhs. lift-constraints
. remove-lhs-existential
. normalize-implication-context
@@ -174,7 +174,9 @@ for guessing an instantiation of the inductive hypothesis.
syntax Strategy ::= "kt-forall-intro"
rule \implies(LHS, RHS) #as GOAL
=> \implies( LHS
- , \forall { getUniversalVariables(GOAL) -Patterns getFreeVariables(LHS, .Patterns) }
+ , \forall { filterSetVariables(getUniversalVariables(GOAL))
+ -Patterns getFreeVariables(LHS, .Patterns)
+ }
RHS
)
@@ -192,13 +194,28 @@ for guessing an instantiation of the inductive hypothesis.
requires getFreeVariables(LHS) -Patterns Vs ==K getFreeVariables(LHS)
```
+## `kt-unfold`
+
+### `kt-unfold` for `\mu`
+
+```k
+ // TODO: combine with other kt-unfold rules
+ rule \implies(\mu X . P, RHS)
+ => \implies(subst(P, X, alphaRename(RHS)), RHS)
+
+ kt-unfold
+ => lift-or . and-split
+ ...
+
+```
-// unfold+lfp
+### `kt-unfold` for `\iff-lfp`
```k
syntax Strategy ::= "kt-unfold" | "kt-unfold" "(" Pattern ")"
- rule \implies(LHS, RHS)
+ rule \implies(LRP:Symbol(ARGS) #as LHS, RHS)
kt-unfold => kt-unfold(unfold(LHS)) ...
+ requires isUnfoldable(LRP)
rule \implies(LRP(ARGS) #as LHS, RHS)
=> \implies(UNFOLDED_LHS, RHS)
@@ -342,8 +359,8 @@ Move #holes to the front
, _), _)
normalize-implication-context ...
- requires P =/=K #hole { Bool }
- andBool #hole { Bool } in Ps
+ requires (P =/=K #hole { Bool } orBool P =/=K #hole { TopSort })
+ andBool (#hole { Bool } in Ps orBool #hole { TopSort } in Ps)
rule \implies(\and(sep(\forall { _ }
implicationContext( \and(P, Ps)
@@ -367,7 +384,7 @@ Move #holes to the front
```
```k
- rule \implies(\and( \forall { UNIVs } implicationContext( \and(#hole { Bool }, _) , _ ) , _ ) , _ )
+ rule \implies(\and( \forall { UNIVs } implicationContext( \and(#hole { SORT }, _) , _ ) , _ ) , _ )
normalize-implication-context => noop ...
rule \implies(\and( sep(\forall { UNIVs } implicationContext( \and(sep(#hole { Heap }, _), _) , _ ) , _ ), _ ), _ )
normalize-implication-context => noop ...
diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md
index 8b51fcd48..d774fe096 100644
--- a/prover/strategies/matching.md
+++ b/prover/strategies/matching.md
@@ -56,7 +56,6 @@ module MATCHING-FUNCTIONAL
, rest: .Patterns
)
)
- requires isSpatialPattern(sep(T))
syntax MatchResults ::= #filterErrors(MatchResults) [function]
rule #filterErrors(MR:Error , MRs) => #filterErrors(MRs)
@@ -144,7 +143,15 @@ Recurse over assoc-only constructors (including `pto`):
// ground variable: identical
rule #matchAssoc( terms: P:Variable, Ts => Ts
- , pattern: P:Variable, Ps => Ps
+ , pattern: P, Ps => Ps
+ , variables: Vs
+ , subst: _
+ , rest: REST
+ )
+ requires notBool P in Vs
+
+ rule #matchAssoc( terms: P:SetVariable, Ts => Ts
+ , pattern: P, Ps => Ps
, variables: Vs
, subst: _
, rest: REST
@@ -161,7 +168,18 @@ Recurse over assoc-only constructors (including `pto`):
=> #error( "No valid substitution" ), .MatchResults
requires T =/=K P
andBool notBool P in Vs
-
+
+ // ground variable: non-identical
+ rule #matchAssoc( terms: T, Ts
+ , pattern: P:SetVariable, Ps
+ , variables: Vs
+ , subst: _
+ , rest: REST
+ )
+ => #error( "No valid substitution" ), .MatchResults
+ requires T =/=K P
+ andBool notBool P in Vs
+
// free variable: different sorts
rule #matchAssoc( terms: T , Ts
, pattern: P:Variable, Ps
@@ -658,6 +676,42 @@ Instantiate the axiom: `\forall { L, D } (pto L D) -> L != nil
requires S1 =/=K S2 orBool notBool isConstructor(S1)
```
+If the RHS is empty, we have nothing to do
+
+```k
+ rule \implies(LHS, \exists { Vs } \and(.Patterns))
+ patterns-equal => noop ...
+```
+
+Remove any patterns on the RHS that match a pattern on the LHS:
+
+```k
+ rule \implies(\and(LHS), \exists{Vs} \and(RHS, REST))
+ patterns-equal
+ => with-each-match( #match( terms: LHS
+ , pattern: RHS
+ , variables: .Patterns
+ )
+ , patterns-equal
+ )
+ ...
+
+ rule \implies(LHS, \exists{ Vs } \and(RHS, REST))
+ => \implies(LHS, \exists{ Vs } \and(REST))
+
+ #matchResult(subst: .Map , rest: .Patterns)
+ ~> patterns-equal
+ => patterns-equal
+ ...
+
+
+ rule #matchResult(subst: .Map , rest: P, Ps)
+ ~> patterns-equal
+ => fail
+ ...
+
+```
+
If the RHS has no spatial part, then there is nothing to do:
```k
diff --git a/prover/strategies/simplification.md b/prover/strategies/simplification.md
index f2a9ed5c0..ea4d4116c 100644
--- a/prover/strategies/simplification.md
+++ b/prover/strategies/simplification.md
@@ -348,6 +348,8 @@ Bring predicate constraints to the top of a term.
requires isPredicatePattern(P)
rule #liftConstraintsPs(P, REST) => sep(P), #liftConstraintsPs(REST)
requires isSpatialPattern(P)
+ rule #liftConstraintsPs(V:SetVariable, REST) => V, #liftConstraintsPs(REST)
+ rule #liftConstraintsPs(\mu X . P, REST) => \mu X . P, #liftConstraintsPs(REST)
rule #liftConstraintsPs(\and(Ps), REST) => #liftConstraintsPs(Ps ++Patterns REST)
requires notBool isPredicatePattern(\and(Ps))
// note the rule below assumes we hever have a pure predicate pattern inside a sep
diff --git a/prover/strategies/unfolding.md b/prover/strategies/unfolding.md
index a25656077..c05a00558 100644
--- a/prover/strategies/unfolding.md
+++ b/prover/strategies/unfolding.md
@@ -12,6 +12,7 @@ module STRATEGY-UNFOLDING
rule [[ unfold(S:Symbol(ARGs)) => {("ifflfp axiom has free variables!" ~> S ~> (getFreeVariables(DEF) -Patterns Vs))}:>Pattern ]]
axiom _: \forall { Vs } \iff-lfp(S(Vs), DEF)
requires getFreeVariables(DEF) -Patterns Vs =/=K .Patterns
+ rule unfold(\mu X . P) => subst(P, X, alphaRename(\mu X . P))
syntax SymbolDeclaration ::= getSymbolDeclaration(Symbol) [function]
rule [[ getSymbolDeclaration(S) => DECL ]]
@@ -30,6 +31,8 @@ module STRATEGY-UNFOLDING
=> R(ARGS), (getUnfoldables(ARGS)
++Patterns getUnfoldables(REST))
requires isUnfoldable(R)
+ rule getUnfoldables(\mu X . P, REST)
+ => \mu X . P, getUnfoldables(REST)
rule getUnfoldables(S:Symbol, REST)
=> getUnfoldables(REST)
requires notBool isUnfoldable(S)
diff --git a/prover/t/ltl/until-implies-eventually.kore b/prover/t/ltl/until-implies-eventually.kore
index 6f1587545..9dd34b605 100644
--- a/prover/t/ltl/until-implies-eventually.kore
+++ b/prover/t/ltl/until-implies-eventually.kore
@@ -7,8 +7,8 @@ axiom inf: next(\top())
axiom lin: \implies(next(#X), \not(next(\not(#X))))
// phi1 U phi2 => []phi2
-claim \implies( \mu #X . \or(#PHI2, \and(#PHI1, next(#X)))
- , \mu #X . \or(#PHI2, next(#X))
+claim \implies( \mu #X . \or(\exists { } \and(#PHI2), \exists { } \and(#PHI1, next(#X)))
+ , \mu #X . \or(\exists { } \and(#PHI2), \exists { } \and(next(#X)))
)
/*
@@ -37,4 +37,4 @@ right-unfold-Nth(0, 1)
phi-implies-phi
*/
-strategy normalize . kt
+strategy normalize . kt . right-unfold-Nth(0, 0) . normalize . patterns-equal . rhs-top