pyk.kore.rule module

final class AppRule(lhs: 'App', rhs: 'Pattern', req: 'Pattern | None', ens: 'Pattern | None', sort: 'Sort', priority: 'int', uid: 'str', label: 'str | None')[source]

Bases: SimpliRule[App]

ens: Pattern | None

static from_axiom(axiom: Axiom) → AppRule[source]

label: str | None

lhs: App

priority: int

req: Pattern | None

rhs: Pattern

sort: Sort

uid: str

final class CeilRule(lhs: 'Ceil', rhs: 'Pattern', req: 'Pattern | None', ens: 'Pattern | None', sort: 'Sort', priority: 'int', uid: 'str', label: 'str | None')[source]

Bases: SimpliRule[Ceil]

ens: Pattern | None

static from_axiom(axiom: Axiom) → CeilRule[source]

label: str | None

lhs: Ceil

priority: int

req: Pattern | None

rhs: Pattern

sort: Sort

uid: str

final class EqualsRule(lhs: 'Equals', rhs: 'Pattern', req: 'Pattern | None', ens: 'Pattern | None', sort: 'Sort', priority: 'int', uid: 'str', label: 'str | None')[source]

Bases: SimpliRule[Equals]

ens: Pattern | None

static from_axiom(axiom: Axiom) → EqualsRule[source]

label: str | None

lhs: Equals

priority: int

req: Pattern | None

rhs: Pattern

sort: Sort

uid: str

final class FunctionRule(lhs: 'App', rhs: 'Pattern', req: 'Pattern | None', ens: 'Pattern | None', sort: 'Sort', arg_sorts: 'tuple[Sort, ...]', anti_left: 'Pattern | None', priority: 'int', uid: 'str', label: 'str | None')[source]

Bases: Rule

anti_left: Pattern | None

arg_sorts: tuple[Sort, ...]

ens: Pattern | None

static from_axiom(axiom: Axiom) → FunctionRule[source]

label: str | None

lhs: App

priority: int

req: Pattern | None

rhs: Pattern

sort: Sort

to_axiom() → Axiom[source]

uid: str

final class RewriteRule(lhs: 'App', rhs: 'App', req: 'Pattern | None', ens: 'Pattern | None', ctx: 'EVar | None', priority: 'int', uid: 'str', label: 'str | None')[source]