MR Solver SMT fixes for testing on Heapster models by eddywestbrook · Pull Request #1594 · GaloisInc/saw-script

Commits on Feb 12, 2022

added parse_core_mod command; made ensureMonadicTerm a bit smarter by making it normalize the input type before deciding if it is already computational
Eddy Westbrook
committed
fixed mrFunOutType, isCompFunType, and askMRSolver to normalize types
Eddy Westbrook
committed

Commits on Feb 14, 2022

expanded the notion of a "function name" for MR Solver to include not just globals but also (tuple and record) projections of globals
Eddy Westbrook
committed
added support for recognizing multiFixM computations to normComp
Eddy Westbrook
committed

Commits on Feb 15, 2022

Commits on Feb 17, 2022

Merge branch 'master' into mr-solver/heapster-tests
Eddy Westbrook
committed

Commits on Feb 18, 2022

added applyGlobalOpenTerm and vectorTypeOpenTerm combinators
Eddy Westbrook
committed
trying a new approach to getting SMT solving to work, by substiting uninterpreted functions in place of variable-length vectors
Eddy Westbrook
committed
whoops: need to coerce the type of the condition in MaybeElim to a proposition by adding an EqTrue
Eddy Westbrook
committed
added back the implementaiton of atBVVec; enriched primBVTermFun to handle vector values
Eddy Westbrook
committed
refactored mrProveEq to support proving equality of arbitrary vectors by proving equality at all indices
Eddy Westbrook
committed

Commits on Feb 19, 2022

Commits on Feb 21, 2022

added MR solver test case for the arrays example
Eddy Westbrook
committed
added a comment about withUVars being wrong
Eddy Westbrook
committed
changed MR Solver to use the What4 backend in place of SBV
Eddy Westbrook
committed
lowered the debug level of arrays_mr_solver.saw to 1
Eddy Westbrook
committed
Merge branch 'master' into mr-solver/heapster-tests
Eddy Westbrook
committed

Commits on Feb 22, 2022

fix typo in definition of liftSC5
m-yac
authored

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

MR Solver SMT fixes for testing on Heapster models#1594

Commits on Feb 12, 2022

added parse_core_mod command; made ensureMonadicTerm a bit smarter by making it normalize the input type before deciding if it is already computational

fixed mrFunOutType, isCompFunType, and askMRSolver to normalize types

Commits on Feb 14, 2022

expanded the notion of a "function name" for MR Solver to include not just globals but also (tuple and record) projections of globals

added support for recognizing multiFixM computations to normComp

Commits on Feb 15, 2022

fixed a bug in withUVars; added some debugging around calling into an SMT solver

changed mrProvable so now it instantiates all uvars with ExtCnss, so that we do not pass the SMT solver uvars that do not occur in the proposition we want to prove

whoops, fixed instantiateUVarsM to reverse the list of uvars and substitute outer instantiations into the types of inner ones as it goes

added support for the maybe eliminator

Commits on Feb 17, 2022

Merge branch 'master' into mr-solver/heapster-tests

Commits on Feb 18, 2022

added applyGlobalOpenTerm and vectorTypeOpenTerm combinators

trying a new approach to getting SMT solving to work, by substiting uninterpreted functions in place of variable-length vectors

whoops: need to coerce the type of the condition in MaybeElim to a proposition by adding an EqTrue

added back the implementaiton of atBVVec; enriched primBVTermFun to handle vector values

refactored mrProveEq to support proving equality of arbitrary vectors by proving equality at all indices

Commits on Feb 19, 2022

Merge remote-tracking branch 'origin/master' into mr-solver/heapster-tests

got mrProveEq to handle pair types by changing it to return a TermInCtx; fixed a bug in withUVar, that assumptions added under the extended context should be thrown away when that context ends

got mrProveEq to handle pair types by changing it to return a TermInCtx; fixed a bug in withUVar, that assumptions need to be lifted in the new context and then reverted when that context ends

Merge branch 'mr-solver/heapster-tests' of github.com:GaloisInc/saw-script into mr-solver/heapster-tests

reordered some mrRefines cases; removed some unneeded debugging; changed variable instantiation in mrProvable to use the normalized types

bug fix in mrSetEVarClosed, to instantiate evars in the type of the evar being instantiated; trying to figure out why my uninterpreted functions do not work when passing them to the SMT solver...

Commits on Feb 21, 2022

added MR solver test case for the arrays example

added a comment about withUVars being wrong

changed MR Solver to use the What4 backend in place of SBV

lowered the debug level of arrays_mr_solver.saw to 1

Merge branch 'master' into mr-solver/heapster-tests

Commits on Feb 22, 2022

fix typo in definition of `liftSC5`