introducing the optimize_kcfg parameter (#2666)

runtimeverification · Dec 17, 2024 · 5e7a593 · 5e7a593
1 parent afce9a6
commit 5e7a593
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 0 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
@@ -365,6 +365,7 @@ def create_kcfg_explore() -> KCFGExplore:
                 max_frontier_parallel=options.max_frontier_parallel,
                 force_sequential=options.force_sequential,
                 assume_defined=options.assume_defined,
+                optimize_kcfg=options.optimize_kcfg,
             )
             end_time = time.time()
             _LOGGER.info(f'Proof timing {proof_problem.id}: {end_time - start_time}s')

diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py
@@ -381,6 +381,7 @@ class KProveOptions(Options):
     direct_subproof_rules: bool
     maintenance_rate: int
     assume_defined: bool
+    optimize_kcfg: bool
 
     @staticmethod
     def default() -> dict[str, Any]:
@@ -390,6 +391,7 @@ def default() -> dict[str, Any]:
             'direct_subproof_rules': False,
             'maintenance_rate': 1,
             'assume_defined': False,
+            'optimize_kcfg': False,
         }
 
 
@@ -850,6 +852,13 @@ def kprove_args(self) -> ArgumentParser:
             action='store_true',
             help='Use the implication check of the Booster (experimental).',
         )
+        args.add_argument(
+            '--optimize-kcfg',
+            dest='optimize_kcfg',
+            default=None,
+            action='store_true',
+            help='Optimize the constructed KCFG on-the-fly.',
+        )
         return args
 
     @cached_property

diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py
@@ -115,6 +115,7 @@ def run_prover(
     maintenance_rate: int = 1,
     assume_defined: bool = False,
     extra_module: KFlatModule | None = None,
+    optimize_kcfg: bool = False,
 ) -> bool:
     prover: APRProver | ImpliesProver
     try:
@@ -131,6 +132,7 @@ def create_prover() -> APRProver:
                     direct_subproof_rules=direct_subproof_rules,
                     assume_defined=assume_defined,
                     extra_module=extra_module,
+                    optimize_kcfg=optimize_kcfg,
                 )
 
             def update_status_bar(_proof: Proof) -> None: