From 82f8e27794727ce7ca66d1dd32c1a4a90a1b4e61 Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Tue, 17 Dec 2024 10:15:47 +0000
Subject: [PATCH] introducing the optimize_kcfg parameter

---
 kevm-pyk/src/kevm_pyk/__main__.py | 1 +
 kevm-pyk/src/kevm_pyk/cli.py      | 9 +++++++++
 kevm-pyk/src/kevm_pyk/utils.py    | 2 ++
 3 files changed, 12 insertions(+)

diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
index 23f1453486..3203d3fd53 100644
--- 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
index 43e3f90daa..5b0c32885b 100644
--- 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
index 26bcf540b4..5831776b7d 100644
--- 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: