[FEATURE] Pack arithmetic operations in a single SMT expression

[konnov]

Currently, arithmetic operations are translated one by one, see IntArithRule and IntCmpRule. This is done mainly for historical reasons, as we wanted to keep the translation simple. For instance, the TLA+ expression x + 1 = 10 would be translated into a series of constraints:

// c_1 is the cell for x
(assert (= c_2 1))
(assert (= c_3 (+ c_1 c_2)))
(assert (= c_4 10))
(assert (= c_5 (= c_3 c_4)))

The Boolean result of the translation is stored in the cell c_5, whereas c_1, c_2, c_3, and c_4 are intermediate cells.

Instead of doing this translation, we could directly translate the above expression into the assertion:

(assert (= c_5 (c_1 + 1 = 10)))

We should only take care of the leaf expressions, which require rewriting, unless they are integer literals. It is not obvious, whether this would significantly improve the performance. However, it will decrease the number of constraints and ease debugging.

• Pack arithmetic expressions in IntArithRule #1540 (IntArithRule)
• Pack integer arithmetic comparisons in IntCmpRule #1545 (IntCmpRule, EqRule)

[konnov]

@thpani if you like to add this one on your queue, this is a very simple task related to the translator.