From 98e7f3b9f016ed2785d8d59c34b218fe3fc7ee75 Mon Sep 17 00:00:00 2001 From: Lucas Pena Date: Wed, 22 Apr 2020 18:45:05 -0500 Subject: [PATCH] spatial-patterns-match: works with multiple seps anywhere on lhs --- prover/strategies/matching.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/prover/strategies/matching.md b/prover/strategies/matching.md index d920597b3..c8caa5f58 100644 --- a/prover/strategies/matching.md +++ b/prover/strategies/matching.md @@ -702,10 +702,11 @@ Instantiate the axiom: `\forall { L, D } (pto L D) -> L != nil // // requires RSPATIAL -Patterns REST ==K .Patterns - rule \implies(LHS, RHS) + rule \implies(\and(LHS), RHS) + => \implies(\and(LHS -Patterns getSpatialPatterns(LHS)), RHS) + spatial-patterns-match => noop ... - requires isPredicatePattern(LHS) - andBool isPredicatePattern(RHS) + requires isPredicatePattern(RHS) ``` ### Footprint Analysis