add internal Array theory, elaborate Set theory into it#688
Conversation
|
Performance charts (on LH test suite):
|
nikivazou
left a comment
There was a problem hiding this comment.
Looks good to me! But does it come with a relevant LH pull request to ensure that it does not break any tests?
| -- | Theory Symbols ------------------------------------------------------------ | ||
| -------------------------------------------------------------------------------- | ||
|
|
||
| -- TODO drop all of Set and Map symbols when Map is handled through arrays |
There was a problem hiding this comment.
Yes, as currently the Map theory is still done via monomorphizing and it has operations for converting to Sets, we can't yet remove the SMT-interacting parts for Maps+Sets. Once Maps are also converted, we can drop this code and only leave the Array theory to be written to SMT. These TODOs serve as a reminder of this.
| , interpSym setSub sub setCmpSort | ||
| , interpSym setCom com setCmpSort | ||
| [ | ||
| -- TODO we'll probably need two versions of these - one for sets and one for maps |
There was a problem hiding this comment.
Once we start converting Maps, there are likely to be some design choices whether to try making Array theory more polymorphic, or simply have a second set of Array operations specialized for Sets. This TODO is a heads-up for this.
| | SBool | ||
| | SReal | ||
| | SString | ||
| -- TODO remove these now that we use SArray directly |
Might require documentation: Does this PR narrow in some way the list of SMT solvers that LH/LF can work with? |
This uses the same SMTLIBv2-compliant ArraysEx theory encoding as before, we're just now inlining the definitions so that the LF elaborator can produce local signatures instead of hardcoding all Sets to be However, the concern that by now we're pretty much vendor-locked into Z3 is valid; I've tried running the .smt files produced by LF even before this PR through CVC5 and failed; investigating this is our next step (after converting the Map theory to use Arrays as well). |
The tests pass successfully after adapting LH to the |
|
@ranjitjhala we can merge this tomorrow (just checking it does not break flux or anything else) |
|
Yes please merge, thanks @nikivazou and @clayrat -- this is a really huge step!!! |
|
[I think its a big enough change to warrant a version number bump?] |
|
Alex wants to apply the same inlining for Maps (for uniformity) so we can change the version number after this pending edit. |
Fixes ucsd-progsys/liquidhaskell#2272 by elaborating Set operations into Array operations which are "internally" polymorphic in Z3.
Currently, this only touches Sets but presumably Maps also need to undergo the same treatment.