Evaluate pending nodes in parallel

package/version

@@ -1 +1 @@
-0.1.359
+0.1.360

pyproject.toml

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

src/pyk/kcfg/explore.py

@@ -18,7 +18,7 @@
 )
 from ..kast.outer import KRule
 from ..konvert import krule_to_kore
-from ..kore.rpc import KoreClient, KoreServer, SatResult, StopReason, UnknownResult, UnsatResult
+from ..kore.rpc import SatResult, StopReason, UnknownResult, UnsatResult
 from ..kore.syntax import Import, Module
 from ..ktool.kprove import KoreExecLogFormat
 from ..prelude import k
@@ -35,10 +35,9 @@
 
     from ..kast import KInner
     from ..kast.outer import KClaim
-    from ..kore.rpc import LogEntry
+    from ..kore.rpc import KoreServerBase, LogEntry
     from ..kore.syntax import Sentence
     from ..ktool.kprint import KPrint
-    from ..utils import BugReport
     from .kcfg import NodeIdLike
 
 
@@ -48,45 +47,28 @@
 class KCFGExplore(ContextManager['KCFGExplore']):
     kprint: KPrint
     id: str
-    _port: int | None
-    _kore_rpc_command: str | Iterable[str]
-    _smt_timeout: int | None
-    _smt_retry_limit: int | None
-    _bug_report: BugReport | None
-
-    _kore_server: KoreServer | None
-    _kore_client: KoreClient | None
-    _rpc_closed: bool
+
     _trace_rewrites: bool
 
+    _kore_server: KoreServerBase
+
     def __init__(
         self,
+        kore_server: KoreServerBase,
         kprint: KPrint,
         *,
         id: str | None = None,
-        port: int | None = None,
-        kore_rpc_command: str | Iterable[str] = 'kore-rpc',
-        smt_timeout: int | None = None,
-        smt_retry_limit: int | None = None,
-        bug_report: BugReport | None = None,
         haskell_log_format: KoreExecLogFormat = KoreExecLogFormat.ONELINE,
         haskell_log_entries: Iterable[str] = (),
         log_axioms_file: Path | None = None,
         trace_rewrites: bool = False,
     ):
+        self._kore_server = kore_server
         self.kprint = kprint
         self.id = id if id is not None else 'NO ID'
-        self._port = port
-        self._kore_rpc_command = kore_rpc_command
-        self._smt_timeout = smt_timeout
-        self._smt_retry_limit = smt_retry_limit
-        self._bug_report = bug_report
         self._haskell_log_format = haskell_log_format
         self._haskell_log_entries = haskell_log_entries
         self._log_axioms_file = log_axioms_file
-        self._kore_server = None
-        self._kore_client = None
-        self._rpc_closed = False
         self._trace_rewrites = trace_rewrites
 
     def __enter__(self) -> KCFGExplore:
@@ -95,35 +77,8 @@ def __enter__(self) -> KCFGExplore:
     def __exit__(self, *args: Any) -> None:
         self.close()
 
-    @property
-    def _kore_rpc(self) -> tuple[KoreServer, KoreClient]:
-        if self._rpc_closed:
-            raise ValueError('RPC server already closed!')
-        if not self._kore_server:
-            self._kore_server = KoreServer(
-                self.kprint.definition_dir,
-                self.kprint.main_module,
-                port=self._port,
-                bug_report=self._bug_report,
-                command=self._kore_rpc_command,
-                smt_timeout=self._smt_timeout,
-                smt_retry_limit=self._smt_retry_limit,
-                haskell_log_format=self._haskell_log_format,
-                haskell_log_entries=self._haskell_log_entries,
-                log_axioms_file=self._log_axioms_file,
-            )
-        if not self._kore_client:
-            self._kore_client = KoreClient('localhost', self._kore_server._port, bug_report=self._bug_report)
-        return (self._kore_server, self._kore_client)
-
     def close(self) -> None:
-        self._rpc_closed = True
-        if self._kore_server is not None:
-            self._kore_server.close()
-            self._kore_server = None
-        if self._kore_client is not None:
-            self._kore_client.close()
-            self._kore_client = None
+        self.close()
 
     def cterm_execute(
         self,
@@ -135,7 +90,7 @@ def cterm_execute(
     ) -> tuple[int, CTerm, list[CTerm], tuple[LogEntry, ...]]:
         _LOGGER.debug(f'Executing: {cterm}')
         kore = self.kprint.kast_to_kore(cterm.kast, GENERATED_TOP_CELL)
-        _, kore_client = self._kore_rpc
+        _, kore_client = self._kore_server._kore_rpc
         er = kore_client.execute(
             kore,
             max_depth=depth,
@@ -163,23 +118,23 @@ def cterm_execute(
     def cterm_simplify(self, cterm: CTerm) -> tuple[KInner, tuple[LogEntry, ...]]:
         _LOGGER.debug(f'Simplifying: {cterm}')
         kore = self.kprint.kast_to_kore(cterm.kast, GENERATED_TOP_CELL)
-        _, kore_client = self._kore_rpc
+        _, kore_client = self._kore_server._kore_rpc
         kore_simplified, logs = kore_client.simplify(kore)
         kast_simplified = self.kprint.kore_to_kast(kore_simplified)
         return kast_simplified, logs
 
     def kast_simplify(self, kast: KInner) -> tuple[KInner, tuple[LogEntry, ...]]:
         _LOGGER.debug(f'Simplifying: {kast}')
         kore = self.kprint.kast_to_kore(kast, GENERATED_TOP_CELL)
-        _, kore_client = self._kore_rpc
+        _, kore_client = self._kore_server._kore_rpc
         kore_simplified, logs = kore_client.simplify(kore)
         kast_simplified = self.kprint.kore_to_kast(kore_simplified)
         return kast_simplified, logs
 
     def cterm_get_model(self, cterm: CTerm, module_name: str | None = None) -> Subst | None:
         _LOGGER.info(f'Getting model: {cterm}')
         kore = self.kprint.kast_to_kore(cterm.kast, GENERATED_TOP_CELL)
-        _, kore_client = self._kore_rpc
+        _, kore_client = self._kore_server._kore_rpc
         result = kore_client.get_model(kore, module_name=module_name)
         if type(result) is UnknownResult:
             _LOGGER.debug('Result is Unknown')
@@ -217,7 +172,7 @@ def cterm_implies(
                 _consequent = KApply(KLabel('#Exists', [GENERATED_TOP_CELL]), [KVariable(uc), _consequent])
         antecedent_kore = self.kprint.kast_to_kore(antecedent.kast, GENERATED_TOP_CELL)
         consequent_kore = self.kprint.kast_to_kore(_consequent, GENERATED_TOP_CELL)
-        _, kore_client = self._kore_rpc
+        _, kore_client = self._kore_server._kore_rpc
         result = kore_client.implies(antecedent_kore, consequent_kore)
         if not result.satisfiable:
             if result.substitution is not None:
@@ -326,7 +281,7 @@ def cterm_assume_defined(self, cterm: CTerm) -> CTerm:
         _LOGGER.debug(f'Computing definedness condition for: {cterm}')
         kast = KApply(KLabel('#Ceil', [GENERATED_TOP_CELL, GENERATED_TOP_CELL]), [cterm.config])
         kore = self.kprint.kast_to_kore(kast, GENERATED_TOP_CELL)
-        _, kore_client = self._kore_rpc
+        _, kore_client = self._kore_server._kore_rpc
         kore_simplified, _logs = kore_client.simplify(kore)
         kast_simplified = self.kprint.kore_to_kast(kore_simplified)
         _LOGGER.debug(f'Definedness condition computed: {kast_simplified}')
@@ -499,9 +454,9 @@ def add_dependencies_module(
             for c in dependencies
         ]
         kore_axioms: list[Sentence] = [krule_to_kore(self.kprint.kompiled_kore, r) for r in kast_rules]
-        _, kore_client = self._kore_rpc
-        sentences: list[Sentence] = [Import(module_name=old_module_name, attrs=())]
-        sentences = sentences + kore_axioms
-        m = Module(name=new_module_name, sentences=sentences)
-        _LOGGER.info(f'Adding dependencies module {self.id}: {new_module_name}')
-        kore_client.add_module(m)
+        for _, kore_client in self._kore_server._kore_rpcs:
+            sentences: list[Sentence] = [Import(module_name=old_module_name, attrs=())]
+            sentences = sentences + kore_axioms
+            m = Module(name=new_module_name, sentences=sentences)
+            _LOGGER.info(f'Adding dependencies module {self.id}: {new_module_name}')
+            kore_client.add_module(m)