diff --git a/pyk/regression-new/kprove-haskell/sum-spec.k.out b/pyk/regression-new/kprove-haskell/sum-spec.k.out index c1e50df076c..28179677cdc 100644 --- a/pyk/regression-new/kprove-haskell/sum-spec.k.out +++ b/pyk/regression-new/kprove-haskell/sum-spec.k.out @@ -31,7 +31,9 @@ Subproofs: 0 │ #And { true #Equals N:Int >=Int 0 } ┃ ┃ (branch) -┣━━┓ constraint: N:Int >Int 0 +┣━━┓ subst: .Subst +┃ ┃ constraint: +┃ ┃ N:Int >Int 0 ┃ │ ┃ ├─ 3 ┃ │ @@ -92,8 +94,11 @@ Subproofs: 0 ┃ │ #And { true #Equals N:Int >=Int 0 } ┃ │ #And { true #Equals N:Int +Int -1 >=Int 0 } ┃ │ -┃ ┊ constraint: OMITTED CONSTRAINT -┃ ┊ subst: OMITTED SUBST +┃ ┊ constraint: +┃ ┊ S:Int +Int C:Int +Int N:Int +Int -1 *Int C:Int +Int 1 +Int N:Int +Int -2 *Int N:Int +Int -1 /Int 2 ==K S:Int +Int N:Int *Int C:Int +Int N:Int +Int -1 *Int N:Int /Int 2 +┃ ┊ subst: +┃ ┊ ?_COUNTER_CELL_af8c44a5 <- COUNTER_CELL_af8c44a5:Int +┃ ┊ ?_GENERATEDCOUNTER_CELL_5e3e01ba <- GENERATEDCOUNTER_CELL_5e3e01ba:Int ┃ └─ 2 (leaf, target) ┃ ┃ @@ -112,7 +117,9 @@ Subproofs: 0 ┃ #And { true #Equals N:Int >=Int 0 } ┃ #And { true #Equals ?S:Int ==Int S:Int +Int N:Int *Int C:Int +Int N:Int -Int 1 *Int N:Int /Int 2 } ┃ -┗━━┓ constraint: N:Int ==Int 0 +┗━━┓ subst: .Subst + ┃ constraint: + ┃ N:Int ==Int 0 │ ├─ 4 │ @@ -151,8 +158,11 @@ Subproofs: 0 │ │ #And { N:Int #Equals 0 } │ - ┊ constraint: OMITTED CONSTRAINT - ┊ subst: OMITTED SUBST + ┊ constraint: + ┊ S:Int ==Int S:Int +Int N:Int *Int COUNTER_CELL_af8c44a5:Int +Int N:Int +Int -1 *Int N:Int /Int 2 + ┊ subst: + ┊ C <- COUNTER_CELL_af8c44a5:Int + ┊ GENERATEDCOUNTER_CELL_5e3e01ba <- GENERATEDCOUNTER_CELL_949ec677:Int └─ 2 (leaf, target) diff --git a/pyk/regression-new/kprove-haskell/test-spec.k.out b/pyk/regression-new/kprove-haskell/test-spec.k.out index 57c171d4601..c63c190355f 100644 --- a/pyk/regression-new/kprove-haskell/test-spec.k.out +++ b/pyk/regression-new/kprove-haskell/test-spec.k.out @@ -48,7 +48,8 @@ Subproofs: 0 │ │ ┊ constraint: true -┊ subst: GENERATEDCOUNTER_CELL_6de8d71b <- GENERATEDCOUNTER_CELL_c84b0b5f:Int +┊ subst: +┊ GENERATEDCOUNTER_CELL_6de8d71b <- GENERATEDCOUNTER_CELL_c84b0b5f:Int └─ 2 (leaf, target) diff --git a/pyk/src/pyk/__main__.py b/pyk/src/pyk/__main__.py index 9f1c2dc871f..81d09295acb 100644 --- a/pyk/src/pyk/__main__.py +++ b/pyk/src/pyk/__main__.py @@ -282,7 +282,7 @@ def explore_context() -> Iterator[KCFGExplore]: if options.show_kcfg and type(proof) is APRProof: node_printer = APRProofNodePrinter(proof, kprove, full_printer=True, minimize=False) show = APRProofShow(kprove, node_printer=node_printer) - print('\n'.join(show.show(proof))) + print('\n'.join(show.show(proof, minimize=False))) sys.exit(len([p.id for p in proofs if not p.passed])) diff --git a/pyk/src/pyk/kast/manip.py b/pyk/src/pyk/kast/manip.py index f92c8d69798..7a56ab62e60 100644 --- a/pyk/src/pyk/kast/manip.py +++ b/pyk/src/pyk/kast/manip.py @@ -215,39 +215,39 @@ def extract_rhs(term: KInner) -> KInner: def extract_subst(term: KInner) -> tuple[Subst, KInner]: - _subst = {} + subst = {} rem_conjuncts: list[KInner] = [] - def _extract_subst(_term1: KInner, _term2: KInner) -> tuple[str, KInner] | None: + def _extract_subst(term: KInner, term2: KInner) -> tuple[str, KInner] | None: if ( - (type(_term1) is KVariable and _term1.name not in _subst) - and not (type(_term2) is KVariable and _term2.name in _subst) - and _term1.name not in free_vars(_term2) + (isinstance(term, KVariable) and term.name not in subst) + and not (isinstance(term2, KVariable) and term2.name in subst) + and term.name not in free_vars(term2) ): - return (_term1.name, _term2) + return (term.name, term2) if ( - (type(_term2) is KVariable and _term2.name not in _subst) - and not (type(_term1) is KVariable and _term1.name in _subst) - and _term2.name not in free_vars(_term1) + (isinstance(term2, KVariable) and term2.name not in subst) + and not (isinstance(term, KVariable) and term.name in subst) + and term2.name not in free_vars(term) ): - return (_term2.name, _term1) - if _term1 == TRUE and type(_term2) is KApply and _term2.label.name in {'_==K_', '_==Int_'}: - return _extract_subst(_term2.args[0], _term2.args[1]) - if _term2 == TRUE and type(_term1) is KApply and _term1.label.name in {'_==K_', '_==Int_'}: - return _extract_subst(_term1.args[0], _term1.args[1]) + return (term2.name, term) + if term == TRUE and isinstance(term2, KApply) and term2.label.name in {'_==K_', '_==Int_'}: + return _extract_subst(term2.args[0], term2.args[1]) + if term2 == TRUE and isinstance(term, KApply) and term.label.name in {'_==K_', '_==Int_'}: + return _extract_subst(term.args[0], term.args[1]) return None for conjunct in flatten_label('#And', term): - if type(conjunct) is KApply and conjunct.label.name == '#Equals': + if isinstance(conjunct, KApply) and conjunct.label.name == '#Equals': if _conjunct_subst := _extract_subst(conjunct.args[0], conjunct.args[1]): name, value = _conjunct_subst - _subst[name] = value + subst[name] = value else: rem_conjuncts.append(conjunct) else: rem_conjuncts.append(conjunct) - return Subst(_subst), mlAnd(rem_conjuncts) + return Subst(subst), mlAnd(rem_conjuncts) def count_vars(term: KInner) -> Counter[str]: diff --git a/pyk/src/pyk/kcfg/show.py b/pyk/src/pyk/kcfg/show.py index 6ace8d1abd8..b4e2db73338 100644 --- a/pyk/src/pyk/kcfg/show.py +++ b/pyk/src/pyk/kcfg/show.py @@ -27,6 +27,7 @@ from pathlib import Path from typing import Final + from ..cterm import CSubst from ..kast import KInner from ..kast.outer import KFlatModule, KSentence from ..ktool.kprint import KPrint @@ -126,6 +127,34 @@ def pretty_segments(self, kcfg: KCFG, minimize: bool = True) -> Iterable[tuple[s processed_nodes: list[KCFG.Node] = [] ret_lines: list[tuple[str, list[str]]] = [] + def _multi_line_print( + label: str, lines: list[str], default: str = 'None', indent: int = 4, max_width: int | None = None + ) -> list[str]: + ret_lines = [] + if len(lines) == 0: + ret_lines.append(f'{label}: {default}') + else: + ret_lines.append(f'{label}:') + ret_lines.extend([f'{indent * " "}{line}' for line in lines]) + if max_width is not None: + ret_lines = [ + ret_line if len(ret_line) <= max_width else ret_line[0:max_width] + '...' for ret_line in ret_lines + ] + return ret_lines + + def _print_csubst( + csubst: CSubst, subst_first: bool = False, indent: int = 4, max_width: int | None = None + ) -> list[str]: + _constraint_strs = [ + self.kprint.pretty_print(ml_pred_to_bool(constraint, unsafe=True)) for constraint in csubst.constraints + ] + constraint_strs = _multi_line_print('constraint', _constraint_strs, 'true', max_width=max_width) + _subst_strs = [f'{k} <- {self.kprint.pretty_print(v)}' for k, v in csubst.subst.minimize().items()] + subst_strs = _multi_line_print('subst', _subst_strs, '.Subst', max_width=max_width) + if subst_first: + return subst_strs + constraint_strs + return constraint_strs + subst_strs + def _print_node(node: KCFG.Node) -> list[str]: return self.node_short_info(kcfg, node) @@ -143,46 +172,12 @@ def _print_merged_edge(merged_edge: KCFG.MergedEdge) -> list[str]: return [res] if len(res) < 78 else ['(merged edge)'] def _print_cover(cover: KCFG.Cover) -> Iterable[str]: - subst_strs = [f'{k} <- {self.kprint.pretty_print(v)}' for k, v in cover.csubst.subst.items()] - subst_str = '' - if len(subst_strs) == 0: - subst_str = '.Subst' - if len(subst_strs) == 1: - subst_str = subst_strs[0] - if len(subst_strs) > 1 and minimize: - subst_str = 'OMITTED SUBST' - if len(subst_strs) > 1 and not minimize: - subst_str = '{\n ' + '\n '.join(subst_strs) + '\n}' - constraint_str = self.kprint.pretty_print(ml_pred_to_bool(cover.csubst.constraint, unsafe=True)) - if len(constraint_str) > 78: - constraint_str = 'OMITTED CONSTRAINT' - return [ - f'constraint: {constraint_str}', - f'subst: {subst_str}', - ] + max_width = None if not minimize else 78 + return _print_csubst(cover.csubst, subst_first=False, indent=4, max_width=max_width) def _print_split_edge(split: KCFG.Split, target_id: int) -> list[str]: - csubst = split.splits[target_id] - ret_split_lines: list[str] = [] - substs = csubst.subst.minimize().items() - constraints = [ml_pred_to_bool(c, unsafe=True) for c in csubst.constraints] - if len(constraints) == 1: - first_line, *rest_lines = self.kprint.pretty_print(constraints[0]).split('\n') - ret_split_lines.append(f'constraint: {first_line}') - ret_split_lines.extend(f' {line}' for line in rest_lines) - elif len(constraints) > 1: - ret_split_lines.append('constraints:') - for constraint in constraints: - first_line, *rest_lines = self.kprint.pretty_print(constraint).split('\n') - ret_split_lines.append(f' {first_line}') - ret_split_lines.extend(f' {line}' for line in rest_lines) - if len(substs) == 1: - vname, term = list(substs)[0] - ret_split_lines.append(f'subst: {vname} <- {self.kprint.pretty_print(term)}') - elif len(substs) > 1: - ret_split_lines.append('substs:') - ret_split_lines.extend(f' {vname} <- {self.kprint.pretty_print(term)}' for vname, term in substs) - return ret_split_lines + max_width = None if not minimize else 78 + return _print_csubst(split.splits[target_id], subst_first=True, indent=4, max_width=max_width) def _print_subgraph(indent: str, curr_node: KCFG.Node, prior_on_trace: list[KCFG.Node]) -> None: processed = curr_node in processed_nodes diff --git a/pyk/src/tests/unit/kcfg/test_minimize.py b/pyk/src/tests/unit/kcfg/test_minimize.py index 001f22998c4..4221f3eb650 100644 --- a/pyk/src/tests/unit/kcfg/test_minimize.py +++ b/pyk/src/tests/unit/kcfg/test_minimize.py @@ -340,56 +340,64 @@ def x_lt(n: int) -> KApply: '┌─ 1 (root, split)\n' '┃\n' '┃ (branch)\n' - '┣━━┓ constraints:\n' + '┣━━┓ subst: .Subst\n' + '┃ ┃ constraint:\n' '┃ ┃ _>=Int_ ( X , 0 )\n' '┃ ┃ _>=Int_ ( X , 32 )\n' '┃ ┃ _>=Int_ ( X , 64 )\n' '┃ │\n' '┃ └─ 8 (leaf)\n' '┃\n' - '┣━━┓ constraints:\n' + '┣━━┓ subst: .Subst\n' + '┃ ┃ constraint:\n' '┃ ┃ _>=Int_ ( X , 0 )\n' '┃ ┃ _>=Int_ ( X , 32 )\n' '┃ ┃ _=Int_ ( X , 0 )\n' '┃ ┃ _=Int_ ( X , 16 )\n' '┃ │\n' '┃ └─ 10 (leaf)\n' '┃\n' - '┣━━┓ constraints:\n' + '┣━━┓ subst: .Subst\n' + '┃ ┃ constraint:\n' '┃ ┃ _>=Int_ ( X , 0 )\n' '┃ ┃ _=Int_ ( X , -32 )\n' '┃ ┃ _>=Int_ ( X , -16 )\n' '┃ │\n' '┃ └─ 12 (leaf)\n' '┃\n' - '┣━━┓ constraints:\n' + '┣━━┓ subst: .Subst\n' + '┃ ┃ constraint:\n' '┃ ┃ _=Int_ ( X , -32 )\n' '┃ ┃ _=Int_ ( X , -64 )\n' '┃ │\n' '┃ └─ 14 (leaf)\n' '┃\n' - '┗━━┓ constraints:\n' + '┗━━┓ subst: .Subst\n' + ' ┃ constraint:\n' ' ┃ _ None: '├─ 14 (split, @bar, @foo)\n' '┃\n' '┃ (branch)\n' - '┣━━┓ constraint: _==K_ ( X , 15 )\n' - '┃ ┃ subst: V14 <- V15\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V15\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 15 )\n' '┃ │\n' '┃ ├─ 15\n' '┃ │\n' @@ -602,27 +604,35 @@ def test_pretty_print() -> None: '┃ └─ 13\n' '┃ (looped back)\n' '┃\n' - '┣━━┓ constraint: _==K_ ( X , 16 )\n' - '┃ ┃ subst: V14 <- V16\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V16\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 16 )\n' '┃ │\n' '┃ └─ 16\n' '┃ (continues as previously)\n' '┃\n' - '┣━━┓ constraint: _==K_ ( X , 17 )\n' - '┃ ┃ subst: V14 <- V17\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V17\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 17 )\n' '┃ │\n' '┃ └─ 17 (vacuous, leaf)\n' '┃\n' - '┣━━┓ constraint: _==K_ ( X , 18 )\n' - '┃ ┃ subst: V14 <- V18\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V18\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 18 )\n' '┃ │\n' '┃ ├─ 18\n' '┃ │\n' '┃ │ (1 step)\n' '┃ └─ 17 (vacuous, leaf)\n' '┃\n' - '┣━━┓ constraint: _==K_ ( X , 20 )\n' - '┃ ┃ subst: V14 <- V20\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V20\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 20 )\n' '┃ │\n' '┃ ├─ 20\n' '┃ ┃\n' @@ -635,13 +645,17 @@ def test_pretty_print() -> None: '┃ │\n' '┃ └─ 25 (leaf)\n' '┃\n' - '┣━━┓ constraint: _==K_ ( X , 23 )\n' - '┃ ┃ subst: V14 <- V23\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V23\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 23 )\n' '┃ │\n' '┃ └─ 23 (stuck, leaf)\n' '┃\n' - '┗━━┓ constraint: _==K_ ( X , 22 )\n' - ' ┃ subst: V14 <- V22\n' + '┗━━┓ subst:\n' + ' ┃ V14 <- V22\n' + ' ┃ constraint:\n' + ' ┃ _==K_ ( X , 22 )\n' ' │\n' ' ├─ 22\n' ' │\n' @@ -649,7 +663,8 @@ def test_pretty_print() -> None: ' ├─ 19\n' ' │\n' ' ┊ constraint: true\n' - ' ┊ subst: V22 <- V19\n' + ' ┊ subst:\n' + ' ┊ V22 <- V19\n' ' └─ 22\n' ' (looped back)\n' '\n' @@ -685,8 +700,10 @@ def test_pretty_print() -> None: '│ \n' '┃\n' '┃ (branch)\n' - '┣━━┓ constraint: _==K_ ( X , 15 )\n' - '┃ ┃ subst: V14 <- V15\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V15\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 15 )\n' '┃ │\n' '┃ ├─ 15\n' '┃ │ \n' @@ -706,8 +723,10 @@ def test_pretty_print() -> None: '┃ \n' '┃ (looped back)\n' '┃\n' - '┣━━┓ constraint: _==K_ ( X , 16 )\n' - '┃ ┃ subst: V14 <- V16\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V16\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 16 )\n' '┃ │\n' '┃ └─ 16\n' '┃ \n' @@ -715,16 +734,20 @@ def test_pretty_print() -> None: '┃ \n' '┃ (continues as previously)\n' '┃\n' - '┣━━┓ constraint: _==K_ ( X , 17 )\n' - '┃ ┃ subst: V14 <- V17\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V17\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 17 )\n' '┃ │\n' '┃ └─ 17 (vacuous, leaf)\n' '┃ \n' '┃ V17\n' '┃ \n' '┃\n' - '┣━━┓ constraint: _==K_ ( X , 18 )\n' - '┃ ┃ subst: V14 <- V18\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V18\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 18 )\n' '┃ │\n' '┃ ├─ 18\n' '┃ │ \n' @@ -737,8 +760,10 @@ def test_pretty_print() -> None: '┃ V17\n' '┃ \n' '┃\n' - '┣━━┓ constraint: _==K_ ( X , 20 )\n' - '┃ ┃ subst: V14 <- V20\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V20\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 20 )\n' '┃ │\n' '┃ ├─ 20\n' '┃ │ \n' @@ -761,16 +786,20 @@ def test_pretty_print() -> None: '┃ \n' '┃ #And #Equals ( X , 25 )\n' '┃\n' - '┣━━┓ constraint: _==K_ ( X , 23 )\n' - '┃ ┃ subst: V14 <- V23\n' + '┣━━┓ subst:\n' + '┃ ┃ V14 <- V23\n' + '┃ ┃ constraint:\n' + '┃ ┃ _==K_ ( X , 23 )\n' '┃ │\n' '┃ └─ 23 (stuck, leaf)\n' '┃ \n' '┃ V23\n' '┃ \n' '┃\n' - '┗━━┓ constraint: _==K_ ( X , 22 )\n' - ' ┃ subst: V14 <- V22\n' + '┗━━┓ subst:\n' + ' ┃ V14 <- V22\n' + ' ┃ constraint:\n' + ' ┃ _==K_ ( X , 22 )\n' ' │\n' ' ├─ 22\n' ' │ \n' @@ -784,7 +813,8 @@ def test_pretty_print() -> None: ' │ \n' ' │\n' ' ┊ constraint: true\n' - ' ┊ subst: V22 <- V19\n' + ' ┊ subst:\n' + ' ┊ V22 <- V19\n' ' └─ 22\n' ' \n' ' V22\n'