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: MLSyntaxSugar

app: App¶

property ctor_patterns: tuple[App]¶

abstract property pattern: Pattern¶

property patterns: tuple[()]¶

property sorts: tuple[()]¶

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

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

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

modules: tuple[Module, ...]¶

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(app: 'App')[source]¶

Bases: Assoc

app: App¶

let(*, app: App | None = None) → LeftAssoc[source]¶

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

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

property pattern: Pattern¶

classmethod symbol() → str[source]¶

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, ...]¶: Patterns used to construct the term with of. Except for Assoc, DV, MLFixpoint and MLQuant it 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]¶

class MLSyntaxSugar[source]¶: Bases: MLPattern

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

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(app: 'App')[source]¶

Bases: Assoc

app: App¶

let(*, app: App | None = None) → RightAssoc[source]¶

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

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

property pattern: Pattern¶

classmethod symbol() → str[source]¶

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