From bce2ea7075f88feb2720d6e4afbe430ef55fbe4e Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 27 Nov 2024 00:29:52 +0700 Subject: [PATCH] Thread through option to add modules to prover context (#2654) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * kevm-pyk/utils: thread through option `extra_module` to run_prover * kevm-pyk/utils: add import of KFlatModule --------- Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> --- kevm-pyk/src/kevm_pyk/utils.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py index 4aeebc356a..26bcf540b4 100644 --- a/kevm-pyk/src/kevm_pyk/utils.py +++ b/kevm-pyk/src/kevm_pyk/utils.py @@ -30,7 +30,7 @@ from collections.abc import Callable, Collection, Iterable, Iterator from typing import Final, TypeVar - from pyk.kast.outer import KClaim, KDefinition + from pyk.kast.outer import KClaim, KDefinition, KFlatModule from pyk.kcfg import KCFG from pyk.kcfg.semantics import KCFGSemantics from pyk.kore.rpc import FallbackReason @@ -114,6 +114,7 @@ def run_prover( task_id: TaskID | None = None, maintenance_rate: int = 1, assume_defined: bool = False, + extra_module: KFlatModule | None = None, ) -> bool: prover: APRProver | ImpliesProver try: @@ -129,6 +130,7 @@ def create_prover() -> APRProver: fast_check_subsumption=fast_check_subsumption, direct_subproof_rules=direct_subproof_rules, assume_defined=assume_defined, + extra_module=extra_module, ) def update_status_bar(_proof: Proof) -> None: