Allowing multiple constraints in splits preceding nodes to be refuted (…

…runtimeverification/pyk#1066)

Currently, the refutation mechanism cannot handle the case in which the
split preceding the node to be refuted contains more than one
constraint. Such scenarios, however, have become commonplace given the
newly introduced KCFG minimization mechanism.

This PR extends the refutation mechanism by allowing it to handle splits
with multiple constraints.

---------

Co-authored-by: devops <devops@runtimeverification.com>

pyk/docs/conf.py

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

pyk/package/version

@@ -1 +1 @@
-0.1.776
+0.1.777

pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.776"
+version = "0.1.777"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

pyk/src/pyk/proof/reachability.py

@@ -584,13 +584,8 @@ def construct_node_refutation(self, node: KCFG.Node) -> RefutationProof | None:
                 f'Cannot refute node {node.id}: unexpected non-identity substitution {csubst.subst} in Split from {closest_branch.source.id}'
             )
             return None
-        if len(csubst.constraints) > 1:
-            _LOGGER.error(
-                f'Cannot refute node {node.id}: unexpected non-singleton constraints {csubst.constraints} in Split from {closest_branch.source.id}'
-            )
-            return None
 
-        last_constraint = ml_pred_to_bool(csubst.constraints[0])
+        last_constraint = ml_pred_to_bool(csubst.constraint)
         relevant_vars = free_vars(last_constraint)
         pre_split_constraints = [
             ml_pred_to_bool(c)

pyk/src/tests/integration/proof/test_refute_node.py

@@ -5,6 +5,7 @@
 
 import pytest
 
+from pyk.cterm import CTerm
 from pyk.kast import Atts, KAtt
 from pyk.kast.inner import KApply, KRewrite, KSequence, KToken, KVariable
 from pyk.kast.manip import free_vars
@@ -15,7 +16,7 @@
 from pyk.prelude.ml import is_top, mlEqualsTrue
 from pyk.proof import APRProof, APRProver, ImpliesProver, ProofStatus, RefutationProof
 from pyk.testing import KCFGExploreTest, KProveTest
-from pyk.utils import single
+from pyk.utils import not_none, single
 
 from ..utils import K_FILES
 
@@ -25,7 +26,6 @@
 
     from pytest import TempPathFactory
 
-    from pyk.cterm import CTerm
     from pyk.kast.inner import KInner
     from pyk.kast.outer import KDefinition
     from pyk.kcfg import KCFGExplore
@@ -317,3 +317,68 @@ def test_apr_proof_refute_node_to_claim(
         )
 
         assert claim == expected
+
+    def test_apr_proof_refute_node_multiple_constraints(
+        self,
+        kprove: KProve,
+        proof_dir: Path,
+        kcfg_explore: KCFGExplore,
+    ) -> None:
+        # Given
+        spec_file = K_FILES / 'refute-node-spec.k'
+        spec_module = 'REFUTE-NODE-SPEC'
+        claim_id = 'multi-constraint-split'
+
+        prover = self.build_prover(kprove, proof_dir, kcfg_explore, spec_file, spec_module, claim_id)
+        cfg = prover.proof.kcfg
+
+        config = cfg.node(1).cterm.config
+        l_gt_0 = mlEqualsTrue(gtInt(KVariable('L'), intToken(0)))
+        l_le_0 = mlEqualsTrue(leInt(KVariable('L'), intToken(0)))
+        m_gt_0 = mlEqualsTrue(gtInt(KVariable('M'), intToken(0)))
+        m_le_0 = mlEqualsTrue(leInt(KVariable('M'), intToken(0)))
+
+        cfg.create_node(CTerm(config, [l_gt_0, m_gt_0]))
+        cfg.create_node(CTerm(config, [l_gt_0, m_le_0]))
+        cfg.create_node(CTerm(config, [l_le_0, m_gt_0]))
+        cfg.create_node(CTerm(config, [l_le_0, m_le_0]))
+
+        prover.proof.kcfg.create_split(
+            1,
+            [
+                (
+                    3,
+                    not_none(cfg.node(1).cterm.match_with_constraint(cfg.node(3).cterm))
+                    .add_constraint(l_gt_0)
+                    .add_constraint(m_gt_0),
+                ),
+                (
+                    4,
+                    not_none(cfg.node(1).cterm.match_with_constraint(cfg.node(4).cterm))
+                    .add_constraint(l_gt_0)
+                    .add_constraint(m_le_0),
+                ),
+                (
+                    5,
+                    not_none(cfg.node(1).cterm.match_with_constraint(cfg.node(5).cterm))
+                    .add_constraint(l_le_0)
+                    .add_constraint(m_gt_0),
+                ),
+                (
+                    6,
+                    not_none(cfg.node(1).cterm.match_with_constraint(cfg.node(6).cterm))
+                    .add_constraint(l_le_0)
+                    .add_constraint(m_gt_0),
+                ),
+            ],
+        )
+
+        # When
+        prover.advance_proof(max_iterations=4)
+        # After the minimization, nodes 7-10 created by the advancement of the proof
+        # will have multiple constraints in their immediately preceding splits
+        prover.proof.kcfg.minimize()
+
+        # Then
+        for i in [7, 8, 9, 10]:
+            assert prover.proof.refute_node(cfg.node(i)) is not None

pyk/src/tests/integration/test-data/k-files/refute-node-spec.k

@@ -8,4 +8,6 @@ module REFUTE-NODE-SPEC
     claim [split-int-succeed]: <k> a(N) => f(N) ... </k>
 
     claim [triple-split-int-fail]: <k> g(L +Int N, M, N) => e(N +Int 1) ... </k>
+
+    claim [multi-constraint-split]: <k> g(L, M, N) => e(N +Int 1) ... </k>
 endmodule