Ordered constraint accumulation

docs/conf.py

@@ -9,8 +9,8 @@
 project = 'pyk'
 author = 'Runtime Verification, Inc'
 copyright = '2024, Runtime Verification, Inc'
-version = '0.1.779'
-release = '0.1.779'
+version = '0.1.780'
+release = '0.1.780'
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

package/version

@@ -1 +1 @@
-0.1.779
+0.1.780

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.779"
+version = "0.1.780"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/pyk/cterm/cterm.py

@@ -93,11 +93,12 @@ def _check_config(config: KInner) -> None:
             raise ValueError(f'Expected cell label, found: {config}')
 
     @staticmethod
-    def _normalize_constraints(constraints: Iterable[KInner]) -> tuple[KInner, ...]:
+    def _normalize_constraints(constraints: Iterable[KInner], maintain_order: bool = False) -> tuple[KInner, ...]:
         constraints = (constraint for _constraint in constraints for constraint in flatten_label('#And', _constraint))
         constraints = unique(constraints)
         constraints = (constraint for constraint in constraints if not CTerm._is_spurious_constraint(constraint))
-        constraints = sorted(constraints, key=CTerm._constraint_sort_key)
+        if not maintain_order:
+            constraints = sorted(constraints, key=CTerm._constraint_sort_key)
         return tuple(constraints)
 
     @staticmethod
@@ -314,10 +315,14 @@ class CSubst:
     subst: Subst
     constraints: tuple[KInner, ...]
 
-    def __init__(self, subst: Subst | None = None, constraints: Iterable[KInner] = ()) -> None:
+    def __init__(
+        self, subst: Subst | None = None, constraints: Iterable[KInner] = (), maintain_order: bool = False
+    ) -> None:
         """Construct a new `CSubst` given a `Subst` and set of constraints as `KInner`, performing basic sanity checks."""
         object.__setattr__(self, 'subst', subst if subst is not None else Subst({}))
-        object.__setattr__(self, 'constraints', CTerm._normalize_constraints(constraints))
+        object.__setattr__(
+            self, 'constraints', CTerm._normalize_constraints(constraints, maintain_order=maintain_order)
+        )
 
     def __iter__(self) -> Iterator[Subst | KInner]:
         """Return an iterator with the head being the `subst` and the tail being the `constraints`."""
@@ -344,7 +349,7 @@ def constraint(self) -> KInner:
 
     def add_constraint(self, constraint: KInner) -> CSubst:
         """Return this `CSubst` with an additional constraint added."""
-        return CSubst(self.subst, list(self.constraints) + [constraint])
+        return CSubst(self.subst, list(self.constraints) + [constraint], maintain_order=True)
 
     def apply(self, cterm: CTerm) -> CTerm:
         """Apply this `CSubst` to the given `CTerm` (instantiating the free variables, and adding the constraints)."""

src/pyk/kcfg/kcfg.py

@@ -1054,8 +1054,8 @@ def lift_split_split(self, b_id: NodeIdLike) -> None:
         # the constraints are cumulative, resulting in `cond_B #And cond_I`
         additional_csubsts = [
             not_none(a.cterm.match_with_constraint(self.node(ci).cterm))
-            .add_constraint(csubst.constraint)
             .add_constraint(csubst_b.constraint)
+            .add_constraint(csubst.constraint)
             for ci, csubst in splits_from_b.items()
         ]
         # Create the targets of the new split

src/tests/unit/test_kcfg.py

@@ -752,6 +752,102 @@ def test_minimize_02() -> None:
     assert contains_edge(cfg, 8, 6, 40, ('r1', 'r3'))
 
 
+def test_split_constraint_accumulation() -> None:
+    def x_ge(n: int) -> KApply:
+        return mlEqualsTrue(geInt(KVariable('X'), intToken(n)))
+
+    def x_lt(n: int) -> KApply:
+        return mlEqualsTrue(ltInt(KVariable('X'), intToken(n)))
+
+    d = {
+        'next': 16,
+        'nodes': node_dicts(15, config=x_config()),
+        'edges': edge_dicts(),
+        'splits': split_dicts(
+            (1, [(2, x_ge(0)), (3, x_lt(0))]),
+            (2, [(4, x_ge(32)), (5, x_lt(32))]),
+            (3, [(6, x_ge(-32)), (7, x_lt(-32))]),
+            (4, [(8, x_ge(64)), (9, x_lt(64))]),
+            (5, [(10, x_ge(16)), (11, x_lt(16))]),
+            (6, [(12, x_ge(-16)), (13, x_lt(-16))]),
+            (7, [(14, x_ge(-64)), (15, x_lt(-64))]),
+            csubst=x_subst(),
+        ),
+    }
+    cfg = KCFG.from_dict(d)
+    propagate_split_constraints(cfg)
+
+    cfg.minimize()
+
+    kcfg_show = KCFGShow(MockKPrint(), node_printer=NodePrinter(MockKPrint()))
+    actual = '\n'.join(kcfg_show.pretty(cfg)) + '\n'
+
+    expected = (
+        '\n'
+        '┌─ 1 (root, split)\n'
+        '┃\n'
+        '┃ (branch)\n'
+        '┣━━┓ constraints:\n'
+        '┃  ┃     _>=Int_ ( X , 0 )\n'
+        '┃  ┃     _>=Int_ ( X , 32 )\n'
+        '┃  ┃     _>=Int_ ( X , 64 )\n'
+        '┃  │\n'
+        '┃  └─ 8 (leaf)\n'
+        '┃\n'
+        '┣━━┓ constraints:\n'
+        '┃  ┃     _>=Int_ ( X , 0 )\n'
+        '┃  ┃     _>=Int_ ( X , 32 )\n'
+        '┃  ┃     _<Int_ ( X , 64 )\n'
+        '┃  │\n'
+        '┃  └─ 9 (leaf)\n'
+        '┃\n'
+        '┣━━┓ constraints:\n'
+        '┃  ┃     _>=Int_ ( X , 0 )\n'
+        '┃  ┃     _<Int_ ( X , 32 )\n'
+        '┃  ┃     _>=Int_ ( X , 16 )\n'
+        '┃  │\n'
+        '┃  └─ 10 (leaf)\n'
+        '┃\n'
+        '┣━━┓ constraints:\n'
+        '┃  ┃     _>=Int_ ( X , 0 )\n'
+        '┃  ┃     _<Int_ ( X , 32 )\n'
+        '┃  ┃     _<Int_ ( X , 16 )\n'
+        '┃  │\n'
+        '┃  └─ 11 (leaf)\n'
+        '┃\n'
+        '┣━━┓ constraints:\n'
+        '┃  ┃     _<Int_ ( X , 0 )\n'
+        '┃  ┃     _>=Int_ ( X , -32 )\n'
+        '┃  ┃     _>=Int_ ( X , -16 )\n'
+        '┃  │\n'
+        '┃  └─ 12 (leaf)\n'
+        '┃\n'
+        '┣━━┓ constraints:\n'
+        '┃  ┃     _<Int_ ( X , 0 )\n'
+        '┃  ┃     _>=Int_ ( X , -32 )\n'
+        '┃  ┃     _<Int_ ( X , -16 )\n'
+        '┃  │\n'
+        '┃  └─ 13 (leaf)\n'
+        '┃\n'
+        '┣━━┓ constraints:\n'
+        '┃  ┃     _<Int_ ( X , 0 )\n'
+        '┃  ┃     _<Int_ ( X , -32 )\n'
+        '┃  ┃     _>=Int_ ( X , -64 )\n'
+        '┃  │\n'
+        '┃  └─ 14 (leaf)\n'
+        '┃\n'
+        '┗━━┓ constraints:\n'
+        '   ┃     _<Int_ ( X , 0 )\n'
+        '   ┃     _<Int_ ( X , -32 )\n'
+        '   ┃     _<Int_ ( X , -64 )\n'
+        '   │\n'
+        '   └─ 15 (leaf)\n'
+        '\n'
+    )
+
+    assert actual == expected
+
+
 def test_split_csubsts() -> None:
     cfg = KCFG()
     cfg.create_node(term(11))