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 <[email protected]>

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. <[email protected]>",

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'

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')

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

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}')

package/version

@@ -1 +1 @@
-1.0.675
+1.0.676