pyk.kore.internal module

final class KoreDefn(sorts: 'FrozenDict[str, SortDecl]', symbols: 'FrozenDict[str, SymbolDecl]', subsorts: 'FrozenDict[str, frozenset[str]]', rewrites: 'tuple[RewriteRule, ...]', functions: 'FrozenDict[str, tuple[FunctionRule, ...]]')[source]

Bases: object

property ctor_symbols: FrozenDict[str, tuple[str, ...]]

static from_definition(defn: Definition) → KoreDefn[source]

functions: FrozenDict[str, tuple[FunctionRule, ...]]

let(*, sorts: FrozenDict[str, SortDecl] | None = None, symbols: FrozenDict[str, SymbolDecl] | None = None, subsorts: FrozenDict[str, frozenset[str]] | None = None, rewrites: tuple[RewriteRule, ...] | None = None, functions: FrozenDict[str, tuple[FunctionRule, ...]] | None = None) → KoreDefn[source]

project_to_rewrites() → KoreDefn[source]: Project definition to symbols that are part of the configuration or are (transitively) referred to from rewrite axioms.

project_to_symbols() → KoreDefn[source]: Project definition to symbols present in the definition.

rewrites: tuple[RewriteRule, ...]

sorts: FrozenDict[str, SortDecl]

subsorts: FrozenDict[str, frozenset[str]]

symbols: FrozenDict[str, SymbolDecl]