Encode infinite sets in the arrays encoding #1802
Conversation
Codecov Report
@@ Coverage Diff @@
## unstable #1802 +/- ##
============================================
+ Coverage 76.81% 76.82% +0.01%
============================================
Files 383 383
Lines 11837 11843 +6
Branches 548 549 +1
============================================
+ Hits 9092 9098 +6
Misses 2745 2745
Continue to review full report at Codecov.
|
There was a problem hiding this comment.
Nice! There is definitely something about supporting functions of infinite domains in the arrays encoding. However, we should be real careful about not letting cells like that to propagate into the rules that expect bounded sets, e.g., what happens if we do DOMAN f \union { 1 }?
|
Is this ready to be merged? |
…into ro/infinite-sets-bug � Conflicts: � UNRELEASED.md � tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala
…into ro/infinite-sets-bug
|
This PR fixes the immediate crash problem reported on #1798. Further improvements to the handling of infinite sets will be done at a later stage. |
make fmt-fix(or had formatting run automatically on all files edited)Documentation added for any new functionalityThis PR encodes infinite sets as constant SMT arrays in the arrays encoding. This fixes a problem first mentioned by @konnov when checking a version of EWD998. It is also the cause of the exception thrown by the arrays encoding mentioned in #1798.