From 2d26b93482c5b967c84e65e2c55ffc1cb2967dbb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Petar=20Maksimovi=C4=87?= Date: Thu, 17 Oct 2024 17:02:43 +0100 Subject: [PATCH] Marking simplifications that preserve definedness (#4662) For the booster-with-remainders to be fully operational and therefore the dependency on Kore be reduced, the simplifications that contain partial functions but which we know preserve definedness must be marked as such. --- k-distribution/include/kframework/builtin/domains.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index b04af99c8e..bd6ea7716e 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -1366,10 +1366,10 @@ module INT-SYMBOLIC [symbolic] rule X %Int N => X requires 0 <=Int X andBool X X [simplification] - rule 0 < 0 [simplification] - rule X >>Int 0 => X [simplification] - rule 0 >>Int _ => 0 [simplification] + rule X < X [simplification, preserves-definedness] + rule 0 < 0 requires 0 <=Int Y [simplification, preserves-definedness] + rule X >>Int 0 => X [simplification, preserves-definedness] + rule 0 >>Int Y => 0 requires 0 <=Int Y [simplification, preserves-definedness] endmodule module INT-SYMBOLIC-KORE [symbolic, haskell]