Add --simplify-each option for booster

Author: palinatolmach

pyk/src/pyk/cterm/symbolic.py

@@ -308,6 +308,7 @@ def cterm_symbolic(
     start_server: bool = True,
     fallback_on: Iterable[FallbackReason] | None = None,
     interim_simplification: int | None = None,
+    simplify_each: int | None = None,
     no_post_exec_simplify: bool = False,
 ) -> Iterator[CTermSymbolic]:
     if start_server:
@@ -327,6 +328,7 @@ def cterm_symbolic(
             log_axioms_file=log_axioms_file,
             fallback_on=fallback_on,
             interim_simplification=interim_simplification,
+            simplify_each=simplify_each,
             no_post_exec_simplify=no_post_exec_simplify,
         ) as server:
             with KoreClient('localhost', server.port, bug_report=bug_report, bug_report_id=id) as client:

pyk/src/pyk/kore/rpc.py

@@ -1267,6 +1267,7 @@ class BoosterServerArgs(KoreServerArgs, total=False):
     llvm_kompiled_dir: Required[str | Path]
     fallback_on: Iterable[str | FallbackReason] | None
     interim_simplification: int | None
+    simplify_each: int | None
     no_post_exec_simplify: bool | None
     log_context: Iterable[str] | None
     not_log_context: Iterable[str] | None
@@ -1280,6 +1281,7 @@ class BoosterServer(KoreServer):
 
     _fallback_on: list[FallbackReason] | None
     _interim_simplification: int | None
+    _simplify_each: int | None
     _no_post_exec_simplify: bool
     _log_context: list[str]
     _not_log_context: list[str]
@@ -1306,6 +1308,7 @@ def __init__(self, args: BoosterServerArgs):
             self._fallback_on = None
 
         self._interim_simplification = args.get('interim_simplification')
+        self._simplify_each = args.get('simplify_each')
         self._no_post_exec_simplify = bool(args.get('no_post_exec_simplify'))
         self._log_context = list(args.get('log_context') or [])
         self._not_log_context = list(args.get('not_log_context') or [])
@@ -1326,6 +1329,10 @@ def _validate(self) -> None:
 
         if self._interim_simplification and self._interim_simplification < 0:
             raise ValueError(f"'interim_simplification' must not be negative, got: {self._interim_simplification}")
+
+        if self._simplify_each and self._simplify_each < 0:
+            raise ValueError(f"'simplify_each' must not be negative, got: {self._simplify_each}")
+
         super()._validate()
 
     def _extra_args(self) -> list[str]:
@@ -1335,6 +1342,8 @@ def _extra_args(self) -> list[str]:
             res += ['--fallback-on', ','.join(reason.value for reason in self._fallback_on)]
         if self._interim_simplification is not None:
             res += ['--interim-simplification', str(self._interim_simplification)]
+        if self._simplify_each is not None:
+            res += ['--simplify-each', str(self._simplify_each)]
         if self._no_post_exec_simplify:
             res += ['--no-post-exec-simplify']
         res += [arg for glob in self._log_context for arg in ['--log-context', glob]]
@@ -1365,6 +1374,7 @@ def kore_server(
     llvm_definition_dir: Path | None = None,
     fallback_on: Iterable[str | FallbackReason] | None = None,
     interim_simplification: int | None = None,
+    simplify_each: int | None = None,
     no_post_exec_simplify: bool | None = None,
     # ---
     bug_report: BugReport | None = None,
@@ -1388,6 +1398,7 @@ def kore_server(
             'llvm_kompiled_dir': llvm_definition_dir,
             'fallback_on': fallback_on,
             'interim_simplification': interim_simplification,
+            'simplify_each': simplify_each,
             'no_post_exec_simplify': no_post_exec_simplify,
             **kore_args,
         }

pyk/src/tests/integration/kore/test_kore_client.py

@@ -971,6 +971,7 @@ def test_add_module_with_hash_name_as_id_second_fails(self, kore_client: KoreCli
     {},
     {'fallback_on': ['Aborted', 'Stuck']},
     {'interim_simplification': 3},
+    {'simplify_each': 5},
     {'no_post_exec_simpify': True},
     {'log_context': ['booster*']},
     {'log_context': ['kore*', '!detail']},