Refactor adding modules via CTermSymbolic (#4771)

This PR factors out the ability to add KAST level modules to the RPC
server via `CTermSymbolic`, so that the user doesn't need to manually do
the conversions needed for adding such modules. The `APRProver` is
refactored to use this new `CTermSymbolic.add_module` as well.

This is part of
runtimeverification/kontrol#977, and blocking
runtimeverification/kontrol#979.

Author: ehildenb

pyk/src/pyk/cterm/symbolic.py

@@ -5,13 +5,11 @@
 from dataclasses import dataclass
 from typing import TYPE_CHECKING, NamedTuple, final
 
-from pyk.utils import not_none
-
 from ..cterm import CSubst, CTerm
 from ..kast.inner import KApply, KLabel, KRewrite, KToken, KVariable, Subst
 from ..kast.manip import flatten_label, is_spurious_constraint, sort_ac_collections
 from ..kast.pretty import PrettyPrinter
-from ..konvert import kast_to_kore, kore_to_kast
+from ..konvert import kast_to_kore, kflatmodule_to_kore, kore_to_kast
 from ..kore.rpc import (
     AbortedResult,
     KoreClient,
@@ -26,14 +24,15 @@
 )
 from ..prelude.k import GENERATED_TOP_CELL, K_ITEM
 from ..prelude.ml import mlAnd
+from ..utils import not_none
 
 if TYPE_CHECKING:
     from collections.abc import Iterable, Iterator
     from pathlib import Path
     from typing import Final
 
     from ..kast import KInner
-    from ..kast.outer import KDefinition
+    from ..kast.outer import KDefinition, KFlatModule
     from ..kore.rpc import FallbackReason, LogEntry
     from ..kore.syntax import Pattern
     from ..utils import BugReport
@@ -279,6 +278,10 @@ def assume_defined(self, cterm: CTerm, module_name: str | None = None) -> CTerm:
         _LOGGER.debug(f'Definedness condition computed: {kast_simplified}')
         return cterm.add_constraint(kast_simplified)
 
+    def add_module(self, module: KFlatModule, name_as_id: bool = False) -> str:
+        _kore_module = kflatmodule_to_kore(self._definition, module)
+        return self._kore_client.add_module(_kore_module, name_as_id=name_as_id)
+
     def _smt_solver_error(self, err: SmtSolverError) -> CTermSMTError:
         kast = self.kore_to_kast(err.pattern)
         pretty_pattern = PrettyPrinter(self._definition).print(kast)

pyk/src/pyk/proof/reachability.py

@@ -14,7 +14,6 @@
 from ..kast.outer import KFlatModule, KImport, KRule
 from ..kcfg import KCFG, KCFGStore
 from ..kcfg.exploration import KCFGExploration
-from ..konvert import kflatmodule_to_kore
 from ..ktool.claim_index import ClaimIndex
 from ..prelude.ml import mlAnd, mlTop
 from ..utils import FrozenDict, ensure_dir_path, hash_str, shorten_hashes, single
@@ -752,15 +751,11 @@ def close(self) -> None:
     def init_proof(self, proof: APRProof) -> None:
         main_module_name = self.main_module_name
         if self.extra_module:
-            _kore_module = kflatmodule_to_kore(self.kcfg_explore.cterm_symbolic._definition, self.extra_module)
-            _LOGGER.warning(f'_kore_module: {_kore_module.text}')
-            self.kcfg_explore.cterm_symbolic._kore_client.add_module(_kore_module, name_as_id=True)
-            main_module_name = self.extra_module.name
+            main_module_name = self.kcfg_explore.cterm_symbolic.add_module(self.extra_module, name_as_id=True)
 
         def _inject_module(module_name: str, import_name: str, sentences: list[KRule]) -> None:
             _module = KFlatModule(module_name, sentences, [KImport(import_name)])
-            _kore_module = kflatmodule_to_kore(self.kcfg_explore.cterm_symbolic._definition, _module)
-            self.kcfg_explore.cterm_symbolic._kore_client.add_module(_kore_module, name_as_id=True)
+            self.kcfg_explore.cterm_symbolic.add_module(_module, name_as_id=True)
 
         subproofs: list[Proof] = (
             [Proof.read_proof_data(proof.proof_dir, i) for i in proof.subproof_ids]