From 25be7669a6d42341d563cf53354ba0bbd29d9372 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Petar=20Maksimovi=C4=87?=
 <PetarMax@users.noreply.github.com>
Date: Thu, 8 Aug 2024 16:43:59 +0200
Subject: [PATCH] Adding support for the `--assume-defined` flag (#2568)

* adding support for assume-defined flag

* Set Version: 1.0.675

* Set Version: 1.0.676

* correction

---------

Co-authored-by: devops <devops@runtimeverification.com>
---
 kevm-pyk/pyproject.toml           | 2 +-
 kevm-pyk/src/kevm_pyk/__init__.py | 2 +-
 kevm-pyk/src/kevm_pyk/__main__.py | 1 +
 kevm-pyk/src/kevm_pyk/cli.py      | 9 +++++++++
 kevm-pyk/src/kevm_pyk/utils.py    | 4 +++-
 package/version                   | 2 +-
 6 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
index 95a1ec6b20..e6365ff167 100644
--- a/kevm-pyk/pyproject.toml
+++ b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.675"
+version = "1.0.676"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py
index 835d845de9..371912bbe7 100644
--- a/kevm-pyk/src/kevm_pyk/__init__.py
+++ b/kevm-pyk/src/kevm_pyk/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '1.0.675'
+VERSION: Final = '1.0.676'
diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
index 4950486f63..cf5df3e531 100644
--- a/kevm-pyk/src/kevm_pyk/__main__.py
+++ b/kevm-pyk/src/kevm_pyk/__main__.py
@@ -356,6 +356,7 @@ def create_kcfg_explore() -> KCFGExplore:
                 direct_subproof_rules=options.direct_subproof_rules,
                 max_frontier_parallel=options.max_frontier_parallel,
                 force_sequential=options.force_sequential,
+                assume_defined=options.assume_defined,
             )
             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 356b4c6ad7..1b4f62e718 100644
--- a/kevm-pyk/src/kevm_pyk/cli.py
+++ b/kevm-pyk/src/kevm_pyk/cli.py
@@ -376,6 +376,7 @@ class KProveOptions(Options):
     fast_check_subsumption: bool
     direct_subproof_rules: bool
     maintenance_rate: int
+    assume_defined: bool
 
     @staticmethod
     def default() -> dict[str, Any]:
@@ -385,6 +386,7 @@ def default() -> dict[str, Any]:
             'fast_check_subsumption': False,
             'direct_subproof_rules': False,
             'maintenance_rate': 1,
+            'assume_defined': False,
         }
 
 
@@ -853,6 +855,13 @@ def kprove_args(self) -> ArgumentParser:
             type=int,
             help='The number of proof iterations performed between two writes to disk and status bar updates. Note that setting to >1 may result in work being discarded if proof is interrupted.',
         )
+        args.add_argument(
+            '--assume-defined',
+            dest='assume_defined',
+            default=None,
+            action='store_true',
+            help='Use the implication check of the Booster (experimental).',
+        )
         return args
 
     @cached_property
diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py
index ce150a041e..315aeddb55 100644
--- a/kevm-pyk/src/kevm_pyk/utils.py
+++ b/kevm-pyk/src/kevm_pyk/utils.py
@@ -114,6 +114,7 @@ def run_prover(
     progress: Progress | None = None,
     task_id: TaskID | None = None,
     maintenance_rate: int = 1,
+    assume_defined: bool = False,
 ) -> bool:
     prover: APRProver | ImpliesProver
     try:
@@ -129,6 +130,7 @@ def create_prover() -> APRProver:
                     always_check_subsumption=always_check_subsumption,
                     fast_check_subsumption=fast_check_subsumption,
                     direct_subproof_rules=direct_subproof_rules,
+                    assume_defined=assume_defined,
                 )
 
             def update_status_bar(_proof: Proof) -> None:
@@ -156,7 +158,7 @@ def update_status_bar(_proof: Proof) -> None:
                 )
 
         elif type(proof) is EqualityProof:
-            prover = ImpliesProver(proof, kcfg_explore=create_kcfg_explore())
+            prover = ImpliesProver(proof, kcfg_explore=create_kcfg_explore(), assume_defined=assume_defined)
             prover.advance_proof(proof)
         else:
             raise ValueError(f'Do not know how to build prover for proof: {proof}')
diff --git a/package/version b/package/version
index b6da864894..59a11504ad 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-1.0.675
+1.0.676