pyk.kcfg.explore module

class KCFGExplore(cterm_symbolic: CTermSymbolic, *, kcfg_semantics: KCFGSemantics | None = None, id: str | None = None)[source]

Bases: object

check_extendable(kcfg_exploration: KCFGExploration, node: KCFG.Node) → None[source]

cterm_symbolic: CTermSymbolic

extend_cterm(_cterm: CTerm, node_id: int, *, execute_depth: int | None = None, cut_point_rules: Iterable[str] = (), terminal_rules: Iterable[str] = (), module_name: str | None = None) → list[KCFGExtendResult][source]

id: str

implication_failure_reason(antecedent: CTerm, consequent: CTerm, assume_defined: bool = False) → tuple[bool, str][source]

kcfg_semantics: KCFGSemantics

pretty_print(kinner: KInner) → str[source]

section_edge(cfg: KCFG, source_id: NodeIdLike, target_id: NodeIdLike, logs: dict[int, tuple[LogEntry, ...]], sections: int = 2) → tuple[int, ...][source]

simplify(cfg: KCFG, logs: dict[int, tuple[LogEntry, ...]]) → None[source]

step(cfg: KCFG, node_id: NodeIdLike, logs: dict[int, tuple[LogEntry, ...]], depth: int = 1, module_name: str | None = None) → int[source]