pyk.kore.syntax module

final class AliasDecl(alias: 'Symbol', param_sorts: 'Iterable[Sort]', sort: 'Sort', left: 'App', right: 'Pattern', attrs: 'Iterable[App]' = ())[source]

Bases: Sentence

alias: Symbol

attrs: tuple[App, ...]

left: App

let(*, alias: Symbol | None = None, param_sorts: Iterable[Sort] | None = None, sort: Sort | None = None, left: App | None = None, right: Pattern | None = None, attrs: Iterable[App] | None = None) → AliasDecl[source]

let_attrs(attrs: Iterable[App]) → AliasDecl[source]

param_sorts: tuple[Sort, ...]

right: Pattern

sort: Sort

write(output: IO[str]) → None[source]

final class And(sort: 'Sort', ops: 'Iterable[Pattern]' = ())[source]

Bases: MultiaryConn

let(*, sort: Sort | None = None, ops: Iterable[Pattern] | None = None) → And[source]

let_patterns(patterns: Iterable[Pattern]) → And[source]

let_sort(sort: Sort) → And[source]

classmethod of(symbol: str, sorts: Iterable[Sort] = (), patterns: Iterable[Pattern] = ()) → And[source]

ops: tuple[Pattern, ...]

sort: Sort

classmethod symbol() → str[source]

final class App(symbol: 'str | SymbolId', sorts: 'Iterable[Sort]' = (), args: 'Iterable[Pattern]' = ())[source]

Bases: Pattern

args: tuple[Pattern, ...]

let(*, symbol: str | SymbolId | None = None, sorts: Iterable | None = None, args: Iterable | None = None) → App[source]

let_patterns(patterns: Iterable[Pattern]) → App[source]

property patterns: tuple[Pattern, ...]

sorts: tuple[Sort, ...]

symbol: str

write(output: IO[str]) → None[source]

class Assoc[source]

Bases: Pattern

property app: App

args: tuple[Pattern, ...]

abstract classmethod kore_symbol() → str[source]

abstract property pattern: Pattern

property patterns: tuple[Pattern, ...]

sorts: tuple[Sort, ...]

symbol: str

write(output: IO[str]) → None[source]

final class Axiom(vars: 'Iterable[SortVar]', pattern: 'Pattern', attrs: 'Iterable[App]' = ())[source]

Bases: AxiomLike

attrs: tuple[App, ...]

let(*, vars: Iterable[SortVar] | None = None, pattern: Pattern | None = None, attrs: Iterable[App] | None = None) → Axiom[source]

let_attrs(attrs: Iterable[App]) → Axiom[source]

pattern: Pattern

vars: tuple[SortVar, ...]

class AxiomLike[source]

Bases: Sentence

pattern: Pattern

vars: tuple[SortVar, ...]

write(output: IO[str]) → None[source]

class BinaryConn[source]

Bases: MLConn

left: Pattern

property patterns: tuple[Pattern, Pattern]

right: Pattern

class BinaryPred[source]

Bases: MLPred

left: Pattern

property patterns: tuple[Pattern, Pattern]

right: Pattern

property sorts: tuple[Sort, Sort]

final class Bottom(sort: 'Sort')[source]

Bases: NullaryConn

let(*, sort: Sort | None = None) → Bottom[source]

let_patterns(patterns: Iterable[Pattern]) → Bottom[source]

let_sort(sort: Sort) → Bottom[source]

classmethod of(symbol: str, sorts: Iterable[Sort] = (), patterns: Iterable[Pattern] = ()) → Bottom[source]

sort: Sort

classmethod symbol() → str[source]

final class Ceil(op_sort: 'Sort', sort: 'Sort', pattern: 'Pattern')[source]

Bases: RoundPred

let(*, op_sort: Sort | None = None, sort: Sort | None = None, pattern: Pattern | None = None) → Ceil[source]

let_patterns(patterns: Iterable[Pattern]) → Ceil[source]

let_sort(sort: Sort) → Ceil[source]

classmethod of(symbol: str, sorts: Iterable[Sort] = (), patterns: Iterable[Pattern] = ()) → Ceil[source]

op_sort: Sort

pattern: Pattern

sort: Sort

classmethod symbol() → str[source]

final class Claim(vars: 'Iterable[SortVar]', pattern: 'Pattern', attrs: 'Iterable[App]' = ())[source]

Bases: AxiomLike

attrs: tuple[App, ...]

let(*, vars: Iterable[SortVar] | None = None, pattern: Pattern | None = None, attrs: Iterable[App] | None = None) → Claim[source]

let_attrs(attrs: Iterable[App]) → Claim[source]

pattern: Pattern

vars: tuple[SortVar, ...]

final class DV(sort: 'Sort', value: 'String')[source]

Bases: MLPattern, WithSort

property ctor_patterns: tuple[String]

let(*, sort: Sort | None = None, value: String | None = None) → DV[source]

let_patterns(patterns: Iterable[Pattern]) → DV[source]

let_sort(sort: Sort) → DV[source]

classmethod of(symbol: str, sorts: Iterable[Sort] = (), patterns: Iterable[Pattern] = ()) → DV[source]

property patterns: tuple[()]

sort: Sort

property sorts: tuple[Sort]

classmethod symbol() → str[source]

value: String

final class Definition(modules: 'Iterable[Module]' = (), attrs: 'Iterable[App]' = ())[source]

Bases: Kore, WithAttrs, Iterable[Module]

attrs: tuple[App, ...]

property axioms: tuple[Axiom, ...]

compute_ordinals() → Definition[source]

get_axiom_by_ordinal(ordinal: int) → Axiom[source]

let(*, modules: Iterable[Module] | None = None, attrs: Iterable[App] | None = None) → Definition[source]

let_attrs(attrs: Iterable[App]) → Definition[source]

modules: tuple[Module, ...]

property sentences: tuple[Sentence, ...]

write(output: IO[str]) → None[source]

final class EVar(name: 'str | Id', sort: 'Sort')[source]

Bases: VarPattern

let(*, name: str | Id | None = None, sort: Sort | None = None) → EVar[source]

let_patterns(patterns: Iterable[Pattern]) → EVar[source]

let_sort(sort: Sort) → EVar[source]

name: str

sort: Sort

final class Equals(op_sort: 'Sort', sort: 'Sort', left: 'Pattern', right: 'Pattern')[source]

Bases: BinaryPred

left: Pattern

let(*, op_sort: Sort | None = None, sort: Sort | None = None, left: Pattern | None = None, right: Pattern | None = None) → Equals[source]

let_patterns(patterns: Iterable[Pattern]) → Equals[source]

let_sort(sort: Sort) → Equals[source]

classmethod of(symbol: str, sorts: Iterable[Sort] = (), patterns: Iterable[Pattern] = ()) → Equals[source]

op_sort: Sort

right: Pattern

sort: Sort

classmethod symbol() → str[source]

final class Exists(sort: 'Sort', var: 'EVar', pattern: 'Pattern')[source]

Bases: MLQuant

let(*, sort: Sort | None = None, var: EVar | None = None, pattern: Pattern | None = None) → Exists[source]

let_patterns(patterns: Iterable[Pattern]) → Exists[source]

let_sort(sort: Sort) → Exists[source]

classmethod of(symbol: str, sorts: Iterable[Sort] = (), patterns: Iterable[Pattern] = ()) → Exists[source]

pattern: Pattern

sort: Sort

classmethod symbol() → str[source]

var: EVar

final class Floor(op_sort: 'Sort', sort: 'Sort', pattern: 'Pattern')[source]

Bases: RoundPred

let(*, op_sort: Sort | None = None, sort: Sort | None = None, pattern: Pattern | None = None) → Floor[source]

let_patterns(patterns: Iterable[Pattern]) → Floor[source]

let_sort(sort: Sort) → Floor[source]

classmethod of(symbol: str, sorts: Iterable[Sort] = (), patterns: Iterable[Pattern] = ()) → Floor[source]

op_sort: Sort

pattern: Pattern

sort: Sort

classmethod symbol() → str[source]

final class Forall(sort: 'Sort', var: 'EVar', pattern: 'Pattern')[source]

Bases: MLQuant

let(*, sort: Sort | None = None, var: EVar | None = None, pattern: Pattern | None = None) → Forall[source]

let_patterns(patterns: Iterable[Pattern]) → Forall[source]

let_sort(sort: Sort) → Forall[source]

classmethod of(symbol: str, sorts: Iterable[Sort] = (), patterns: Iterable[Pattern] = ()) → Forall[source]

pattern: Pattern

sort: Sort

classmethod symbol() → str[source]

var: EVar

final class Id(value: 'str')[source]

Bases: object

value: str

final class Iff(sort: 'Sort', left: 'Pattern', right: 'Pattern')[source]

Bases: BinaryConn

left: Pattern

let(*, sort: Sort | None = None, left: Pattern | None = None, right: Pattern | None = None) → Iff[source]

let_patterns(patterns: Iterable[Pattern]) → Iff[source]

let_sort(sort: Sort) → Iff[source]

classmethod of(symbol: str, sorts: Iterable[Sort] = (), patterns: Iterable[Pattern] = ()) → Iff[source]

right: Pattern

sort: Sort

classmethod symbol() → str[source]

final class Implies(sort: 'Sort', left: 'Pattern', right: 'Pattern')[source]

Bases: BinaryConn

left: Pattern

let(*, sort: Sort | None = None, left: Pattern | None = None, right: Pattern | None = None) → Implies[source]

let_patterns(patterns: Iterable[Pattern]) → Implies[source]

let_sort(sort: Sort) → Implies[source]

classmethod of(symbol: str, sorts: Iterable[Sort] = (), patterns: Iterable[Pattern] = ()) → Implies[source]

right: Pattern

sort: Sort

classmethod symbol() → str[source]

final class Import(module_name: 'str | Id', attrs: 'Iterable[App]' = ())[source]

Bases: Sentence

attrs: tuple[App, ...]

let(*, module_name: str | Id | None = None, attrs: Iterable[App] | None = None) → Import[source]

let_attrs(attrs: Iterable[App]) → Import[source]

module_name: str

write(output: IO[str]) → None[source]

final class In(op_sort: 'Sort', sort: 'Sort', left: 'Pattern', right: 'Pattern')[source]

Bases: BinaryPred

left: Pattern

let(*, op_sort: Sort | None = None, sort: Sort | None = None, left: Pattern | None = None, right: Pattern | None = None) → In[source]

let_patterns(patterns: Iterable[Pattern]) → In[source]

let_sort(sort: Sort) → In[source]

classmethod of(symbol: str, sorts: Iterable[Sort] = (), patterns: Iterable[Pattern] = ()) → In[source]

op_sort: Sort

right: Pattern

sort: Sort

classmethod symbol() → str[source]

class Kore[source]

Bases: ABC

property text: str

abstract write(output: IO[str]) → None[source]

final class LeftAssoc(symbol: 'str | SymbolId', sorts: 'Iterable[Sort]' = (), args: 'Iterable[Pattern]' = ())[source]

Bases: Assoc

args: tuple[Pattern, ...]

classmethod kore_symbol() → str[source]

let(*, symbol: str | SymbolId | None = None, sorts: Iterable | None = None, args: Iterable | None = None) → LeftAssoc[source]

let_patterns(patterns: Iterable[Pattern]) → LeftAssoc[source]

property pattern: Pattern

sorts: tuple[Sort, ...]

symbol: str

class MLConn[source]

Bases: MLPattern, WithSort

property sorts: tuple[Sort]

class MLFixpoint[source]

Bases: MLPattern

property ctor_patterns: tuple[SVar, Pattern]

pattern: Pattern

property patterns: tuple[Pattern]

property sorts: tuple[()]

var: SVar

class MLPattern[source]

Bases: Pattern

property ctor_patterns: tuple[Pattern, ...]

Return patterns used to construct the term with of.

Except for DV, MLFixpoint and MLQuant this coincides with patterns.

classmethod of(symbol: str, sorts: Iterable[Sort] = (), patterns: Iterable[Pattern] = ()) → ML[source]

abstract property sorts: tuple[Sort, ...]

abstract classmethod symbol() → str[source]

write(output: IO[str]) → None[source]

class MLPred[source]

Bases: MLPattern, WithSort

op_sort: Sort

class MLQuant[source]

Bases: MLPattern, WithSort

property ctor_patterns: tuple[EVar, Pattern]

pattern: Pattern

property patterns: tuple[Pattern]

sort: Sort

property sorts: tuple[Sort]

var: EVar

class MLRewrite[source]

Bases: MLPattern, WithSort

property sorts: tuple[Sort]

final class Module(name: 'str | Id', sentences: 'Iterable[Sentence]' = (), attrs: 'Iterable[App]' = ())[source]

Bases: Kore, WithAttrs, Iterable[Sentence]

attrs: tuple[App, ...]

property axioms: tuple[Axiom, ...]

let(*, name: str | Id | None = None, sentences: Iterable[Sentence] | None = None, attrs: Iterable[App] | None = None) → Module[source]

let_attrs(attrs: Iterable[App]) → Module[source]

name: str

sentences: tuple[Sentence, ...]

property symbol_decls: tuple[SymbolDecl, ...]

write(output: IO[str]) → None[source]

final class Mu(var: 'SVar', pattern: 'Pattern')[source]

Bases: MLFixpoint

let(*, var: SVar | None = None, pattern: Pattern | None = None) → Mu[source]

let_patterns(patterns: Iterable[Pattern]) → Mu[source]

classmethod of(symbol: str, sorts: Iterable[Sort] = (), patterns: Iterable[Pattern] = ()) → Mu[source]

pattern: Pattern

classmethod symbol() → str[source]

var: SVar

class MultiaryConn[source]

Bases: MLConn

ops: tuple[Pattern, ...]

property patterns: tuple[Pattern, ...]

final class Next(sort: 'Sort', pattern: 'Pattern')[source]

Bases: MLRewrite

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

let_patterns(patterns: Iterable[Pattern]) → Next[source]

let_sort(sort: Sort) → Next[source]

classmethod of(symbol: str, sorts: Iterable[Sort] = (), patterns: Iterable[Pattern] = ()) → Next[source]

pattern: Pattern

property patterns: tuple[Pattern]

sort: Sort

classmethod symbol() → str[source]

final class Not(sort: 'Sort', pattern: 'Pattern')[source]

Bases: UnaryConn

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

let_patterns(patterns: Iterable[Pattern]) → Not[source]

let_sort(sort: Sort) → Not[source]

classmethod of(symbol: str, sorts: Iterable[Sort] = (), patterns: Iterable[Pattern] = ()) → Not[source]

pattern: Pattern

sort: Sort

classmethod symbol() → str[source]

final class Nu(var: 'SVar', pattern: 'Pattern')[source]

Bases: MLFixpoint

let(*, var: SVar | None = None, pattern: Pattern | None = None) → Nu[source]

let_patterns(patterns: Iterable[Pattern]) → Nu[source]

classmethod of(symbol: str, sorts: Iterable[Sort] = (), patterns: Iterable[Pattern] = ()) → Nu[source]

pattern: Pattern

classmethod symbol() → str[source]

var: SVar

class NullaryConn[source]

Bases: MLConn

property patterns: tuple[()]

final class Or(sort: 'Sort', ops: 'Iterable[Pattern]' = ())[source]

Bases: MultiaryConn

let(*, sort: Sort | None = None, ops: Iterable[Pattern] | None = None) → Or[source]

let_patterns(patterns: Iterable[Pattern]) → Or[source]

let_sort(sort: Sort) → Or[source]

classmethod of(symbol: str, sorts: Iterable[Sort] = (), patterns: Iterable[Pattern] = ()) → Or[source]

ops: tuple[Pattern, ...]

sort: Sort

classmethod symbol() → str[source]

class Pattern[source]

Bases: Kore

bottom_up(f: Callable[[Pattern], Pattern]) → Pattern[source]

bottom_up_with_summary(f: Callable[[Pattern, list[A]], tuple[Pattern, A]]) → tuple[Pattern, A][source]

collect(f: Callable[[Pattern], None]) → None[source]

property dict: dict[str, Any]

static from_dict(dct: Mapping[str, Any]) → Pattern[source]

static from_json(s: str) → Pattern[source]

property json: str

abstract let_patterns(patterns: Iterable[Pattern]) → P[source]

map_patterns(f: Callable[[Pattern], Pattern]) → P[source]

abstract property patterns: tuple[Pattern, ...]

top_down(f: Callable[[Pattern], Pattern]) → Pattern[source]

final class Rewrites(sort: 'Sort', left: 'Pattern', right: 'Pattern')[source]

Bases: MLRewrite

left: Pattern

let(*, sort: Sort | None = None, left: Pattern | None = None, right: Pattern | None = None) → Rewrites[source]

let_patterns(patterns: Iterable[Pattern]) → Rewrites[source]

let_sort(sort: Sort) → Rewrites[source]

classmethod of(symbol: str, sorts: Iterable[Sort] = (), patterns: Iterable[Pattern] = ()) → Rewrites[source]

property patterns: tuple[Pattern, Pattern]

right: Pattern

sort: Sort

classmethod symbol() → str[source]

final class RightAssoc(symbol: 'str | SymbolId', sorts: 'Iterable[Sort]' = (), args: 'Iterable[Pattern]' = ())[source]

Bases: Assoc

args: tuple[Pattern, ...]

classmethod kore_symbol() → str[source]

let(*, symbol: str | SymbolId | None = None, sorts: Iterable | None = None, args: Iterable | None = None) → RightAssoc[source]

let_patterns(patterns: Iterable[Pattern]) → RightAssoc[source]

property pattern: Pattern

sorts: tuple[Sort, ...]

symbol: str

class RoundPred[source]

Bases: MLPred

pattern: Pattern

property patterns: tuple[Pattern]

property sorts: tuple[Sort, Sort]

final class SVar(name: 'str | SetVarId', sort: 'Sort')[source]

Bases: VarPattern

let(*, name: str | SetVarId | None = None, sort: Sort | None = None) → SVar[source]

let_patterns(patterns: Iterable[Pattern]) → SVar[source]

let_sort(sort: Sort) → SVar[source]

name: str

sort: Sort

class Sentence[source]: Bases: Kore, WithAttrs

final class SetVarId(value: 'str')[source]

Bases: object

value: str

class Sort[source]

Bases: Kore

abstract property dict: dict[str, Any]

static from_dict(dct: Mapping[str, Any]) → Sort[source]

static from_json(s: str) → Sort[source]

property json: str

name: str

final class SortApp(name: 'str | Id', sorts: 'Iterable[Sort]' = ())[source]

Bases: Sort

property dict: dict[str, Any]

let(*, name: str | Id | None = None, sorts: Iterable[Sort] | None = None) → SortApp[source]

name: str

sorts: tuple[Sort, ...]

write(output: IO[str]) → None[source]

final class SortDecl(name: 'str | Id', vars: 'Iterable[SortVar]', attrs: 'Iterable[App]' = (), *, hooked: 'bool' = False)[source]

Bases: Sentence

attrs: tuple[App, ...]

hooked: bool

let(*, name: str | Id | None = None, vars: Iterable[SortVar] | None = None, attrs: Iterable[App] | None = None, hooked: bool | None = None) → SortDecl[source]

let_attrs(attrs: Iterable[App]) → SortDecl[source]

name: str

vars: tuple[SortVar, ...]

write(output: IO[str]) → None[source]

final class SortVar(name: 'str | Id')[source]

Bases: Sort

property dict: dict[str, Any]

let(*, name: str | Id | None = None) → SortVar[source]

name: str

write(output: IO[str]) → None[source]

final class String(value: 'str')[source]

Bases: Pattern

let(*, value: str | None = None) → String[source]

let_patterns(patterns: Iterable[Pattern]) → String[source]

property patterns: tuple[()]

value: str

write(output: IO[str]) → None[source]

final class Symbol(name: 'str | SymbolId', vars: 'Iterable[SortVar]' = ())[source]

Bases: Kore

let(*, name: str | SymbolId | None = None, vars: Iterable[SortVar] | None = None) → Symbol[source]

name: str

vars: tuple[SortVar, ...]

write(output: IO[str]) → None[source]

final class SymbolDecl(symbol: 'Symbol', param_sorts: 'Iterable[Sort]', sort: 'Sort', attrs: 'Iterable[App]' = (), *, hooked: 'bool' = False)[source]

Bases: Sentence

attrs: tuple[App, ...]

hooked: bool

let(*, symbol: Symbol | None = None, param_sorts: Iterable[Sort] | None = None, sort: Sort | None = None, attrs: Iterable[App] | None = None, hooked: bool | None = None) → SymbolDecl[source]