Merge remote-tracking branch 'origin/develop'

pyk/src/pyk/__main__.py

@@ -22,7 +22,7 @@
 from .kast.inner import KInner
 from .kast.manip import (
     flatten_label,
-    minimize_rule,
+    minimize_rule_like,
     minimize_term,
     propagate_up_constraints,
     remove_source_map,
@@ -394,7 +394,7 @@ def exec_coverage(options: CoverageOptions) -> None:
     definition = remove_source_map(read_kast_definition(kompiled_dir / 'compiled.json'))
     pretty_printer = PrettyPrinter(definition)
     for rid in options.coverage_file:
-        rule = minimize_rule(strip_coverage_logger(get_rule_by_id(definition, rid.strip())))
+        rule = minimize_rule_like(strip_coverage_logger(get_rule_by_id(definition, rid.strip())))
         options.output_file.write('\n\n')
         options.output_file.write('Rule: ' + rid.strip())
         options.output_file.write('\nUnparsed:\n')

pyk/src/pyk/cterm/cterm.py

@@ -367,6 +367,7 @@ def cterm_build_rule(
     final_cterm: CTerm,
     priority: int | None = None,
     keep_vars: Iterable[str] = (),
+    defunc_with: KDefinition | None = None,
 ) -> tuple[KRule, Subst]:
     """Return a `KRule` between the supplied initial and final states.
 
@@ -375,6 +376,8 @@ def cterm_build_rule(
         init_cterm: State to put on LHS of the rule (constraints interpreted as `requires` clause).
         final_cterm: State to put on RHS of the rule (constraints interpreted as `ensures` clause).
         keep_vars: Variables to leave in the side-conditions even if not bound in the configuration.
+        priority: Priority index to use for generated rules.
+        defunc_with (optional): KDefinition to be able to defunctionalize LHS appropriately.
 
     Returns:
         A tuple ``(rule, var_map)`` where
@@ -386,4 +389,13 @@ def cterm_build_rule(
     """
     init_config, *init_constraints = init_cterm
     final_config, *final_constraints = final_cterm
-    return build_rule(rule_id, init_config, final_config, init_constraints, final_constraints, priority, keep_vars)
+    return build_rule(
+        rule_id,
+        init_config,
+        final_config,
+        init_constraints,
+        final_constraints,
+        priority,
+        keep_vars,
+        defunc_with=defunc_with,
+    )

pyk/src/pyk/kast/manip.py

@@ -6,7 +6,7 @@
 
 from ..prelude.k import DOTS, GENERATED_TOP_CELL
 from ..prelude.kbool import FALSE, TRUE, andBool, impliesBool, notBool, orBool
-from ..prelude.ml import is_top, mlAnd, mlBottom, mlEqualsTrue, mlImplies, mlOr, mlTop
+from ..prelude.ml import is_top, mlAnd, mlBottom, mlEquals, mlEqualsTrue, mlImplies, mlOr, mlTop
 from ..utils import find_common_items, hash_str, unique
 from .att import EMPTY_ATT, Atts, KAtt, WithKAtt
 from .inner import (
@@ -543,7 +543,7 @@ def minimize_term(
     return term
 
 
-def minimize_rule(rule: RL, keep_vars: Iterable[str] = ()) -> RL:
+def minimize_rule_like(rule: RL, keep_vars: Iterable[str] = ()) -> RL:
     """Minimize a K rule or claim for pretty-printing.
 
     - Variables only used once will be removed.
@@ -756,6 +756,7 @@ def build_rule(
     final_constraints: Iterable[KInner] = (),
     priority: int | None = None,
     keep_vars: Iterable[str] = (),
+    defunc_with: KDefinition | None = None,
 ) -> tuple[KRule, Subst]:
     """Return a `KRule` between the supplied initial and final states.
 
@@ -765,7 +766,9 @@ def build_rule(
         final_config: State to put on RHS of the rule.
         init_constraints: Constraints to use as `requires` clause.
         final_constraints: Constraints to use as `ensures` clause.
+        priority: Priority index to assign to generated rules.
         keep_vars: Variables to leave in the side-conditions even if not bound in the configuration.
+        defunc_with: KDefinition for filtering out function symbols on LHS of rules.
 
     Returns:
         A tuple ``(rule, var_map)`` where
@@ -778,6 +781,9 @@ def build_rule(
     init_constraints = [normalize_ml_pred(c) for c in init_constraints]
     final_constraints = [normalize_ml_pred(c) for c in final_constraints]
     final_constraints = [c for c in final_constraints if c not in init_constraints]
+    if defunc_with is not None:
+        init_config, new_constraints = defunctionalize(defunc_with, init_config)
+        init_constraints = init_constraints + new_constraints
     init_term = mlAnd([init_config] + init_constraints)
     final_term = mlAnd([final_config] + final_constraints)
 
@@ -854,3 +860,30 @@ def _no_cell_rewrite_to_dots(_term: KInner) -> KInner:
     subst = Subst({cell_name: _no_cell_rewrite_to_dots(cell_contents) for cell_name, cell_contents in _subst.items()})
 
     return subst(config)
+
+
+def defunctionalize(defn: KDefinition, kinner: KInner) -> tuple[KInner, list[KInner]]:
+    """Turn non-constructor arguments into side-conditions so that a term is only constructor-like.
+
+    Args:
+        defn: The definition to pull function label information from.
+        kinner: The term to defunctionalize.
+
+    Returns:
+        A tuple of the defunctionalized term and the list of constraints generated.
+    """
+    function_symbols = [prod.klabel for prod in defn.functions if prod.klabel is not None]
+    constraints: list[KInner] = []
+
+    def _defunctionalize(_kinner: KInner) -> KInner:
+        if type(_kinner) is KApply and _kinner.label in function_symbols:
+            sort = defn.sort(_kinner)
+            assert sort is not None
+            new_var = abstract_term_safely(_kinner, base_name='F', sort=sort)
+            var_constraint = mlEquals(new_var, _kinner, arg_sort=sort)
+            constraints.append(var_constraint)
+            return new_var
+        return _kinner
+
+    new_kinner = top_down(_defunctionalize, kinner)
+    return (new_kinner, list(unique(constraints)))

pyk/src/pyk/kast/outer.py

@@ -864,6 +864,10 @@ def is_not_actually_function(label: str) -> bool:
                 '_List_',
                 '_Map_',
                 '_RangeMap_',
+                '.Set',
+                '.List',
+                '.Map',
+                '.RangeMap',
                 'SetItem',
                 'ListItem',
                 '_|->_',

pyk/src/pyk/kcfg/exploration.py

@@ -3,6 +3,7 @@
 from typing import TYPE_CHECKING
 
 from pyk.kcfg.kcfg import KCFG, NodeAttr
+from pyk.kcfg.minimize import KCFGMinimizer
 
 if TYPE_CHECKING:
     from collections.abc import Iterable, Mapping
@@ -109,4 +110,4 @@ def to_dict(self) -> dict[str, Any]:
 
     # Minimizing the KCFG
     def minimize_kcfg(self) -> None:
-        self.kcfg.minimize()
+        KCFGMinimizer(self.kcfg).minimize()

pyk/src/pyk/kcfg/kcfg.py

@@ -18,13 +18,13 @@
     extract_rhs,
     flatten_label,
     inline_cell_maps,
+    minimize_rule_like,
     rename_generated_vars,
     sort_ac_collections,
 )
 from ..kast.outer import KFlatModule
 from ..prelude.kbool import andBool
 from ..utils import ensure_dir_path, not_none
-from .minimize import KCFGMinimizer
 
 if TYPE_CHECKING:
     from collections.abc import Iterable, Mapping, MutableMapping
@@ -218,7 +218,14 @@ def to_dict(self) -> dict[str, Any]:
         def from_dict(dct: dict[str, Any], nodes: Mapping[int, KCFG.Node]) -> KCFG.Edge:
             return KCFG.Edge(nodes[dct['source']], nodes[dct['target']], dct['depth'], tuple(dct['rules']))
 
-        def to_rule(self, label: str, claim: bool = False, priority: int | None = None) -> KRuleLike:
+        def to_rule(
+            self,
+            label: str,
+            claim: bool = False,
+            priority: int | None = None,
+            defunc_with: KDefinition | None = None,
+            minimize: bool = False,
+        ) -> KRuleLike:
             def is_ceil_condition(kast: KInner) -> bool:
                 return type(kast) is KApply and kast.label.name == '#Ceil'
 
@@ -234,7 +241,11 @@ def _simplify_config(config: KInner) -> KInner:
             if claim:
                 rule, _ = cterm_build_claim(sentence_id, init_cterm, target_cterm)
             else:
-                rule, _ = cterm_build_rule(sentence_id, init_cterm, target_cterm, priority=priority)
+                rule, _ = cterm_build_rule(
+                    sentence_id, init_cterm, target_cterm, priority=priority, defunc_with=defunc_with
+                )
+            if minimize:
+                rule = minimize_rule_like(rule)
             return rule
 
         def replace_source(self, node: KCFG.Node) -> KCFG.Edge:
@@ -1234,9 +1245,6 @@ def write_cfg_data(self) -> None:
         self._deleted_nodes.clear()
         self._created_nodes.clear()
 
-    def minimize(self) -> None:
-        KCFGMinimizer(self).minimize()
-
     @staticmethod
     def read_cfg_data(cfg_dir: Path) -> KCFG:
         store = KCFGStore(cfg_dir)

pyk/src/pyk/kcfg/minimize.py

@@ -3,13 +3,13 @@
 from functools import reduce
 from typing import TYPE_CHECKING
 
-from pyk.cterm import CTerm
-from pyk.utils import not_none, single
+from ..cterm import CTerm
+from ..utils import not_none, single
 
 if TYPE_CHECKING:
     from collections.abc import Callable
 
-    from pyk.kcfg.kcfg import KCFG, NodeIdLike
+    from .kcfg import KCFG, NodeIdLike
 
 
 class KCFGMinimizer:

pyk/src/pyk/kcfg/show.py

@@ -9,7 +9,7 @@
 from ..kast.manip import (
     flatten_label,
     inline_cell_maps,
-    minimize_rule,
+    minimize_rule_like,
     minimize_term,
     ml_pred_to_bool,
     push_down_rewrites,
@@ -316,7 +316,7 @@ def _process_sentence(sent: KSentence) -> KSentence:
                 sent = sent.let(body=KCFGShow.hide_cells(sent.body, omit_cells))
                 if parseable_output:
                     sent = sent.let(body=remove_generated_cells(sent.body))
-                    sent = minimize_rule(sent)
+                    sent = minimize_rule_like(sent)
             return sent
 
         module = cfg.to_module(module_name)

pyk/src/tests/integration/cterm/test_simple.py

@@ -4,11 +4,9 @@
 
 import pytest
 
-from pyk.cterm import CTerm
+from pyk.cterm import CTerm, cterm_build_rule
 from pyk.kast.inner import KApply, KSequence, KToken, KVariable
-from pyk.prelude.kint import leInt
 from pyk.prelude.ml import mlEqualsTrue, mlTop
-from pyk.prelude.utils import token
 from pyk.testing import CTermSymbolicTest, KPrintTest
 
 from ..utils import K_FILES
@@ -18,7 +16,6 @@
     from typing import Final, Union
 
     from pyk.cterm import CTermSymbolic
-    from pyk.kast.inner import KInner
     from pyk.ktool.kprint import KPrint
 
     STATE = Union[tuple[str, str], tuple[str, str, str]]
@@ -38,9 +35,13 @@
 
 SIMPLIFY_TEST_DATA: Final = (('bytes-return', ('mybytes', '.Map'), (r'b"\x00\x90\xa0\n\xa1\xf1a" ~> .K', '.Map')),)
 
-
-def le_int(n: int, var: str) -> KInner:
-    return mlEqualsTrue(leInt(token(n), KVariable(var)))
+BUILD_RULE_TEST_DATA: Final = (
+    (
+        'functional-lhs',
+        (('mybytes', '.Map'), (r'mybytes ~> .K', '.Map')),
+        ('( F_e096a1bd:KItem => mybytes )', '.Map', 'F_e096a1bd:KItem ==K mybytes', 'true'),
+    ),
+)
 
 
 class TestSimpleProof(CTermSymbolicTest, KPrintTest):
@@ -130,3 +131,36 @@ def test_simplify(
         # Then
         assert actual_k == expected_k
         assert actual_state == expected_state
+
+    @pytest.mark.parametrize(
+        'test_id,pre,expected_post',
+        BUILD_RULE_TEST_DATA,
+        ids=[test_id for test_id, *_ in BUILD_RULE_TEST_DATA],
+    )
+    def test_cterm_build_rule(
+        self,
+        cterm_symbolic: CTermSymbolic,
+        kprint: KPrint,
+        test_id: str,
+        pre: tuple[tuple[str, str, str | None], tuple[str, str, str | None]],
+        expected_post: tuple[str, str, str | None, str | None],
+    ) -> None:
+        # Given
+        lhs, rhs = pre
+        expected_k, expected_state, expected_requires, expected_ensures = expected_post
+
+        # When
+        config_lhs = self.config(kprint, *lhs)
+        config_rhs = self.config(kprint, *rhs)
+        rule, _ = cterm_build_rule(test_id, config_lhs, config_rhs, defunc_with=kprint.definition)
+        rule_body_cterm = CTerm.from_kast(rule.body)
+        rule_k = kprint.pretty_print(rule_body_cterm.cell('K_CELL'))
+        rule_state = kprint.pretty_print(rule_body_cterm.cell('STATE_CELL'))
+        rule_requires = kprint.pretty_print(rule.requires)
+        rule_ensures = kprint.pretty_print(rule.ensures)
+
+        # Then
+        assert rule_k == expected_k
+        assert rule_state == expected_state
+        assert rule_requires == expected_requires
+        assert rule_ensures == expected_ensures

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

@@ -11,6 +11,7 @@
 from pyk.kast.manip import free_vars
 from pyk.kast.outer import KClaim
 from pyk.kcfg import KCFG
+from pyk.kcfg.minimize import KCFGMinimizer
 from pyk.kcfg.semantics import KCFGSemantics
 from pyk.prelude.kint import gtInt, intToken, leInt
 from pyk.prelude.ml import is_top, mlEqualsTrue
@@ -372,7 +373,7 @@ def test_apr_proof_refute_node_multiple_constraints(
         prover.advance_proof(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
-        proof.kcfg.minimize()
+        KCFGMinimizer(proof.kcfg).minimize()
 
         # Then
         for i in [7, 8, 9, 10]: