pyk.kcfg.kcfg module

final class Abstract(cterm: 'CTerm')[source]

Bases: KCFGExtendResult

cterm: CTerm

final class Branch(constraints: 'Iterable[KInner]', *, heuristic: 'bool' = False, info: 'str' = '')[source]

Bases: KCFGExtendResult

constraints: tuple[KInner, ...]

heuristic: bool

info: str = ''

class KCFG(cfg_dir: Path | None = None, optimize_memory: bool = True)[source]

Bases: Container[KCFG.Node | KCFG.Successor]

final class Cover(source: 'KCFG.Node', target: 'KCFG.Node', csubst: 'CSubst')[source]

Bases: EdgeLike

csubst: CSubst

static from_dict(dct: dict[str, Any], nodes: Mapping[int, KCFG.Node]) → KCFG.Cover[source]

replace_source(node: Node) → Cover[source]

replace_target(node: Node) → Cover[source]

source: Node

target: Node

to_dict() → dict[str, Any][source]

final class Edge(source: 'KCFG.Node', target: 'KCFG.Node', depth: 'int', rules: 'tuple[str, ...]')[source]

Bases: EdgeLike

depth: int

static from_dict(dct: dict[str, Any], nodes: Mapping[int, KCFG.Node]) → KCFG.Edge[source]

replace_source(node: Node) → Edge[source]

replace_target(node: Node) → Edge[source]

rules: tuple[str, ...]

source: Node

target: Node

to_dict() → dict[str, Any][source]

to_rule(label: str, claim: bool = False, priority: int | None = None, defunc_with: KDefinition | None = None, minimize: bool = False) → KRuleLike[source]

class EdgeLike[source]

Bases: Successor

source: Node

target: Node

property targets: tuple[Node, ...]

final class MergedEdge(source: Node, target: Node, edges: tuple[Edge, ...])[source]

Bases: EdgeLike

Merged edge is a collection of edges that have been merged into a single edge.

edges: tuple[Edge, ...]

static from_dict(dct: dict[str, Any], nodes: Mapping[int, KCFG.Node]) → KCFG.Successor[source]

replace_source(node: Node) → Successor[source]

replace_target(node: Node) → Successor[source]

source: Node

target: Node

to_dict() → dict[str, Any][source]

to_rule(label: str, claim: bool = False, priority: int | None = None) → KRuleLike[source]

class MultiEdge(source: 'KCFG.Node')[source]

Bases: Successor

source: Node

abstract with_single_target(target: Node) → MultiEdge[source]

final class NDBranch(source: 'KCFG.Node', _targets: 'Iterable[KCFG.Node]', rules: 'tuple[str, ...]')[source]

Bases: MultiEdge

property edges: tuple[Edge, ...]

static from_dict(dct: dict[str, Any], nodes: Mapping[int, KCFG.Node]) → KCFG.NDBranch[source]

replace_source(node: Node) → NDBranch[source]

replace_target(node: Node) → NDBranch[source]

rules: tuple[str, ...]

source: Node

property targets: tuple[Node, ...]

to_dict() → dict[str, Any][source]

with_single_target(target: Node) → NDBranch[source]

final class Node(id: 'int', cterm: 'CTerm', attrs: 'Iterable[NodeAttr]' = ())[source]

Bases: object

add_attr(attr: NodeAttr) → Node[source]

attrs: frozenset[NodeAttr]

cterm: CTerm

discard_attr(attr: NodeAttr) → Node[source]

property free_vars: frozenset[str]

static from_dict(dct: dict[str, Any]) → KCFG.Node[source]

id: int

let(cterm: CTerm | None = None, attrs: Iterable[KCFGNodeAttr] | None = None) → KCFG.Node[source]

remove_attr(attr: NodeAttr) → Node[source]

to_dict() → dict[str, Any][source]

final class Split(source: 'KCFG.Node', _targets: 'Iterable[tuple[KCFG.Node, CSubst]]')[source]

Bases: MultiEdge

property covers: tuple[Cover, ...]

static from_dict(dct: dict[str, Any], nodes: Mapping[int, KCFG.Node]) → KCFG.Split[source]

replace_source(node: Node) → Split[source]

replace_target(node: Node) → Split[source]

source: Node

property splits: dict[int, CSubst]

property targets: tuple[Node, ...]

to_dict() → dict[str, Any][source]

with_single_target(target: Node) → Split[source]

class Successor[source]

Bases: ABC

abstract static from_dict(dct: dict[str, Any], nodes: Mapping[int, KCFG.Node]) → KCFG.Successor[source]

abstract replace_source(node: Node) → Successor[source]

abstract replace_target(node: Node) → Successor[source]

source: Node

property source_vars: frozenset[str]

property target_ids: list[int]

property target_vars: frozenset[str]

abstract property targets: tuple[Node, ...]

abstract to_dict() → dict[str, Any][source]

add_alias(alias: str, node_id: int | str) → None[source]

add_attr(node_id: int | str, attr: NodeAttr) → None[source]

add_node(node: Node) → None[source]

add_stuck(node_id: int | str) → None[source]

add_successor(succ: Successor) → None[source]

add_vacuous(node_id: int | str) → None[source]

aliases(node_id: int | str) → list[str][source]

contains_cover(cover: Cover) → bool[source]

contains_edge(edge: Edge) → bool[source]

contains_merged_edge(edge: MergedEdge) → bool[source]

contains_ndbranch(ndbranch: NDBranch) → bool[source]

contains_node(node: Node) → bool[source]

contains_split(split: Split) → bool[source]

cover(source_id: NodeIdLike, target_id: NodeIdLike) → Cover | None[source]

property covered: list[Node]

covers(*, source_id: NodeIdLike | None = None, target_id: NodeIdLike | None = None) → list[Cover][source]

create_cover(source_id: NodeIdLike, target_id: NodeIdLike, csubst: CSubst | None = None) → Cover[source]

create_edge(source_id: NodeIdLike, target_id: NodeIdLike, depth: int, rules: Iterable[str] = ()) → Edge[source]

create_merged_edge(source_id: NodeIdLike, target_id: NodeIdLike, edges: Iterable[Edge]) → MergedEdge[source]

create_ndbranch(source_id: NodeIdLike, ndbranches: Iterable[NodeIdLike], rules: Iterable[str] = ()) → KCFG.NDBranch[source]

create_node(cterm: CTerm) → Node[source]

create_split(source_id: NodeIdLike, splits: Iterable[tuple[NodeIdLike, CSubst]]) → KCFG.Split[source]

create_split_by_nodes(source_id: NodeIdLike, target_ids: Iterable[NodeIdLike]) → KCFG.Split | None[source]: Create a split without crafting a CSubst.

discard_attr(node_id: int | str, attr: NodeAttr) → None[source]

discard_stuck(node_id: int | str) → None[source]

discard_vacuous(node_id: int | str) → None[source]

edge(source_id: NodeIdLike, target_id: NodeIdLike) → Edge | None[source]

edge_likes(*, source_id: NodeIdLike | None = None, target_id: NodeIdLike | None = None) → list[EdgeLike][source]

edges(*, source_id: NodeIdLike | None = None, target_id: NodeIdLike | None = None) → list[Edge][source]

extend(extend_result: KCFGExtendResult, node: KCFG.Node, logs: dict[int, tuple[LogEntry, ...]]) → None[source]

static from_claim(defn: KDefinition, claim: KClaim, cfg_dir: Path | None = None, optimize_memory: bool = True) → tuple[KCFG, NodeIdLike, NodeIdLike][source]

static from_dict(dct: Mapping[str, Any], optimize_memory: bool = True) → KCFG[source]

static from_json(s: str, optimize_memory: bool = True) → KCFG[source]

get_node(node_id: int | str) → Node | None[source]

is_covered(node_id: int | str) → bool[source]

is_leaf(node_id: int | str) → bool[source]

is_ndbranch(node_id: int | str) → bool[source]

is_root(node_id: int | str) → bool[source]

is_split(node_id: int | str) → bool[source]

is_stuck(node_id: int | str) → bool[source]

is_vacuous(node_id: int | str) → bool[source]

property leaves: list[Node]

let_node(node_id: NodeIdLike, cterm: CTerm | None = None, attrs: Iterable[KCFGNodeAttr] | None = None) → None[source]

merged_edge(source_id: NodeIdLike, target_id: NodeIdLike) → MergedEdge | None[source]

merged_edges(*, source_id: NodeIdLike | None = None, target_id: NodeIdLike | None = None) → list[MergedEdge][source]

ndbranches(*, source_id: int | str | None = None, target_id: int | str | None = None) → list[NDBranch][source]

node(node_id: int | str) → Node[source]

property nodes: list[Node]

static path_length(_path: Iterable[KCFG.Successor]) → int[source]

paths_between(source_id: NodeIdLike, target_id: NodeIdLike) → list[tuple[Successor, ...]][source]

predecessors(target_id: NodeIdLike) → list[Successor][source]

prune(node_id: NodeIdLike, keep_nodes: Iterable[NodeIdLike] = ()) → list[int][source]

reachable_nodes(source_id: int | str, *, reverse: bool = False) → set[Node][source]

static read_cfg_data(cfg_dir: Path) → KCFG[source]

static read_node_data(cfg_dir: Path, node_id: int) → KCFG.Node[source]

remove_alias(alias: str) → None[source]

remove_attr(node_id: int | str, attr: NodeAttr) → None[source]

remove_cover(source_id: int | str, target_id: int | str) → None[source]

remove_edge(source_id: int | str, target_id: int | str) → None[source]

remove_merged_edge(source_id: int | str, target_id: int | str) → None[source]

remove_node(node_id: int | str) → None[source]

remove_stuck(node_id: int | str) → None[source]

remove_vacuous(node_id: int | str) → None[source]

replace_node(node: Node) → None[source]

property root: list[Node]

shortest_distance_between(node_1_id: int | str, node_2_id: int | str) → int | None[source]

shortest_path_between(source_node_id: NodeIdLike, target_node_id: NodeIdLike) → tuple[Successor, ...] | None[source]

split_on_constraints(source_id: NodeIdLike, constraints: Iterable[KInner]) → list[int][source]

splits(*, source_id: NodeIdLike | None = None, target_id: NodeIdLike | None = None) → list[Split][source]

property stuck: list[Node]

successors(source_id: NodeIdLike) → list[Successor][source]

to_dict() → dict[str, Any][source]

to_dict_no_nodes() → dict[str, Any][source]

to_json() → str[source]

to_module(module_name: str | None = None, imports: Iterable[KImport] = (), priority: int = 20, att: KAtt = KAtt(atts=FrozenDict({}))) → KFlatModule[source]

to_rules(_id: str | None = None, priority: int = 20) → list[KRuleLike][source]

property uncovered: list[Node]

property vacuous: list[Node]

write_cfg_data() → None[source]

zero_depth_between(node_1_id: int | str, node_2_id: int | str) → bool[source]

class KCFGExtendResult[source]: Bases: ABC

class KCFGNodeAttr(value: str)[source]

Bases: NodeAttr

STUCK = NodeAttr(value='stuck')

VACUOUS = NodeAttr(value='vacuous')

class KCFGStore(store_path: Path)[source]

Bases: object

property kcfg_json_path: Path

property kcfg_node_dir: Path

kcfg_node_path(node_id: int) → Path[source]

read_cfg_data() → dict[str, Any][source]

read_node_data(node_id: int) → dict[str, Any][source]

store_path: Path

write_cfg_data(kcfg: KCFG, dct: dict[str, Any], deleted_nodes: Iterable[int] = (), created_nodes: Iterable[int] = ()) → None[source]

final class NDBranch(cterms: 'Iterable[CTerm]', logs: 'Iterable[LogEntry,]', rule_labels: 'Iterable[str]')[source]

Bases: KCFGExtendResult

cterms: tuple[CTerm, ...]

logs: tuple[LogEntry, ...]

rule_labels: tuple[str, ...]

class NodeAttr(value: 'str')[source]

Bases: object

value: str

final class Step(cterm: 'CTerm', depth: 'int', logs: 'tuple[LogEntry, ...]', rule_labels: 'list[str]', cut: 'bool' = False, info: 'str' = '')[source]

Bases: KCFGExtendResult

cterm: CTerm

cut: bool = False

depth: int

info: str = ''

logs: tuple[LogEntry, ...]

rule_labels: list[str]

final class Stuck[source]: Bases: KCFGExtendResult

final class Vacuous[source]: Bases: KCFGExtendResult