Remove manip.get_cell, add CTerm.free_vars (#1040)

Inspired while reviewing:
#1009

This makes two changes which hopefully tighten the `CTerm` abstraction
slightly by reducing the places where `CTerm.kast` is used:

- Places that were doing `get_cell(CTerm.kast, CELL_NAME)` now say
`CTerm.cell(CELL_NAME)`. There are no more uses of `get_cell` here or in
downstream repos, so it's removed.
- A new `@cached_property CTerm.free_vars` is added, which is used to
replace the pattern `free_vars(CTerm.kast)`.

This means that the remaining uses of `CTerm.kast` are doing something
weird with the resulting kast, or printing it, or converting it to Kore.

---------

Co-authored-by: devops <[email protected]>

Author: ehildenb

docs/conf.py

@@ -9,8 +9,8 @@
 project = 'pyk'
 author = 'Runtime Verification, Inc'
 copyright = '2024, Runtime Verification, Inc'
-version = '0.1.754'
-release = '0.1.754'
+version = '0.1.755'
+release = '0.1.755'
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

package/version

@@ -1 +1 @@
-0.1.754
+0.1.755

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.754"
+version = "0.1.755"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/pyk/cterm/cterm.py

@@ -148,6 +148,11 @@ def kast(self) -> KInner:
         """Return the unstructured bare `KInner` representation of a `CTerm` (see `CTerm.from_kast`)."""
         return mlAnd(self, GENERATED_TOP_CELL)
 
+    @cached_property
+    def free_vars(self) -> frozenset[str]:
+        """Return the set of free variable names contained in this `CTerm`"""
+        return frozenset(free_vars(self.kast))
+
     @property
     def hash(self) -> str:
         """Unique hash representing the contents of this `CTerm`."""
@@ -235,7 +240,7 @@ def anti_unify(
                 new_cterm = new_cterm.add_constraint(mlEqualsTrue(orBool([disjunct_lhs, disjunct_rhs])))
 
         new_constraints = []
-        fvs = free_vars(new_cterm.kast)
+        fvs = list(new_cterm.free_vars)
         len_fvs = 0
         while len_fvs < len(fvs):
             len_fvs = len(fvs)

src/pyk/cterm/symbolic.py

@@ -7,7 +7,7 @@
 
 from ..cterm import CSubst, CTerm
 from ..kast.inner import KApply, KLabel, KRewrite, KVariable, Subst
-from ..kast.manip import flatten_label, free_vars, sort_ac_collections
+from ..kast.manip import flatten_label, sort_ac_collections
 from ..kast.pretty import PrettyPrinter
 from ..konvert import kast_to_kore, kore_to_kast
 from ..kore.rpc import (
@@ -186,8 +186,7 @@ def implies(
     ) -> CTermImplies:
         _LOGGER.debug(f'Checking implication: {antecedent} #Implies {consequent}')
         _consequent = consequent.kast
-        fv_antecedent = free_vars(antecedent.kast)
-        unbound_consequent = [v for v in free_vars(_consequent) if v not in fv_antecedent]
+        unbound_consequent = [v for v in consequent.free_vars if v not in antecedent.free_vars]
         if len(unbound_consequent) > 0:
             bind_text, bind_label = ('existentially', '#Exists')
             if bind_universally:

src/pyk/kast/manip.py

@@ -565,12 +565,6 @@ def is_anon_var(kast: KInner) -> bool:
     return type(kast) is KVariable and kast.name.startswith('_')
 
 
-def get_cell(constrained_term: KInner, cell_variable: str) -> KInner:
-    state, _ = split_config_and_constraints(constrained_term)
-    _, subst = split_config_from(state)
-    return subst[cell_variable]
-
-
 def set_cell(constrained_term: KInner, cell_variable: str, cell_value: KInner) -> KInner:
     state, constraint = split_config_and_constraints(constrained_term)
     config, subst = split_config_from(state)

src/pyk/kcfg/kcfg.py

@@ -932,7 +932,7 @@ def lift_split(self, id: NodeIdLike) -> None:
         split_from_b = single(self.splits(source_id=id))
         ci, csubsts = list(split_from_b.splits.keys()), list(split_from_b.splits.values())
         # If any of the `cond_I` contains variables not present in `A`, the lift cannot be performed soundly.
-        fv_a = set(free_vars(a.cterm.kast))
+        fv_a = a.cterm.free_vars
         for subst in csubsts:
             assert set(free_vars(mlAnd(subst.constraints))).issubset(
                 fv_a

src/tests/integration/cterm/test_simple.py

@@ -6,7 +6,6 @@
 
 from pyk.cterm import CTerm
 from pyk.kast.inner import KApply, KSequence, KToken, KVariable
-from pyk.kast.manip import get_cell
 from pyk.prelude.ml import mlEqualsTrue, mlTop
 from pyk.testing import CTermSymbolicTest, KPrintTest
 
@@ -116,8 +115,8 @@ def test_simplify(
 
         # When
         actual_post, _logs = cterm_symbolic.simplify(self.config(kprint, *pre))
-        actual_k = kprint.pretty_print(get_cell(actual_post.kast, 'K_CELL'))
-        actual_state = kprint.pretty_print(get_cell(actual_post.kast, 'STATE_CELL'))
+        actual_k = kprint.pretty_print(actual_post.cell('K_CELL'))
+        actual_state = kprint.pretty_print(actual_post.cell('STATE_CELL'))
 
         # Then
         assert actual_k == expected_k

src/tests/integration/proof/test_imp.py

@@ -8,7 +8,7 @@
 
 from pyk.cterm import CSubst, CTerm
 from pyk.kast.inner import KApply, KSequence, KSort, KToken, KVariable, Subst
-from pyk.kast.manip import get_cell, minimize_term
+from pyk.kast.manip import minimize_term
 from pyk.kcfg.semantics import KCFGSemantics
 from pyk.kcfg.show import KCFGShow
 from pyk.prelude.kbool import BOOL, andBool, notBool, orBool
@@ -1208,7 +1208,7 @@ def test_anti_unify_forget_values(
 
         anti_unifier, subst1, subst2 = cterm1.anti_unify(cterm2, keep_values=False, kdef=kprove.definition)
 
-        k_cell = get_cell(anti_unifier.kast, 'STATE_CELL')
+        k_cell = anti_unifier.cell('STATE_CELL')
         assert type(k_cell) is KApply
         assert k_cell.label.name == '_|->_'
         assert type(k_cell.args[1]) is KVariable
@@ -1221,7 +1221,7 @@ def test_anti_unify_forget_values(
             constraint=mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])),
         )
 
-        assert anti_unifier.kast == expected_anti_unifier.kast
+        assert anti_unifier == expected_anti_unifier
 
     def test_anti_unify_keep_values(
         self,
@@ -1259,7 +1259,7 @@ def test_anti_unify_keep_values(
 
         anti_unifier, subst1, subst2 = cterm1.anti_unify(cterm2, keep_values=True, kdef=kprove.definition)
 
-        k_cell = get_cell(anti_unifier.kast, 'STATE_CELL')
+        k_cell = anti_unifier.cell('STATE_CELL')
         assert type(k_cell) is KApply
         assert k_cell.label.name == '_|->_'
         assert type(k_cell.args[1]) is KVariable
@@ -1296,7 +1296,7 @@ def test_anti_unify_keep_values(
             ),
         )
 
-        assert anti_unifier.kast == expected_anti_unifier.kast
+        assert anti_unifier == expected_anti_unifier
 
     def test_anti_unify_subst_true(
         self,
@@ -1318,7 +1318,7 @@ def test_anti_unify_subst_true(
 
         anti_unifier, _, _ = cterm1.anti_unify(cterm2, keep_values=True, kdef=kprove.definition)
 
-        assert anti_unifier.kast == cterm1.kast
+        assert anti_unifier == cterm1
 
     @pytest.mark.parametrize(
         'test_id,antecedent,consequent,expected',