Code

Rewriting SAW core vector folds#1811

Code

Merged

eddywestbrook merged 5 commits intomasterGaloisInc/saw-script:masterfrom saw-core/vector-fold-axiomsGaloisInc/saw-script:saw-core/vector-fold-axiomsCopy head branch name to clipboardFeb 7, 2023

+152-5

Commits

Commits on Jan 27, 2023

• added axioms about one-step unfoldings of foldl and foldr; fixed the rewriter to be able to rewrite with these axioms by allowing patterns of the form Succ x to match nat literals

  

  Eddy Westbrook

  committed
  5a8f2fd

  Copy full SHA for 5a8f2fd

Commits on Feb 3, 2023

• added axioms head_gen and tail_gen to define head and tail of a gen

  

  Eddy Westbrook

  committed
  d617daf

  Copy full SHA for d617daf

• added integration test to test the new foldl rewrite rules

  

  Eddy Westbrook

  committed
  edc0dd5

  Copy full SHA for edc0dd5

• added comments to explain some of how the rewriter works

  

  Eddy Westbrook

  committed
  0e10161

  Copy full SHA for 0e10161

• Merge branch 'master' into saw-core/vector-fold-axioms

  

  Eddy Westbrook

  authored
  8f7d9c0

  Copy full SHA for 8f7d9c0