From f705bcd96224b80a35619a8e4112f7880bcaae81 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Tue, 9 Apr 2024 03:07:37 -0600 Subject: [PATCH 1/2] Update dependency: deps/k_release (#1070) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Related: * runtimeverification/k#4146 * runtimeverification/haskell-backend#3761 --------- Co-authored-by: devops Co-authored-by: Tamás Tóth --- deps/k_release | 2 +- docs/conf.py | 4 ++-- package/version | 2 +- pyproject.toml | 2 +- src/pyk/__init__.py | 2 +- src/pyk/konvert/_module_to_kore.py | 20 +++++++++++-------- src/tests/integration/proof/test_mini_kevm.py | 2 ++ 7 files changed, 20 insertions(+), 14 deletions(-) diff --git a/deps/k_release b/deps/k_release index 0ea0dfb42..a545989c7 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -6.3.75 +6.3.77 diff --git a/docs/conf.py b/docs/conf.py index 26cf730b3..53c007fdd 100644 --- a/docs/conf.py +++ b/docs/conf.py @@ -9,8 +9,8 @@ project = 'pyk' author = 'Runtime Verification, Inc' copyright = '2024, Runtime Verification, Inc' -version = '0.1.777' -release = '0.1.777' +version = '0.1.778' +release = '0.1.778' # -- General configuration --------------------------------------------------- # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration diff --git a/package/version b/package/version index da9223fb7..3f36f20c5 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.777 +0.1.778 diff --git a/pyproject.toml b/pyproject.toml index a128f511a..ccf8943e3 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.777" +version = "0.1.778" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/src/pyk/__init__.py b/src/pyk/__init__.py index 1e56c2a9d..62113f5bd 100644 --- a/src/pyk/__init__.py +++ b/src/pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -K_VERSION: Final = '6.3.75' +K_VERSION: Final = '6.3.77' diff --git a/src/pyk/konvert/_module_to_kore.py b/src/pyk/konvert/_module_to_kore.py index a6f9aec2b..e038e62af 100644 --- a/src/pyk/konvert/_module_to_kore.py +++ b/src/pyk/konvert/_module_to_kore.py @@ -722,20 +722,27 @@ def simplified_module(definition: KDefinition, module_name: str | None = None) - PullUpRewrites(), DiscardSymbolAtts( [ + Atts.ASSOC, Atts.CELL, Atts.CELL_FRAGMENT, Atts.CELL_NAME, Atts.CELL_OPT_ABSENT, + Atts.COLOR, + Atts.COLORS, + Atts.COMM, + Atts.FORMAT, Atts.GROUP, Atts.IMPURE, Atts.INDEX, Atts.INITIALIZER, + Atts.LEFT, Atts.MAINCELL, Atts.PREDICATE, Atts.PREFER, Atts.PRIVATE, Atts.PRODUCTION, Atts.PROJECTION, + Atts.RIGHT, Atts.SEQSTRICT, Atts.STRICT, Atts.USER_LIST, @@ -747,14 +754,6 @@ def simplified_module(definition: KDefinition, module_name: str | None = None) - AddSymbolAtts(Atts.FUNCTIONAL(None), _is_functional), AddSymbolAtts(Atts.INJECTIVE(None), _is_injective), AddSymbolAtts(Atts.CONSTRUCTOR(None), _is_constructor), - AddDefaultFormatAtts(), - DiscardFormatAtts(), - InlineFormatTerminals(), - AddColorAtts(), - DiscardSymbolAtts([Atts.COLOR]), - AddTerminalAtts(), - AddPrioritiesAtts(), - AddAssocAtts(), ) definition = reduce(lambda defn, step: step.execute(defn), pipeline, definition) module = definition.modules[0] @@ -1118,6 +1117,11 @@ def _update(self, production: KProduction) -> KProduction: return production.let(att=production.att.discard(self.keys)) +# ----------------- +# Syntax attributes +# ----------------- + + @dataclass class AddDefaultFormatAtts(SingleModulePass): """Add a default format attribute value to each symbol profuction missing one.""" diff --git a/src/tests/integration/proof/test_mini_kevm.py b/src/tests/integration/proof/test_mini_kevm.py index c15723bd1..136354bfc 100644 --- a/src/tests/integration/proof/test_mini_kevm.py +++ b/src/tests/integration/proof/test_mini_kevm.py @@ -50,6 +50,8 @@ def leaf_number(proof: APRProof) -> int: class TestMiniKEVM(KCFGExploreTest, KProveTest): KOMPILE_MAIN_FILE = K_FILES / 'mini-kevm.k' + # Disabled until resolved: https://github.com/runtimeverification/haskell-backend/issues/3761 + DISABLE_LEGACY = True @pytest.mark.parametrize( 'test_id,spec_file,spec_module,claim_id,max_iterations,max_depth,cut_rules,proof_status,expected_leaf_number', From 68bffc5ed0994d2c462d91fa3415f170cb0ec91f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Tue, 9 Apr 2024 11:45:33 +0200 Subject: [PATCH 2/2] Process branch `rule-id` and condition from `kore-rpc` response (#942) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Related: * runtimeverification/haskell-backend#3716 Blocked on: * ~runtimeverification/hs-backend-booster#536~ --------- Co-authored-by: devops Co-authored-by: Petar Maksimović --- docs/conf.py | 4 +- package/version | 2 +- pyproject.toml | 2 +- src/pyk/kore/manip.py | 10 ++- src/pyk/kore/prelude.py | 1 + src/pyk/kore/rpc.py | 73 +++++++++++++++++-- .../integration/kore/test_kore_client.py | 63 +++++++++++----- src/tests/unit/kore/test_client.py | 40 +++++++--- src/tests/unit/kore/test_manip.py | 29 +++++++- 9 files changed, 182 insertions(+), 42 deletions(-) diff --git a/docs/conf.py b/docs/conf.py index 53c007fdd..09efd2158 100644 --- a/docs/conf.py +++ b/docs/conf.py @@ -9,8 +9,8 @@ project = 'pyk' author = 'Runtime Verification, Inc' copyright = '2024, Runtime Verification, Inc' -version = '0.1.778' -release = '0.1.778' +version = '0.1.779' +release = '0.1.779' # -- General configuration --------------------------------------------------- # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration diff --git a/package/version b/package/version index 3f36f20c5..eddad3c85 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.778 +0.1.779 diff --git a/pyproject.toml b/pyproject.toml index ccf8943e3..4469514ac 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.778" +version = "0.1.779" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/src/pyk/kore/manip.py b/src/pyk/kore/manip.py index eb25c32a8..90fb2cb2d 100644 --- a/src/pyk/kore/manip.py +++ b/src/pyk/kore/manip.py @@ -2,7 +2,7 @@ from typing import TYPE_CHECKING -from .syntax import Assoc, EVar, MLQuant +from .syntax import And, Assoc, EVar, MLQuant, Top if TYPE_CHECKING: from collections.abc import Collection @@ -10,6 +10,14 @@ from .syntax import Pattern +def conjuncts(pattern: Pattern) -> tuple[Pattern, ...]: + if isinstance(pattern, Top): + return () + if isinstance(pattern, And): + return tuple(conjunct for op in pattern.ops for conjunct in conjuncts(op)) + return (pattern,) + + def free_occs(pattern: Pattern, *, bound_vars: Collection[str] = ()) -> dict[str, list[EVar]]: occurrences: dict[str, list[EVar]] = {} diff --git a/src/pyk/kore/prelude.py b/src/pyk/kore/prelude.py index 97992a397..6b8bd629b 100644 --- a/src/pyk/kore/prelude.py +++ b/src/pyk/kore/prelude.py @@ -143,6 +143,7 @@ def le_int(left: Pattern, right: Pattern) -> Pattern: SORT_K_ITEM: Final = SortApp('SortKItem') SORT_K_CONFIG_VAR: Final = SortApp('SortKConfigVar') SORT_GENERATED_TOP_CELL: Final = SortApp('SortGeneratedTopCell') +SORT_GENERATED_COUNTER_CELL: Final = SortApp('SortGeneratedCounterCell') LBL_INIT_GENERATED_TOP_CELL: Final = SymbolId('LblinitGeneratedTopCell') LBL_GENERATED_TOP: Final = SymbolId("Lbl'-LT-'generatedTop'-GT-'") diff --git a/src/pyk/kore/rpc.py b/src/pyk/kore/rpc.py index 81eb64e20..6fb48cdbd 100644 --- a/src/pyk/kore/rpc.py +++ b/src/pyk/kore/rpc.py @@ -18,8 +18,10 @@ from psutil import Process -from ..utils import check_dir_path, check_file_path, filter_none, run_process -from .syntax import And, SortApp, kore_term +from ..utils import FrozenDict, check_dir_path, check_file_path, filter_none, run_process +from . import manip +from .prelude import SORT_GENERATED_TOP_CELL +from .syntax import And, Equals, EVar, kore_term if TYPE_CHECKING: from collections.abc import Iterable, Mapping @@ -457,24 +459,83 @@ class StopReason(str, Enum): @dataclass(frozen=True) class State: term: Pattern - substitution: Pattern | None + substitution: FrozenDict[EVar, Pattern] | None predicate: Pattern | None + rule_id: str | None + rule_substitution: FrozenDict[EVar, Pattern] | None + rule_predicate: Pattern | None + + def __init__( + self, + term: Pattern, + *, + substitution: Mapping[EVar, Pattern] | None = None, + predicate: Pattern | None = None, + rule_id: str | None = None, + rule_substitution: Mapping[EVar, Pattern] | None = None, + rule_predicate: Pattern | None = None, + ): + substitution = FrozenDict(substitution) if substitution is not None else None + rule_substitution = FrozenDict(rule_substitution) if rule_substitution is not None else None + object.__setattr__(self, 'term', term) + object.__setattr__(self, 'substitution', substitution) + object.__setattr__(self, 'predicate', predicate) + object.__setattr__(self, 'rule_id', rule_id) + object.__setattr__(self, 'rule_substitution', rule_substitution) + object.__setattr__(self, 'rule_predicate', rule_predicate) @staticmethod def from_dict(dct: Mapping[str, Any]) -> State: return State( term=kore_term(dct['term']), - substitution=kore_term(dct['substitution']) if 'substitution' in dct else None, + substitution=State._subst_to_dict(kore_term(dct['substitution'])) if 'substitution' in dct else None, predicate=kore_term(dct['predicate']) if 'predicate' in dct else None, + rule_id=dct.get('rule-id'), + rule_substitution=( + State._subst_to_dict(kore_term(dct['rule-substitution'])) if 'rule-substitution' in dct else None + ), + rule_predicate=kore_term(dct['rule-predicate']) if 'rule-predicate' in dct else None, + ) + + @staticmethod + def _subst_to_dict(pattern: Pattern) -> dict[EVar, Pattern]: + def extract_entry(pattern: Pattern) -> tuple[EVar, Pattern]: + if not isinstance(pattern, Equals): + raise ValueError(fr'Expected \equals as substituion entry, got: {pattern.text}') + if pattern.sort != SORT_GENERATED_TOP_CELL: + raise ValueError( + f'Expected {SORT_GENERATED_TOP_CELL.text} as substitution entry sort, got: {pattern.sort.text}' + ) + if not isinstance(pattern.left, EVar): + raise ValueError(f'Expected EVar as substitution entry key, got: {pattern.left.text}') + if pattern.left.sort != pattern.op_sort: + raise ValueError( + f'Mismatch between substitution entry and key sort: {pattern.op_sort.text} and {pattern.left.sort.text}' + ) + return pattern.left, pattern.right + + res: dict[EVar, Pattern] = {} + for conjunct in manip.conjuncts(pattern): + key, value = extract_entry(conjunct) + if key in res: + raise ValueError(f'Duplicate substitution entry key: {key.text}') + res[key] = value + return res + + @staticmethod + def _dict_to_subst(dct: Mapping[EVar, Pattern]) -> And: + return And( + SORT_GENERATED_TOP_CELL, + tuple(Equals(var.sort, SORT_GENERATED_TOP_CELL, var, val) for var, val in dct.items()), ) @property def kore(self) -> Pattern: _kore = self.term if self.substitution is not None: - _kore = And(SortApp('SortGeneratedTopCell'), (_kore, self.substitution)) + _kore = And(SORT_GENERATED_TOP_CELL, (_kore,) + self._dict_to_subst(self.substitution).ops) if self.predicate is not None: - _kore = And(SortApp('SortGeneratedTopCell'), (_kore, self.predicate)) + _kore = And(SORT_GENERATED_TOP_CELL, (_kore, self.predicate)) return _kore diff --git a/src/tests/integration/kore/test_kore_client.py b/src/tests/integration/kore/test_kore_client.py index 1e809a114..e4e1bb05a 100644 --- a/src/tests/integration/kore/test_kore_client.py +++ b/src/tests/integration/kore/test_kore_client.py @@ -12,7 +12,9 @@ from pyk.kore.prelude import ( BOOL, INT, + SORT_GENERATED_COUNTER_CELL, SORT_GENERATED_TOP_CELL, + SORT_K, SORT_K_ITEM, TRUE, and_bool, @@ -89,11 +91,38 @@ def term(n: int) -> Pattern: def state(n: int) -> State: - return State(term=term(n), substitution=None, predicate=None) + return State(term=term(n)) EXECUTE_TEST_DATA: Final[tuple[tuple[str, int, Mapping[str, Any], ExecuteResult], ...]] = ( - ('branching', 0, {}, BranchingResult(state=state(2), depth=2, next_states=(state(4), state(3)), logs=())), + ( + 'branching', + 0, + {}, + BranchingResult( + state=state(2), + depth=2, + next_states=( + State( + term=term(3), + rule_id='ae0c978867ef4cc5cbfbadf7be2ff55e30e59465697ceaffa1d9fd5343a21fc6', + rule_substitution={ + EVar('GCC', SORT_GENERATED_COUNTER_CELL): EVar("Var'Unds'DotVar0", SORT_GENERATED_COUNTER_CELL), + EVar('K', SORT_K): EVar("Var'Unds'DotVar1", SORT_K), + }, + ), + State( + term=term(4), + rule_id='37a544ff4b6da9b4fb839f86d2ad51b770bcaf3dd578b716c38cf0da33458374', + rule_substitution={ + EVar('GCC', SORT_GENERATED_COUNTER_CELL): EVar("Var'Unds'DotVar0", SORT_GENERATED_COUNTER_CELL), + EVar('K', SORT_K): EVar("Var'Unds'DotVar1", SORT_K), + }, + ), + ), + logs=(), + ), + ), ('depth-bound', 0, {'max_depth': 2}, DepthBoundResult(state=state(2), depth=2, logs=())), ('stuck', 4, {}, StuckResult(state=state(6), depth=2, logs=())), ( @@ -473,7 +502,7 @@ def rule(lhs: int, rhs: int) -> Axiom: def test_base_module(self, kore_client: KoreClient) -> None: # Given config = self.config(0) - expected = StuckResult(State(term=config, substitution=None, predicate=None), depth=0, logs=()) + expected = StuckResult(State(term=config), depth=0, logs=()) # When actual = kore_client.execute(config) @@ -484,7 +513,7 @@ def test_base_module(self, kore_client: KoreClient) -> None: def test_base_module_explicitly(self, kore_client: KoreClient) -> None: # Given config = self.config(0) - expected = StuckResult(State(term=config, substitution=None, predicate=None), depth=0, logs=()) + expected = StuckResult(State(term=config), depth=0, logs=()) # When actual = kore_client.execute(config, module_name=self.KOMPILE_MAIN_MODULE) @@ -496,7 +525,7 @@ def test_add_a_single_module(self, kore_client: KoreClient) -> None: # Given config = self.config(0) module = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 1))) - expected = StuckResult(State(term=self.config(1), substitution=None, predicate=None), depth=1, logs=()) + expected = StuckResult(State(term=self.config(1)), depth=1, logs=()) # When module_id = kore_client.add_module(module) @@ -509,7 +538,7 @@ def test_add_a_single_module_but_dont_use_it(self, kore_client: KoreClient) -> N # Given config = self.config(0) module = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 1))) - expected = StuckResult(State(term=self.config(0), substitution=None, predicate=None), depth=0, logs=()) + expected = StuckResult(State(term=self.config(0)), depth=0, logs=()) # When kore_client.add_module(module) @@ -522,7 +551,7 @@ def test_name_as_id(self, kore_client: KoreClient) -> None: # Given config = self.config(0) module = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 1))) - expected = StuckResult(State(term=self.config(1), substitution=None, predicate=None), depth=1, logs=()) + expected = StuckResult(State(term=self.config(1)), depth=1, logs=()) # When kore_client.add_module(module, name_as_id=True) @@ -545,7 +574,7 @@ def test_add_module_twice(self, kore_client: KoreClient) -> None: # Given config = self.config(0) module = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 1))) - expected = StuckResult(State(term=self.config(1), substitution=None, predicate=None), depth=1, logs=()) + expected = StuckResult(State(term=self.config(1)), depth=1, logs=()) # When module_id = kore_client.add_module(module) @@ -564,7 +593,7 @@ def test_add_module_twice_with_name(self, kore_client: KoreClient) -> None: # Given config = self.config(0) module = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 1))) - expected = StuckResult(State(term=self.config(1), substitution=None, predicate=None), depth=1, logs=()) + expected = StuckResult(State(term=self.config(1)), depth=1, logs=()) # When module_id = kore_client.add_module(module, name_as_id=True) @@ -583,7 +612,7 @@ def test_add_module_without_name_then_with_name(self, kore_client: KoreClient) - # Given config = self.config(0) module = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 1))) - expected = StuckResult(State(term=self.config(1), substitution=None, predicate=None), depth=1, logs=()) + expected = StuckResult(State(term=self.config(1)), depth=1, logs=()) # When module_id = kore_client.add_module(module) @@ -608,7 +637,7 @@ def test_add_module_with_name_then_without_name(self, kore_client: KoreClient) - # Given config = self.config(0) module = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 1))) - expected = StuckResult(State(term=self.config(1), substitution=None, predicate=None), depth=1, logs=()) + expected = StuckResult(State(term=self.config(1)), depth=1, logs=()) # When module_id = kore_client.add_module(module, name_as_id=True) @@ -650,8 +679,8 @@ def test_add_two_modules_second_with_same_name_as_id(self, kore_client: KoreClie config = self.config(0) module_1 = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 1))) module_2 = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 2))) - expected_1 = StuckResult(State(term=self.config(1), substitution=None, predicate=None), depth=1, logs=()) - expected_2 = StuckResult(State(term=self.config(2), substitution=None, predicate=None), depth=1, logs=()) + expected_1 = StuckResult(State(term=self.config(1)), depth=1, logs=()) + expected_2 = StuckResult(State(term=self.config(2)), depth=1, logs=()) # When module_id = kore_client.add_module(module_1) @@ -672,8 +701,8 @@ def test_add_two_modules_first_with_same_name_as_id(self, kore_client: KoreClien config = self.config(0) module_1 = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 1))) module_2 = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 2))) - expected_1 = StuckResult(State(term=self.config(1), substitution=None, predicate=None), depth=1, logs=()) - expected_2 = StuckResult(State(term=self.config(2), substitution=None, predicate=None), depth=1, logs=()) + expected_1 = StuckResult(State(term=self.config(1)), depth=1, logs=()) + expected_2 = StuckResult(State(term=self.config(2)), depth=1, logs=()) # When kore_client.add_module(module_1, name_as_id=True) @@ -693,7 +722,7 @@ def test_add_module_with_import(self, kore_client: KoreClient) -> None: # Given config = self.config(0) module_1 = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 1))) - expected = StuckResult(State(term=self.config(2), substitution=None, predicate=None), depth=2, logs=()) + expected = StuckResult(State(term=self.config(2)), depth=2, logs=()) # When module_1_id = kore_client.add_module(module_1) @@ -709,7 +738,7 @@ def test_add_module_with_named_import(self, kore_client: KoreClient) -> None: config = self.config(0) module_1 = Module('A', sentences=(Import(self.KOMPILE_MAIN_MODULE), self.rule(0, 1))) module_2 = Module('B', sentences=(Import('A'), self.rule(1, 2))) - expected = StuckResult(State(term=self.config(2), substitution=None, predicate=None), depth=2, logs=()) + expected = StuckResult(State(term=self.config(2)), depth=2, logs=()) # When kore_client.add_module(module_1, name_as_id=True) diff --git a/src/tests/unit/kore/test_client.py b/src/tests/unit/kore/test_client.py index e99437a1d..febe82a03 100644 --- a/src/tests/unit/kore/test_client.py +++ b/src/tests/unit/kore/test_client.py @@ -6,7 +6,7 @@ import pytest -from pyk.kore.prelude import INT, int_dv +from pyk.kore.prelude import INT, SORT_GENERATED_TOP_CELL, int_dv from pyk.kore.rpc import ( AbortedResult, DefaultError, @@ -28,7 +28,7 @@ UnsatResult, VacuousResult, ) -from pyk.kore.syntax import And, App, Bottom, Module, Top +from pyk.kore.syntax import And, App, Bottom, Equals, EVar, Module, Top if TYPE_CHECKING: from collections.abc import Iterator @@ -38,6 +38,7 @@ from pyk.kore.rpc import ExecuteResult from pyk.kore.syntax import Pattern +x, y = (EVar(name, INT) for name in ['x', 'y']) int_top = Top(INT) int_bottom = Bottom(INT) @@ -102,35 +103,50 @@ def kore_client(mock: Mock, mock_class: Mock) -> Iterator[KoreClient]: # noqa: App('IntAdd', (), (int_dv(1), int_dv(1))), {'state': kore(App('IntAdd', [], [int_dv(1), int_dv(1)]))}, { - 'state': {'term': kore(int_dv(2)), 'substitution': kore(int_top), 'predicate': kore(int_top)}, + 'state': { + 'term': kore(int_dv(2)), + 'substitution': kore( + And( + SORT_GENERATED_TOP_CELL, + ( + Equals(INT, SORT_GENERATED_TOP_CELL, x, int_dv(3)), + Equals(INT, SORT_GENERATED_TOP_CELL, y, int_dv(4)), + ), + ) + ), + 'predicate': kore(int_top), + }, 'depth': 1, 'reason': 'stuck', }, - StuckResult(State(int_dv(2), int_top, int_top), 1, logs=()), + StuckResult(State(int_dv(2), substitution={x: int_dv(3), y: int_dv(4)}, predicate=int_top), 1, logs=()), ), ( App('IntAdd', (), (int_dv(1), int_dv(1))), {'state': kore(App('IntAdd', [], [int_dv(1), int_dv(1)]))}, { - 'state': {'term': kore(int_dv(2)), 'substitution': kore(int_top), 'predicate': kore(int_top)}, + 'state': { + 'term': kore(int_dv(2)), + 'substitution': kore(Equals(INT, SORT_GENERATED_TOP_CELL, x, int_dv(3))), + }, 'depth': 1, 'reason': 'vacuous', }, - VacuousResult(State(int_dv(2), int_top, int_top), 1, logs=()), + VacuousResult(State(int_dv(2), substitution={x: int_dv(3)}), 1, logs=()), ), ( int_dv(0), {'state': kore(int_dv(0))}, { - 'state': {'term': kore(int_dv(1)), 'substitution': kore(int_dv(2)), 'predicate': kore(int_dv(3))}, - 'depth': 4, - 'unknown-predicate': kore(int_dv(5)), + 'state': {'term': kore(int_dv(1))}, + 'depth': 2, + 'unknown-predicate': kore(int_dv(3)), 'reason': 'aborted', }, AbortedResult( - state=State(term=int_dv(1), substitution=int_dv(2), predicate=int_dv(3)), - depth=4, - unknown_predicate=int_dv(5), + state=State(term=int_dv(1)), + depth=2, + unknown_predicate=int_dv(3), logs=(), ), ), diff --git a/src/tests/unit/kore/test_manip.py b/src/tests/unit/kore/test_manip.py index 83835a842..43b593692 100644 --- a/src/tests/unit/kore/test_manip.py +++ b/src/tests/unit/kore/test_manip.py @@ -5,16 +5,41 @@ import pytest -from pyk.kore.manip import free_occs +from pyk.kore import manip +from pyk.kore.prelude import dv from pyk.kore.syntax import And, EVar, Exists, SortApp, Top if TYPE_CHECKING: from collections.abc import Collection, Iterable + from typing import Final from pyk.kore.syntax import Pattern S = SortApp('S') x, y = (EVar(name, S) for name in ('x', 'y')) +a, b, c = (dv(val) for val in ['a', 'b', 'c']) + + +CONJUNCTS_TEST_DATA: Final = ( + (Top(S), ()), + (a, (a,)), + (And(S, (a,)), (a,)), + (And(S, (a, b)), (a, b)), + (And(S, (a, b, c)), (a, b, c)), + (And(S, (a, b, Top(S))), (a, b)), + (And(S, (And(S, (a, b)), c)), (a, b, c)), + (And(S, (a, And(S, (b, c)))), (a, b, c)), +) + + +@pytest.mark.parametrize('pattern,expected', CONJUNCTS_TEST_DATA, ids=count()) +def test_conjuncts(pattern: Pattern, expected: tuple[Pattern, ...]) -> None: + # When + actual = manip.conjuncts(pattern) + + # Then + assert actual == expected + FREE_OCCS_TEST_DATA: Iterable = ( (Top(S), [], {}), @@ -33,7 +58,7 @@ @pytest.mark.parametrize('pattern,bound_vars,expected', FREE_OCCS_TEST_DATA, ids=count()) def test_free_occs(pattern: Pattern, bound_vars: Collection[str], expected: dict[str, list[EVar]]) -> None: # When - actual = free_occs(pattern, bound_vars=bound_vars) + actual = manip.free_occs(pattern, bound_vars=bound_vars) # Then assert actual == expected