pyk.kore.internal module

class Collection(sort, concat, element, unit, kind)[source]

Bases: NamedTuple

concat: str: Alias for field number 1

element: str: Alias for field number 2

static from_decl(decl: SortDecl) → Collection[source]

kind: CollectionKind: Alias for field number 4

sort: str: Alias for field number 0

unit: str: Alias for field number 3

class CollectionKind(value)[source]

Bases: Enum

An enumeration.

LIST = 'List'

MAP = 'Map'

SET = 'Set'

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 collections: FrozenDict[str, Collection]

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

filter_rewrites(labels: Iterable[str]) → KoreDefn[source]: Keep only rewrite rules with certain labels in the definition.

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