PyK: Misc enhancements to KCFG and anti-unification (#4775)

*  KCFG: Shorten log message for easier readability

    This brings the more important parts of the messages into focus.

*  CTerm.anti_unify: Don't call ml_pred_to_bool unless necessary

Since these values are only used if keep_values is set, we do not need
to always
compute them. In addition, it avoids exceptions when the predicate
cannot be
converted to a bool expression: e.g. when using #Ceil as a side
condition

    This is only a work-around (it would
still break for a #Ceil side condition, if keep_values=True), but lets
us move forward without risking
    breaking other projects that rely on the original behaviour.
    
* pyk:KCFGShow.to_module: Thread imports and defunc_with parameters
through to KCFG.to_module

     This lets us use those options for printing the modules.

---------

Co-authored-by: Everett Hildenbrandt <[email protected]>

Author: nishantjr

pyk/src/pyk/cterm/cterm.py

@@ -204,18 +204,18 @@ def anti_unify(
             - ``csubst2``: Constrained substitution to apply to `cterm` to obtain `other`.
         """
         new_config, self_subst, other_subst = anti_unify(self.config, other.config, kdef=kdef)
-        # todo: It's not able to distinguish between constraints in different cterms,
-        #  because variable names may be used inconsistently in different cterms.
         common_constraints = [constraint for constraint in self.constraints if constraint in other.constraints]
-        self_unique_constraints = [
-            ml_pred_to_bool(constraint) for constraint in self.constraints if constraint not in other.constraints
-        ]
-        other_unique_constraints = [
-            ml_pred_to_bool(constraint) for constraint in other.constraints if constraint not in self.constraints
-        ]
 
         new_cterm = CTerm(config=new_config, constraints=())
         if keep_values:
+            # todo: It's not able to distinguish between constraints in different cterms,
+            #  because variable names may be used inconsistently in different cterms.
+            self_unique_constraints = [
+                ml_pred_to_bool(constraint) for constraint in self.constraints if constraint not in other.constraints
+            ]
+            other_unique_constraints = [
+                ml_pred_to_bool(constraint) for constraint in other.constraints if constraint not in self.constraints
+            ]
             disjunct_lhs = andBool([self_subst.pred] + self_unique_constraints)
             disjunct_rhs = andBool([other_subst.pred] + other_unique_constraints)
             if KToken('true', 'Bool') not in [disjunct_lhs, disjunct_rhs]:

pyk/src/pyk/kcfg/kcfg.py

@@ -568,7 +568,7 @@ def log(message: str, *, warning: bool = False) -> None:
             result_info_message = f': {result_info}' if result_info else ''
             _LOGGER.log(
                 logging.WARNING if warning else logging.INFO,
-                f'Extending current KCFG with the following: {message}{result_info_message}',
+                f'Extending KCFG with: {message}{result_info_message}',
             )
 
         match extend_result:
@@ -711,9 +711,14 @@ def to_json(self) -> str:
     def from_json(s: str, optimize_memory: bool = True) -> KCFG:
         return KCFG.from_dict(json.loads(s), optimize_memory=optimize_memory)
 
-    def to_rules(self, _id: str | None = None, priority: int = 20) -> list[KRuleLike]:
+    def to_rules(
+        self,
+        _id: str | None = None,
+        priority: int = 20,
+        defunc_with: KDefinition | None = None,
+    ) -> list[KRuleLike]:
         _id = 'BASIC-BLOCK' if _id is None else _id
-        return [e.to_rule(_id, priority=priority) for e in self.edges()] + [
+        return [e.to_rule(_id, priority=priority, defunc_with=defunc_with) for e in self.edges()] + [
             m.to_rule(_id, priority=priority) for m in self.merged_edges()
         ]
 
@@ -723,9 +728,12 @@ def to_module(
         imports: Iterable[KImport] = (),
         priority: int = 20,
         att: KAtt = EMPTY_ATT,
+        defunc_with: KDefinition | None = None,
     ) -> KFlatModule:
         module_name = 'KCFG' if module_name is None else module_name
-        return KFlatModule(module_name, self.to_rules(priority=priority), imports=imports, att=att)
+        return KFlatModule(
+            module_name, self.to_rules(priority=priority, defunc_with=defunc_with), imports=imports, att=att
+        )
 
     def _resolve_or_none(self, id_like: NodeIdLike) -> int | None:
         if type(id_like) is int:

pyk/src/pyk/kcfg/show.py

@@ -29,7 +29,7 @@
 
     from ..cterm import CSubst
     from ..kast import KInner
-    from ..kast.outer import KFlatModule, KSentence
+    from ..kast.outer import KDefinition, KFlatModule, KImport, KSentence
     from ..ktool.kprint import KPrint
     from .kcfg import NodeIdLike
 
@@ -311,6 +311,8 @@ def to_module(
         module_name: str | None = None,
         omit_cells: Iterable[str] = (),
         parseable_output: bool = True,
+        defunc_with: KDefinition | None = None,
+        imports: Iterable[KImport] = (),
     ) -> KFlatModule:
         def _process_sentence(sent: KSentence) -> KSentence:
             if type(sent) is KRule:
@@ -320,7 +322,7 @@ def _process_sentence(sent: KSentence) -> KSentence:
                     sent = minimize_rule_like(sent)
             return sent
 
-        module = cfg.to_module(module_name)
+        module = cfg.to_module(module_name, defunc_with=defunc_with, imports=imports)
         return module.let(sentences=[_process_sentence(sent) for sent in module.sentences])
 
     def show(