Code

matching over heap variables#74

Code

Merged

lucaspena merged 12 commits intomasterkframework/matching-logic-prover:masterfrom match-heap-varkframework/matching-logic-prover:match-heap-varCopy head branch name to clipboardJun 17, 2020

+201-39

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