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]¶