Add ability to pass in custom function to KCFGExplore for modifying new nodes (#498)

This PR adds the ability to pass in a function simplify_node:
CTerm->CTerm to `KCFGExplore()` which modifies new nodes as they are
added during exploration. This is intended to be used to accomplish
runtimeverification/evm-semantics#1909.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>

Author: 3 people

package/version

@@ -1 +1 @@
-0.1.338
+0.1.339

pyproject.toml

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

src/pyk/proof/reachability.py

@@ -257,16 +257,19 @@ class APRProver:
     proof: APRProof
     _is_terminal: Callable[[CTerm], bool] | None
     _extract_branches: Callable[[CTerm], Iterable[KInner]] | None
+    _abstract_node: Callable[[CTerm], CTerm] | None
 
     def __init__(
         self,
         proof: APRProof,
         is_terminal: Callable[[CTerm], bool] | None = None,
         extract_branches: Callable[[CTerm], Iterable[KInner]] | None = None,
+        abstract_node: Callable[[CTerm], CTerm] | None = None,
     ) -> None:
         self.proof = proof
         self._is_terminal = is_terminal
         self._extract_branches = extract_branches
+        self._abstract_node = abstract_node
 
     def _check_terminal(self, curr_node: KCFG.Node) -> bool:
         if self._is_terminal is not None:
@@ -290,6 +293,18 @@ def _check_subsume(self, kcfg_explore: KCFGExplore, node: KCFG.Node) -> bool:
             return True
         return False
 
+    def _check_abstract(self, node: KCFG.Node) -> bool:
+        if self._abstract_node is None:
+            return False
+
+        new_cterm = self._abstract_node(node.cterm)
+        if new_cterm == node.cterm:
+            return False
+
+        new_node = self.proof.kcfg.create_node(new_cterm)
+        self.proof.kcfg.create_cover(node.id, new_node.id)
+        return True
+
     def advance_proof(
         self,
         kcfg_explore: KCFGExplore,
@@ -316,6 +331,9 @@ def advance_proof(
             if self._check_terminal(curr_node):
                 continue
 
+            if self._check_abstract(curr_node):
+                continue
+
             if self._extract_branches is not None and len(self.proof.kcfg.splits(target_id=curr_node.id)) == 0:
                 branches = list(self._extract_branches(curr_node.cterm))
                 if len(branches) > 0:
@@ -349,8 +367,9 @@ def __init__(
         same_loop: Callable[[CTerm, CTerm], bool],
         is_terminal: Callable[[CTerm], bool] | None = None,
         extract_branches: Callable[[CTerm], Iterable[KInner]] | None = None,
+        abstract_node: Callable[[CTerm], CTerm] | None = None,
     ) -> None:
-        super().__init__(proof, is_terminal=is_terminal, extract_branches=extract_branches)
+        super().__init__(proof, is_terminal=is_terminal, extract_branches=extract_branches, abstract_node=abstract_node)
         self._same_loop = same_loop
         self._checked_nodes = []