Code

Mr solver: sorted insert example#1666

Code

Merged

mergify[bot] merged 7 commits intomasterGaloisInc/saw-script:masterfrom mr-solver/insert-exampleGaloisInc/saw-script:mr-solver/insert-exampleCopy head branch name to clipboardMay 16, 2022

+37-2

Commits

Commits on May 14, 2022

• added eta-expanded versions of the Left and Right constructors to the prelude

  

  Eddy Westbrook

  committed
  1ea0237

  Copy full SHA for 1ea0237

• added support to the monadifier for monadifying the unit type

  

  Eddy Westbrook

  committed
  60b6bf5

  Copy full SHA for 60b6bf5

• fixed the monadification of the Left and Right cryptol primitives so they now use the new eta-expanded left and right functions in the saw-core prelude

  

  Eddy Westbrook

  committed
  cf91641

  Copy full SHA for cf91641

• added MR solver test case for sorted_insert_no_malloc

  

  Eddy Westbrook

  committed
  534ffda

  Copy full SHA for 534ffda

Commits on May 16, 2022

• whoops, fixed a bug in the cryptol spec for sorted_insert_spec

  

  Eddy Westbrook

  committed
  4882819

  Copy full SHA for 4882819

• fixed a bug in sorted_insert_spec: need to use signed instead of unsigned comparison

  

  Eddy Westbrook

  committed
  13a1a86

  Copy full SHA for 13a1a86

• removed the debug output from linked_list_mr_solver.saw

  

  Eddy Westbrook

  committed
  477a051

  Copy full SHA for 477a051