Merge remote-tracking branch 'upstream/develop' into fix-subst-ml-pred

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