diff --git a/package/version b/package/version index 5a002f41e..464d50765 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.340 +0.1.341 diff --git a/pyproject.toml b/pyproject.toml index 5de3762a2..eb584251e 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.340" +version = "0.1.341" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/src/pyk/kast/manip.py b/src/pyk/kast/manip.py index 80f97a1ab..a5fd72458 100644 --- a/src/pyk/kast/manip.py +++ b/src/pyk/kast/manip.py @@ -51,16 +51,9 @@ def sort_assoc_label(label: str, kast: KInner) -> KInner: return kast -def sort_ac_collections(definition: KDefinition, kast: KInner) -> KInner: - ac_hooks = {'MAP.concat', 'SET.concat', 'BAG.concat'} - ac_collections = [ - prod.klabel.name - for prod in definition.productions - if prod.klabel is not None and 'hook' in prod.att and prod.att['hook'] in ac_hooks - ] - +def sort_ac_collections(kast: KInner) -> KInner: def _sort_ac_collections(_kast: KInner) -> KInner: - if type(_kast) is KApply and _kast.label.name in ac_collections: + if type(_kast) is KApply and (_kast.label.name in {'_Set_', '_Map_'} or _kast.label.name.endswith('CellMap_')): return sort_assoc_label(_kast.label.name, _kast) return _kast diff --git a/src/pyk/kast/pretty.py b/src/pyk/kast/pretty.py index 376707db4..87ea13b95 100644 --- a/src/pyk/kast/pretty.py +++ b/src/pyk/kast/pretty.py @@ -90,7 +90,7 @@ def print(self, kast: KAst) -> str: if self._unalias: kast = undo_aliases(self.definition, kast) if self._sort_collections: - kast = sort_ac_collections(self.definition, kast) + kast = sort_ac_collections(kast) return self._print_kinner(kast) raise AssertionError(f'Error unparsing: {kast}') diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index ccbab5e25..0a4773462 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -378,10 +378,10 @@ def extend( cut_point_rules: Iterable[str] = (), terminal_rules: Iterable[str] = (), ) -> None: - if not kcfg.is_frontier(node.id): - raise ValueError(f'Cannot extend non-frontier node {self.id}: {node.id}') - - kcfg.add_expanded(node.id) + if not kcfg.is_leaf(node.id): + raise ValueError(f'Cannot extend non-leaf node {self.id}: {node.id}') + if kcfg.is_stuck(node.id): + raise ValueError(f'Cannot extend stuck node {self.id}: {node.id}') _LOGGER.info(f'Extending KCFG from node {self.id}: {shorten_hashes(node.id)}') depth, cterm, next_cterms, next_node_logs = self.cterm_execute( @@ -399,6 +399,7 @@ def extend( # Stuck elif len(next_cterms) == 0: + kcfg.add_stuck(node.id) _LOGGER.info(f'Found stuck node {self.id}: {shorten_hashes(node.id)}') # Cut Rule diff --git a/src/pyk/kcfg/kcfg.py b/src/pyk/kcfg/kcfg.py index 5aeacf44d..40b18a28f 100644 --- a/src/pyk/kcfg/kcfg.py +++ b/src/pyk/kcfg/kcfg.py @@ -9,23 +9,27 @@ from ..cterm import CSubst, CTerm, build_claim, build_rule from ..kast.inner import KApply +from ..kast.kast import EMPTY_ATT from ..kast.manip import ( bool_to_ml_pred, extract_lhs, extract_rhs, flatten_label, + inline_cell_maps, remove_source_attributes, rename_generated_vars, + sort_ac_collections, ) -from ..utils import single +from ..kast.outer import KFlatModule if TYPE_CHECKING: from collections.abc import Iterable, Mapping from types import TracebackType from typing import Any + from ..kast import KAtt from ..kast.inner import KInner - from ..kast.outer import KClaim, KDefinition, KRuleLike + from ..kast.outer import KClaim, KDefinition, KImport, KRuleLike NodeIdLike = int | str @@ -84,11 +88,14 @@ def to_rule(self, label: str, claim: bool = False, priority: int | None = None) def is_ceil_condition(kast: KInner) -> bool: return type(kast) is KApply and kast.label.name == '#Ceil' + def _simplify_config(config: KInner) -> KInner: + return sort_ac_collections(inline_cell_maps(config)) + sentence_id = f'{label}-{self.source.id}-TO-{self.target.id}' init_constraints = [c for c in self.source.cterm.constraints if not is_ceil_condition(c)] - init_cterm = CTerm(self.source.cterm.config, init_constraints) + init_cterm = CTerm(_simplify_config(self.source.cterm.config), init_constraints) target_constraints = [c for c in self.target.cterm.constraints if not is_ceil_condition(c)] - target_cterm = CTerm(self.target.cterm.config, target_constraints) + target_cterm = CTerm(_simplify_config(self.target.cterm.config), target_constraints) rule: KRuleLike if claim: rule, _ = build_claim(sentence_id, init_cterm, target_cterm) @@ -193,9 +200,7 @@ def edges(self) -> tuple[KCFG.Edge, ...]: _covers: dict[int, dict[int, Cover]] _splits: dict[int, Split] _ndbranches: dict[int, NDBranch] - _init: set[int] - _target: set[int] - _expanded: set[int] + _stuck: set[int] _aliases: dict[str, int] _lock: RLock @@ -206,9 +211,7 @@ def __init__(self) -> None: self._covers = {} self._splits = {} self._ndbranches = {} - self._init = set() - self._target = set() - self._expanded = set() + self._stuck = set() self._aliases = {} self._lock = RLock() @@ -245,16 +248,12 @@ def nodes(self) -> list[Node]: return list(self._nodes.values()) @property - def init(self) -> list[Node]: - return [node for node in self.nodes if self.is_init(node.id)] - - @property - def target(self) -> list[Node]: - return [node for node in self.nodes if self.is_target(node.id)] + def root(self) -> list[Node]: + return [node for node in self.nodes if self.is_root(node.id)] @property - def expanded(self) -> list[Node]: - return [node for node in self.nodes if self.is_expanded(node.id)] + def stuck(self) -> list[Node]: + return [node for node in self.nodes if self.is_stuck(node.id)] @property def leaves(self) -> list[Node]: @@ -268,14 +267,6 @@ def covered(self) -> list[Node]: def uncovered(self) -> list[Node]: return [node for node in self.nodes if not self.is_covered(node.id)] - @property - def frontier(self) -> list[Node]: - return [node for node in self.nodes if self.is_frontier(node.id)] - - @property - def stuck(self) -> list[Node]: - return [node for node in self.nodes if self.is_stuck(node.id)] - @staticmethod def from_claim(defn: KDefinition, claim: KClaim) -> tuple[KCFG, NodeIdLike, NodeIdLike]: cfg = KCFG() @@ -285,14 +276,25 @@ def from_claim(defn: KDefinition, claim: KClaim) -> tuple[KCFG, NodeIdLike, Node claim_lhs = CTerm.from_kast(extract_lhs(claim_body)).add_constraint(bool_to_ml_pred(claim.requires)) init_node = cfg.create_node(claim_lhs) - cfg.add_init(init_node.id) claim_rhs = CTerm.from_kast(extract_rhs(claim_body)).add_constraint(bool_to_ml_pred(claim.ensures)) target_node = cfg.create_node(claim_rhs) - cfg.add_target(target_node.id) return cfg, init_node.id, target_node.id + @staticmethod + def path_length(_path: Iterable[KCFG.Successor]) -> int: + _path = tuple(_path) + if len(_path) == 0: + return 0 + if type(_path[0]) is KCFG.Split or type(_path[0]) is KCFG.Cover: + return KCFG.path_length(_path[1:]) + elif type(_path[0]) is KCFG.NDBranch: + return 1 + KCFG.path_length(_path[1:]) + elif type(_path[0]) is KCFG.Edge: + return _path[0].depth + KCFG.path_length(_path[1:]) + raise ValueError(f'Cannot handle Successor type: {type(_path[0])}') + def to_dict(self) -> dict[str, Any]: nodes = [node.to_dict() for node in self.nodes] edges = [edge.to_dict() for edge in self.edges()] @@ -300,9 +302,7 @@ def to_dict(self) -> dict[str, Any]: splits = [split.to_dict() for split in self.splits()] ndbranches = [ndbranch.to_dict() for ndbranch in self.ndbranches()] - init = sorted(self._init) - target = sorted(self._target) - expanded = sorted(self._expanded) + stuck = sorted(self._stuck) aliases = dict(sorted(self._aliases.items())) res = { @@ -312,9 +312,7 @@ def to_dict(self) -> dict[str, Any]: 'covers': covers, 'splits': splits, 'ndbranches': ndbranches, - 'init': init, - 'target': target, - 'expanded': expanded, + 'stuck': stuck, 'aliases': aliases, } return {k: v for k, v in res.items() if v} @@ -345,14 +343,8 @@ def from_dict(dct: Mapping[str, Any]) -> KCFG: csubst = CSubst.from_dict(cover_dict['csubst']) cfg.create_cover(source_id, target_id, csubst=csubst) - for init_id in dct.get('init') or []: - cfg.add_init(init_id) - - for target_id in dct.get('target') or []: - cfg.add_target(target_id) - - for expanded_id in dct.get('expanded') or []: - cfg.add_expanded(expanded_id) + for stuck_id in dct.get('stuck') or []: + cfg.add_stuck(stuck_id) for alias, node_id in dct.get('aliases', {}).items(): cfg.add_alias(alias=alias, node_id=node_id) @@ -383,16 +375,16 @@ def to_json(self) -> str: def from_json(s: str) -> KCFG: return KCFG.from_dict(json.loads(s)) - def get_unique_init(self) -> Node: - return single(self.init) - - def get_unique_target(self) -> Node: - return single(self.target) - - def get_first_frontier(self) -> Node: - if len(self.frontier) == 0: - raise ValueError('No frontiers remaining!') - return self.frontier[0] + def to_module( + self, + module_name: str | None = None, + imports: Iterable[KImport] = (), + att: KAtt = EMPTY_ATT, + ) -> KFlatModule: + module_name = module_name if module_name is not None else 'KCFG' + rules = [e.to_rule('BASIC-BLOCK') for e in self.edges()] + nd_steps = [edge.to_rule('ND-STEP') for ndbranch in self.ndbranches() for edge in ndbranch.edges] + return KFlatModule(module_name, rules + nd_steps, imports=imports, att=att) def _resolve_or_none(self, id_like: NodeIdLike) -> int | None: if type(id_like) is int: @@ -404,13 +396,6 @@ def _resolve_or_none(self, id_like: NodeIdLike) -> int | None: if type(id_like) is not str: raise TypeError(f'Expected int or str for id_like, got: {id_like}') - if id_like == '#init': - return self.get_unique_init().id - if id_like == '#target': - return self.get_unique_target().id - if id_like == '#frontier': - return self.get_first_frontier().id - if id_like.startswith('@'): if id_like[1:] in self._aliases: return self._aliases[id_like[1:]] @@ -454,9 +439,6 @@ def create_node(self, cterm: CTerm) -> Node: def remove_node(self, node_id: NodeIdLike) -> None: node_id = self._resolve(node_id) - for edge_in in [edge.source for edge in self.edges(target_id=node_id)]: - self.discard_expanded(edge_in.id) - self._nodes.pop(node_id) self._edges.pop(node_id, None) @@ -471,9 +453,7 @@ def remove_node(self, node_id: NodeIdLike) -> None: if not self._covers[source_id]: self._covers.pop(source_id) - self._init.discard(node_id) - self._target.discard(node_id) - self._expanded.discard(node_id) + self._stuck.discard(node_id) self._splits = {k: s for k, s in self._splits.items() if k != node_id and node_id not in s.target_ids} self._ndbranches = {k: b for k, b in self._ndbranches.items() if k != node_id and node_id not in b.target_ids} @@ -524,7 +504,7 @@ def _check_no_successors(self, source_id: NodeIdLike) -> None: def _check_no_zero_loops(self, source_id: NodeIdLike, target_ids: Iterable[NodeIdLike]) -> None: for target_id in target_ids: path = self.shortest_path_between(target_id, source_id) - if path is not None and path_length(path) == 0: + if path is not None and KCFG.path_length(path) == 0: raise ValueError( f'Adding successor would create zero-length loop with backedge: {source_id} -> {target_id}' ) @@ -638,17 +618,9 @@ def edge_likes(self, *, source_id: NodeIdLike | None = None, target_id: NodeIdLi 'List[KCFG.EdgeLike]', self.covers(source_id=source_id, target_id=target_id) ) - def add_init(self, node_id: NodeIdLike) -> None: - node_id = self._resolve(node_id) - self._init.add(node_id) - - def add_target(self, node_id: NodeIdLike) -> None: - node_id = self._resolve(node_id) - self._target.add(node_id) - - def add_expanded(self, node_id: NodeIdLike) -> None: + def add_stuck(self, node_id: NodeIdLike) -> None: node_id = self._resolve(node_id) - self._expanded.add(node_id) + self._stuck.add(node_id) def splits(self, *, source_id: NodeIdLike | None = None, target_id: NodeIdLike | None = None) -> list[Split]: source_id = self._resolve(source_id) if source_id is not None else None @@ -715,52 +687,28 @@ def add_alias(self, alias: str, node_id: NodeIdLike) -> None: node_id = self._resolve(node_id) self._aliases[alias] = node_id - def remove_init(self, node_id: NodeIdLike) -> None: + def remove_stuck(self, node_id: NodeIdLike) -> None: node_id = self._resolve(node_id) - if node_id not in self._init: - raise ValueError(f'Node is not init: {node_id}') - self._init.remove(node_id) - - def remove_target(self, node_id: NodeIdLike) -> None: - node_id = self._resolve(node_id) - if node_id not in self._target: - raise ValueError(f'Node is not target: {node_id}') - self._target.remove(node_id) - - def remove_expanded(self, node_id: NodeIdLike) -> None: - node_id = self._resolve(node_id) - if node_id not in self._expanded: - raise ValueError(f'Node is not expanded: {node_id}') - self._expanded.remove(node_id) + if node_id not in self._stuck: + raise ValueError(f'Node is not stuck: {node_id}') + self._stuck.remove(node_id) def remove_alias(self, alias: str) -> None: if alias not in self._aliases: raise ValueError(f'Alias does not exist: {alias}') self._aliases.pop(alias) - def discard_init(self, node_id: NodeIdLike) -> None: - node_id = self._resolve(node_id) - self._init.discard(node_id) - - def discard_target(self, node_id: NodeIdLike) -> None: + def discard_stuck(self, node_id: NodeIdLike) -> None: node_id = self._resolve(node_id) - self._target.discard(node_id) + self._stuck.discard(node_id) - def discard_expanded(self, node_id: NodeIdLike) -> None: + def is_root(self, node_id: NodeIdLike) -> bool: node_id = self._resolve(node_id) - self._expanded.discard(node_id) + return len(self.predecessors(node_id)) == 0 - def is_init(self, node_id: NodeIdLike) -> bool: - node_id = self._resolve(node_id) - return node_id in self._init - - def is_target(self, node_id: NodeIdLike) -> bool: - node_id = self._resolve(node_id) - return node_id in self._target - - def is_expanded(self, node_id: NodeIdLike) -> bool: + def is_stuck(self, node_id: NodeIdLike) -> bool: node_id = self._resolve(node_id) - return node_id in self._expanded + return node_id in self._stuck def is_split(self, node_id: NodeIdLike) -> bool: node_id = self._resolve(node_id) @@ -771,38 +719,20 @@ def is_ndbranch(self, node_id: NodeIdLike) -> bool: return node_id in self._ndbranches def is_leaf(self, node_id: NodeIdLike) -> bool: - node_id = self._resolve(node_id) - return node_id not in self._edges and node_id not in self._splits and node_id not in self._ndbranches + return len(self.successors(node_id)) == 0 def is_covered(self, node_id: NodeIdLike) -> bool: node_id = self._resolve(node_id) return node_id in self._covers - def is_frontier(self, node_id: NodeIdLike) -> bool: - node_id = self._resolve(node_id) - return not any( - [ - self.is_target(node_id), - self.is_expanded(node_id), - self.is_covered(node_id), - self.is_split(node_id), - ] - ) - - def is_stuck(self, node_id: NodeIdLike) -> bool: - node_id = self._resolve(node_id) - return self.is_expanded(node_id) and self.is_leaf(node_id) - - def prune(self, node_id: NodeIdLike, keep_init: bool = True, keep_target: bool = True) -> list[int]: + def prune(self, node_id: NodeIdLike, keep_nodes: Iterable[NodeIdLike] = ()) -> list[NodeIdLike]: nodes = self.reachable_nodes(node_id) - pruned_nodes = [] + keep_nodes = [self._resolve(nid) for nid in keep_nodes] + pruned_nodes: list[NodeIdLike] = [] for node in nodes: - if self.is_init(node.id) and keep_init: - continue - if self.is_target(node.id) and keep_target: - continue - self.remove_node(node.id) - pruned_nodes.append(node.id) + if node.id not in keep_nodes: + self.remove_node(node.id) + pruned_nodes.append(node.id) return pruned_nodes def shortest_path_between( @@ -811,7 +741,7 @@ def shortest_path_between( paths = self.paths_between(source_node_id, target_node_id) if len(paths) == 0: return None - return sorted(paths, key=(lambda path: path_length(path)))[0] + return sorted(paths, key=(lambda path: KCFG.path_length(path)))[0] def paths_between(self, source_id: NodeIdLike, target_id: NodeIdLike) -> list[tuple[Successor, ...]]: source_id = self._resolve(source_id) @@ -911,16 +841,3 @@ def reachable_nodes( ) return visited - - -def path_length(_path: Iterable[KCFG.Successor]) -> int: - _path = tuple(_path) - if len(_path) == 0: - return 0 - if type(_path[0]) is KCFG.Split or type(_path[0]) is KCFG.Cover: - return path_length(_path[1:]) - elif type(_path[0]) is KCFG.NDBranch: - return 1 + path_length(_path[1:]) - elif type(_path[0]) is KCFG.Edge: - return _path[0].depth + path_length(_path[1:]) - raise ValueError(f'Cannot handle Successor type: {type(_path[0])}') diff --git a/src/pyk/kcfg/show.py b/src/pyk/kcfg/show.py index c3e6b7a30..5aba44f11 100644 --- a/src/pyk/kcfg/show.py +++ b/src/pyk/kcfg/show.py @@ -14,7 +14,7 @@ push_down_rewrites, sort_ac_collections, ) -from ..kast.outer import KFlatModule +from ..kast.outer import KRule from ..prelude.k import DOTS from ..prelude.ml import mlAnd from ..utils import add_indent, ensure_dir_path @@ -26,7 +26,7 @@ from typing import Final from ..kast import KInner - from ..kast.outer import KDefinition + from ..kast.outer import KFlatModule, KSentence from ..ktool.kprint import KPrint from .kcfg import NodeIdLike @@ -51,21 +51,15 @@ def print_node(self, kcfg: KCFG, node: KCFG.Node) -> list[str]: kast = node.cterm.kast if self.minimize: kast = minimize_term(kast) - node_strs.extend(' ' + line for line in self.kprint.pretty_print(kast).split('\n')) + node_strs.extend(' ' + line for line in self.kprint.pretty_print(kast).split('\n')) return node_strs def node_attrs(self, kcfg: KCFG, node: KCFG.Node) -> list[str]: attrs = [] - if kcfg.is_init(node.id): - attrs.append('init') - if kcfg.is_target(node.id): - attrs.append('target') - if kcfg.is_expanded(node.id): - attrs.append('expanded') + if kcfg.is_root(node.id): + attrs.append('root') if kcfg.is_stuck(node.id): attrs.append('stuck') - if kcfg.is_frontier(node.id): - attrs.append('frontier') if kcfg.is_leaf(node.id): attrs.append('leaf') if kcfg.is_split(node.id): @@ -97,17 +91,39 @@ def _hide_cells(_k: KInner) -> KInner: return term @staticmethod - def simplify_config(defn: KDefinition, config: KInner, omit_cells: Iterable[str]) -> KInner: + def hide_cells_in_rules( + module: KFlatModule, module_name: str | None = None, omit_cells: Iterable[str] = () + ) -> KFlatModule: + def _hide_cells_in_rule(_sent: KSentence) -> KSentence: + if type(_sent) is KRule: + return _sent.let(body=KCFGShow.hide_cells(_sent.body, omit_cells)) + return _sent + + return module.let(sentences=map(_hide_cells_in_rule, module.sentences)) + + @staticmethod + def simplify_config(config: KInner, omit_cells: Iterable[str]) -> KInner: config = inline_cell_maps(config) - config = sort_ac_collections(defn, config) + config = sort_ac_collections(config) config = KCFGShow.hide_cells(config, omit_cells) return config - def pretty_segments( - self, - kcfg: KCFG, - minimize: bool = True, - ) -> Iterable[tuple[str, Iterable[str]]]: + @staticmethod + def make_unique_segments(segments: Iterable[tuple[str, Iterable[str]]]) -> Iterable[tuple[str, Iterable[str]]]: + _segments = [] + used_ids = [] + for id, seg_lines in segments: + suffix = '' + counter = 0 + while f'{id}{suffix}' in used_ids: + suffix = f'_{counter}' + counter += 1 + new_id = f'{id}{suffix}' + used_ids.append(new_id) + _segments.append((f'{new_id}', [l.rstrip() for l in seg_lines])) + return _segments + + def pretty_segments(self, kcfg: KCFG, minimize: bool = True) -> Iterable[tuple[str, Iterable[str]]]: """Return a pretty version of the KCFG in segments. Each segment is a tuple of an identifier and a list of lines to be printed for that segment (Tuple[str, Iterable[str]). @@ -180,14 +196,14 @@ def _print_subgraph(indent: str, curr_node: KCFG.Node, prior_on_trace: list[KCFG suffix = [] elbow = '├─' node_indent = '│ ' - if kcfg.is_init(curr_node.id): + if kcfg.is_root(curr_node.id): elbow = '┌─' - elif processed or kcfg.is_target(curr_node.id) or not successors: + elif processed or not successors: elbow = '└─' node_indent = ' ' if curr_node in prior_on_trace: suffix = ['(looped back)', ''] - elif processed and not kcfg.is_target(curr_node.id): + elif processed and not kcfg.is_leaf(curr_node.id): suffix = ['(continues as previously)', ''] else: suffix = [''] @@ -196,10 +212,7 @@ def _print_subgraph(indent: str, curr_node: KCFG.Node, prior_on_trace: list[KCFG ret_node_lines.extend(add_indent(indent + ' ', suffix)) ret_lines.append((f'node_{curr_node.id}', ret_node_lines)) - if processed or kcfg.is_target(curr_node.id): - return - - if not successors: + if processed or not successors: return successor = successors[0] @@ -253,32 +266,24 @@ def _print_subgraph(indent: str, curr_node: KCFG.Node, prior_on_trace: list[KCFG def _sorted_init_nodes() -> tuple[list[KCFG.Node], list[KCFG.Node]]: sorted_init_nodes = sorted(node for node in kcfg.nodes if node not in processed_nodes) - init_expanded_nodes = [] - init_unexpanded_nodes = [] - target_nodes = [] + init_nodes = [] + init_leaf_nodes = [] remaining_nodes = [] for node in sorted_init_nodes: - if kcfg.is_init(node.id): - if kcfg.is_expanded(node.id): - init_expanded_nodes.append(node) + if kcfg.is_root(node.id): + if kcfg.is_leaf(node.id): + init_leaf_nodes.append(node) else: - init_unexpanded_nodes.append(node) - elif kcfg.is_target(node.id): - target_nodes.append(node) + init_nodes.append(node) else: remaining_nodes.append(node) - return (init_expanded_nodes + init_unexpanded_nodes + target_nodes, remaining_nodes) + return (init_nodes + init_leaf_nodes, remaining_nodes) init, _ = _sorted_init_nodes() while init: ret_lines.append(('unknown', [''])) _print_subgraph('', init[0], []) init, _ = _sorted_init_nodes() - if kcfg.frontier or kcfg.stuck: - ret_lines.append(('unknown', ['', 'Target Nodes:'])) - for target in kcfg.target: - ret_node_lines = [''] + _print_node(target) - ret_lines.append((f'node_{target.id}', ret_node_lines)) _, remaining = _sorted_init_nodes() if remaining: ret_lines.append(('unknown', ['', 'Remaining Nodes:'])) @@ -286,18 +291,7 @@ def _sorted_init_nodes() -> tuple[list[KCFG.Node], list[KCFG.Node]]: ret_node_lines = [''] + _print_node(node) ret_lines.append((f'node_{node.id}', ret_node_lines)) - _ret_lines = [] - used_ids = [] - for id, seg_lines in ret_lines: - suffix = '' - counter = 0 - while f'{id}{suffix}' in used_ids: - suffix = f'_{counter}' - counter += 1 - new_id = f'{id}{suffix}' - used_ids.append(new_id) - _ret_lines.append((f'{new_id}', [l.rstrip() for l in seg_lines])) - return _ret_lines + return KCFGShow.make_unique_segments(ret_lines) def pretty( self, @@ -306,9 +300,11 @@ def pretty( ) -> Iterable[str]: return (line for _, seg_lines in self.pretty_segments(kcfg, minimize=minimize) for line in seg_lines) + def to_module(self, cfg: KCFG, module_name: str | None = None, omit_cells: Iterable[str] = ()) -> KFlatModule: + return KCFGShow.hide_cells_in_rules(cfg.to_module(module_name), omit_cells=omit_cells) + def show( self, - cfgid: str, cfg: KCFG, nodes: Iterable[NodeIdLike] = (), node_deltas: Iterable[tuple[NodeIdLike, NodeIdLike]] = (), @@ -316,6 +312,7 @@ def show( minimize: bool = True, sort_collections: bool = False, omit_cells: Iterable[str] = (), + module_name: str | None = None, ) -> list[str]: res_lines: list[str] = [] res_lines += self.pretty(cfg, minimize=minimize) @@ -337,8 +334,8 @@ def show( for node_id_1, node_id_2 in node_deltas: nodes_printed = True - config_1 = KCFGShow.simplify_config(self.kprint.definition, cfg.node(node_id_1).cterm.config, omit_cells) - config_2 = KCFGShow.simplify_config(self.kprint.definition, cfg.node(node_id_2).cterm.config, omit_cells) + config_1 = KCFGShow.simplify_config(cfg.node(node_id_1).cterm.config, omit_cells) + config_2 = KCFGShow.simplify_config(cfg.node(node_id_2).cterm.config, omit_cells) config_delta = push_down_rewrites(KRewrite(config_1, config_2)) if minimize: config_delta = minimize_term(config_delta) @@ -355,38 +352,11 @@ def show( res_lines.append('') if to_module: - module = self.to_module(cfgid, cfg, omit_cells=omit_cells) + module = self.to_module(cfg, module_name, omit_cells=omit_cells) res_lines.append(self.kprint.pretty_print(module, sort_collections=sort_collections)) return res_lines - def to_module( - self, - cfgid: str, - cfg: KCFG, - module_name: str | None = None, - imports: Iterable[str] = (), - omit_cells: Iterable[str] = (), - ) -> KFlatModule: - rules = [e.to_rule('BASIC-BLOCK') for e in cfg.edges()] - rules = [ - r.let(body=KCFGShow.simplify_config(self.kprint.definition, r.body, omit_cells=omit_cells)) for r in rules - ] - nd_steps = [edge.to_rule('ND-STEP') for ndbranch in cfg.ndbranches() for edge in ndbranch.edges] - nd_steps = [ - r.let(body=KCFGShow.simplify_config(self.kprint.definition, r.body, omit_cells=omit_cells)) - for r in nd_steps - ] - claims = [KCFG.Edge(nd, cfg.get_unique_target(), -1).to_rule('UNPROVEN', claim=True) for nd in cfg.frontier] - claims = [ - c.let(body=KCFGShow.simplify_config(self.kprint.definition, c.body, omit_cells=omit_cells)) for c in claims - ] - - cfg_module_name = ( - module_name if module_name is not None else f'SUMMARY-{cfgid.upper().replace(".", "-").replace("_", "-")}' - ) - return KFlatModule(cfg_module_name, rules + nd_steps + claims) - def dot(self, kcfg: KCFG) -> Digraph: def _short_label(label: str) -> str: return '\n'.join( @@ -429,14 +399,6 @@ def _short_label(label: str) -> str: label = '1 step' graph.edge(tail_name=ndbranch.source.id, head_name=target, label=f' {label} ') - for target_id in kcfg._target: - for node in kcfg.frontier: - attrs = {'class': 'target', 'style': 'solid'} - graph.edge(tail_name=node.id, head_name=target_id, label=' ???', **attrs) - for node in kcfg.stuck: - attrs = {'class': 'target', 'style': 'solid'} - graph.edge(tail_name=node.id, head_name=target_id, label=' false', **attrs) - return graph def dump(self, cfgid: str, cfg: KCFG, dump_dir: Path, dot: bool = False) -> None: @@ -449,7 +411,7 @@ def dump(self, cfgid: str, cfg: KCFG, dump_dir: Path, dot: bool = False) -> None if dot: cfg_dot = self.dot(cfg) dot_file = dump_dir / f'{cfgid}.dot' - dot_file.write_text(cfg_dot) + dot_file.write_text(cfg_dot.source) _LOGGER.info(f'Wrote DOT file {cfgid}: {dot_file}') nodes_dir = dump_dir / 'nodes' diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index acab87fc6..932f69c23 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -67,17 +67,28 @@ def terminal(self) -> list[KCFG.Node]: @property def pending(self) -> list[KCFG.Node]: - return [ - nd - for nd in self.kcfg.leaves - if nd not in self.terminal + self.kcfg.target and not self.kcfg.is_covered(nd.id) - ] + return [nd for nd in self.kcfg.leaves if self.is_pending(nd.id)] + + @property + def failing(self) -> list[KCFG.Node]: + return [nd for nd in self.kcfg.leaves if self.is_failing(nd.id)] def is_terminal(self, node_id: NodeIdLike) -> bool: - return self.kcfg._resolve(node_id) in (nd.id for nd in self.terminal) + return self.kcfg._resolve(node_id) in (self.kcfg._resolve(nid) for nid in self._terminal_nodes) def is_pending(self, node_id: NodeIdLike) -> bool: - return self.kcfg._resolve(node_id) in (nd.id for nd in self.pending) + return self.kcfg.is_leaf(node_id) and not ( + self.is_terminal(node_id) or self.kcfg.is_stuck(node_id) or self.is_target(node_id) + ) + + def is_init(self, node_id: NodeIdLike) -> bool: + return self.kcfg._resolve(node_id) == self.kcfg._resolve(self.init) + + def is_target(self, node_id: NodeIdLike) -> bool: + return self.kcfg._resolve(node_id) == self.kcfg._resolve(self.target) + + def is_failing(self, node_id: NodeIdLike) -> bool: + return self.kcfg.is_leaf(node_id) and not (self.is_pending(node_id) or self.is_target(node_id)) @staticmethod def read_proof(id: str, proof_dir: Path) -> APRProof: @@ -90,15 +101,12 @@ def read_proof(id: str, proof_dir: Path) -> APRProof: @property def status(self) -> ProofStatus: - if len(self.terminal) > 0: + if len(self.failing) > 0 or self.subproofs_status == ProofStatus.FAILED: return ProofStatus.FAILED elif len(self.pending) > 0 or self.subproofs_status == ProofStatus.PENDING: return ProofStatus.PENDING else: - if self.subproofs_status == ProofStatus.PASSED: - return ProofStatus.PASSED - else: - return ProofStatus.FAILED + return ProofStatus.PASSED @classmethod def from_dict(cls: type[APRProof], dct: Mapping[str, Any], proof_dir: Path | None = None) -> APRProof: @@ -164,11 +172,11 @@ def summary(self) -> Iterable[str]: f'APRProof: {self.id}', f' status: {self.status}', f' nodes: {len(self.kcfg.nodes)}', - f' frontier: {len(self.kcfg.frontier)}', - f' stuck: {len(self.kcfg.stuck)}', - 'Subproofs:' if len(self.subproof_ids) else '', f' pending: {len(self.pending)}', + f' failing: {len(self.failing)}', + f' stuck: {len(self.kcfg.stuck)}', f' terminal: {len(self.terminal)}', + f'Subproofs: {len(self.subproof_ids)}', ] for summary in subproofs_summaries: yield from summary @@ -207,30 +215,23 @@ def read_proof(id: str, proof_dir: Path) -> APRBMCProof: @property def bounded(self) -> list[KCFG.Node]: - return [self.kcfg.node(nid) for nid in self._bounded_nodes] - - @property - def pending(self) -> list[KCFG.Node]: - return [ - nd - for nd in self.kcfg.leaves - if nd not in self.terminal + self.kcfg.target + self.bounded and not self.kcfg.is_covered(nd.id) - ] + return [nd for nd in self.kcfg.leaves if self.is_bounded(nd.id)] def is_bounded(self, node_id: NodeIdLike) -> bool: - return self.kcfg._resolve(node_id) in (nd.id for nd in self.bounded) + return self.kcfg._resolve(node_id) in (self.kcfg._resolve(nid) for nid in self._bounded_nodes) - @property - def status(self) -> ProofStatus: - if ( - any(nd.id not in self._bounded_nodes for nd in self.kcfg.stuck) - or self.subproofs_status == ProofStatus.FAILED - ): - return ProofStatus.FAILED - elif len(self.pending) > 0 or self.subproofs_status == ProofStatus.PENDING: - return ProofStatus.PENDING - else: - return ProofStatus.PASSED + def is_failing(self, node_id: NodeIdLike) -> bool: + return self.kcfg.is_leaf(node_id) and not ( + self.is_pending(node_id) or self.is_target(node_id) or self.is_bounded(node_id) + ) + + def is_pending(self, node_id: NodeIdLike) -> bool: + return self.kcfg.is_leaf(node_id) and not ( + self.is_terminal(node_id) + or self.kcfg.is_stuck(node_id) + or self.is_bounded(node_id) + or self.is_target(node_id) + ) @classmethod def from_dict(cls: type[APRBMCProof], dct: Mapping[str, Any], proof_dir: Path | None = None) -> APRBMCProof: @@ -282,13 +283,12 @@ def summary(self) -> Iterable[str]: f'APRBMCProof(depth={self.bmc_depth}): {self.id}', f' status: {self.status}', f' nodes: {len(self.kcfg.nodes)}', - f' frontier: {len(self.kcfg.frontier)}', - f' stuck: {len([nd for nd in self.kcfg.stuck if nd.id not in self._bounded_nodes])}', - f' bmc-depth-bounded: {len(self._bounded_nodes)}', - 'Subproofs' if len(self.subproof_ids) else '', f' pending: {len(self.pending)}', + f' failing: {len(self.failing)}', + f' stuck: {len(self.kcfg.stuck)}', f' terminal: {len(self.terminal)}', f' bounded: {len(self.bounded)}', + f'Subproofs: {len(self.subproof_ids)}', ] for summary in subproofs_summaries: yield from summary @@ -318,7 +318,6 @@ def _check_terminal(self, curr_node: KCFG.Node) -> bool: if self._is_terminal(curr_node.cterm): _LOGGER.info(f'Terminal node {self.proof.id}: {shorten_hashes(curr_node.id)}.') self.proof.add_terminal(curr_node.id) - self.proof.kcfg.add_expanded(curr_node.id) return True return False @@ -442,7 +441,6 @@ def advance_proof( if nd.id != f.id and self._same_loop(nd.cterm, f.cterm) ] if len(prior_loops) >= self.proof.bmc_depth: - self.proof.kcfg.add_expanded(f.id) self.proof.add_bounded(f.id) super().advance_proof( diff --git a/src/pyk/proof/show.py b/src/pyk/proof/show.py index 330816f4c..365b6424f 100644 --- a/src/pyk/proof/show.py +++ b/src/pyk/proof/show.py @@ -3,12 +3,18 @@ import logging from typing import TYPE_CHECKING -from ..kcfg.show import NodePrinter +from ..kcfg.show import KCFGShow, NodePrinter +from ..utils import ensure_dir_path if TYPE_CHECKING: + from collections.abc import Iterable + from pathlib import Path from typing import Final + from graphviz import Digraph + from ..kcfg import KCFG + from ..kcfg.kcfg import NodeIdLike from ..ktool.kprint import KPrint from .reachability import APRBMCProof, APRProof @@ -46,3 +52,67 @@ def node_attrs(self, kcfg: KCFG, node: KCFG.Node) -> list[str]: if 'stuck' in attrs: attrs.remove('stuck') return attrs + + +class APRProofShow: + kcfg_show: KCFGShow + + def __init__(self, kprint: KPrint, node_printer: NodePrinter | None = None): + self.kcfg_show = KCFGShow(kprint, node_printer=node_printer) + + def pretty_segments(self, proof: APRProof, minimize: bool = True) -> Iterable[tuple[str, Iterable[str]]]: + ret_lines = list(self.kcfg_show.pretty_segments(proof.kcfg, minimize=minimize)) + if len(proof.pending) > 0: + target_node_lines = ['', 'Target Node:'] + target_node_lines += self.kcfg_show.node_printer.print_node(proof.kcfg, proof.kcfg.node(proof.target)) + ret_lines.append((f'node_{proof.target}', target_node_lines)) + return KCFGShow.make_unique_segments(ret_lines) + + def pretty(self, proof: APRProof, minimize: bool = True) -> Iterable[str]: + return (line for _, seg_lines in self.pretty_segments(proof, minimize=minimize) for line in seg_lines) + + def show( + self, + proof: APRProof, + nodes: Iterable[NodeIdLike] = (), + node_deltas: Iterable[tuple[NodeIdLike, NodeIdLike]] = (), + to_module: bool = False, + minimize: bool = True, + sort_collections: bool = False, + omit_cells: Iterable[str] = (), + ) -> list[str]: + res_lines = self.kcfg_show.show( + proof.kcfg, + nodes=nodes, + node_deltas=node_deltas, + to_module=to_module, + minimize=minimize, + sort_collections=sort_collections, + omit_cells=omit_cells, + module_name=f'SUMMARY-{proof.id.upper().replace("_", "-")}', + ) + return res_lines + + def dot(self, proof: APRProof) -> Digraph: + graph = self.kcfg_show.dot(proof.kcfg) + attrs = {'class': 'target', 'style': 'solid'} + for node in proof.pending: + graph.edge(tail_name=node.id, head_name=proof.target, label=' ???', **attrs) + for node in proof.kcfg.stuck: + graph.edge(tail_name=node.id, head_name=proof.target, label=' false', **attrs) + return graph + + def dump(self, proof: APRProof, dump_dir: Path, dot: bool = False) -> None: + ensure_dir_path(dump_dir) + + proof_file = dump_dir / f'{proof.id}.json' + proof_file.write_text(proof.json) + _LOGGER.info(f'Wrote CFG file {proof.id}: {proof_file}') + + if dot: + proof_dot = self.dot(proof) + dot_file = dump_dir / f'{proof.id}.dot' + dot_file.write_text(proof_dot.source) + _LOGGER.info(f'Wrote DOT file {proof.id}: {dot_file}') + + self.kcfg_show.dump(f'{proof.id}_cfg', proof.kcfg, dump_dir, dot=False) diff --git a/src/tests/integration/kcfg/test_cell_map.py b/src/tests/integration/kcfg/test_cell_map.py index 6cedb2521..4854fda4b 100644 --- a/src/tests/integration/kcfg/test_cell_map.py +++ b/src/tests/integration/kcfg/test_cell_map.py @@ -135,7 +135,7 @@ def test_all_path_reachability_prove( ) proof = APRProof.from_claim(kprove.definition, claim) - init = proof.kcfg.get_unique_init() + init = proof.kcfg.node(proof.init) new_init_term = kcfg_explore.cterm_assume_defined(init.cterm) proof.kcfg.replace_node(init.id, new_init_term) prover = APRProver(proof) @@ -149,7 +149,7 @@ def test_all_path_reachability_prove( kcfg_show = KCFGShow( kcfg_explore.kprint, node_printer=APRProofNodePrinter(proof, kcfg_explore.kprint, full_printer=True) ) - cfg_lines = kcfg_show.show('test', proof.kcfg) + cfg_lines = kcfg_show.show(proof.kcfg) _LOGGER.info('\n'.join(cfg_lines)) assert proof.status == ProofStatus.PASSED diff --git a/src/tests/integration/kcfg/test_imp.py b/src/tests/integration/kcfg/test_imp.py index 75b870719..2648aabeb 100644 --- a/src/tests/integration/kcfg/test_imp.py +++ b/src/tests/integration/kcfg/test_imp.py @@ -26,7 +26,7 @@ from pyk.kast.inner import KInner from pyk.kast.outer import KDefinition - from pyk.kcfg import KCFG, KCFGExplore + from pyk.kcfg import KCFGExplore from pyk.ktool.kprint import KPrint, SymbolTable from pyk.ktool.kprove import KProve @@ -462,16 +462,9 @@ ) -def leaf_number(kcfg: KCFG) -> int: - target_id = kcfg.get_unique_target().id - target_subsumed_nodes = ( - len(kcfg.edges(target_id=target_id)) - + len(kcfg.covers(target_id=target_id)) - + len(kcfg.splits(target_id=target_id)) - ) - frontier_nodes = len(kcfg.frontier) - stuck_nodes = len(kcfg.stuck) - return target_subsumed_nodes + frontier_nodes + stuck_nodes +def leaf_number(proof: APRProof) -> int: + non_target_leaves = [nd for nd in proof.kcfg.leaves if not proof.is_target(nd.id)] + return len(non_target_leaves) + len(proof.kcfg.predecessors(proof.target)) class TestImpProof(KCFGExploreTest): @@ -656,11 +649,11 @@ def test_all_path_reachability_prove( kcfg_show = KCFGShow( kcfg_explore.kprint, node_printer=APRProofNodePrinter(proof, kcfg_explore.kprint, full_printer=True) ) - cfg_lines = kcfg_show.show('test', proof.kcfg) + cfg_lines = kcfg_show.show(proof.kcfg) _LOGGER.info('\n'.join(cfg_lines)) assert proof.status == proof_status - assert leaf_number(proof.kcfg) == expected_leaf_number + assert leaf_number(proof) == expected_leaf_number @pytest.mark.parametrize( 'test_id,spec_file,spec_module,claim_id,max_iterations,max_depth,terminal_rules,cut_rules,expected_constraint', @@ -704,8 +697,8 @@ def _node_printer(cterm: CTerm) -> list[str]: terminal_rules=terminal_rules, ) - assert len(proof.kcfg.stuck) == 1 - path_constraint = proof.path_constraints(proof.kcfg.stuck[0].id) + assert len(proof.terminal) == 1 + path_constraint = proof.path_constraints(proof.terminal[0].id) actual_constraint = kcfg_explore.kprint.pretty_print(path_constraint).replace('\n', ' ') assert actual_constraint == expected_constraint @@ -748,8 +741,8 @@ def test_all_path_bmc_reachability_prove( kcfg_show = KCFGShow( kcfg_explore.kprint, node_printer=APRBMCProofNodePrinter(proof, kcfg_explore.kprint, full_printer=True) ) - cfg_lines = kcfg_show.show('test', proof.kcfg) + cfg_lines = kcfg_show.show(proof.kcfg) _LOGGER.info('\n'.join(cfg_lines)) assert proof.status == proof_status - assert leaf_number(proof.kcfg) == expected_leaf_number + assert leaf_number(proof) == expected_leaf_number diff --git a/src/tests/integration/kcfg/test_non_det.py b/src/tests/integration/kcfg/test_non_det.py index e63f0d840..d2651e07f 100644 --- a/src/tests/integration/kcfg/test_non_det.py +++ b/src/tests/integration/kcfg/test_non_det.py @@ -19,6 +19,7 @@ from typing import Final from pyk.kcfg import KCFGExplore + from pyk.kcfg.kcfg import NodeIdLike from pyk.ktool.kprove import KProve _LOGGER: Final = logging.getLogger(__name__) @@ -64,7 +65,7 @@ def test_all_path_reachability_prove( kcfg_show = KCFGShow( kcfg_explore.kprint, node_printer=APRProofNodePrinter(proof, kcfg_explore.kprint, full_printer=True) ) - cfg_lines = kcfg_show.show('test', proof.kcfg) + cfg_lines = kcfg_show.show(proof.kcfg) _LOGGER.info('\n'.join(cfg_lines)) # We expect this graph, in which all splits are non-deterministic: @@ -77,9 +78,9 @@ def test_all_path_reachability_prove( # \ # id1b2 - final3 - success - id1 = proof.kcfg.get_unique_init().id + id1 = proof.init - def assert_nd_branch(id: int) -> tuple[int, int]: + def assert_nd_branch(id: NodeIdLike) -> tuple[int, int]: assert len(proof.kcfg.successors(source_id=id)) == 1 ndbranches = proof.kcfg.ndbranches(source_id=id) assert len(ndbranches) == 1 diff --git a/src/tests/unit/test_kcfg.py b/src/tests/unit/test_kcfg.py index 1d2c9401e..3ce4e1f84 100644 --- a/src/tests/unit/test_kcfg.py +++ b/src/tests/unit/test_kcfg.py @@ -200,7 +200,7 @@ def test_create_node() -> None: # Then assert new_node == node(1) assert set(cfg.nodes) == {node(1)} - assert not cfg.is_expanded(new_node.id) + assert not cfg.is_stuck(new_node.id) def test_remove_unknown_node() -> None: @@ -217,8 +217,6 @@ def test_remove_node() -> None: # Given d = {'nodes': node_dicts(3), 'edges': edge_dicts((1, 2), (2, 3))} cfg = KCFG.from_dict(d) - cfg.add_expanded(node(1).id) - cfg.add_expanded(node(2).id) # When cfg.remove_node(2) @@ -226,7 +224,7 @@ def test_remove_node() -> None: # Then assert set(cfg.nodes) == {node(1), node(3)} assert set(cfg.edges()) == set() - assert not cfg.is_expanded(1) + assert not cfg.is_stuck(1) with pytest.raises(ValueError): cfg.node(2) with pytest.raises(ValueError): @@ -247,8 +245,6 @@ def test_cover_then_remove() -> None: # Then assert cfg.is_covered(node1.id) assert not cfg.is_covered(node2.id) - assert not cfg.is_expanded(node1.id) - assert not cfg.is_expanded(node2.id) assert dict(cover.csubst.subst) == {'X': token(1)} assert cfg.covers() == [cover] @@ -258,8 +254,6 @@ def test_cover_then_remove() -> None: # Then assert not cfg.is_covered(node1.id) assert not cfg.is_covered(node2.id) - assert not cfg.is_expanded(node1.id) - assert not cfg.is_expanded(node2.id) assert cfg.covers() == [] @@ -401,8 +395,6 @@ def test_resolve() -> None: def test_aliases() -> None: # Given d = { - 'init': [1], - 'target': [4], 'nodes': node_dicts(4), 'edges': edge_dicts((1, 2), (2, 3)), 'aliases': {'foo': 2}, @@ -411,12 +403,6 @@ def test_aliases() -> None: cfg = KCFG.from_dict(d) assert cfg.node('@foo'), node(2) - assert cfg.node('#init'), node(1) - assert cfg.node('#target'), node(4) - cfg.add_expanded(1) - cfg.add_expanded(2) - assert cfg.node('#frontier'), node(3) - cfg.add_alias('bar', 1) cfg.add_alias('bar2', 1) assert cfg.node('@bar'), node(1) @@ -438,8 +424,6 @@ def _x_equals(i: int) -> KInner: return mlEquals(KVariable('x'), token(i)) d = { - 'init': [21], - 'target': [17], 'nodes': node_dicts(15, start=10) + predicate_node_dicts(1, start=25), 'aliases': {'foo': 14, 'bar': 14}, 'edges': edge_dicts((21, 12), (12, 13, 5), (13, 14), (15, 16), (16, 13), (18, 17), (22, 19)), @@ -459,250 +443,235 @@ def _x_equals(i: int) -> KInner: ) ), 'ndbranches': ndbranch_dicts((20, [(24, False), (25, True)])), - 'expanded': [21, 12, 13, 14, 15, 16, 18, 20, 22, 23], + 'stuck': [23], } cfg = KCFG.from_dict(d) expected = ( '\n' - '┌─ 21 (init, expanded)\n' + '┌─ 21 (root)\n' '│\n' '│ (1 step)\n' - '├─ 12 (expanded)\n' + '├─ 12\n' '│\n' '│ (5 steps)\n' - '├─ 13 (expanded)\n' + '├─ 13\n' '│\n' '│ (1 step)\n' - '├─ 14 (expanded, split, @bar, @foo)\n' + '├─ 14 (split, @bar, @foo)\n' '┃\n' '┃ (branch)\n' '┣━━┓ constraint: #Equals ( x , 15 )\n' '┃ ┃ subst: V14 <- V15\n' '┃ │\n' - '┃ ├─ 15 (expanded)\n' + '┃ ├─ 15\n' '┃ │\n' '┃ │ (1 step)\n' - '┃ ├─ 16 (expanded)\n' + '┃ ├─ 16\n' '┃ │\n' '┃ │ (1 step)\n' - '┃ └─ 13 (expanded)\n' + '┃ └─ 13\n' '┃ (looped back)\n' '┃\n' '┣━━┓ constraint: #Equals ( x , 16 )\n' '┃ ┃ subst: V14 <- V16\n' '┃ │\n' - '┃ └─ 16 (expanded)\n' + '┃ └─ 16\n' '┃ (continues as previously)\n' '┃\n' '┣━━┓ constraint: #Equals ( x , 17 )\n' '┃ ┃ subst: V14 <- V17\n' '┃ │\n' - '┃ └─ 17 (target, leaf)\n' + '┃ └─ 17 (leaf)\n' '┃\n' '┣━━┓ constraint: #Equals ( x , 18 )\n' '┃ ┃ subst: V14 <- V18\n' '┃ │\n' - '┃ ├─ 18 (expanded)\n' + '┃ ├─ 18\n' '┃ │\n' '┃ │ (1 step)\n' - '┃ └─ 17 (target, leaf)\n' + '┃ └─ 17 (leaf)\n' '┃\n' '┣━━┓ constraint: #Equals ( x , 20 )\n' '┃ ┃ subst: V14 <- V20\n' '┃ │\n' - '┃ ├─ 20 (expanded)\n' + '┃ ├─ 20\n' '┃ ┃\n' '┃ ┃ (1 step)\n' '┃ ┣━━┓\n' '┃ ┃ │\n' - '┃ ┃ └─ 24 (frontier, leaf)\n' + '┃ ┃ └─ 24 (leaf)\n' '┃ ┃\n' '┃ ┗━━┓\n' '┃ │\n' - '┃ └─ 25 (frontier, leaf)\n' + '┃ └─ 25 (leaf)\n' '┃\n' '┣━━┓ constraint: #Equals ( x , 23 )\n' '┃ ┃ subst: V14 <- V23\n' '┃ │\n' - '┃ └─ 23 (expanded, stuck, leaf)\n' + '┃ └─ 23 (stuck, leaf)\n' '┃\n' '┗━━┓ constraint: #Equals ( x , 22 )\n' ' ┃ subst: V14 <- V22\n' ' │\n' - ' ├─ 22 (expanded)\n' + ' ├─ 22\n' ' │\n' ' │ (1 step)\n' - ' ├─ 19 (leaf)\n' + ' ├─ 19\n' ' │\n' ' ┊ constraint: true\n' ' ┊ subst: V22 <- V19\n' - ' └─ 22 (expanded)\n' + ' └─ 22\n' ' (looped back)\n' '\n' '\n' - 'Target Nodes:\n' - '\n' - '17 (target, leaf)\n' - '\n' - 'Remaining Nodes:\n' - '\n' - '10 (frontier, leaf)\n' + '┌─ 10 (root, leaf)\n' '\n' - '11 (frontier, leaf)\n' + '┌─ 11 (root, leaf)\n' ) expected_full_printer = ( '\n' - '┌─ 21 (init, expanded)\n' - '│ \n' - '│ V21\n' - '│ \n' + '┌─ 21 (root)\n' + '│ \n' + '│ V21\n' + '│ \n' '│\n' '│ (1 step)\n' - '├─ 12 (expanded)\n' - '│ \n' - '│ V12\n' - '│ \n' + '├─ 12\n' + '│ \n' + '│ V12\n' + '│ \n' '│\n' '│ (5 steps)\n' - '├─ 13 (expanded)\n' - '│ \n' - '│ V13\n' - '│ \n' + '├─ 13\n' + '│ \n' + '│ V13\n' + '│ \n' '│\n' '│ (1 step)\n' - '├─ 14 (expanded, split, @bar, @foo)\n' - '│ \n' - '│ V14\n' - '│ \n' + '├─ 14 (split, @bar, @foo)\n' + '│ \n' + '│ V14\n' + '│ \n' '┃\n' '┃ (branch)\n' '┣━━┓ constraint: #Equals ( x , 15 )\n' '┃ ┃ subst: V14 <- V15\n' '┃ │\n' - '┃ ├─ 15 (expanded)\n' - '┃ │ \n' - '┃ │ V15\n' - '┃ │ \n' + '┃ ├─ 15\n' + '┃ │ \n' + '┃ │ V15\n' + '┃ │ \n' '┃ │\n' '┃ │ (1 step)\n' - '┃ ├─ 16 (expanded)\n' - '┃ │ \n' - '┃ │ V16\n' - '┃ │ \n' + '┃ ├─ 16\n' + '┃ │ \n' + '┃ │ V16\n' + '┃ │ \n' '┃ │\n' '┃ │ (1 step)\n' - '┃ └─ 13 (expanded)\n' - '┃ \n' - '┃ V13\n' - '┃ \n' + '┃ └─ 13\n' + '┃ \n' + '┃ V13\n' + '┃ \n' '┃ (looped back)\n' '┃\n' '┣━━┓ constraint: #Equals ( x , 16 )\n' '┃ ┃ subst: V14 <- V16\n' '┃ │\n' - '┃ └─ 16 (expanded)\n' - '┃ \n' - '┃ V16\n' - '┃ \n' + '┃ └─ 16\n' + '┃ \n' + '┃ V16\n' + '┃ \n' '┃ (continues as previously)\n' '┃\n' '┣━━┓ constraint: #Equals ( x , 17 )\n' '┃ ┃ subst: V14 <- V17\n' '┃ │\n' - '┃ └─ 17 (target, leaf)\n' - '┃ \n' - '┃ V17\n' - '┃ \n' + '┃ └─ 17 (leaf)\n' + '┃ \n' + '┃ V17\n' + '┃ \n' '┃\n' '┣━━┓ constraint: #Equals ( x , 18 )\n' '┃ ┃ subst: V14 <- V18\n' '┃ │\n' - '┃ ├─ 18 (expanded)\n' - '┃ │ \n' - '┃ │ V18\n' - '┃ │ \n' + '┃ ├─ 18\n' + '┃ │ \n' + '┃ │ V18\n' + '┃ │ \n' '┃ │\n' '┃ │ (1 step)\n' - '┃ └─ 17 (target, leaf)\n' - '┃ \n' - '┃ V17\n' - '┃ \n' + '┃ └─ 17 (leaf)\n' + '┃ \n' + '┃ V17\n' + '┃ \n' '┃\n' '┣━━┓ constraint: #Equals ( x , 20 )\n' '┃ ┃ subst: V14 <- V20\n' '┃ │\n' - '┃ ├─ 20 (expanded)\n' - '┃ │ \n' - '┃ │ V20\n' - '┃ │ \n' + '┃ ├─ 20\n' + '┃ │ \n' + '┃ │ V20\n' + '┃ │ \n' '┃ ┃\n' '┃ ┃ (1 step)\n' '┃ ┣━━┓\n' '┃ ┃ │\n' - '┃ ┃ └─ 24 (frontier, leaf)\n' - '┃ ┃ \n' - '┃ ┃ V24\n' - '┃ ┃ \n' + '┃ ┃ └─ 24 (leaf)\n' + '┃ ┃ \n' + '┃ ┃ V24\n' + '┃ ┃ \n' '┃ ┃\n' '┃ ┗━━┓\n' '┃ │\n' - '┃ └─ 25 (frontier, leaf)\n' - '┃ \n' - '┃ V25\n' - '┃ \n' - '┃ #And #Equals ( x , 25 )\n' + '┃ └─ 25 (leaf)\n' + '┃ \n' + '┃ V25\n' + '┃ \n' + '┃ #And #Equals ( x , 25 )\n' '┃\n' '┣━━┓ constraint: #Equals ( x , 23 )\n' '┃ ┃ subst: V14 <- V23\n' '┃ │\n' - '┃ └─ 23 (expanded, stuck, leaf)\n' - '┃ \n' - '┃ V23\n' - '┃ \n' + '┃ └─ 23 (stuck, leaf)\n' + '┃ \n' + '┃ V23\n' + '┃ \n' '┃\n' '┗━━┓ constraint: #Equals ( x , 22 )\n' ' ┃ subst: V14 <- V22\n' ' │\n' - ' ├─ 22 (expanded)\n' - ' │ \n' - ' │ V22\n' - ' │ \n' + ' ├─ 22\n' + ' │ \n' + ' │ V22\n' + ' │ \n' ' │\n' ' │ (1 step)\n' - ' ├─ 19 (leaf)\n' - ' │ \n' - ' │ V19\n' - ' │ \n' + ' ├─ 19\n' + ' │ \n' + ' │ V19\n' + ' │ \n' ' │\n' ' ┊ constraint: true\n' ' ┊ subst: V22 <- V19\n' - ' └─ 22 (expanded)\n' - ' \n' - ' V22\n' - ' \n' + ' └─ 22\n' + ' \n' + ' V22\n' + ' \n' ' (looped back)\n' '\n' '\n' - 'Target Nodes:\n' - '\n' - '17 (target, leaf)\n' - ' \n' - ' V17\n' - ' \n' - '\n' - 'Remaining Nodes:\n' - '\n' - '10 (frontier, leaf)\n' - ' \n' - ' 10\n' - ' \n' + '┌─ 10 (root, leaf)\n' + '│ \n' + '│ 10\n' + '│ \n' '\n' - '11 (frontier, leaf)\n' - ' \n' - ' V11\n' - ' \n' + '┌─ 11 (root, leaf)\n' + '│ \n' + '│ V11\n' + '│ \n' ) # When