From 098d73704a5494163a810253f5dc319eaeee86e3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Petar=20Maksimovi=C4=87?= Date: Sat, 6 Apr 2024 11:43:37 +0100 Subject: [PATCH] Allowing multiple constraints in splits preceding nodes to be refuted (https://github.com/runtimeverification/pyk/pull/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 --- pyk/docs/conf.py | 4 +- pyk/package/version | 2 +- pyk/pyproject.toml | 2 +- pyk/src/pyk/proof/reachability.py | 7 +- .../integration/proof/test_refute_node.py | 69 ++++++++++++++++++- .../test-data/k-files/refute-node-spec.k | 2 + 6 files changed, 74 insertions(+), 12 deletions(-) diff --git a/pyk/docs/conf.py b/pyk/docs/conf.py index 48e4480ebb7..26cf730b314 100644 --- a/pyk/docs/conf.py +++ b/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 diff --git a/pyk/package/version b/pyk/package/version index 83a470132e4..da9223fb727 100644 --- a/pyk/package/version +++ b/pyk/package/version @@ -1 +1 @@ -0.1.776 +0.1.777 diff --git a/pyk/pyproject.toml b/pyk/pyproject.toml index d4567b587f6..a128f511ad7 100644 --- a/pyk/pyproject.toml +++ b/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. ", diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 3326365976e..09ccdc6ecf5 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/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) diff --git a/pyk/src/tests/integration/proof/test_refute_node.py b/pyk/src/tests/integration/proof/test_refute_node.py index 5bd68f58c2f..b41c409bff8 100644 --- a/pyk/src/tests/integration/proof/test_refute_node.py +++ b/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 diff --git a/pyk/src/tests/integration/test-data/k-files/refute-node-spec.k b/pyk/src/tests/integration/test-data/k-files/refute-node-spec.k index ce653a4bffd..d64aed39742 100644 --- a/pyk/src/tests/integration/test-data/k-files/refute-node-spec.k +++ b/pyk/src/tests/integration/test-data/k-files/refute-node-spec.k @@ -8,4 +8,6 @@ module REFUTE-NODE-SPEC claim [split-int-succeed]: a(N) => f(N) ... claim [triple-split-int-fail]: g(L +Int N, M, N) => e(N +Int 1) ... + + claim [multi-constraint-split]: g(L, M, N) => e(N +Int 1) ... endmodule