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) → KCFGExtendResult[source]¶

id: str¶

implication_failure_reason(antecedent: CTerm, consequent: CTerm) → 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]¶