Ordered constraint accumulation (#4249)

Transfer of: runtimeverification/pyk#1065
runtimeverification · Apr 22, 2024 · f6a39b8 · f6a39b8
2 parents 5f7dc66 + dd26ca9
commit f6a39b8
Show file tree

Hide file tree

Showing 5 changed files with 102 additions and 7 deletions.
diff --git a/pyk/regression-new/kprove-haskell/sum-spec.k.out b/pyk/regression-new/kprove-haskell/sum-spec.k.out
@@ -69,8 +69,8 @@ Subproofs: 0
 ┃  │       </generatedCounter>
 ┃  │     </generatedTop>
 ┃  │     #And { true #Equals N:Int >Int 0 }
-┃  │     #And { true #Equals N:Int >=Int 0 }
 ┃  │     #And { true #Equals N:Int +Int -1 >=Int 0 }
+┃  │     #And { true #Equals N:Int >=Int 0 }
 ┃  │
 ┃  ┊  constraint: OMITTED CONSTRAINT
 ┃  ┊  subst: OMITTED SUBST

diff --git a/pyk/src/pyk/cterm/cterm.py b/pyk/src/pyk/cterm/cterm.py
@@ -97,7 +97,6 @@ def _normalize_constraints(constraints: Iterable[KInner]) -> 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)
         return tuple(constraints)
 
     @staticmethod
@@ -207,7 +206,7 @@ def _ml_impl(antecedents: Iterable[KInner], consequents: Iterable[KInner]) -> KI
 
     def add_constraint(self, new_constraint: KInner) -> CTerm:
         """Return a new `CTerm` with the additional constraints."""
-        return CTerm(self.config, [new_constraint] + list(self.constraints))
+        return CTerm(self.config, list(self.constraints) + [new_constraint])
 
     def anti_unify(
         self, other: CTerm, keep_values: bool = False, kdef: KDefinition | None = None

diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/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

diff --git a/pyk/src/tests/integration/proof/test_imp.py b/pyk/src/tests/integration/proof/test_imp.py
@@ -1268,9 +1268,6 @@ def test_anti_unify_keep_values(
             state=f'N |-> {abstracted_var.name}:Int',
             constraint=mlAnd(
                 [
-                    mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])),
-                    mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])),
-                    mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])),
                     mlEqualsTrue(
                         orBool(
                             [
@@ -1289,6 +1286,9 @@ def test_anti_unify_keep_values(
                             ]
                         )
                     ),
+                    mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])),
+                    mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])),
+                    mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])),
                 ]
             ),
         )

diff --git a/pyk/src/tests/unit/test_kcfg.py b/pyk/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))