Code

Term utilities#1698

Code

Merged

robdockins merged 6 commits intomasterGaloisInc/saw-script:masterfrom rwd/congruenceGaloisInc/saw-script:rwd/congruenceCopy head branch name to clipboardJul 26, 2022

+203-11

Commits

Commits on Jul 25, 2022

• Add a utility operation, congruence_for, that takes a term

  Show description for 9f7b31b
  robdockins

  committed
  9f7b31b

  Copy full SHA for 9f7b31b

• Add some additional ways to construct terms; in particular,

  Show description for 15f48fd
  robdockins

  committed
  15f48fd

  Copy full SHA for 15f48fd

• Add an axiom stating the unrolling behavior of fix.

  Show description for 3582846
  robdockins

  committed
  3582846

  Copy full SHA for 3582846

• Respond to review comments

  robdockins

  committed
  8e6eb32

  Copy full SHA for 8e6eb32

• Add a test for the "congruence_for" primitive

  robdockins

  committed
  4e1c921

  Copy full SHA for 4e1c921

• Skip translating the new "fix_unfold" axiom to Coq.

  robdockins

  committed
  e2fd6d4

  Copy full SHA for e2fd6d4