Code

Generalize matching#78

Code

Open

lucaspena wants to merge 33 commits intomasterkframework/matching-logic-prover:masterfrom generalize-matchingkframework/matching-logic-prover:generalize-matchingCopy head branch name to clipboard

+388-54

Commits

Commits on Jun 10, 2020

• matching: match over heap variable

  lucaspena

  committed
  ce98bfa

  Copy full SHA for ce98bfa

• matching: #matchStuck is own sort now, results in stuck configuration if fires

  lucaspena

  committed
  449aa2a

  Copy full SHA for 449aa2a

• matching: remove spurious side condition in matchAssocComm rule causing rule not to fire

  lucaspena

  committed
  0425b75

  Copy full SHA for 0425b75

• kore-lang: getSpatialPatterns and getPredicatePatterns

  lucaspena

  committed
  65a620b

  Copy full SHA for 65a620b

• matching: allow multiple heaps in terms

  lucaspena

  committed
  3922c7a

  Copy full SHA for 3922c7a

• matching with heap variable must be at end of pattern list

  lucaspena

  committed
  b52dad9

  Copy full SHA for b52dad9

• match: rotate heap variable when not at end of pattern list

  lucaspena

  committed
  75911fb

  Copy full SHA for 75911fb

• match: lhs can have multiple seps

  lucaspena

  committed
  9f4b7bb

  Copy full SHA for 9f4b7bb

• matching: match on multiple heaps on RHS

  lucaspena

  committed
  32177c5

  Copy full SHA for 32177c5

• match-assoc-comm: H1 is a token

  lucaspena

  committed
  6557873

  Copy full SHA for 6557873

• matching: remove extraneous side condition

  lucaspena

  committed
  4d2c0a4

  Copy full SHA for 4d2c0a4

• t/unit/match: fix test cases

  lucaspena

  committed
  2c3ab94

  Copy full SHA for 2c3ab94

• match: terms can be and(.Patterns)

  lucaspena

  committed
  cf5ff71

  Copy full SHA for cf5ff71

Commits on Jun 17, 2020

• match-debug

  lucaspena

  committed
  73153f1

  Copy full SHA for 73153f1

• matching: match: Everything matches \top

  lucaspena

  committed
  6c196f3

  Copy full SHA for 6c196f3

• matching: allow set variables

  lucaspena

  committed
  2fb6c9f

  Copy full SHA for 2fb6c9f

• matching: begin matching over context patterns

  lucaspena

  committed
  9dcda07

  Copy full SHA for 9dcda07

• kore-lang: add Context sort

  lucaspena

  committed
  4801d96

  Copy full SHA for 4801d96

• matching: hole not parameterized

  lucaspena

  committed
  0efa47e

  Copy full SHA for 0efa47e

• matching: #match: Fix missing side condition

  lucaspena

  committed
  20ad367

  Copy full SHA for 20ad367

• kore-lang: add syntax for mu

  lucaspena

  committed
  ef208fa

  Copy full SHA for ef208fa

• matching: recurse over and/or/mu (incorrect for and/or)

  lucaspena

  committed
  9e6d79c

  Copy full SHA for 9e6d79c

• match-assoc-comm: mu test

  lucaspena

  committed
  119ad56

  Copy full SHA for 119ad56

• matching: owise case instead of requiring spatial pattern for more general matching

  lucaspena

  committed
  7e3860b

  Copy full SHA for 7e3860b

• match: recurse over exists

  lucaspena

  committed
  582f306

  Copy full SHA for 582f306

• unit/match-assoc-comm: change test name

  lucaspena

  committed
  4a7605a

  Copy full SHA for 4a7605a

• unit/match-assoc-comm: add test 13

  lucaspena

  committed
  d1b0359

  Copy full SHA for d1b0359

• matching: fix preprocessing

  lucaspena

  committed
  bcf3e05

  Copy full SHA for bcf3e05

• kore-lang: add syntax for nu

  lucaspena

  committed
  5aa40f7

  Copy full SHA for 5aa40f7

• matching: both term and pattern are nu

  lucaspena

  committed
  3795bd8

  Copy full SHA for 3795bd8

• matching: #matchAssoc: Syntactically match on \not

  lucaspena

  committed
  618dedc

  Copy full SHA for 618dedc

• matching: #matchAssoc: Patterns may use set variables too

  lucaspena

  committed
  9d1f267

  Copy full SHA for 9d1f267

• match: fix test cases

  lucaspena

  committed
  e2385f2

  Copy full SHA for e2385f2