Code

Add basic prove_refinement tactic#1849

Code

Merged

m-yac merged 16 commits intomasterGaloisInc/saw-script:masterfrom mrs-solverGaloisInc/saw-script:mrs-solverCopy head branch name to clipboardApr 18, 2023

+340-114

Commits

Commits on Mar 2, 2023

• Start of something cool

  

  Brett Boston

  committed
  446dffc

  Copy full SHA for 446dffc

Commits on Mar 3, 2023

• add refinesS_eq, fix errors in Prelude.sawcore

  m-yac

  committed
  ced11d7

  Copy full SHA for ced11d7

Commits on Mar 8, 2023

• Move proveRefinement to builtins

  

  Brett Boston

  committed
  55dfa7b

  Copy full SHA for 55dfa7b

• refactor to eliminate env and timeout params

  

  Brett Boston

  committed
  4a6cffc

  Copy full SHA for 4a6cffc

• Wire up prove_refinement in the interpreter

  

  Brett Boston

  committed
  44f23eb

  Copy full SHA for 44f23eb

• Merge remote-tracking branch 'origin/master' into mrs-solver

  

  Brett Boston

  committed
  79004cf

  Copy full SHA for 79004cf

Commits on Mar 12, 2023

• Debug info

  

  Brett Boston

  committed
  d978cca

  Copy full SHA for d978cca

Commits on Mar 14, 2023

• Start of refinesS_fun

  

  Brett Boston

  committed
  658bacb

  Copy full SHA for 658bacb

Commits on Mar 28, 2023

• add args to askMRSolver, get first prove_refinemen tactic example working

  m-yac

  committed
  20210d5

  Copy full SHA for 20210d5

• add prove_refinement tactic tests in mr_solver_unit_tests.saw

  m-yac

  committed
  1830a2c

  Copy full SHA for 1830a2c

• add docs, remove unused EqDep

  m-yac

  committed
  368ace7

  Copy full SHA for 368ace7

Commits on Mar 29, 2023

• move test_funs out of Prelude, add doc to MrSolverEvidence, some reverts

  m-yac

  committed
  6d81c44

  Copy full SHA for 6d81c44

Commits on Mar 30, 2023

• rename prove_refinement tactic to mrsolver

  m-yac

  committed
  c0f364c

  Copy full SHA for c0f364c

• add docs to FunStackE-related defs in Prelude.sawcore

  m-yac

  committed
  e99d03d

  Copy full SHA for e99d03d

Commits on Apr 10, 2023

• get List1#rec to translate to list_rect in Coq

  m-yac

  committed
  b25fb57

  Copy full SHA for b25fb57

Commits on Apr 13, 2023

• Merge remote-tracking branch 'origin/master' into mrs-solver

  m-yac

  committed
  2403b1d

  Copy full SHA for 2403b1d