Feature FARR: new SMT encoding with arrays

[konnov]

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

[rodrigo7491]

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

• Write an ADR to describe the new encoding.
• [FEATURE] Document the handling of sets in the SMT encoding with arrays #1041
• [FEATURE] Document the handling of functions and sequences in the SMT encoding with arrays #1154
• Add TACAS'23 info #2549
• Add tests for the new encoding.
• [FEATURE] Make unit tests parametric w.r.t. SymbStateRewriter #1051
• [FEATURE] Benchmarking setup for the arrays encoding #1099
• [BUG] Benchmark results are producing strange results on encoding tests #1134
• The SNEAKY bug in the arrays encoding #1589
• An error in the arrays encoding #1660
• Unhandled Z3Exception with arrays encoding: domain <> parameter sort mismatch #1680
• Add smt-encoding option to CLI check command.
• [FEATURE] Add SMT encoding option to CLI #1053
• [FEATURE] Refactor SMT encoding option flag use #1159
• Replace uninterpreted constants by arrays in the encoding of KerA+ sets into SMT formulas.
• [FEATURE] Add support for sets to the SMT encoding with arrays #1092
• [FEATURE] Remove duplicate empty set representations in arrays encoding #1100
• [FEATURE] Add Apalache IR operators for SMT select and store #1106
• [BUG] Sets becoming unconstrained after set minus operation #1152
• [BUG] Unconstrained sets due to incorrect use of set membership implications #1162
• [FEATURE] Streamline set update operations #1171
• [FEATURE] Use SMT map in the rewriting rule for TLA+ set filters #1229
• [FEATURE] Move some operators to ApalacheInternalOper #1287
• [FEATURE] Replace the chaining with a loop again? #1339
• Refactor Z3SolverContext caches #1595
• Slowdown of the arrays encoding in the presence of set union and set membership #1737
• Encode infinite sets in the arrays encoding #1802
• Undefined solver evaluation leading to spurious counter-example #1819
• Update of set filter rule with SMT arrays  #2057
• Encode KerA+ functions into SMT arrays.
• [FEATURE] Add support for TLA+ functions to the SMT encoding with arrays #1169
• Problem with static check on function application in the arrays encoding #1490
• Incorrect SMT logging in the arrays encoding #1594
• Problem with functions sets that have function sets as their range in the arrays encoding #1774
• Comparison problem with functions with an empty domain in the arrays encoding #1811
• Fix unguarded constraining #2001
• Enable TLA+ constructs not encoded as SMT arrays to work in the new encoding.
• [FEATURE] Add support for TLA+ records in the arrays encoding #1288
• [FEATURE] Enable the remaining TLA+ features as they are to work in the arrays encoding #1418
• Spurious counter-examples with functions of records in the arrays encoding #1840
• Fix potential arena damage #2000
• Fix cell type in DomainRuleWithArrays #2112
• Add funArrays encoding
• Add SMT encoding with sets as uninterpreted constants and functions as arrays #2011

[rodrigo7491]

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

[konnov]

Yes, definitely!