pyk.ktool.krun module

class KRun(definition_dir: Path, use_directory: Path | None = None, command: str = 'krun', bug_report: BugReport | None = None, extra_unparsing_modules: Iterable[KFlatModule] = (), patch_symbol_table: Callable[[SymbolTable], None] | None = None)[source]

Bases: KPrint

command: str

krun(input_file: Path) → tuple[int, KInner][source]

run(pgm: Pattern, *, cmap: Mapping[str, str] | None = None, pmap: Mapping[str, str] | None = None, term: bool = False, depth: int | None = None, expand_macros: bool = True, search_final: bool = False, no_pattern: bool = False, output: KRunOutput | None = KRunOutput.PRETTY, check: bool = False, pipe_stderr: bool = True, bug_report: BugReport | None = None, debugger: bool = False) → None[source]

run_pattern(pattern: Pattern, *, depth: int | None = None, expand_macros: bool = False, search_final: bool = False, no_pattern: bool = False, pipe_stderr: bool = True, check: bool = False, bug_report: BugReport | None = None, debugger: bool = False) → Pattern[source]

run_process(pgm: Pattern, *, cmap: Mapping[str, str] | None = None, pmap: Mapping[str, str] | None = None, term: bool = False, depth: int | None = None, expand_macros: bool = True, search_final: bool = False, no_pattern: bool = False, output: KRunOutput | None = KRunOutput.PRETTY, pipe_stderr: bool = True, bug_report: BugReport | None = None, debugger: bool = False) → CompletedProcess[source]

run_proof_hint(pgm: Pattern, *, cmap: Mapping[str, str] | None = None, pmap: Mapping[str, str] | None = None, output: KRunOutput | None = None, parser: str | None = None, term: bool = False, temp_dir: Path | None = None, depth: int | None = None, expand_macros: bool = True, search_final: bool = False, no_pattern: bool = False, check: bool = False, pipe_stderr: bool = True, debugger: bool = False, proof_hint: bool = False) → bytes[source]

class KRunOutput(value)[source]

Bases: Enum

An enumeration.

BINARY = 'binary'

JSON = 'json'

KAST = 'kast'

KORE = 'kore'

LATEX = 'latex'

NONE = 'none'

PRETTY = 'pretty'

PROGRAM = 'program'

llvm_interpret(definition_dir: str | Path, pattern: Pattern, *, depth: int | None = None, check: bool = True) → Pattern[source]

Execute the interpreter binary generated by the LLVM Backend.

Parameters:

definition_dir – Path to the kompiled definition directory.
pattern – KORE pattern to start rewriting from.
depth – Maximal number of rewrite steps to take.

Returns:

The pattern resulting from the rewrites.

Raises:

RuntimeError – If check and the interpreter fails.

llvm_interpret_raw(definition_dir: str | Path, kore: str, *, depth: int | None = None, check: bool = True) → CompletedProcess[source]

Execute the interpreter binary generated by the LLVM Backend, with no processing of input/output.

Parameters:

definition_dir – Path to the kompiled definition directory.
pattern – KORE string to start rewriting from.
depth – Maximal number of rewrite steps to take.
check – check the return code of the CompletedProcess

Returns:

The CompletedProcess of the interpreter.

Raises:

CalledProcessError – If check and the interpreter fails.