pyk.ktool.kprove module

class KProve(definition_dir: Path, main_file: Path | None = None, use_directory: Path | None = None, command: str = 'kprove', bug_report: BugReport | None = None, extra_unparsing_modules: Iterable[KFlatModule] = (), patch_symbol_table: Callable[[SymbolTable], None] | None = None)

Bases: KPrint

get_claim_modules(spec_file: Path, spec_module_name: str | None = None, include_dirs: Iterable[Path] = (), md_selector: str | None = None, type_inference_mode: TypeInferenceMode | None = None) → KFlatModuleList

get_claims(spec_file: Path, spec_module_name: str | None = None, include_dirs: Iterable[Path] = (), md_selector: str | None = None, claim_labels: Iterable[str] | None = None, exclude_claim_labels: Iterable[str] | None = None, include_dependencies: bool = True, type_inference_mode: TypeInferenceMode | None = None) → list[KClaim]

main_file: Path | None

prove(spec_file: Path, spec_module_name: str | None = None, args: Iterable[str] = (), include_dirs: Iterable[Path] = (), md_selector: str | None = None, haskell_args: Iterable[str] = (), depth: int | None = None) → list[CTerm]

prove_claim(claim: KClaim, claim_id: str, lemmas: Iterable[KRule] = (), args: Iterable[str] = (), haskell_args: Iterable[str] = (), depth: int | None = None) → list[CTerm]

prove_claim_rpc(claim: KClaim, kcfg_semantics: KCFGSemantics | None = None, id: str | None = None, port: int | None = None, kore_rpc_command: str | Iterable[str] | None = None, llvm_definition_dir: Path | None = None, smt_timeout: int | None = None, smt_retry_limit: int | None = None, smt_tactic: str | None = None, bug_report: BugReport | None = None, haskell_log_format: KoreExecLogFormat = KoreExecLogFormat.ONELINE, haskell_log_entries: Iterable[str] = (), log_axioms_file: Path | None = None, trace_rewrites: bool = False, start_server: bool = True, maude_port: int | None = None, fallback_on: Iterable[FallbackReason] | None = None, interim_simplification: int | None = None, no_post_exec_simplify: bool = False) → Proof

prove_rpc(options: ProveOptions, claim_labels: Iterable[str] | None = None, exclude_claim_labels: Iterable[str] | None = None, kcfg_semantics: KCFGSemantics | None = None, id: str | None = None, port: int | None = None, kore_rpc_command: str | Iterable[str] | None = None, llvm_definition_dir: Path | None = None, smt_timeout: int | None = None, smt_retry_limit: int | None = None, smt_tactic: str | None = None, bug_report: BugReport | None = None, haskell_log_format: KoreExecLogFormat = KoreExecLogFormat.ONELINE, haskell_log_entries: Iterable[str] = (), log_axioms_file: Path | None = None, trace_rewrites: bool = False, start_server: bool = True, maude_port: int | None = None, fallback_on: Iterable[FallbackReason] | None = None, interim_simplification: int | None = None, no_post_exec_simplify: bool = False) → list[Proof]

prover: list[str]

prover_args: list[str]

class KProveOutput(value)

Bases: Enum

An enumeration.

BINARY = 'binary'

JSON = 'json'

KAST = 'KAST'

KORE = 'kore'

LATEX = 'latex'

NONE = 'none'

PRETTY = 'pretty'

PROGAM = 'program'