pyk.kcfg.kcfg module

final class Abstract(cterm: 'CTerm')

Bases: KCFGExtendResult

cterm: CTerm

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

Bases: KCFGExtendResult

constraints: tuple[KInner, ...]

heuristic: bool

class KCFG(cfg_dir: Path | None = None, optimize_memory: bool = True)

Bases: Container[Union[KCFG.Node, KCFG.Successor]]

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

Bases: EdgeLike

csubst: CSubst

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

replace_source(node: Node) → Cover

replace_target(node: Node) → Cover

source: Node

target: Node

to_dict() → dict[str, Any]

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

Bases: EdgeLike

depth: int

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

replace_source(node: Node) → Edge

replace_target(node: Node) → Edge

rules: tuple[str, ...]

source: Node

target: Node

to_dict() → dict[str, Any]

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

class EdgeLike

Bases: Successor

source: Node

target: Node

property targets: tuple[Node, ...]

class MultiEdge(source: 'KCFG.Node')

Bases: Successor

source: Node

abstract with_single_target(target: Node) → MultiEdge

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

Bases: MultiEdge

property edges: tuple[Edge, ...]

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

replace_source(node: Node) → NDBranch

replace_target(node: Node) → NDBranch

rules: tuple[str, ...]

source: Node

property targets: tuple[Node, ...]

to_dict() → dict[str, Any]

with_single_target(target: Node) → NDBranch

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

Bases: object

add_attr(attr: NodeAttr) → Node

attrs: frozenset[NodeAttr]

cterm: CTerm

discard_attr(attr: NodeAttr) → Node

property free_vars: frozenset[str]

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

id: int

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

remove_attr(attr: NodeAttr) → Node

to_dict() → dict[str, Any]

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

Bases: MultiEdge

property covers: tuple[Cover, ...]

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

replace_source(node: Node) → Split

replace_target(node: Node) → Split

source: Node

property splits: dict[int, CSubst]

property targets: tuple[Node, ...]

to_dict() → dict[str, Any]

with_single_target(target: Node) → Split

class Successor

Bases: ABC

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

abstract replace_source(node: Node) → Successor

abstract replace_target(node: Node) → Successor

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]

add_alias(alias: str, node_id: int | str) → None

add_attr(node_id: int | str, attr: NodeAttr) → None

add_node(node: Node) → None

add_stuck(node_id: int | str) → None

add_successor(succ: Successor) → None

add_vacuous(node_id: int | str) → None

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

contains_cover(cover: Cover) → bool

contains_edge(edge: Edge) → bool

contains_ndbranch(ndbranch: NDBranch) → bool

contains_node(node: Node) → bool

contains_split(split: Split) → bool

cover(source_id: NodeIdLike, target_id: NodeIdLike) → Cover | None

property covered: list[Node]

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

create_cover(source_id: NodeIdLike, target_id: NodeIdLike, csubst: CSubst | None = None) → Cover

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

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

create_node(cterm: CTerm) → Node

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

discard_attr(node_id: int | str, attr: NodeAttr) → None

discard_stuck(node_id: int | str) → None

discard_vacuous(node_id: int | str) → None

edge(source_id: NodeIdLike, target_id: NodeIdLike) → Edge | None

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

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

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

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

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

static from_json(s: str, optimize_memory: bool = True) → KCFG

get_node(node_id: int | str) → Node | None

is_covered(node_id: int | str) → bool

is_leaf(node_id: int | str) → bool

is_ndbranch(node_id: int | str) → bool

is_root(node_id: int | str) → bool

is_split(node_id: int | str) → bool

is_stuck(node_id: int | str) → bool

is_vacuous(node_id: int | str) → bool

property leaves: list[Node]

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

lift_edge(b_id: int | str) → None

Lift an edge up another edge directly preceding it.

Input:

• b_id: the identifier of the central node B of a sequence of edges A –> B –> C.

Effect: A –M steps–> B –N steps–> C becomes A –(M + N) steps–> C. Node B is removed.

Output: None

Raises: An AssertionError if the edges in question are not in place.

lift_edges() → bool

Perform all possible edge lifts across the KCFG.

Given the KCFG design, it is not possible for one edge lift to either disallow another or allow another that was not previously possible. Therefore, this function is guaranteed to lift all possible edges without having to loop.

Input: None

Effect: The KCFG is transformed to an equivalent in which no further edge lifts are possible.

Output:

• bool: An indicator of whether or not at least one edge lift was performed.

lift_split_edge(b_id: int | str) → None

Lift a split up an edge directly preceding it.

Input:

• b_id: the identifier of the central node B of the structure A –> B –> [C_1, …, C_N].

Effect:

A –M steps–> B –[cond_1, …, cond_N]–> [C_1, …, C_N] becomes A –[cond_1, …, cond_N]–> [A #And cond_1 –M steps–> C_1, …, A #And cond_N –M steps–> C_N]. Node B is removed.

Output: None

Raises:

• AssertionError, if the structure in question is not in place.

• AssertionError, if any of the cond_i contain variables not present in A.

lift_split_split(b_id: int | str) → None

Lift a split up a split directly preceding it, joining them into a single split.

Input:

• b_id: the identifier of the node B of the structure A –[…, cond_B, …]–> […, B, …] with B –[cond_1, …, cond_N]–> [C_1, …, C_N]

Effect:

A –[…, cond_B, …]–> […, B, …] with B –[cond_1, …, cond_N]–> [C_1, …, C_N] becomes A –[…, cond_B #And cond_1, …, cond_B #And cond_N, …]–> […, C_1, …, C_N, …]. Node B is removed.

Output: None

Raises:

• AssertionError, if the structure in question is not in place.

lift_splits() → bool

Perform all possible split liftings.

Input: None

Effect: The KCFG is transformed to an equivalent in which no further split lifts are possible.

Output:

• bool: An indicator of whether or not at least one split lift was performed.

minimize() → None

Minimize KCFG by repeatedly performing the lifting transformations.

The loop is designed so that each transformation is performed once in each iteration.

Input: None

Effect: The KCFG is transformed to an equivalent in which no further lifting transformations are possible.

Output: None

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

node(node_id: int | str) → Node

property nodes: list[Node]

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

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

predecessors(target_id: NodeIdLike) → list[Successor]

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

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

static read_cfg_data(cfg_dir: Path) → KCFG

static read_node_data(cfg_dir: Path, node_id: int) → KCFG.Node

remove_alias(alias: str) → None

remove_attr(node_id: int | str, attr: NodeAttr) → None

remove_cover(source_id: int | str, target_id: int | str) → None

remove_edge(source_id: int | str, target_id: int | str) → None

remove_node(node_id: int | str) → None

remove_stuck(node_id: int | str) → None

remove_vacuous(node_id: int | str) → None

replace_node(node: Node) → None

property root: list[Node]

shortest_distance_between(node_1_id: int | str, node_2_id: int | str) → int | None

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

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

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

property stuck: list[Node]

successors(source_id: NodeIdLike) → list[Successor]

to_dict() → dict[str, Any]

to_json() → str

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

to_rules(priority: int = 20) → list[KRuleLike]

property uncovered: list[Node]

property vacuous: list[Node]

write_cfg_data() → None

zero_depth_between(node_1_id: int | str, node_2_id: int | str) → bool

class KCFGExtendResult

Bases: ABC

class KCFGNodeAttr(value: str)

Bases: NodeAttr

STUCK = NodeAttr(value='stuck')

VACUOUS = NodeAttr(value='vacuous')

class KCFGStore(store_path: Path)

Bases: object

property kcfg_json_path: Path

property kcfg_node_dir: Path

kcfg_node_path(node_id: int) → Path

read_cfg_data() → dict[str, Any]

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

store_path: Path

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

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

Bases: KCFGExtendResult

cterms: tuple[CTerm, ...]

logs: tuple[LogEntry, ...]

rule_labels: tuple[str, ...]

class NodeAttr(value: 'str')

Bases: object

value: str

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

Bases: KCFGExtendResult

cterm: CTerm

cut: bool = False

depth: int

logs: tuple[LogEntry, ...]

rule_labels: list[str]

final class Stuck

Bases: KCFGExtendResult

final class Vacuous

Bases: KCFGExtendResult