Generic state merging, cover pullbacks

package/version

@@ -1 +1 @@
-0.1.371
+0.1.372

pyproject.toml

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

src/pyk/cterm.py

@@ -7,6 +7,7 @@
 
 from .kast.inner import KApply, KAtt, KInner, KRewrite, KVariable, Subst
 from .kast.manip import (
+    anti_unify,
     apply_existential_substitutions,
     count_vars,
     flatten_label,
@@ -137,6 +138,29 @@ def _ml_impl(antecedents: Iterable[KInner], consequents: Iterable[KInner]) -> KI
     def add_constraint(self, new_constraint: KInner) -> CTerm:
         return CTerm(self.config, [new_constraint] + list(self.constraints))
 
+    def anti_unify(self, other: CTerm) -> tuple[CTerm, CSubst, CSubst]:
+        new_config, _, _ = anti_unify(self.config, other.config)
+        common_constraints = [constraint for constraint in self.constraints if constraint in other.constraints]
+        new_constraints = []
+        fvs = free_vars(new_config)
+        len_fvs = 0
+        while len_fvs < len(fvs):
+            len_fvs = len(fvs)
+            for constraint in common_constraints:
+                if constraint not in new_constraints:
+                    constraint_fvs = free_vars(constraint)
+                    if any(fv in fvs for fv in constraint_fvs):
+                        new_constraints.append(constraint)
+                        fvs.extend(constraint_fvs)
+        new_cterm = CTerm(config=new_config, constraints=new_constraints)
+        self_csubst = new_cterm.match_with_constraint(self)
+        other_csubst = new_cterm.match_with_constraint(other)
+        if self_csubst is None or other_csubst is None:
+            raise ValueError(
+                f'Anti-unification failed to produce a more general state: {(new_cterm, (self, self_csubst), (other, other_csubst))}'
+            )
+        return (new_cterm, self_csubst, other_csubst)
+
 
 @dataclass(frozen=True, order=True)
 class CSubst:
@@ -173,6 +197,10 @@ def apply(self, cterm: CTerm) -> CTerm:
         _kast = self.subst(cterm.kast)
         return CTerm(_kast, [self.constraint])
 
+    @property
+    def ml_pred(self) -> KInner:
+        return mlAnd(flatten_label('#And', self.subst.ml_pred) + list(self.constraints))
+
 
 def remove_useless_constraints(cterm: CTerm, keep_vars: Iterable[str] = ()) -> CTerm:
     used_vars = free_vars(cterm.config) + list(keep_vars)

src/pyk/kcfg/kcfg.py

@@ -646,6 +646,31 @@ def create_split(self, source_id: NodeIdLike, splits: Iterable[tuple[NodeIdLike,
         split = KCFG.Split(self.node(source_id), tuple((self.node(nid), csubst) for nid, csubst in splits))
         self._splits[source_id] = split
 
+    def create_merge(self, node_ids: Iterable[NodeIdLike]) -> NodeIdLike:
+        node_ids = list(node_ids)
+        if len(node_ids) < 2:
+            raise ValueError(f'Cannot create merge node with less than 2 input nodes: {node_ids}')
+        cterms = [self.node(nid).cterm for nid in node_ids]
+        new_cterm = cterms[0]
+        for cterm in cterms[1:]:
+            new_cterm, _, _ = new_cterm.anti_unify(cterm)
+        new_node = self.create_node(new_cterm)
+        for nid in node_ids:
+            self.create_cover(nid, new_node.id)
+        return new_node.id
+
+    def pullback_covers(self, target_id: NodeIdLike) -> tuple[list[NodeIdLike], NodeIdLike] | None:
+        covers = self.covers(target_id=target_id)
+        source_ids: list[NodeIdLike] = [cover.source.id for cover in covers]
+        if len(source_ids) < 2:
+            return None
+        merge_id = self.create_merge(source_ids)
+        for cover in covers:
+            self.remove_cover(cover.source.id, target_id)
+            self.create_cover(cover.source.id, merge_id)
+        self.create_cover(merge_id, target_id)
+        return source_ids, merge_id
+
     def ndbranches(self, *, source_id: NodeIdLike | None = None, target_id: NodeIdLike | None = None) -> list[NDBranch]:
         source_id = self._resolve(source_id) if source_id is not None else None
         target_id = self._resolve(target_id) if target_id is not None else None

src/pyk/proof/reachability.py

@@ -253,6 +253,14 @@ def summary(self) -> Iterable[str]:
     def get_refutation_id(self, node_id: int) -> str:
         return f'{self.id}.node-infeasible-{node_id}'
 
+    def specialize_target_node(self) -> None:
+        pullback = self.kcfg.pullback_covers(self.target)
+        if pullback is None:
+            _LOGGER.warning(f'Could not make a cover pullback for target node: {self.target}')
+        else:
+            merge_id, source_ids = pullback
+            _LOGGER.info(f'Created specialized target subsumed node {self.id}: {pullback}')
+
 
 class APRBMCProof(APRProof):
     """APRBMCProof and APRBMCProver perform bounded model-checking of an all-path reachability logic claim."""