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.