Pack integer arithmetic comparisons in IntCmpRule

[thpani]

Closes #1342

Pack arithmetic expressions in IntCmpRule and EqRule. Translate TLA+ arithmetic comparisons into a single SMT constraint, without introducing intermediate cells.

Uses the same logic for packing arithmetic expressions as #1541, which is refactored into a trait in 835e717.

[codecov-commenter]

Codecov Report

Merging #1545 (840d543) into unstable (4107967) will increase coverage by 0.02%.
The diff coverage is 96.42%.

❗ Current head 840d543 differs from pull request most recent head feaa9f3. Consider uploading reports for the commit feaa9f3 to get more accurate results

@@             Coverage Diff              @@
##           unstable    #1545      +/-   ##
============================================
+ Coverage     74.97%   75.00%   +0.02%     
============================================
  Files           359      360       +1     
  Lines         11518    11526       +8     
  Branches        550      557       +7     
============================================
+ Hits           8636     8645       +9     
+ Misses         2882     2881       -1     

Impacted Files	Coverage Δ
.../forsyte/apalache/tla/bmcmt/rules/IntCmpRule.scala	82.35% <90.00%> (+5.88%)	⬆️
...a/at/forsyte/apalache/tla/bmcmt/rules/EqRule.scala	92.00% <100.00%> (+3.76%)	⬆️
...syte/apalache/tla/bmcmt/rules/IntArithPacker.scala	100.00% <100.00%> (ø)
...orsyte/apalache/tla/bmcmt/rules/IntArithRule.scala	85.71% <100.00%> (-5.60%)	⬇️

---

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 4107967...feaa9f3. Read the comment docs.

[konnov]

Looks good!