pyk.kore.kompiled module

final class KompiledKore(sort_table: 'KoreSortTable', symbol_table: 'KoreSymbolTable')[source]

Bases: object

add_injections(pattern: Pattern, sort: Sort | None = None) → Pattern[source]

static for_definition(definition: Definition) → KompiledKore[source]

static from_dict(dct: dict[str, Any]) → KompiledKore[source]

static load(definition_dir: str | Path) → KompiledKore[source]

static load_from_json(json_file: str | Path) → KompiledKore[source]

static load_from_kore(kore_file: str | Path) → KompiledKore[source]

sort_table: KoreSortTable

symbol_table: KoreSymbolTable

to_dict() → dict[str, Any][source]

write(definition_dir: str | Path) → None[source]

final class KoreSortTable(subsorts: 'Iterable[tuple[Sort, Sort]]')[source]

Bases: object

static for_definition(definition: Definition) → KoreSortTable[source]

is_subsort(sort1: Sort, sort2: Sort) → bool[source]

meet(sort1: Sort, sort2: Sort) → Sort[source]

final class KoreSymbolTable(symbol_decls: 'Iterable[SymbolDecl]' = ())[source]

Bases: object

static for_definition(definition: Definition, *, with_ml_symbols: bool = True) → KoreSymbolTable[source]

infer_sort(pattern: Pattern) → Sort[source]

pattern_sorts(pattern: Pattern) → tuple[Sort, ...][source]

resolve(symbol_id: str, sorts: Iterable[Sort] = ()) → tuple[Sort, tuple[Sort, ...]][source]