apalache Feature FARR: new SMT encoding with arrays

Feature FARR: new SMT encoding with arrays

Open konnov opened this issue 4 years ago • 1 comments

This is a meta-issue on implementing a new SMT encoding that efficiently uses arrays. All issues in this feature are labeled with FARR.

Dec 06 '20 13:12 konnov

The initial idea is to have an alternative SMT encoding using arrays as an experimental feature, enabled under a CLI option.

[x] Write an ADR to describe the new encoding.
#1041
#1154
#2549
[ ] Add tests for the new encoding.
#1051
#1099
#1134
#1589
#1660
#1680
[x] Add smt-encoding option to CLI check command.
#1053
#1159
[x] Replace uninterpreted constants by arrays in the encoding of KerA+ sets into SMT formulas.
#1092
#1100
#1106
#1152
#1162
#1171
#1229
#1287
#1339
#1595
#1737
#1802
#1819
#2057
[x] Encode KerA+ functions into SMT arrays.
#1169
#1490
#1594
#1774
#1811
#2001
[x] Enable TLA+ constructs not encoded as SMT arrays to work in the new encoding.
#1288
#1418
#1840
#2000
#2112
[x] Add funArrays encoding
#2011

Oct 01 '21 12:10 rodrigo7491

@konnov after #2549 is merged, only #1589 will remain open. Should we close this issue?

May 01 '23 11:05 rodrigo7491

Yes, definitely!

May 10 '23 08:05 konnov