Code

Mr Solver precondition hints#1605

Code

Merged

mergify[bot] merged 16 commits intomasterGaloisInc/saw-script:masterfrom mr-solver/preconditionsGaloisInc/saw-script:mr-solver/preconditionsCopy head branch name to clipboardMar 9, 2022

+447-155

Commits

Commits on Mar 4, 2022

• added preconditions to Mr Solver

  

  Eddy Westbrook

  committed
  3a9fb91

Commits on Mar 5, 2022

• changed how preconditions work so that they are given with a precondHint in the spec rather than with a separate mr_solver_set_precond command

  

  Eddy Westbrook

  committed
  5352afb

Commits on Mar 7, 2022

• added logic to normalize precondHint terms

  

  Eddy Westbrook

  committed
  670f641

• fixed a bug in smallestBitSetElem

  

  Eddy Westbrook

  committed
  4fab1e8

• fixed a subtle free variable bug in mrTrySetAppliedEVar; also changed mrSetEVarClosed to have a more understandable error message

  

  Eddy Westbrook

  committed
  4c8f7a1

• added some printing helper functions

  

  Eddy Westbrook

  committed
  fe62c84

• removed the type equality check in mrProveEq

  

  Eddy Westbrook

  committed
  3962bdc

• added Mr Solver proof that contains0 |= noErrorsContains0

  

  Eddy Westbrook

  committed
  eccfdeb

• removed mr_solver_set_precond; removed preconditions from MR Solver environments; changed mr_solver command to remember refinements that have been proved

  

  Eddy Westbrook

  committed
  02aed40

Commits on Mar 8, 2022

• added initialization of rwMRSolverEnv field to saw-remote-api

  

  Eddy Westbrook

  committed
  7ee43cf

• whoops, need to avoid calling maximum on an empty list

  

  Eddy Westbrook

  committed
  ee4b67b

• updated efq1 to call Eq__rec instead of the Eq#rec recursor

  

  Eddy Westbrook

  committed
  a301dc6

• changed multiFixM to be primitive, because the translator was not working correctly on some of its helper functions...

  

  Eddy Westbrook

  committed
  34518a6

• Merge branch 'master' into mr-solver/preconditions

  

  Eddy Westbrook

  authored
  b21c705

• remove old comments

  m-yac

  committed
  3929005

• add orM and add more mapsToExpls to SpecialTreatment.hs

  m-yac

  committed
  f182756