Encode function sets as SMT arrays

[rodrigo7491]

• Tests added for any new code
• Ran make fmt-fix (or had formatting run automatically on all files edited)
• Documentation added for any new functionality
• Entry added to UNRELEASED.md for any new functionality

This PR makes elements of type FinFunSetT be encoded as SMT arrays. Closes #1680.

[codecov-commenter]

Codecov Report

Merging #1701 (b98ba8c) into unstable (0fff5ac) will increase coverage by 0.00%.
The diff coverage is 100.00%.

@@            Coverage Diff            @@
##           unstable    #1701   +/-   ##
=========================================
  Coverage     75.31%   75.31%           
=========================================
  Files           357      357           
  Lines         11541    11543    +2     
  Branches        595      596    +1     
=========================================
+ Hits           8692     8694    +2     
  Misses         2849     2849           

Impacted Files	Coverage Δ
...rsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala	81.28% <100.00%> (+0.09%)	⬆️

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 0fff5ac...b98ba8c. Read the comment docs.

[shonfeder]

LGTM!