pyk.kcfg.semantics module

class DefaultSemantics[source]

Bases: KCFGSemantics

abstract_node(c: CTerm) → CTerm[source]

can_make_custom_step(c: CTerm) → bool[source]

custom_step(c: CTerm, cs: CTermSymbolic) → KCFGExtendResult | None[source]

is_loop(c: CTerm) → bool[source]

is_mergeable(c1: CTerm, c2: CTerm) → bool[source]

is_terminal(c: CTerm) → bool[source]

same_loop(c1: CTerm, c2: CTerm) → bool[source]

class KCFGSemantics[source]

Bases: ABC

abstract abstract_node(c: CTerm) → CTerm[source]

abstract can_make_custom_step(c: CTerm) → bool[source]

abstract custom_step(c: CTerm, cs: CTermSymbolic) → KCFGExtendResult | None[source]

abstract is_loop(c: CTerm) → bool[source]

abstract is_mergeable(c1: CTerm, c2: CTerm) → bool[source]

abstract is_terminal(c: CTerm) → bool[source]

abstract same_loop(c1: CTerm, c2: CTerm) → bool[source]