From e6fc73bb31865b4d3fc28945dc2abb8265064b10 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 15:26:37 +0000
Subject: [PATCH 01/26] Fix pattern order

---
 pyk/src/pyk/kore/rule.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index 680d91082f..4a50caa510 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -246,12 +246,12 @@ def _extract(axiom: Axiom) -> tuple[Pattern, Pattern, Pattern | None, Pattern |
         # Cases 11-12 of get_left_hand_side
         # Case 0 of get_right_hand_side
         match axiom.pattern:
+            case Implies(right=Equals(left=Ceil())):
+                raise ValueError(f'Axiom is a ceil rule: {axiom.text}')
             case Implies(left=Top(), right=Equals(left=lhs, right=And(ops=(rhs, Top() | Equals() as _ens)))):
                 pass
             case Implies(left=Equals(left=req), right=Equals(left=lhs, right=And(ops=(rhs, Top() | Equals() as _ens)))):
                 pass
-            case Implies(right=Equals(left=Ceil())):
-                raise ValueError(f'Axiom is a ceil rule: {axiom.text}')
             case _:
                 raise ValueError(f'Cannot extract simplification rule from axiom: {axiom.text}')
         ens = _extract_ensures(_ens)

From 024b059b9e5501a80abe360fe63df345759f66e0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 15:28:32 +0000
Subject: [PATCH 02/26] Skip `\equals` simplifications

---
 pyk/src/pyk/kore/rule.py | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index 4a50caa510..bc49ba69d7 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -74,8 +74,7 @@ def _is_rule(axiom: Axiom) -> bool:
             return False
 
         match axiom.pattern:
-            case Implies(right=Equals(left=Ceil())):
-                # Ceil rule
+            case Implies(right=Equals(left=Ceil() | Equals())):
                 return False
 
         return True
@@ -246,8 +245,8 @@ def _extract(axiom: Axiom) -> tuple[Pattern, Pattern, Pattern | None, Pattern |
         # Cases 11-12 of get_left_hand_side
         # Case 0 of get_right_hand_side
         match axiom.pattern:
-            case Implies(right=Equals(left=Ceil())):
-                raise ValueError(f'Axiom is a ceil rule: {axiom.text}')
+            case Implies(right=Equals(left=Ceil() | Equals())):
+                raise ValueError(fr'Axiom is a \ceil or \equals rule: {axiom.text}')
             case Implies(left=Top(), right=Equals(left=lhs, right=And(ops=(rhs, Top() | Equals() as _ens)))):
                 pass
             case Implies(left=Equals(left=req), right=Equals(left=lhs, right=And(ops=(rhs, Top() | Equals() as _ens)))):

From 026e08b3f83ec4e024f47e34924ef800c5bbb392 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 15:29:19 +0000
Subject: [PATCH 03/26] Strengthen filter condition

---
 pyk/src/pyk/kore/rule.py | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index bc49ba69d7..5cdc83dacc 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -73,9 +73,16 @@ def _is_rule(axiom: Axiom) -> bool:
         if any(attr in axiom.attrs_by_key for attr in _SKIPPED_ATTRS):
             return False
 
-        match axiom.pattern:
-            case Implies(right=Equals(left=Ceil() | Equals())):
-                return False
+        if 'simplification' in axiom.attrs_by_key:
+            match axiom.pattern:
+                case Implies(
+                    left=Top() | Equals(),
+                    right=Equals(
+                        left=Ceil() | Equals(),
+                        right=And(ops=(_, Top() | Equals())),
+                    ),
+                ):
+                    return False
 
         return True
 

From 7ae6fb175b14402f75a739487e056e51f9d24075 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 15:45:14 +0000
Subject: [PATCH 04/26] Make `SimpliRule.lhs` an `App`

---
 pyk/src/pyk/kore/rule.py | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index 5cdc83dacc..9fd66cbb6f 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -228,7 +228,7 @@ def _extract_rhs(axiom: Axiom) -> tuple[App, Pattern, Pattern | None]:
 @final
 @dataclass
 class SimpliRule(Rule):
-    lhs: Pattern
+    lhs: App
     rhs: Pattern
     req: Pattern | None
     ens: Pattern | None
@@ -247,17 +247,19 @@ def from_axiom(axiom: Axiom) -> SimpliRule:
         )
 
     @staticmethod
-    def _extract(axiom: Axiom) -> tuple[Pattern, Pattern, Pattern | None, Pattern | None]:
+    def _extract(axiom: Axiom) -> tuple[App, Pattern, Pattern | None, Pattern | None]:
         req: Pattern | None = None
         # Cases 11-12 of get_left_hand_side
         # Case 0 of get_right_hand_side
         match axiom.pattern:
-            case Implies(right=Equals(left=Ceil() | Equals())):
-                raise ValueError(fr'Axiom is a \ceil or \equals rule: {axiom.text}')
-            case Implies(left=Top(), right=Equals(left=lhs, right=And(ops=(rhs, Top() | Equals() as _ens)))):
+            case Implies(left=Top(), right=Equals(left=App() as lhs, right=And(ops=(rhs, Top() | Equals() as _ens)))):
                 pass
-            case Implies(left=Equals(left=req), right=Equals(left=lhs, right=And(ops=(rhs, Top() | Equals() as _ens)))):
+            case Implies(
+                left=Equals(left=req), right=Equals(left=App() as lhs, right=And(ops=(rhs, Top() | Equals() as _ens)))
+            ):
                 pass
+            case Implies(right=Equals(left=Ceil() | Equals())):
+                raise ValueError(fr'Axiom is a \ceil or \equals rule: {axiom.text}')
             case _:
                 raise ValueError(f'Cannot extract simplification rule from axiom: {axiom.text}')
         ens = _extract_ensures(_ens)

From e2e7293e360cb2f0c6f8586bfccf424162647c00 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 15:56:52 +0000
Subject: [PATCH 05/26] Rename `_extract_ensures` to `_extract_condition`

---
 pyk/src/pyk/kore/rule.py | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index 9fd66cbb6f..fa27691601 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -157,7 +157,7 @@ def _extract_rhs(axiom: Axiom) -> tuple[App, Pattern | None]:
                 pass
             case _:
                 raise ValueError(f'Cannot extract RHS from axiom: {axiom.text}')
-        ens = _extract_ensures(_ens)
+        ens = _extract_condition(_ens)
         return rhs, ens
 
 
@@ -221,7 +221,7 @@ def _extract_rhs(axiom: Axiom) -> tuple[App, Pattern, Pattern | None]:
                 pass
             case _:
                 raise ValueError(f'Cannot extract RHS from axiom: {axiom.text}')
-        ens = _extract_ensures(_ens)
+        ens = _extract_condition(_ens)
         return app, rhs, ens
 
 
@@ -262,16 +262,16 @@ def _extract(axiom: Axiom) -> tuple[App, Pattern, Pattern | None, Pattern | None
                 raise ValueError(fr'Axiom is a \ceil or \equals rule: {axiom.text}')
             case _:
                 raise ValueError(f'Cannot extract simplification rule from axiom: {axiom.text}')
-        ens = _extract_ensures(_ens)
+        ens = _extract_condition(_ens)
         return lhs, rhs, req, ens
 
 
-def _extract_ensures(ens: Top | Equals | None) -> Pattern | None:
-    match ens:
+def _extract_condition(pattern: Top | Equals) -> Pattern | None:
+    match pattern:
         case Top():
             return None
-        case Equals(left=res):
-            return res
+        case Equals(left=cond):
+            return cond
         case _:
             raise AssertionError()
 

From e8bc49e73b6a294cbb18d6caabcbbb630fd62ec0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 15:59:22 +0000
Subject: [PATCH 06/26] Strengthen signature

---
 pyk/src/pyk/kore/rule.py | 12 +++++-------
 1 file changed, 5 insertions(+), 7 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index fa27691601..64dcbd23f2 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -153,7 +153,7 @@ def _extract_rhs(axiom: Axiom) -> tuple[App, Pattern | None]:
         # 2: rhs(\rewrites(_, \and(X, Y))) = get_builtin(\and(X, Y))
         # Below is a special case without get_builtin
         match axiom.pattern:
-            case Rewrites(right=And(ops=(App("Lbl'-LT-'generatedTop'-GT-'") as rhs, Top() | Equals() as _ens))):
+            case Rewrites(right=And(ops=(App("Lbl'-LT-'generatedTop'-GT-'") as rhs, _ens))):
                 pass
             case _:
                 raise ValueError(f'Cannot extract RHS from axiom: {axiom.text}')
@@ -217,7 +217,7 @@ def _get_patterns(pattern: Pattern) -> tuple[Pattern, ...]:
     def _extract_rhs(axiom: Axiom) -> tuple[App, Pattern, Pattern | None]:
         # Case 0 of get_right_hand_side
         match axiom.pattern:
-            case Implies(right=Equals(left=App() as app, right=And(ops=(rhs, Top() | Equals() as _ens)))):
+            case Implies(right=Equals(left=App() as app, right=And(ops=(rhs, _ens)))):
                 pass
             case _:
                 raise ValueError(f'Cannot extract RHS from axiom: {axiom.text}')
@@ -252,11 +252,9 @@ def _extract(axiom: Axiom) -> tuple[App, Pattern, Pattern | None, Pattern | None
         # Cases 11-12 of get_left_hand_side
         # Case 0 of get_right_hand_side
         match axiom.pattern:
-            case Implies(left=Top(), right=Equals(left=App() as lhs, right=And(ops=(rhs, Top() | Equals() as _ens)))):
+            case Implies(left=Top(), right=Equals(left=App() as lhs, right=And(ops=(rhs, _ens)))):
                 pass
-            case Implies(
-                left=Equals(left=req), right=Equals(left=App() as lhs, right=And(ops=(rhs, Top() | Equals() as _ens)))
-            ):
+            case Implies(left=Equals(left=req), right=Equals(left=App() as lhs, right=And(ops=(rhs, _ens)))):
                 pass
             case Implies(right=Equals(left=Ceil() | Equals())):
                 raise ValueError(fr'Axiom is a \ceil or \equals rule: {axiom.text}')
@@ -266,7 +264,7 @@ def _extract(axiom: Axiom) -> tuple[App, Pattern, Pattern | None, Pattern | None
         return lhs, rhs, req, ens
 
 
-def _extract_condition(pattern: Top | Equals) -> Pattern | None:
+def _extract_condition(pattern: Pattern) -> Pattern | None:
     match pattern:
         case Top():
             return None

From 65dcac888aeb6bb7f02935edc3948b7523987e68 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 16:01:41 +0000
Subject: [PATCH 07/26] Replace `AssertionError` by `ValueError`

---
 pyk/src/pyk/kore/rule.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index 64dcbd23f2..045d0d2da9 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -211,7 +211,7 @@ def _get_patterns(pattern: Pattern) -> tuple[Pattern, ...]:
             case And(ops=(In(right=x), y)):
                 return (x,) + FunctionRule._get_patterns(y)
             case _:
-                raise AssertionError()
+                raise ValueError(f'Cannot extract argument list from pattern: {pattern.text}')
 
     @staticmethod
     def _extract_rhs(axiom: Axiom) -> tuple[App, Pattern, Pattern | None]:
@@ -271,7 +271,7 @@ def _extract_condition(pattern: Pattern) -> Pattern | None:
         case Equals(left=cond):
             return cond
         case _:
-            raise AssertionError()
+            raise ValueError(f'Cannot extract condition from pattern: {pattern.text}')
 
 
 def _extract_uid(axiom: Axiom) -> str:

From 2e7186ce2eac11d797857a7b1af9d6adb12b50a9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 16:04:08 +0000
Subject: [PATCH 08/26] Strengthen pattern

---
 pyk/src/pyk/kore/rule.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index 045d0d2da9..24ada95a00 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -208,8 +208,8 @@ def _get_patterns(pattern: Pattern) -> tuple[Pattern, ...]:
         match pattern:
             case Top():
                 return ()
-            case And(ops=(In(right=x), y)):
-                return (x,) + FunctionRule._get_patterns(y)
+            case And(ops=(In(left=EVar(), right=arg), rest)):
+                return (arg,) + FunctionRule._get_patterns(rest)
             case _:
                 raise ValueError(f'Cannot extract argument list from pattern: {pattern.text}')
 

From 3c49f033edb54ab18f75fa143d70baa165660d26 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 16:06:48 +0000
Subject: [PATCH 09/26] Remove vacuous cases

---
 pyk/src/pyk/kore/rule.py | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index 24ada95a00..fd477ec8a6 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -123,10 +123,6 @@ def _extract_lhs(axiom: Axiom) -> tuple[App, Pattern | None, EVar | None]:
         # Cases 0-5 of get_left_hand_side
         # Cases 5-10 of get_requires
         match axiom.pattern:
-            case Rewrites(left=And(ops=(Top(), lhs))):
-                pass
-            case Rewrites(left=And(ops=(Equals(left=req), lhs))):
-                pass
             case Rewrites(left=And(ops=(lhs, Top()))):
                 pass
             case Rewrites(left=And(ops=(lhs, Equals(left=req)))):

From 5a4485c8d7842237cfa7b0cd2b1dd40b6b57c8cb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 16:22:24 +0000
Subject: [PATCH 10/26] Match requires clause using `_extract_condition`

---
 pyk/src/pyk/kore/rule.py | 30 ++++++++++--------------------
 1 file changed, 10 insertions(+), 20 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index fd477ec8a6..b539ba40aa 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -119,21 +119,18 @@ def from_axiom(axiom: Axiom) -> RewriteRule:
 
     @staticmethod
     def _extract_lhs(axiom: Axiom) -> tuple[App, Pattern | None, EVar | None]:
-        req: Pattern | None = None
         # Cases 0-5 of get_left_hand_side
         # Cases 5-10 of get_requires
         match axiom.pattern:
-            case Rewrites(left=And(ops=(lhs, Top()))):
+            case Rewrites(left=And(ops=(Not(), And(ops=(_req, lhs))))):
                 pass
-            case Rewrites(left=And(ops=(lhs, Equals(left=req)))):
-                pass
-            case Rewrites(left=And(ops=(Not(), And(ops=(Top(), lhs))))):
-                pass
-            case Rewrites(left=And(ops=(Not(), And(ops=(Equals(left=req), lhs))))):
+            case Rewrites(left=And(ops=(lhs, _req))):
                 pass
             case _:
                 raise ValueError(f'Cannot extract LHS from axiom: {axiom.text}')
 
+        req = _extract_condition(_req)
+
         ctx: EVar | None = None
         match lhs:
             case App("Lbl'-LT-'generatedTop'-GT-'") as app:
@@ -182,18 +179,13 @@ def from_axiom(axiom: Axiom) -> FunctionRule:
 
     @staticmethod
     def _extract_args(axiom: Axiom) -> tuple[tuple[Pattern, ...], Pattern | None]:
-        req: Pattern | None = None
         # Cases 7-10 of get_left_hand_side
         # Cases 0-3 of get_requires
         match axiom.pattern:
-            case Implies(left=And(ops=(Top(), pat))):
-                return FunctionRule._get_patterns(pat), req
-            case Implies(left=And(ops=(Equals(left=req), pat))):
-                return FunctionRule._get_patterns(pat), req
-            case Implies(left=And(ops=(Not(), And(ops=(Top(), pat))))):
-                return FunctionRule._get_patterns(pat), req
-            case Implies(left=And(ops=(Not(), And(ops=(Equals(left=req), pat))))):
-                return FunctionRule._get_patterns(pat), req
+            case Implies(left=And(ops=(Not(), And(ops=(_req, pat))))):
+                return FunctionRule._get_patterns(pat), _extract_condition(_req)
+            case Implies(left=And(ops=(_req, pat))):
+                return FunctionRule._get_patterns(pat), _extract_condition(_req)
             case _:
                 raise ValueError(f'Cannot extract LHS from axiom: {axiom.text}')
 
@@ -244,18 +236,16 @@ def from_axiom(axiom: Axiom) -> SimpliRule:
 
     @staticmethod
     def _extract(axiom: Axiom) -> tuple[App, Pattern, Pattern | None, Pattern | None]:
-        req: Pattern | None = None
         # Cases 11-12 of get_left_hand_side
         # Case 0 of get_right_hand_side
         match axiom.pattern:
-            case Implies(left=Top(), right=Equals(left=App() as lhs, right=And(ops=(rhs, _ens)))):
-                pass
-            case Implies(left=Equals(left=req), right=Equals(left=App() as lhs, right=And(ops=(rhs, _ens)))):
+            case Implies(left=_req, right=Equals(left=App() as lhs, right=And(ops=(rhs, _ens)))):
                 pass
             case Implies(right=Equals(left=Ceil() | Equals())):
                 raise ValueError(fr'Axiom is a \ceil or \equals rule: {axiom.text}')
             case _:
                 raise ValueError(f'Cannot extract simplification rule from axiom: {axiom.text}')
+        req = _extract_condition(_req)
         ens = _extract_condition(_ens)
         return lhs, rhs, req, ens
 

From 04650314cc8b1d92d5736e0e06c5da6868084f7e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 16:23:48 +0000
Subject: [PATCH 11/26] Remove special case for error

---
 pyk/src/pyk/kore/rule.py | 2 --
 1 file changed, 2 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index b539ba40aa..13668be8f4 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -241,8 +241,6 @@ def _extract(axiom: Axiom) -> tuple[App, Pattern, Pattern | None, Pattern | None
         match axiom.pattern:
             case Implies(left=_req, right=Equals(left=App() as lhs, right=And(ops=(rhs, _ens)))):
                 pass
-            case Implies(right=Equals(left=Ceil() | Equals())):
-                raise ValueError(fr'Axiom is a \ceil or \equals rule: {axiom.text}')
             case _:
                 raise ValueError(f'Cannot extract simplification rule from axiom: {axiom.text}')
         req = _extract_condition(_req)

From 069d38bcb9baa22014b93202deb87ab1fbc56073 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 16:39:10 +0000
Subject: [PATCH 12/26] Remove spurious case

Such rules only seem to be generated when KORE anti-left is enabled.
---
 pyk/src/pyk/kore/rule.py | 2 --
 1 file changed, 2 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index 13668be8f4..ec8aa385a1 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -122,8 +122,6 @@ def _extract_lhs(axiom: Axiom) -> tuple[App, Pattern | None, EVar | None]:
         # Cases 0-5 of get_left_hand_side
         # Cases 5-10 of get_requires
         match axiom.pattern:
-            case Rewrites(left=And(ops=(Not(), And(ops=(_req, lhs))))):
-                pass
             case Rewrites(left=And(ops=(lhs, _req))):
                 pass
             case _:

From 88ca3b0995c5de883882f4f9379fa6731d424565 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 17:09:39 +0000
Subject: [PATCH 13/26] Combine `_extract_lhs` and `_extract_rhs`

---
 pyk/src/pyk/kore/rule.py | 39 ++++++++++++++++++---------------------
 1 file changed, 18 insertions(+), 21 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index ec8aa385a1..6d1068d20c 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -101,8 +101,7 @@ class RewriteRule(Rule):
 
     @staticmethod
     def from_axiom(axiom: Axiom) -> RewriteRule:
-        lhs, req, ctx = RewriteRule._extract_lhs(axiom)
-        rhs, ens = RewriteRule._extract_rhs(axiom)
+        lhs, rhs, req, ens, ctx = RewriteRule._extract(axiom)
         priority = _extract_priority(axiom)
         uid = _extract_uid(axiom)
         label = _extract_label(axiom)
@@ -118,38 +117,36 @@ def from_axiom(axiom: Axiom) -> RewriteRule:
         )
 
     @staticmethod
-    def _extract_lhs(axiom: Axiom) -> tuple[App, Pattern | None, EVar | None]:
+    def _extract(axiom: Axiom) -> tuple[App, App, Pattern | None, Pattern | None, EVar | None]:
         # Cases 0-5 of get_left_hand_side
         # Cases 5-10 of get_requires
+        # Case 2 of get_right_hand_side:
+        # 2: rhs(\rewrites(_, \and(X, Y))) = get_builtin(\and(X, Y))
+        # Below is a special case without get_builtin
         match axiom.pattern:
-            case Rewrites(left=And(ops=(lhs, _req))):
+            case Rewrites(left=And(ops=(_lhs, _req)), right=And(ops=(rhs, _ens))):
                 pass
             case _:
-                raise ValueError(f'Cannot extract LHS from axiom: {axiom.text}')
-
-        req = _extract_condition(_req)
+                raise ValueError(f'Cannot extract rewrite rule from axiom: {axiom.text}')
 
         ctx: EVar | None = None
-        match lhs:
-            case App("Lbl'-LT-'generatedTop'-GT-'") as app:
+        match _lhs:
+            case App("Lbl'-LT-'generatedTop'-GT-'") as lhs:
                 pass
-            case And(_, (App("Lbl'-LT-'generatedTop'-GT-'") as app, EVar("Var'Hash'Configuration") as ctx)):
+            case And(_, (App("Lbl'-LT-'generatedTop'-GT-'") as lhs, EVar("Var'Hash'Configuration") as ctx)):
                 pass
+            case _:
+                raise ValueError(f'Cannot extract LHS configuration from axiom: {axiom.text}')
 
-        return app, req, ctx
-
-    @staticmethod
-    def _extract_rhs(axiom: Axiom) -> tuple[App, Pattern | None]:
-        # Case 2 of get_right_hand_side:
-        # 2: rhs(\rewrites(_, \and(X, Y))) = get_builtin(\and(X, Y))
-        # Below is a special case without get_builtin
-        match axiom.pattern:
-            case Rewrites(right=And(ops=(App("Lbl'-LT-'generatedTop'-GT-'") as rhs, _ens))):
+        match rhs:
+            case App("Lbl'-LT-'generatedTop'-GT-'"):
                 pass
             case _:
-                raise ValueError(f'Cannot extract RHS from axiom: {axiom.text}')
+                raise ValueError(f'Cannot extract RHS configuration from axiom: {axiom.text}')
+
+        req = _extract_condition(_req)
         ens = _extract_condition(_ens)
-        return rhs, ens
+        return lhs, rhs, req, ens, ctx
 
 
 @final

From a275957150a8cf4deda13513787498b5cb3d4055 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 17:18:32 +0000
Subject: [PATCH 14/26] Slide `return` statement

---
 pyk/src/pyk/kore/rule.py | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index 6d1068d20c..5058e6d948 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -177,13 +177,17 @@ def _extract_args(axiom: Axiom) -> tuple[tuple[Pattern, ...], Pattern | None]:
         # Cases 7-10 of get_left_hand_side
         # Cases 0-3 of get_requires
         match axiom.pattern:
-            case Implies(left=And(ops=(Not(), And(ops=(_req, pat))))):
-                return FunctionRule._get_patterns(pat), _extract_condition(_req)
-            case Implies(left=And(ops=(_req, pat))):
-                return FunctionRule._get_patterns(pat), _extract_condition(_req)
+            case Implies(left=And(ops=(Not(), And(ops=(_req, _args))))):
+                pass
+            case Implies(left=And(ops=(_req, _args))):
+                pass
             case _:
                 raise ValueError(f'Cannot extract LHS from axiom: {axiom.text}')
 
+        args = FunctionRule._get_patterns(_args)
+        req = _extract_condition(_req)
+        return args, req
+
     @staticmethod
     def _get_patterns(pattern: Pattern) -> tuple[Pattern, ...]:
         # get_patterns(\top()) = []

From 490eb7b102a5a39eea93f5fb449d0b5b37eb1f01 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 17:53:28 +0000
Subject: [PATCH 15/26] Extract function `_extract_rhs`

---
 pyk/src/pyk/kore/rule.py | 22 +++++++++++++++-------
 1 file changed, 15 insertions(+), 7 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index 5058e6d948..b1d13ff0a7 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -124,7 +124,7 @@ def _extract(axiom: Axiom) -> tuple[App, App, Pattern | None, Pattern | None, EV
         # 2: rhs(\rewrites(_, \and(X, Y))) = get_builtin(\and(X, Y))
         # Below is a special case without get_builtin
         match axiom.pattern:
-            case Rewrites(left=And(ops=(_lhs, _req)), right=And(ops=(rhs, _ens))):
+            case Rewrites(left=And(ops=(_lhs, _req)), right=_rhs):
                 pass
             case _:
                 raise ValueError(f'Cannot extract rewrite rule from axiom: {axiom.text}')
@@ -138,14 +138,14 @@ def _extract(axiom: Axiom) -> tuple[App, App, Pattern | None, Pattern | None, EV
             case _:
                 raise ValueError(f'Cannot extract LHS configuration from axiom: {axiom.text}')
 
+        req = _extract_condition(_req)
+        rhs, ens = _extract_rhs(_rhs)
         match rhs:
             case App("Lbl'-LT-'generatedTop'-GT-'"):
                 pass
             case _:
                 raise ValueError(f'Cannot extract RHS configuration from axiom: {axiom.text}')
 
-        req = _extract_condition(_req)
-        ens = _extract_condition(_ens)
         return lhs, rhs, req, ens, ctx
 
 
@@ -204,11 +204,11 @@ def _get_patterns(pattern: Pattern) -> tuple[Pattern, ...]:
     def _extract_rhs(axiom: Axiom) -> tuple[App, Pattern, Pattern | None]:
         # Case 0 of get_right_hand_side
         match axiom.pattern:
-            case Implies(right=Equals(left=App() as app, right=And(ops=(rhs, _ens)))):
+            case Implies(right=Equals(left=App() as app, right=_rhs)):
                 pass
             case _:
                 raise ValueError(f'Cannot extract RHS from axiom: {axiom.text}')
-        ens = _extract_condition(_ens)
+        rhs, ens = _extract_rhs(_rhs)
         return app, rhs, ens
 
 
@@ -238,15 +238,23 @@ def _extract(axiom: Axiom) -> tuple[App, Pattern, Pattern | None, Pattern | None
         # Cases 11-12 of get_left_hand_side
         # Case 0 of get_right_hand_side
         match axiom.pattern:
-            case Implies(left=_req, right=Equals(left=App() as lhs, right=And(ops=(rhs, _ens)))):
+            case Implies(left=_req, right=Equals(left=App() as lhs, right=_rhs)):
                 pass
             case _:
                 raise ValueError(f'Cannot extract simplification rule from axiom: {axiom.text}')
         req = _extract_condition(_req)
-        ens = _extract_condition(_ens)
+        rhs, ens = _extract_rhs(_rhs)
         return lhs, rhs, req, ens
 
 
+def _extract_rhs(pattern: Pattern) -> tuple[Pattern, Pattern | None]:
+    match pattern:
+        case And(ops=(rhs, _ens)):
+            return rhs, _extract_condition(_ens)
+        case _:
+            raise ValueError(f'Cannot extract RHS from pattern: {pattern.text}')
+
+
 def _extract_condition(pattern: Pattern) -> Pattern | None:
     match pattern:
         case Top():

From d5772b3eda76c7bbb1e848868ce7747b60c105c2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 18:01:19 +0000
Subject: [PATCH 16/26] Consolidate cases

---
 pyk/src/pyk/kore/rule.py | 28 +++++++++++++---------------
 1 file changed, 13 insertions(+), 15 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index b1d13ff0a7..088c70b056 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -177,17 +177,17 @@ def _extract_args(axiom: Axiom) -> tuple[tuple[Pattern, ...], Pattern | None]:
         # Cases 7-10 of get_left_hand_side
         # Cases 0-3 of get_requires
         match axiom.pattern:
-            case Implies(left=And(ops=(Not(), And(ops=(_req, _args))))):
-                pass
-            case Implies(left=And(ops=(_req, _args))):
-                pass
+            case Implies(
+                left=And(
+                    ops=(Not(), And(ops=(_req, _args))) | (_req, _args),
+                ),
+            ):
+                args = FunctionRule._get_patterns(_args)
+                req = _extract_condition(_req)
+                return args, req
             case _:
                 raise ValueError(f'Cannot extract LHS from axiom: {axiom.text}')
 
-        args = FunctionRule._get_patterns(_args)
-        req = _extract_condition(_req)
-        return args, req
-
     @staticmethod
     def _get_patterns(pattern: Pattern) -> tuple[Pattern, ...]:
         # get_patterns(\top()) = []
@@ -205,11 +205,10 @@ def _extract_rhs(axiom: Axiom) -> tuple[App, Pattern, Pattern | None]:
         # Case 0 of get_right_hand_side
         match axiom.pattern:
             case Implies(right=Equals(left=App() as app, right=_rhs)):
-                pass
+                rhs, ens = _extract_rhs(_rhs)
+                return app, rhs, ens
             case _:
                 raise ValueError(f'Cannot extract RHS from axiom: {axiom.text}')
-        rhs, ens = _extract_rhs(_rhs)
-        return app, rhs, ens
 
 
 @final
@@ -239,12 +238,11 @@ def _extract(axiom: Axiom) -> tuple[App, Pattern, Pattern | None, Pattern | None
         # Case 0 of get_right_hand_side
         match axiom.pattern:
             case Implies(left=_req, right=Equals(left=App() as lhs, right=_rhs)):
-                pass
+                req = _extract_condition(_req)
+                rhs, ens = _extract_rhs(_rhs)
+                return lhs, rhs, req, ens
             case _:
                 raise ValueError(f'Cannot extract simplification rule from axiom: {axiom.text}')
-        req = _extract_condition(_req)
-        rhs, ens = _extract_rhs(_rhs)
-        return lhs, rhs, req, ens
 
 
 def _extract_rhs(pattern: Pattern) -> tuple[Pattern, Pattern | None]:

From 47d9b10b1d205909145df008cfceefb262a96569 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 20:29:44 +0000
Subject: [PATCH 17/26] Combine `_extract_args` and `_extract_rhs`

---
 pyk/src/pyk/kore/rule.py | 24 ++++++++----------------
 1 file changed, 8 insertions(+), 16 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index 088c70b056..969d687556 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -160,9 +160,7 @@ class FunctionRule(Rule):
 
     @staticmethod
     def from_axiom(axiom: Axiom) -> FunctionRule:
-        args, req = FunctionRule._extract_args(axiom)
-        app, rhs, ens = FunctionRule._extract_rhs(axiom)
-        lhs = app.let(args=args)
+        lhs, rhs, req, ens = FunctionRule._extract(axiom)
         priority = _extract_priority(axiom)
         return FunctionRule(
             lhs=lhs,
@@ -173,20 +171,24 @@ def from_axiom(axiom: Axiom) -> FunctionRule:
         )
 
     @staticmethod
-    def _extract_args(axiom: Axiom) -> tuple[tuple[Pattern, ...], Pattern | None]:
+    def _extract(axiom: Axiom) -> tuple[App, Pattern, Pattern | None, Pattern | None]:
         # Cases 7-10 of get_left_hand_side
         # Cases 0-3 of get_requires
+        # Case 0 of get_right_hand_side
         match axiom.pattern:
             case Implies(
                 left=And(
                     ops=(Not(), And(ops=(_req, _args))) | (_req, _args),
                 ),
+                right=Equals(left=App() as app, right=_rhs),
             ):
                 args = FunctionRule._get_patterns(_args)
+                lhs = app.let(args=args)
                 req = _extract_condition(_req)
-                return args, req
+                rhs, ens = _extract_rhs(_rhs)
+                return lhs, rhs, req, ens
             case _:
-                raise ValueError(f'Cannot extract LHS from axiom: {axiom.text}')
+                raise ValueError(f'Cannot extract function rule from axiom: {axiom.text}')
 
     @staticmethod
     def _get_patterns(pattern: Pattern) -> tuple[Pattern, ...]:
@@ -200,16 +202,6 @@ def _get_patterns(pattern: Pattern) -> tuple[Pattern, ...]:
             case _:
                 raise ValueError(f'Cannot extract argument list from pattern: {pattern.text}')
 
-    @staticmethod
-    def _extract_rhs(axiom: Axiom) -> tuple[App, Pattern, Pattern | None]:
-        # Case 0 of get_right_hand_side
-        match axiom.pattern:
-            case Implies(right=Equals(left=App() as app, right=_rhs)):
-                rhs, ens = _extract_rhs(_rhs)
-                return app, rhs, ens
-            case _:
-                raise ValueError(f'Cannot extract RHS from axiom: {axiom.text}')
-
 
 @final
 @dataclass

From c61dc4760241e0e1d4a422e2d56e3e376102063b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 20:31:52 +0000
Subject: [PATCH 18/26] Rename `_get_patterns` to `_extract_args`

---
 pyk/src/pyk/kore/rule.py | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index 969d687556..b7f8084a4a 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -182,7 +182,7 @@ def _extract(axiom: Axiom) -> tuple[App, Pattern, Pattern | None, Pattern | None
                 ),
                 right=Equals(left=App() as app, right=_rhs),
             ):
-                args = FunctionRule._get_patterns(_args)
+                args = FunctionRule._extract_args(_args)
                 lhs = app.let(args=args)
                 req = _extract_condition(_req)
                 rhs, ens = _extract_rhs(_rhs)
@@ -191,14 +191,12 @@ def _extract(axiom: Axiom) -> tuple[App, Pattern, Pattern | None, Pattern | None
                 raise ValueError(f'Cannot extract function rule from axiom: {axiom.text}')
 
     @staticmethod
-    def _get_patterns(pattern: Pattern) -> tuple[Pattern, ...]:
-        # get_patterns(\top()) = []
-        # get_patterns(\and(\in(_, X), Y)) = X : get_patterns(Y)
+    def _extract_args(pattern: Pattern) -> tuple[Pattern, ...]:
         match pattern:
             case Top():
                 return ()
             case And(ops=(In(left=EVar(), right=arg), rest)):
-                return (arg,) + FunctionRule._get_patterns(rest)
+                return (arg,) + FunctionRule._extract_args(rest)
             case _:
                 raise ValueError(f'Cannot extract argument list from pattern: {pattern.text}')
 

From c62709ef0afd7e35df646769beaac1e34c73667b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 20:35:26 +0000
Subject: [PATCH 19/26] Remove comments referring to LLVM Backend code

---
 pyk/src/pyk/kore/rule.py | 15 ---------------
 1 file changed, 15 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index b7f8084a4a..e7349b06f0 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -1,8 +1,3 @@
-"""Parse KORE axioms into rewrite rules.
-
-Based on the [LLVM Backend's implementation](https://github.com/runtimeverification/llvm-backend/blob/d5eab4b0f0e610bc60843ebb482f79c043b92702/lib/ast/pattern_matching.cpp).
-"""
-
 from __future__ import annotations
 
 from abc import ABC
@@ -118,11 +113,6 @@ def from_axiom(axiom: Axiom) -> RewriteRule:
 
     @staticmethod
     def _extract(axiom: Axiom) -> tuple[App, App, Pattern | None, Pattern | None, EVar | None]:
-        # Cases 0-5 of get_left_hand_side
-        # Cases 5-10 of get_requires
-        # Case 2 of get_right_hand_side:
-        # 2: rhs(\rewrites(_, \and(X, Y))) = get_builtin(\and(X, Y))
-        # Below is a special case without get_builtin
         match axiom.pattern:
             case Rewrites(left=And(ops=(_lhs, _req)), right=_rhs):
                 pass
@@ -172,9 +162,6 @@ def from_axiom(axiom: Axiom) -> FunctionRule:
 
     @staticmethod
     def _extract(axiom: Axiom) -> tuple[App, Pattern, Pattern | None, Pattern | None]:
-        # Cases 7-10 of get_left_hand_side
-        # Cases 0-3 of get_requires
-        # Case 0 of get_right_hand_side
         match axiom.pattern:
             case Implies(
                 left=And(
@@ -224,8 +211,6 @@ def from_axiom(axiom: Axiom) -> SimpliRule:
 
     @staticmethod
     def _extract(axiom: Axiom) -> tuple[App, Pattern, Pattern | None, Pattern | None]:
-        # Cases 11-12 of get_left_hand_side
-        # Case 0 of get_right_hand_side
         match axiom.pattern:
             case Implies(left=_req, right=Equals(left=App() as lhs, right=_rhs)):
                 req = _extract_condition(_req)

From d99531ab9121e39c2b1261e649e38b51765fcdb7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 20:50:30 +0000
Subject: [PATCH 20/26] Strengthen pattern

---
 pyk/src/pyk/kore/rule.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index e7349b06f0..2d218a6505 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -5,7 +5,7 @@
 from typing import TYPE_CHECKING, final
 
 from .prelude import inj
-from .syntax import And, App, Axiom, Ceil, Equals, EVar, Implies, In, Not, Rewrites, SortVar, String, Top
+from .syntax import DV, And, App, Axiom, Ceil, Equals, EVar, Implies, In, Not, Rewrites, SortApp, SortVar, String, Top
 
 if TYPE_CHECKING:
     from typing import Final
@@ -232,7 +232,7 @@ def _extract_condition(pattern: Pattern) -> Pattern | None:
     match pattern:
         case Top():
             return None
-        case Equals(left=cond):
+        case Equals(left=cond, right=DV(SortApp('SortBool'), String('true'))):
             return cond
         case _:
             raise ValueError(f'Cannot extract condition from pattern: {pattern.text}')

From c5e5ac7f703aa913ed4ca00f534e62d7d6cb9fa3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 20:58:27 +0000
Subject: [PATCH 21/26] Add logging

---
 pyk/src/pyk/kore/rule.py | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index 2d218a6505..f19beb1714 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -1,5 +1,6 @@
 from __future__ import annotations
 
+import logging
 from abc import ABC
 from dataclasses import dataclass
 from typing import TYPE_CHECKING, final
@@ -15,6 +16,9 @@
     Attrs = dict[str, tuple[Pattern, ...]]
 
 
+_LOGGER: Final = logging.getLogger(__name__)
+
+
 # There's a simplification rule with irregular form in the prelude module INJ.
 # This rule is skipped in Rule.extract_all.
 _S1, _S2, _S3, _R = (SortVar(name) for name in ['S1', 'S2', 'S3', 'R'])
@@ -77,6 +81,7 @@ def _is_rule(axiom: Axiom) -> bool:
                         right=And(ops=(_, Top() | Equals())),
                     ),
                 ):
+                    _LOGGER.info(fr'Skipping \ceil or \equals simplification rule: {axiom.text}')
                     return False
 
         return True

From 058b0aa59dc4908a5bf9e2e74f653948fe394795 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 20:59:55 +0000
Subject: [PATCH 22/26] Nest function

---
 pyk/src/pyk/kore/rule.py | 45 ++++++++++++++++++++--------------------
 1 file changed, 22 insertions(+), 23 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index f19beb1714..8fb49eb9d6 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -62,29 +62,28 @@ def from_axiom(axiom: Axiom) -> Rule:
 
     @staticmethod
     def extract_all(defn: Definition) -> list[Rule]:
-        return [Rule.from_axiom(axiom) for axiom in defn.axioms if Rule._is_rule(axiom)]
-
-    @staticmethod
-    def _is_rule(axiom: Axiom) -> bool:
-        if axiom == _INJ_AXIOM:
-            return False
-
-        if any(attr in axiom.attrs_by_key for attr in _SKIPPED_ATTRS):
-            return False
-
-        if 'simplification' in axiom.attrs_by_key:
-            match axiom.pattern:
-                case Implies(
-                    left=Top() | Equals(),
-                    right=Equals(
-                        left=Ceil() | Equals(),
-                        right=And(ops=(_, Top() | Equals())),
-                    ),
-                ):
-                    _LOGGER.info(fr'Skipping \ceil or \equals simplification rule: {axiom.text}')
-                    return False
-
-        return True
+        def is_rule(axiom: Axiom) -> bool:
+            if axiom == _INJ_AXIOM:
+                return False
+
+            if any(attr in axiom.attrs_by_key for attr in _SKIPPED_ATTRS):
+                return False
+
+            if 'simplification' in axiom.attrs_by_key:
+                match axiom.pattern:
+                    case Implies(
+                        left=Top() | Equals(),
+                        right=Equals(
+                            left=Ceil() | Equals(),
+                            right=And(ops=(_, Top() | Equals())),
+                        ),
+                    ):
+                        _LOGGER.info(fr'Skipping \ceil or \equals simplification rule: {axiom.text}')
+                        return False
+
+            return True
+
+        return [Rule.from_axiom(axiom) for axiom in defn.axioms if is_rule(axiom)]
 
 
 @final

From 226fa8bce90445ce942598dad5589ef301636208 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Mon, 2 Dec 2024 10:46:01 +0000
Subject: [PATCH 23/26] Extract subclass `AppRule`

---
 pyk/src/pyk/kore/rule.py | 18 +++++++++++++-----
 1 file changed, 13 insertions(+), 5 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index 8fb49eb9d6..9ad0274ee1 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -56,7 +56,7 @@ def from_axiom(axiom: Axiom) -> Rule:
             return RewriteRule.from_axiom(axiom)
 
         if 'simplification' in axiom.attrs_by_key:
-            return SimpliRule.from_axiom(axiom)
+            return AppRule.from_axiom(axiom)
 
         return FunctionRule.from_axiom(axiom)
 
@@ -192,9 +192,17 @@ def _extract_args(pattern: Pattern) -> tuple[Pattern, ...]:
                 raise ValueError(f'Cannot extract argument list from pattern: {pattern.text}')
 
 
+class SimpliRule(Rule, ABC):
+    lhs: Pattern
+    rhs: Pattern
+    req: Pattern | None
+    ens: Pattern | None
+    priority: int
+
+
 @final
 @dataclass
-class SimpliRule(Rule):
+class AppRule(SimpliRule):
     lhs: App
     rhs: Pattern
     req: Pattern | None
@@ -202,10 +210,10 @@ class SimpliRule(Rule):
     priority: int
 
     @staticmethod
-    def from_axiom(axiom: Axiom) -> SimpliRule:
-        lhs, rhs, req, ens = SimpliRule._extract(axiom)
+    def from_axiom(axiom: Axiom) -> AppRule:
+        lhs, rhs, req, ens = AppRule._extract(axiom)
         priority = _extract_priority(axiom)
-        return SimpliRule(
+        return AppRule(
             lhs=lhs,
             rhs=rhs,
             req=req,

From c0b3c848617b25985c556cd8bdb4b45aa00376be Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Mon, 2 Dec 2024 12:23:32 +0000
Subject: [PATCH 24/26] Add `EqualsRule` and `CeilRule`

---
 pyk/src/pyk/kore/rule.py | 126 +++++++++++++++++++++++++++++----------
 1 file changed, 93 insertions(+), 33 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index 9ad0274ee1..5cd753abd7 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -3,19 +3,39 @@
 import logging
 from abc import ABC
 from dataclasses import dataclass
-from typing import TYPE_CHECKING, final
+from typing import TYPE_CHECKING, Generic, TypeVar, final
 
 from .prelude import inj
-from .syntax import DV, And, App, Axiom, Ceil, Equals, EVar, Implies, In, Not, Rewrites, SortApp, SortVar, String, Top
+from .syntax import (
+    DV,
+    And,
+    App,
+    Axiom,
+    Ceil,
+    Equals,
+    EVar,
+    Implies,
+    In,
+    Not,
+    Pattern,
+    Rewrites,
+    SortApp,
+    SortVar,
+    String,
+    Top,
+)
 
 if TYPE_CHECKING:
     from typing import Final
 
-    from .syntax import Definition, Pattern
+    from .syntax import Definition
 
     Attrs = dict[str, tuple[Pattern, ...]]
 
 
+P = TypeVar('P', bound=Pattern)
+
+
 _LOGGER: Final = logging.getLogger(__name__)
 
 
@@ -55,10 +75,18 @@ def from_axiom(axiom: Axiom) -> Rule:
         if isinstance(axiom.pattern, Rewrites):
             return RewriteRule.from_axiom(axiom)
 
-        if 'simplification' in axiom.attrs_by_key:
-            return AppRule.from_axiom(axiom)
+        if 'simplification' not in axiom.attrs_by_key:
+            return FunctionRule.from_axiom(axiom)
 
-        return FunctionRule.from_axiom(axiom)
+        match axiom.pattern:
+            case Implies(right=Equals(left=App())):
+                return AppRule.from_axiom(axiom)
+            case Implies(right=Equals(left=Ceil())):
+                return CeilRule.from_axiom(axiom)
+            case Implies(right=Equals(left=Equals())):
+                return EqualsRule.from_axiom(axiom)
+            case _:
+                raise ValueError(f'Cannot parse simplification rule: {axiom.text}')
 
     @staticmethod
     def extract_all(defn: Definition) -> list[Rule]:
@@ -69,18 +97,6 @@ def is_rule(axiom: Axiom) -> bool:
             if any(attr in axiom.attrs_by_key for attr in _SKIPPED_ATTRS):
                 return False
 
-            if 'simplification' in axiom.attrs_by_key:
-                match axiom.pattern:
-                    case Implies(
-                        left=Top() | Equals(),
-                        right=Equals(
-                            left=Ceil() | Equals(),
-                            right=And(ops=(_, Top() | Equals())),
-                        ),
-                    ):
-                        _LOGGER.info(fr'Skipping \ceil or \equals simplification rule: {axiom.text}')
-                        return False
-
             return True
 
         return [Rule.from_axiom(axiom) for axiom in defn.axioms if is_rule(axiom)]
@@ -192,28 +208,58 @@ def _extract_args(pattern: Pattern) -> tuple[Pattern, ...]:
                 raise ValueError(f'Cannot extract argument list from pattern: {pattern.text}')
 
 
-class SimpliRule(Rule, ABC):
-    lhs: Pattern
+class SimpliRule(Rule, Generic[P], ABC):
+    lhs: P
+
+    @staticmethod
+    def _extract(axiom: Axiom, lhs_type: type[P]) -> tuple[P, Pattern, Pattern | None, Pattern | None]:
+        match axiom.pattern:
+            case Implies(left=_req, right=Equals(left=lhs, right=_rhs)):
+                req = _extract_condition(_req)
+                rhs, ens = _extract_rhs(_rhs)
+                if not isinstance(lhs, lhs_type):
+                    raise ValueError(f'Invalid LHS type from simplification axiom: {axiom.text}')
+                return lhs, rhs, req, ens
+            case _:
+                raise ValueError(f'Cannot extract simplification rule from axiom: {axiom.text}')
+
+
+@final
+@dataclass
+class AppRule(SimpliRule[App]):
+    lhs: App
     rhs: Pattern
     req: Pattern | None
     ens: Pattern | None
     priority: int
 
+    @staticmethod
+    def from_axiom(axiom: Axiom) -> AppRule:
+        lhs, rhs, req, ens = SimpliRule._extract(axiom, App)
+        priority = _extract_priority(axiom)
+        return AppRule(
+            lhs=lhs,
+            rhs=rhs,
+            req=req,
+            ens=ens,
+            priority=priority,
+        )
+
 
 @final
 @dataclass
-class AppRule(SimpliRule):
-    lhs: App
+class CeilRule(SimpliRule):
+    lhs: Ceil
     rhs: Pattern
     req: Pattern | None
     ens: Pattern | None
     priority: int
 
     @staticmethod
-    def from_axiom(axiom: Axiom) -> AppRule:
-        lhs, rhs, req, ens = AppRule._extract(axiom)
+    def from_axiom(axiom: Axiom) -> CeilRule:
+        lhs, rhs, req, ens = SimpliRule._extract(axiom, Ceil)
         priority = _extract_priority(axiom)
-        return AppRule(
+        return CeilRule(
             lhs=lhs,
             rhs=rhs,
             req=req,
@@ -221,15 +267,29 @@ def from_axiom(axiom: Axiom) -> AppRule:
             priority=priority,
         )
 
+
+@final
+@dataclass
+class EqualsRule(SimpliRule):
+    lhs: Equals
+    rhs: Pattern
+    req: Pattern | None
+    ens: Pattern | None
+    priority: int
+
     @staticmethod
-    def _extract(axiom: Axiom) -> tuple[App, Pattern, Pattern | None, Pattern | None]:
-        match axiom.pattern:
-            case Implies(left=_req, right=Equals(left=App() as lhs, right=_rhs)):
-                req = _extract_condition(_req)
-                rhs, ens = _extract_rhs(_rhs)
-                return lhs, rhs, req, ens
-            case _:
-                raise ValueError(f'Cannot extract simplification rule from axiom: {axiom.text}')
+    def from_axiom(axiom: Axiom) -> EqualsRule:
+        lhs, rhs, req, ens = SimpliRule._extract(axiom, Equals)
+        if not isinstance(lhs, Equals):
+            raise ValueError(f'Cannot extract LHS as Equals from axiom: {axiom.text}')
+        priority = _extract_priority(axiom)
+        return EqualsRule(
+            lhs=lhs,
+            rhs=rhs,
+            req=req,
+            ens=ens,
+            priority=priority,
+        )
 
 
 def _extract_rhs(pattern: Pattern) -> tuple[Pattern, Pattern | None]:

From 86d1ca99ab6cdbc930ab1f20a26b0e1a20adde06 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Mon, 2 Dec 2024 12:53:12 +0000
Subject: [PATCH 25/26] Freeze data classes

---
 pyk/src/pyk/kore/rule.py | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index 5cd753abd7..8bc7fb965e 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -103,7 +103,7 @@ def is_rule(axiom: Axiom) -> bool:
 
 
 @final
-@dataclass
+@dataclass(frozen=True)
 class RewriteRule(Rule):
     lhs: App
     rhs: App
@@ -160,7 +160,7 @@ def _extract(axiom: Axiom) -> tuple[App, App, Pattern | None, Pattern | None, EV
 
 
 @final
-@dataclass
+@dataclass(frozen=True)
 class FunctionRule(Rule):
     lhs: App
     rhs: Pattern
@@ -225,7 +225,7 @@ def _extract(axiom: Axiom, lhs_type: type[P]) -> tuple[P, Pattern, Pattern | Non
 
 
 @final
-@dataclass
+@dataclass(frozen=True)
 class AppRule(SimpliRule[App]):
     lhs: App
     rhs: Pattern
@@ -247,7 +247,7 @@ def from_axiom(axiom: Axiom) -> AppRule:
 
 
 @final
-@dataclass
+@dataclass(frozen=True)
 class CeilRule(SimpliRule):
     lhs: Ceil
     rhs: Pattern
@@ -269,7 +269,7 @@ def from_axiom(axiom: Axiom) -> CeilRule:
 
 
 @final
-@dataclass
+@dataclass(frozen=True)
 class EqualsRule(SimpliRule):
     lhs: Equals
     rhs: Pattern

From d71f6f6c5524bb0b0dae8a419e5049601e6f7a0e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Mon, 2 Dec 2024 13:07:26 +0000
Subject: [PATCH 26/26] Adjust test

---
 pyk/src/tests/integration/kore/test_rule.py | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/pyk/src/tests/integration/kore/test_rule.py b/pyk/src/tests/integration/kore/test_rule.py
index 5f723146d8..fadb530548 100644
--- a/pyk/src/tests/integration/kore/test_rule.py
+++ b/pyk/src/tests/integration/kore/test_rule.py
@@ -18,7 +18,7 @@
 @pytest.fixture(scope='module')
 def definition(kompile: Kompiler) -> Definition:
     main_file = K_FILES / 'imp.k'
-    definition_dir = kompile(main_file=main_file)
+    definition_dir = kompile(main_file=main_file, backend='haskell')
     kore_file = definition_dir / 'definition.kore'
     kore_text = kore_file.read_text()
     definition = KoreParser(kore_text).definition()
@@ -33,4 +33,6 @@ def test_extract_all(definition: Definition) -> None:
     cnt = Counter(type(rule).__name__ for rule in rules)
     assert cnt['RewriteRule']
     assert cnt['FunctionRule']
-    assert cnt['SimpliRule']
+    assert cnt['AppRule']
+    assert cnt['CeilRule']
+    assert cnt['EqualsRule']