kevm-pyk/utils: remove sanitize_config

Author: ehildenb

kevm-pyk/src/kevm_pyk/utils.py

@@ -4,23 +4,15 @@
 from pyk.kast.inner import KApply, KInner, KRewrite, KVariable
 from pyk.kast.manip import (
     abstract_term_safely,
-    bool_to_ml_pred,
     bottom_up,
-    flatten_label,
-    free_vars,
     is_anon_var,
-    ml_pred_to_bool,
-    remove_generated_cells,
     split_config_and_constraints,
     split_config_from,
     substitute,
-    undo_aliases,
 )
 from pyk.kast.outer import KDefinition, KFlatModule, KImport
 from pyk.kcfg import KCFG
 from pyk.ktool import KPrint
-from pyk.prelude.kbool import FALSE
-from pyk.prelude.ml import mlAnd
 
 
 def KDefinition__expand_macros(defn: KDefinition, term: KInner) -> KInner:  # noqa: N802
@@ -102,35 +94,3 @@ def abstract_cell_vars(cterm: KInner, keep_vars: Collection[KVariable] = ()) ->
         if type(subst[s]) is KVariable and not is_anon_var(subst[s]) and subst[s] not in keep_vars:
             subst[s] = abstract_term_safely(KVariable('_'), base_name=s)
     return substitute(config, subst)
-
-
-def sanitize_config(defn: KDefinition, init_term: KInner) -> KInner:
-    def _var_name(vname: str) -> str:
-        new_vname = vname
-        while new_vname.startswith('_') or new_vname.startswith('?'):
-            new_vname = new_vname[1:]
-        return new_vname
-
-    free_vars_subst = {vname: KVariable(_var_name(vname)) for vname in free_vars(init_term)}
-
-    # TODO: This is somewhat hacky. We shouldn't have to touch the config this much.
-    # Likely, the frontend should just be giving us initial states with these already in place.
-    def _remove_cell_map_definedness(_kast: KInner) -> KInner:
-        if type(_kast) is KApply:
-            if _kast.label.name.endswith('CellMap:in_keys'):
-                return FALSE
-            elif _kast.label.name.endswith('CellMapItem'):
-                return _kast.args[1]
-        return _kast
-
-    new_term = substitute(init_term, free_vars_subst)
-    new_term = remove_generated_cells(new_term)
-    new_term = bottom_up(_remove_cell_map_definedness, new_term)
-
-    if not (type(new_term) is KApply and new_term.label.name in ['#Top', '#Bottom']):
-        config, constraint = split_config_and_constraints(new_term)
-        constraints = [bool_to_ml_pred(ml_pred_to_bool(c, unsafe=True)) for c in flatten_label('#And', constraint)]
-        new_term = mlAnd([config] + constraints)
-        new_term = undo_aliases(defn, new_term)
-
-    return new_term