Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Thread through option to add modules to prover context #2654

Merged
merged 4 commits into from
Nov 26, 2024
Merged

Thread through option to add modules to prover context #2654

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
2fe7317
kevm-pyk/utils: thread through option `extra_module` to run_prover
ehildenb Nov 12, 2024
a4321c5
Merge branch 'master' into extra-module-prove
ehildenb Nov 26, 2024
e633433
Merge branch 'master' into extra-module-prove
anvacaru Nov 26, 2024
6555fc7
kevm-pyk/utils: add import of KFlatModule
ehildenb Nov 26, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion kevm-pyk/src/kevm_pyk/utils.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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:
Expand All @@ -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:
Expand Down
Loading