Code

Recursor refactor#1289

Code

Closed

robdockins wants to merge 31 commits intomasterGaloisInc/saw-script:masterfrom recursor-refactorGaloisInc/saw-script:recursor-refactorCopy head branch name to clipboard

+2,495-742

Commits

Commits on Apr 27, 2021

• Add a new experimental "extract_uninterp" command.

  Show description for e9c8947
  robdockins

  committed
  e9c8947

  Copy full SHA for e9c8947

• Add a new evaluation mode for extracting uninterpeted functions.

  Show description for fabdd02
  robdockins

  committed
  fabdd02

  Copy full SHA for fabdd02

• WIP TermModel

  robdockins

  committed
  772b910

  Copy full SHA for 772b910

• Split VToNat into VBVToNat and VIntToNat

  Show description for 6f8b788
  robdockins

  committed
  6f8b788

  Copy full SHA for 6f8b788

• Remove obsolete arguments from concrete bitvector operations

  robdockins

  committed
  7fb8a52

  Copy full SHA for 7fb8a52

Commits on Apr 28, 2021

• Move some operations from the concrete simulator into Prim

  Show description for 8034ab6
  robdockins

  committed
  8034ab6

  Copy full SHA for 8034ab6

Commits on Apr 29, 2021

• Add a notion of NeutralTerm for when evaluation gets stuck

  Show description for 55f8e5e
  robdockins

  committed
  55f8e5e

  Copy full SHA for 55f8e5e

• Lots more work on the TermModel

  robdockins

  committed
  4092654

  Copy full SHA for 4092654

Commits on Apr 30, 2021

• Add neutral handlers for the AIG, SBV and What4 evaluators

  robdockins

  committed
  00288db

  Copy full SHA for 00288db

• Revert "Remove obsolete arguments from concrete bitvector operations"

  Show description for bfec4ec
  robdockins

  committed
  bfec4ec

  Copy full SHA for bfec4ec

• Improve scAbstractExts and scGeneralizeExts

  Show description for b99d75b
  robdockins

  committed
  b99d75b

  Copy full SHA for b99d75b

• Add simulator value support for term model evaluation.

  Show description for 66baf2b
  robdockins

  committed
  66baf2b

  Copy full SHA for 66baf2b

• More work on the TermModel

  robdockins

  committed
  42b0432

  Copy full SHA for 42b0432

• Add a normalize_term command to experiment with the results

  Show description for b3788ce
  robdockins

  committed
  b3788ce

  Copy full SHA for b3788ce

Commits on May 3, 2021

• Pipe type info through mux operations.

  robdockins

  committed
  615ba23

  Copy full SHA for 615ba23

Commits on May 4, 2021

• Put the RME symbolic simulator in the IO monad.

  robdockins

  committed
  7f93efd

  Copy full SHA for 7f93efd

Commits on May 5, 2021

• Put the concrete saw-core evaluator in the IO monad

  robdockins

  committed
  43b236b

  Copy full SHA for 43b236b

• Add a MonadIO constraint to the MonadLazy class.

  Show description for e98a821
  robdockins

  committed
  e98a821

  Copy full SHA for e98a821

• WIP, rework how iota conversions are implemented

  robdockins

  committed
  821c170

  Copy full SHA for 821c170

Commits on May 7, 2021

• Refactor and comment ctxReduceRecursor

  Show description for 1cd1cdb
  robdockins

  committed
  1cd1cdb

  Copy full SHA for 1cd1cdb

Commits on May 8, 2021

• Rearrange some aspects of how recursors are implemented.

  robdockins

  committed
  f1fc706

  Copy full SHA for f1fc706

Commits on May 10, 2021

• WIP, make recursors into first-class values that can be bound

  Show description for aec0507
  robdockins

  committed
  aec0507

  Copy full SHA for aec0507

Commits on May 11, 2021

• WIP, make recursors into values, part 2

  robdockins

  committed
  f6a7b3c

  Copy full SHA for f6a7b3c

• WIP, make recursors values, part 3

  robdockins

  committed
  105034d

  Copy full SHA for 105034d

• Add more type information to compiled recursor values.

  robdockins

  committed
  abd6f20

  Copy full SHA for abd6f20

Commits on May 12, 2021

• Fix the external format printer/parser for recursor values

  robdockins

  committed
  54df8e5

  Copy full SHA for 54df8e5

• Add type information to the simulator evaluation environment

  robdockins

  committed
  ab3d4ea

  Copy full SHA for ab3d4ea

• Fix a typo in the lg2 primitive

  robdockins

  committed
  dbc78fd

  Copy full SHA for dbc78fd

• Fix the readback of open neutral terms.

  robdockins

  committed
  b401c04

  Copy full SHA for b401c04

• Reimplement extract_uninterp via the new term model.

  robdockins

  committed
  ce634e1

  Copy full SHA for ce634e1

Commits on May 13, 2021

• Fix a case where we were muxing with the wrong type.

  robdockins

  committed
  b87f387

  Copy full SHA for b87f387