Code

4012 evaluate pattern pruning#4020

Code

Open

geo2a wants to merge 14 commits intomasterruntimeverification/haskell-backend:masterfrom 4012-evaluate-pattern-pruningruntimeverification/haskell-backend:4012-evaluate-pattern-pruningCopy head branch name to clipboard

+74,873-12,076

Commits

Commits on Aug 21, 2024

• Derive Show for SMT result types

  geo2a

  committed
  a313ce8

  Copy full SHA for a313ce8

• Check consistency of the pattern's constraints before evaluating it

  geo2a

  committed
  0c0e203

  Copy full SHA for 0c0e203

• Check pattern consistency before starting rewriting in "execute"

  geo2a

  committed
  5999a66

  Copy full SHA for 5999a66

• Fix frontend warning in collectiontest.k

  geo2a

  committed
  2f75bc2

  Copy full SHA for 2f75bc2

• Invert --no-fallback-simplify and --no-post-exec-simplify (new default: no simplification)

  Show description for 0de9517
  

  jberthold

  authored and

  geo2a

  committed
  0de9517

  Copy full SHA for 0de9517

• Update integration tests

  Show description for 41e93b1
  geo2a

  committed
  41e93b1

  Copy full SHA for 41e93b1

• Correct typos and test description

  geo2a

  committed
  2359ddc

  Copy full SHA for 2359ddc

• Make Z3 call optional in evaluatePattern

  geo2a

  committed
  998eb07

  Copy full SHA for 998eb07

• Fix unit tests

  geo2a

  committed
  598a00c

  Copy full SHA for 598a00c

• Don't check initial constraints when "assume-state-defined"

  geo2a

  committed
  9c07a05

  Copy full SHA for 9c07a05

• Rename "assume-state-define" to "assume-defined"

  geo2a

  committed
  39e6abc

  Copy full SHA for 39e6abc

• Return vacuous on undefined concrete terms

  geo2a

  committed
  df4cfae

  Copy full SHA for df4cfae

• Rename parameter in integration tests

  geo2a

  committed
  e155e58

  Copy full SHA for e155e58

• Reorganize tests

  geo2a

  committed
  586589f

  Copy full SHA for 586589f