Use Euclidean division/modulus to express T-division/modulus for SMT …

…hooks (#4616)

Fixes #4606

The following reasoning was applied:

Given dividend `D` and divisor `d`, let the `q₋` and `r₋` in
```
D = d · qₑ + rₑ    # Euclidean division
D = d · qₜ + rₜ    # T-division
```
be Euclidean and T division results. In terms of K operations,
```
qₑ = D divInt d    rₑ = D modInt d
qₜ = D /Int d      rₜ = D %Int d
```

According to [1], we can express Euclidean division by T-division:
```
qₑ = qₜ − I
rₑ = rₜ + I · d
  where
    I = if rₜ >= 0
        then 0
        else if d > 0
             then 1
             else −1
```

To transform the equations to isolate `qₜ` and `rₜ`, we need to express
the `where` clause without `rₜ`. We use

1. `rₑ = 0 <=> rₜ = 0`, and
2. `rₜ ≠ 0 => sgn(rₜ) = sgn(D)` (as per [1])

to rewrite the first `if` to `if (rₑ = 0 || D > 0) ...`.

Now we can transform the equations to isolate `qₜ` and `rₜ`, getting
(written with `let`):

```
let I = if (rₑ = 0 || D > 0)
        then 0
        else if d > 0
             then 1
             else -1
 in qₜ = qₑ + I
    rₜ = rₑ - I · d
```

We need two independent equations, so lifting the shared `I` is not
beneficial. we can write two `if` expressions per equation.

```
qₜ = if (rₑ = 0 || D > 0)
     then qₑ
     else if d > 0
          then qₑ + 1
          else qₑ - 1
rₜ = if (rₑ = 0 || D > 0)
     then rₑ
     else if d > 0
          then rₑ - d
          else rₑ + d
```

Written as SMT hook expressions (coherent with [2]):

* (`#1 /Int #2`): `ite (or (= 0 (mod #1 #2)) (>= #1 0)) (div #1 #2) (ite
(> #2 0) (+ (div #1 #2) 1) (- (div #1 #2) 1))`
* (`#1 %Int #2`): `ite (or (= 0 (mod #1 #2)) (>= #1 0)) (mod #1 #2) (ite
(> #2 0) (- (mod #1 #2) #2) (+ (mod #1 #2) #2))`

[1]
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/divmodnote-letter.pdf
[2] https://gist.github.com/Rufflewind/a880e03fb0d13644a1e8

k-distribution/include/kframework/builtin/domains.md

@@ -1241,9 +1241,13 @@ You can:
                > left:
                  Int "*Int" Int                 [function, total, symbol(_*Int_), left, comm, smt-hook(*), hook(INT.mul)]
                /* FIXME: translate /Int and %Int into smtlib */
-               /* /Int and %Int implement t-division, which rounds towards 0 */
-               | Int "/Int" Int                 [function, symbol(_/Int_), left, smt-hook(div), hook(INT.tdiv)]
-               | Int "%Int" Int                 [function, symbol(_%Int_), left, smt-hook(mod), hook(INT.tmod)]
+               /* /Int and %Int implement t-division, which rounds towards 0. SMT hooks need to convert from Euclidian division operations */
+               | Int "/Int" Int                 [function, symbol(_/Int_), left,
+                                                 smt-hook((ite (or (= 0 (mod #1 #2)) (>= #1 0)) (div #1 #2) (ite (> #2 0) (+ (div #1 #2) 1) (- (div #1 #2) 1)))),
+                                                 hook(INT.tdiv)]
+               | Int "%Int" Int                 [function, symbol(_%Int_), left,
+                                                 smt-hook((ite (or (= 0 (mod #1 #2)) (>= #1 0)) (mod #1 #2) (ite (> #2 0) (- (mod #1 #2) #2) (+ (mod #1 #2) #2)))),
+                                                 hook(INT.tmod)]
                /* divInt and modInt implement e-division according to the Euclidean division theorem, therefore the remainder is always positive */
                | Int "divInt" Int               [function, symbol(_divInt_), left, smt-hook(div), hook(INT.ediv)]
                | Int "modInt" Int               [function, symbol(_modInt_), left, smt-hook(mod), hook(INT.emod)]

pyk/src/tests/integration/test_division_hooks.py

@@ -0,0 +1,101 @@
+from __future__ import annotations
+
+from typing import TYPE_CHECKING
+
+import pytest
+
+from pyk.kore.prelude import BOOL, INT, TRUE, eq_int, int_dv
+from pyk.kore.rpc import SatResult
+from pyk.kore.syntax import App, Equals, EVar
+from pyk.testing import KoreClientTest
+
+if TYPE_CHECKING:
+    from typing import Final
+
+    from pyk.kore.rpc import KoreClient
+
+T_DIVISION_TEST_DATA: Final = (
+    # Op   ,  a,  b, a Op b
+    ('/Int', +8, +3, +2),
+    ('/Int', +8, -3, -2),
+    ('/Int', -8, +3, -2),
+    ('/Int', -8, -3, +2),
+    ('%Int', +8, +3, +2),
+    ('%Int', +8, -3, +2),
+    ('%Int', -8, +3, -2),
+    ('%Int', -8, -3, -2),
+    #####################
+    ('/Int', +1, +2, 0),
+    ('/Int', +1, -2, 0),
+    ('/Int', -1, +2, 0),
+    ('/Int', -1, -2, 0),
+    ('%Int', +1, +2, +1),
+    ('%Int', +1, -2, +1),
+    ('%Int', -1, +2, -1),
+    ('%Int', -1, -2, -1),
+    #####################
+    ('/Int', +4, +2, +2),
+    ('/Int', +4, -2, -2),
+    ('/Int', -4, +2, -2),
+    ('/Int', -4, -2, +2),
+    ('%Int', +4, +2, 0),
+    ('%Int', +4, -2, 0),
+    ('%Int', -4, +2, 0),
+    ('%Int', -4, -2, 0),
+)
+
+kore_for = {'/Int': "Lbl'UndsSlsh'Int'Unds'", '%Int': "Lbl'UndsPerc'Int'Unds'"}
+
+
+class TestDivisionHooksHs(KoreClientTest):
+    KOMPILE_DEFINITION = """
+        module SMT
+            imports INT
+        endmodule
+    """
+    KOMPILE_MAIN_MODULE = 'SMT'
+    KOMPILE_ARGS = {'syntax_module': 'SMT'}
+    LLVM_ARGS = {'syntax_module': 'SMT'}
+
+    @pytest.mark.parametrize(
+        'op, a, b, c',
+        T_DIVISION_TEST_DATA,
+        ids=[f'get-model: {a} {op} {b} == {c}' for op, a, b, c in T_DIVISION_TEST_DATA],
+    )
+    def test_smt_t_division(self, kore_client: KoreClient, op: str, a: int, b: int, c: int) -> None:
+        """checks whether the SMT solver returns ``X = c`` for ``X = a op b``."""
+
+        # Given
+        pattern = Equals(
+            BOOL,
+            INT,
+            TRUE,
+            eq_int(App(kore_for[op], (), (int_dv(a), int_dv(b))), EVar('X', INT)),
+        )
+
+        # When
+        actual = kore_client.get_model(pattern, None)
+
+        # Then
+        expected = SatResult(Equals(INT, INT, EVar('X', INT), int_dv(c)))
+
+        assert actual == expected
+
+    @pytest.mark.parametrize(
+        'op, a, b, c',
+        T_DIVISION_TEST_DATA,
+        ids=[f'simplify: {a} {op} {b} == {c}' for op, a, b, c in T_DIVISION_TEST_DATA],
+    )
+    def test_llvm_t_division(self, kore_client: KoreClient, op: str, a: int, b: int, c: int) -> None:
+        """checks whether kore-rpc (HS hook) and booster (LLVM library) both return ``c`` for ``a op b``."""
+
+        # Given
+        pattern = App(kore_for[op], (), (int_dv(a), int_dv(b)))
+
+        # When
+        actual = kore_client.simplify(pattern)
+
+        # Then
+        expected = (int_dv(c), ())
+
+        assert actual == expected