Initial version of theory of array support!#309
Open
RobinWebbers wants to merge 2 commits intolsrcz:mainfrom
Open
Initial version of theory of array support!#309RobinWebbers wants to merge 2 commits intolsrcz:mainfrom
RobinWebbers wants to merge 2 commits intolsrcz:mainfrom
Conversation
…. :) This requires a version of SBV that is not yet on stackage (at the time of writing) and ruins backwards compatibility. There is no optimisation of expressions involving theory of array expressions as of yet.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Hey!
I wanted to use the theory of arrays within
Grisette, so I added support for it. It works from beginning to end (i.e. I can useSymArrayand read a counterexample back from theSMTsolver). It still is a bit rough though in some places, so maybe it is best to not merge immediately!Here are the caveats:
SBVthat is not yet on stackage. I needed to extendSBVin order to properly support this, I'm still waiting for some of the changes to be merged on theSBVside of things. Additionally, this will not support any previous version ofSBVas it indeed only compiles with these changes. I'm not sure how to go about this breakage.ArrayandSymArray)As an aside, I had to remove the instance for
SymOrdforRoundingModeasSBVstopped supportingOrdSymbolicfor it. This is in fact fine, because the SMT solvers do not even support the ordering relation.I also rewrote some of the functions that involved
Typeable: I needed to extend them anyway and I feel like the current rewrite is a lot more intuitive.