From eb23e73af1c12fee62c6b6c01ce8f0fb80dfe21c Mon Sep 17 00:00:00 2001 From: franfran Date: Wed, 30 Aug 2023 23:06:45 +0300 Subject: [PATCH 1/8] implement minimal working for kevm --- src/pyk/__main__.py | 3 +-- src/pyk/cterm.py | 8 ++++++++ src/pyk/ktool/kprove.py | 22 +++++++++----------- src/pyk/proof/reachability.py | 34 ++++++++++++++++--------------- src/tests/integration/test_pyk.py | 2 +- 5 files changed, 38 insertions(+), 31 deletions(-) diff --git a/src/pyk/__main__.py b/src/pyk/__main__.py index bdbda46b2..b4935f7e6 100644 --- a/src/pyk/__main__.py +++ b/src/pyk/__main__.py @@ -1,6 +1,5 @@ from __future__ import annotations -import json import logging import sys from argparse import ArgumentParser, FileType @@ -100,7 +99,7 @@ def exec_prove(args: Namespace) -> None: kompiled_dir: Path = args.definition_dir kprover = KProve(kompiled_dir, args.main_file) final_state = kprover.prove(Path(args.spec_file), spec_module_name=args.spec_module, args=args.kArgs) - args.output_file.write(json.dumps(mlOr([state.kast for state in final_state]).to_dict())) + args.output_file.write(final_state.to_json()) _LOGGER.info(f'Wrote file: {args.output_file.name}') diff --git a/src/pyk/cterm.py b/src/pyk/cterm.py index 89b1dc7ef..8c34c7415 100644 --- a/src/pyk/cterm.py +++ b/src/pyk/cterm.py @@ -98,6 +98,14 @@ def _is_spurious_constraint(term: KInner) -> bool: return True return False + @cached_property + def is_top(self) -> bool: + return CTerm._is_top(self.kast) + + @cached_property + def is_bottom(self) -> bool: + return CTerm._is_bottom(self.kast) + @staticmethod def _is_top(kast: KInner) -> bool: flat = flatten_label('#And', kast) diff --git a/src/pyk/ktool/kprove.py b/src/pyk/ktool/kprove.py index a0b192d46..384337588 100644 --- a/src/pyk/ktool/kprove.py +++ b/src/pyk/ktool/kprove.py @@ -12,7 +12,7 @@ from typing import TYPE_CHECKING from ..cli.utils import check_dir_path, check_file_path -from ..cterm import CTerm, build_claim +from ..cterm import build_claim, CTerm from ..kast import kast_term from ..kast.inner import KInner from ..kast.manip import extract_subst, flatten_label, free_vars @@ -197,7 +197,7 @@ def prove( depth: int | None = None, haskell_log_format: KoreExecLogFormat = KoreExecLogFormat.ONELINE, haskell_log_debug_transition: bool = True, - ) -> list[CTerm]: + ) -> CTerm: log_file = spec_file.with_suffix('.debug-log') if log_axioms_file is None else log_axioms_file if log_file.exists(): log_file.unlink() @@ -245,13 +245,13 @@ def prove( raise RuntimeError('kprove failed!') if dry_run: - return [CTerm.bottom()] + return CTerm.bottom() debug_log = _get_rule_log(log_file) - final_state = kast_term(json.loads(proc_result.stdout), KInner) # type: ignore # https://github.com/python/mypy/issues/4717 - if is_top(final_state) and len(debug_log) == 0 and not allow_zero_step: + final_state = CTerm.from_kast(kast_term(json.loads(proc_result.stdout), KInner)) # type: ignore # https://github.com/python/mypy/issues/4717 + if final_state.is_top() and len(debug_log) == 0 and not allow_zero_step: raise ValueError(f'Proof took zero steps, likely the LHS is invalid: {spec_file}') - return [CTerm.from_kast(disjunct) for disjunct in flatten_label('#Or', final_state)] + return final_state def prove_claim( self, @@ -265,7 +265,7 @@ def prove_claim( allow_zero_step: bool = False, dry_run: bool = False, depth: int | None = None, - ) -> list[CTerm]: + ) -> CTerm: with self._tmp_claim_definition(claim, claim_id, lemmas=lemmas) as (claim_path, claim_module_name): return self.prove( claim_path, @@ -305,12 +305,10 @@ def prove_cterm( allow_zero_step=allow_zero_step, depth=depth, ) - next_states = list(unique(CTerm.from_kast(var_map(ns.kast)) for ns in next_state if not CTerm._is_top(ns.kast))) + next_states = list(unique(var_map(ns) for ns in flatten_label('#Or', next_state) if not is_top(ns))) constraint_subst, _ = extract_subst(init_cterm.kast) - next_states = [ - CTerm.from_kast(mlAnd([constraint_subst.unapply(ns.kast), constraint_subst.ml_pred])) for ns in next_states - ] - return next_states if len(next_states) > 0 else [CTerm.top()] + next_states_cterm = [CTerm.from_kast(mlAnd([constraint_subst.unapply(ns), constraint_subst.ml_pred])) for ns in next_states] + return next_states_cterm if len(next_states_cterm) > 0 else [CTerm.top()] def get_claim_modules( self, diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index ddbedb03d..3acc247ad 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -7,7 +7,7 @@ from pyk.kore.rpc import LogEntry -from ..kast.inner import KInner, KRewrite, KSort, Subst +from ..kast.inner import KRewrite, KSort from ..kast.manip import flatten_label, ml_pred_to_bool from ..kast.outer import KClaim from ..kcfg import KCFG @@ -28,6 +28,7 @@ from ..kcfg import KCFGExplore from ..kcfg.kcfg import NodeIdLike from ..ktool.kprint import KPrint + from ..kast.inner import KInner T = TypeVar('T', bound='Proof') @@ -789,21 +790,22 @@ def from_proof(proof: APRProof, kcfg_explore: KCFGExplore, counterexample_info: failure_reasons = {} models = {} for node in proof.failing: - node_cterm, _ = kcfg_explore.cterm_simplify(node.cterm) - target_cterm, _ = kcfg_explore.cterm_simplify(target.cterm) - _, reason = kcfg_explore.implication_failure_reason(node_cterm, target_cterm) - path_condition = kcfg_explore.kprint.pretty_print(proof.path_constraints(node.id)) - failure_reasons[node.id] = reason - path_conditions[node.id] = path_condition - if counterexample_info: - model_subst = kcfg_explore.cterm_get_model(node.cterm) - if type(model_subst) is Subst: - model: list[tuple[str, str]] = [] - for var, term in model_subst.to_dict().items(): - term_kast = KInner.from_dict(term) - term_pretty = kcfg_explore.kprint.pretty_print(term_kast) - model.append((var, term_pretty)) - models[node.id] = model + pass + # node_cterm, _ = kcfg_explore.cterm_simplify(node.cterm) + # target_cterm, _ = kcfg_explore.cterm_simplify(target.cterm) + # _, reason = kcfg_explore.implication_failure_reason(node_cterm, target_cterm) + # path_condition = kcfg_explore.kprint.pretty_print(proof.path_constraints(node.id)) + # failure_reasons[node.id] = reason + # path_conditions[node.id] = path_condition + # if counterexample_info: + # model_subst = kcfg_explore.cterm_get_model(node.cterm) + # if type(model_subst) is Subst: + # model: list[tuple[str, str]] = [] + # for var, term in model_subst.to_dict().items(): + # term_kast = KInner.from_dict(term) + # term_pretty = kcfg_explore.kprint.pretty_print(term_kast) + # model.append((var, term_pretty)) + # models[node.id] = model return APRFailureInfo( failing_nodes=failing_nodes, pending_nodes=pending_nodes, diff --git a/src/tests/integration/test_pyk.py b/src/tests/integration/test_pyk.py index 58490dfbf..f4534db77 100644 --- a/src/tests/integration/test_pyk.py +++ b/src/tests/integration/test_pyk.py @@ -93,5 +93,5 @@ def test_minimize_term(self, assume_argv: AssumeArgv, tmp_path: Path, definition main() assume_argv(['pyk', 'print', str(definition_dir), str(prove_res_file), '--output-file', str(actual_file)]) main() - # assert expected_file.read_text() == actual_file.read_text() + assert expected_file.read_text() == actual_file.read_text() expected_file.write_text(actual_file.read_text()) From e4a5547e2c448049ea750abee8e59feed1c04b96 Mon Sep 17 00:00:00 2001 From: franfran Date: Thu, 31 Aug 2023 09:17:50 +0300 Subject: [PATCH 2/8] use cached property --- src/pyk/ktool/kprove.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/pyk/ktool/kprove.py b/src/pyk/ktool/kprove.py index 384337588..eb4394f4f 100644 --- a/src/pyk/ktool/kprove.py +++ b/src/pyk/ktool/kprove.py @@ -249,7 +249,7 @@ def prove( debug_log = _get_rule_log(log_file) final_state = CTerm.from_kast(kast_term(json.loads(proc_result.stdout), KInner)) # type: ignore # https://github.com/python/mypy/issues/4717 - if final_state.is_top() and len(debug_log) == 0 and not allow_zero_step: + if final_state.is_top and len(debug_log) == 0 and not allow_zero_step: raise ValueError(f'Proof took zero steps, likely the LHS is invalid: {spec_file}') return final_state From 80658e907bfd8808433e8586004fac73ca8575e4 Mon Sep 17 00:00:00 2001 From: franfran Date: Thu, 31 Aug 2023 09:24:01 +0300 Subject: [PATCH 3/8] linting --- src/pyk/__main__.py | 2 +- src/pyk/ktool/kprove.py | 8 +++-- src/pyk/proof/reachability.py | 34 +++++++++---------- .../integration/kprove/test_emit_json_spec.py | 6 ++-- .../kprove/test_print_prove_rewrite.py | 4 +-- .../kprove/test_prove_claim_with_lemmas.py | 6 ++-- 6 files changed, 27 insertions(+), 33 deletions(-) diff --git a/src/pyk/__main__.py b/src/pyk/__main__.py index b4935f7e6..b217158c3 100644 --- a/src/pyk/__main__.py +++ b/src/pyk/__main__.py @@ -99,7 +99,7 @@ def exec_prove(args: Namespace) -> None: kompiled_dir: Path = args.definition_dir kprover = KProve(kompiled_dir, args.main_file) final_state = kprover.prove(Path(args.spec_file), spec_module_name=args.spec_module, args=args.kArgs) - args.output_file.write(final_state.to_json()) + args.output_file.write(final_state.kast.to_json()) _LOGGER.info(f'Wrote file: {args.output_file.name}') diff --git a/src/pyk/ktool/kprove.py b/src/pyk/ktool/kprove.py index eb4394f4f..0338e1fe8 100644 --- a/src/pyk/ktool/kprove.py +++ b/src/pyk/ktool/kprove.py @@ -12,7 +12,7 @@ from typing import TYPE_CHECKING from ..cli.utils import check_dir_path, check_file_path -from ..cterm import build_claim, CTerm +from ..cterm import CTerm, build_claim from ..kast import kast_term from ..kast.inner import KInner from ..kast.manip import extract_subst, flatten_label, free_vars @@ -305,9 +305,11 @@ def prove_cterm( allow_zero_step=allow_zero_step, depth=depth, ) - next_states = list(unique(var_map(ns) for ns in flatten_label('#Or', next_state) if not is_top(ns))) + next_states = list(unique(var_map(ns) for ns in flatten_label('#Or', next_state.kast) if not is_top(ns))) constraint_subst, _ = extract_subst(init_cterm.kast) - next_states_cterm = [CTerm.from_kast(mlAnd([constraint_subst.unapply(ns), constraint_subst.ml_pred])) for ns in next_states] + next_states_cterm = [ + CTerm.from_kast(mlAnd([constraint_subst.unapply(ns), constraint_subst.ml_pred])) for ns in next_states + ] return next_states_cterm if len(next_states_cterm) > 0 else [CTerm.top()] def get_claim_modules( diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 3acc247ad..ddbedb03d 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -7,7 +7,7 @@ from pyk.kore.rpc import LogEntry -from ..kast.inner import KRewrite, KSort +from ..kast.inner import KInner, KRewrite, KSort, Subst from ..kast.manip import flatten_label, ml_pred_to_bool from ..kast.outer import KClaim from ..kcfg import KCFG @@ -28,7 +28,6 @@ from ..kcfg import KCFGExplore from ..kcfg.kcfg import NodeIdLike from ..ktool.kprint import KPrint - from ..kast.inner import KInner T = TypeVar('T', bound='Proof') @@ -790,22 +789,21 @@ def from_proof(proof: APRProof, kcfg_explore: KCFGExplore, counterexample_info: failure_reasons = {} models = {} for node in proof.failing: - pass - # node_cterm, _ = kcfg_explore.cterm_simplify(node.cterm) - # target_cterm, _ = kcfg_explore.cterm_simplify(target.cterm) - # _, reason = kcfg_explore.implication_failure_reason(node_cterm, target_cterm) - # path_condition = kcfg_explore.kprint.pretty_print(proof.path_constraints(node.id)) - # failure_reasons[node.id] = reason - # path_conditions[node.id] = path_condition - # if counterexample_info: - # model_subst = kcfg_explore.cterm_get_model(node.cterm) - # if type(model_subst) is Subst: - # model: list[tuple[str, str]] = [] - # for var, term in model_subst.to_dict().items(): - # term_kast = KInner.from_dict(term) - # term_pretty = kcfg_explore.kprint.pretty_print(term_kast) - # model.append((var, term_pretty)) - # models[node.id] = model + node_cterm, _ = kcfg_explore.cterm_simplify(node.cterm) + target_cterm, _ = kcfg_explore.cterm_simplify(target.cterm) + _, reason = kcfg_explore.implication_failure_reason(node_cterm, target_cterm) + path_condition = kcfg_explore.kprint.pretty_print(proof.path_constraints(node.id)) + failure_reasons[node.id] = reason + path_conditions[node.id] = path_condition + if counterexample_info: + model_subst = kcfg_explore.cterm_get_model(node.cterm) + if type(model_subst) is Subst: + model: list[tuple[str, str]] = [] + for var, term in model_subst.to_dict().items(): + term_kast = KInner.from_dict(term) + term_pretty = kcfg_explore.kprint.pretty_print(term_kast) + model.append((var, term_pretty)) + models[node.id] = model return APRFailureInfo( failing_nodes=failing_nodes, pending_nodes=pending_nodes, diff --git a/src/tests/integration/kprove/test_emit_json_spec.py b/src/tests/integration/kprove/test_emit_json_spec.py index eff1b41cb..4a1822725 100644 --- a/src/tests/integration/kprove/test_emit_json_spec.py +++ b/src/tests/integration/kprove/test_emit_json_spec.py @@ -5,12 +5,10 @@ import pytest -from pyk.cterm import CTerm from pyk.kast.kast import EMPTY_ATT from pyk.kast.manip import remove_generated_cells from pyk.kast.outer import KDefinition, KRequire from pyk.kast.pretty import paren -from pyk.prelude.ml import mlOr from pyk.testing import KProveTest from ..utils import K_FILES @@ -43,7 +41,7 @@ def test_prove_claim(self, kprove: KProve, spec_module: KFlatModule) -> None: result = kprove.prove_claim(spec_module.claims[0], 'looping-1') # Then - assert CTerm._is_top(mlOr([res.kast for res in result])) + assert result.is_top def test_prove(self, kprove: KProve, spec_module: KFlatModule) -> None: # Given @@ -64,4 +62,4 @@ def test_prove(self, kprove: KProve, spec_module: KFlatModule) -> None: result = kprove.prove(spec_file, spec_module_name=spec_module_name, args=['-I', str(include_dir)]) # Then - assert CTerm._is_top(mlOr([res.kast for res in result])) + assert result.is_top diff --git a/src/tests/integration/kprove/test_print_prove_rewrite.py b/src/tests/integration/kprove/test_print_prove_rewrite.py index 244175283..cd071d8c2 100644 --- a/src/tests/integration/kprove/test_print_prove_rewrite.py +++ b/src/tests/integration/kprove/test_print_prove_rewrite.py @@ -2,11 +2,9 @@ from typing import TYPE_CHECKING -from pyk.cterm import CTerm from pyk.kast.inner import KApply, KRewrite, KVariable from pyk.kast.manip import push_down_rewrites from pyk.kast.outer import KClaim -from pyk.prelude.ml import mlOr from pyk.testing import KProveTest from ..utils import K_FILES @@ -47,4 +45,4 @@ def test_print_prove_rewrite(self, kprove: KProve) -> None: # Then assert actual == expected - assert CTerm._is_top(mlOr([res.kast for res in result])) + assert result.is_top diff --git a/src/tests/integration/kprove/test_prove_claim_with_lemmas.py b/src/tests/integration/kprove/test_prove_claim_with_lemmas.py index b8f30b1a7..b475442c0 100644 --- a/src/tests/integration/kprove/test_prove_claim_with_lemmas.py +++ b/src/tests/integration/kprove/test_prove_claim_with_lemmas.py @@ -2,12 +2,10 @@ from typing import TYPE_CHECKING -from pyk.cterm import CTerm from pyk.kast import KAtt from pyk.kast.inner import KToken from pyk.kast.outer import KClaim, KRule from pyk.prelude.kbool import BOOL -from pyk.prelude.ml import mlOr from pyk.testing import KProveTest from ..utils import K_FILES @@ -36,5 +34,5 @@ def test_prove_claim_with_lemmas(self, kprove: KProve) -> None: result2 = kprove.prove_claim(claim, 'claim-with-lemma', lemmas=[lemma]) # Then - assert not CTerm._is_top(mlOr([res.kast for res in result1])) - assert CTerm._is_top(mlOr([res.kast for res in result2])) + assert not result1.is_top + assert result2.is_top From 5fa1a712f3afe77fa847a5eae41ef65195ff1759 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 31 Aug 2023 06:31:38 +0000 Subject: [PATCH 4/8] Set Version: 0.1.432 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index dbca01d40..adb14616f 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.431 +0.1.432 diff --git a/pyproject.toml b/pyproject.toml index 8c087c6a8..bfe14ddc4 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.431" +version = "0.1.432" description = "" authors = [ "Runtime Verification, Inc. ", From 71095a60dc3e763612690ee43a9456d69d255392 Mon Sep 17 00:00:00 2001 From: franfran Date: Thu, 31 Aug 2023 23:24:20 +0300 Subject: [PATCH 5/8] return list[CTerm] --- src/pyk/__main__.py | 3 ++- src/pyk/ktool/kprove.py | 20 ++++++++++--------- .../integration/kprove/test_emit_json_spec.py | 6 ++++-- .../kprove/test_print_prove_rewrite.py | 4 +++- .../kprove/test_prove_claim_with_lemmas.py | 6 ++++-- 5 files changed, 24 insertions(+), 15 deletions(-) diff --git a/src/pyk/__main__.py b/src/pyk/__main__.py index b217158c3..bdbda46b2 100644 --- a/src/pyk/__main__.py +++ b/src/pyk/__main__.py @@ -1,5 +1,6 @@ from __future__ import annotations +import json import logging import sys from argparse import ArgumentParser, FileType @@ -99,7 +100,7 @@ def exec_prove(args: Namespace) -> None: kompiled_dir: Path = args.definition_dir kprover = KProve(kompiled_dir, args.main_file) final_state = kprover.prove(Path(args.spec_file), spec_module_name=args.spec_module, args=args.kArgs) - args.output_file.write(final_state.kast.to_json()) + args.output_file.write(json.dumps(mlOr([state.kast for state in final_state]).to_dict())) _LOGGER.info(f'Wrote file: {args.output_file.name}') diff --git a/src/pyk/ktool/kprove.py b/src/pyk/ktool/kprove.py index 0338e1fe8..156059651 100644 --- a/src/pyk/ktool/kprove.py +++ b/src/pyk/ktool/kprove.py @@ -17,7 +17,7 @@ from ..kast.inner import KInner from ..kast.manip import extract_subst, flatten_label, free_vars from ..kast.outer import KDefinition, KFlatModule, KFlatModuleList, KImport, KRequire -from ..prelude.ml import is_top, mlAnd +from ..prelude.ml import mlAnd from ..utils import gen_file_timestamp, run_process, unique from .kprint import KPrint @@ -197,7 +197,7 @@ def prove( depth: int | None = None, haskell_log_format: KoreExecLogFormat = KoreExecLogFormat.ONELINE, haskell_log_debug_transition: bool = True, - ) -> CTerm: + ) -> list[CTerm]: log_file = spec_file.with_suffix('.debug-log') if log_axioms_file is None else log_axioms_file if log_file.exists(): log_file.unlink() @@ -245,13 +245,14 @@ def prove( raise RuntimeError('kprove failed!') if dry_run: - return CTerm.bottom() + return [CTerm.bottom()] debug_log = _get_rule_log(log_file) - final_state = CTerm.from_kast(kast_term(json.loads(proc_result.stdout), KInner)) # type: ignore # https://github.com/python/mypy/issues/4717 - if final_state.is_top and len(debug_log) == 0 and not allow_zero_step: + as_kast = kast_term(json.loads(proc_result.stdout), KInner) # type: ignore # https://github.com/python/mypy/issues/4717 + final_states = [CTerm.from_kast(disjunct) for disjunct in flatten_label('#Or', as_kast)] + if next(state.is_top for state in final_states) and len(debug_log) == 0 and not allow_zero_step: raise ValueError(f'Proof took zero steps, likely the LHS is invalid: {spec_file}') - return final_state + return final_states def prove_claim( self, @@ -265,7 +266,7 @@ def prove_claim( allow_zero_step: bool = False, dry_run: bool = False, depth: int | None = None, - ) -> CTerm: + ) -> list[CTerm]: with self._tmp_claim_definition(claim, claim_id, lemmas=lemmas) as (claim_path, claim_module_name): return self.prove( claim_path, @@ -295,7 +296,7 @@ def prove_cterm( depth: int | None = None, ) -> list[CTerm]: claim, var_map = build_claim(claim_id, init_cterm, target_cterm, keep_vars=free_vars(init_cterm.kast)) - next_state = self.prove_claim( + next_states_cterm = self.prove_claim( claim, claim_id, lemmas=lemmas, @@ -305,7 +306,8 @@ def prove_cterm( allow_zero_step=allow_zero_step, depth=depth, ) - next_states = list(unique(var_map(ns) for ns in flatten_label('#Or', next_state.kast) if not is_top(ns))) + # next_states = list(unique(var_map(ns) for ns in flatten_label('#Or', next_state.kast) if not is_top(ns))) + next_states = list(unique(var_map(ns.kast) for ns in next_states_cterm if not ns.is_top)) constraint_subst, _ = extract_subst(init_cterm.kast) next_states_cterm = [ CTerm.from_kast(mlAnd([constraint_subst.unapply(ns), constraint_subst.ml_pred])) for ns in next_states diff --git a/src/tests/integration/kprove/test_emit_json_spec.py b/src/tests/integration/kprove/test_emit_json_spec.py index 4a1822725..eff1b41cb 100644 --- a/src/tests/integration/kprove/test_emit_json_spec.py +++ b/src/tests/integration/kprove/test_emit_json_spec.py @@ -5,10 +5,12 @@ import pytest +from pyk.cterm import CTerm from pyk.kast.kast import EMPTY_ATT from pyk.kast.manip import remove_generated_cells from pyk.kast.outer import KDefinition, KRequire from pyk.kast.pretty import paren +from pyk.prelude.ml import mlOr from pyk.testing import KProveTest from ..utils import K_FILES @@ -41,7 +43,7 @@ def test_prove_claim(self, kprove: KProve, spec_module: KFlatModule) -> None: result = kprove.prove_claim(spec_module.claims[0], 'looping-1') # Then - assert result.is_top + assert CTerm._is_top(mlOr([res.kast for res in result])) def test_prove(self, kprove: KProve, spec_module: KFlatModule) -> None: # Given @@ -62,4 +64,4 @@ def test_prove(self, kprove: KProve, spec_module: KFlatModule) -> None: result = kprove.prove(spec_file, spec_module_name=spec_module_name, args=['-I', str(include_dir)]) # Then - assert result.is_top + assert CTerm._is_top(mlOr([res.kast for res in result])) diff --git a/src/tests/integration/kprove/test_print_prove_rewrite.py b/src/tests/integration/kprove/test_print_prove_rewrite.py index cd071d8c2..244175283 100644 --- a/src/tests/integration/kprove/test_print_prove_rewrite.py +++ b/src/tests/integration/kprove/test_print_prove_rewrite.py @@ -2,9 +2,11 @@ from typing import TYPE_CHECKING +from pyk.cterm import CTerm from pyk.kast.inner import KApply, KRewrite, KVariable from pyk.kast.manip import push_down_rewrites from pyk.kast.outer import KClaim +from pyk.prelude.ml import mlOr from pyk.testing import KProveTest from ..utils import K_FILES @@ -45,4 +47,4 @@ def test_print_prove_rewrite(self, kprove: KProve) -> None: # Then assert actual == expected - assert result.is_top + assert CTerm._is_top(mlOr([res.kast for res in result])) diff --git a/src/tests/integration/kprove/test_prove_claim_with_lemmas.py b/src/tests/integration/kprove/test_prove_claim_with_lemmas.py index b475442c0..b8f30b1a7 100644 --- a/src/tests/integration/kprove/test_prove_claim_with_lemmas.py +++ b/src/tests/integration/kprove/test_prove_claim_with_lemmas.py @@ -2,10 +2,12 @@ from typing import TYPE_CHECKING +from pyk.cterm import CTerm from pyk.kast import KAtt from pyk.kast.inner import KToken from pyk.kast.outer import KClaim, KRule from pyk.prelude.kbool import BOOL +from pyk.prelude.ml import mlOr from pyk.testing import KProveTest from ..utils import K_FILES @@ -34,5 +36,5 @@ def test_prove_claim_with_lemmas(self, kprove: KProve) -> None: result2 = kprove.prove_claim(claim, 'claim-with-lemma', lemmas=[lemma]) # Then - assert not result1.is_top - assert result2.is_top + assert not CTerm._is_top(mlOr([res.kast for res in result1])) + assert CTerm._is_top(mlOr([res.kast for res in result2])) From 3d89bbec664f19998cff94ab9ab2eac3bd808bd6 Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 25 Sep 2023 17:52:41 +0000 Subject: [PATCH 6/8] Set Version: 0.1.449 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 44516207b..868227d78 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.448 +0.1.449 diff --git a/pyproject.toml b/pyproject.toml index 412c91ea1..a9928acb2 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.448" +version = "0.1.449" description = "" authors = [ "Runtime Verification, Inc. ", From ca6064d74c9c380a75faf8434ce2baf5882d5691 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Mon, 25 Sep 2023 13:33:41 -0500 Subject: [PATCH 7/8] Fix tests to not use disjunnct --- src/pyk/cterm.py | 4 ---- src/tests/integration/kprove/test_emit_json_spec.py | 7 ++++--- src/tests/integration/kprove/test_print_prove_rewrite.py | 4 ++-- .../integration/kprove/test_prove_claim_with_lemmas.py | 7 ++++--- 4 files changed, 10 insertions(+), 12 deletions(-) diff --git a/src/pyk/cterm.py b/src/pyk/cterm.py index d16c2a64c..77fd49890 100644 --- a/src/pyk/cterm.py +++ b/src/pyk/cterm.py @@ -102,10 +102,6 @@ def _is_spurious_constraint(term: KInner) -> bool: def is_top(self) -> bool: return CTerm._is_top(self.kast) - @cached_property - def is_bottom(self) -> bool: - return CTerm._is_bottom(self.kast) - @staticmethod def _is_top(kast: KInner) -> bool: flat = flatten_label('#And', kast) diff --git a/src/tests/integration/kprove/test_emit_json_spec.py b/src/tests/integration/kprove/test_emit_json_spec.py index eff1b41cb..15a01973c 100644 --- a/src/tests/integration/kprove/test_emit_json_spec.py +++ b/src/tests/integration/kprove/test_emit_json_spec.py @@ -10,7 +10,6 @@ from pyk.kast.manip import remove_generated_cells from pyk.kast.outer import KDefinition, KRequire from pyk.kast.pretty import paren -from pyk.prelude.ml import mlOr from pyk.testing import KProveTest from ..utils import K_FILES @@ -43,7 +42,8 @@ def test_prove_claim(self, kprove: KProve, spec_module: KFlatModule) -> None: result = kprove.prove_claim(spec_module.claims[0], 'looping-1') # Then - assert CTerm._is_top(mlOr([res.kast for res in result])) + assert len(result) == 1 + assert CTerm.is_top(result[0]) def test_prove(self, kprove: KProve, spec_module: KFlatModule) -> None: # Given @@ -64,4 +64,5 @@ def test_prove(self, kprove: KProve, spec_module: KFlatModule) -> None: result = kprove.prove(spec_file, spec_module_name=spec_module_name, args=['-I', str(include_dir)]) # Then - assert CTerm._is_top(mlOr([res.kast for res in result])) + assert len(result) == 1 + assert CTerm.is_top(result[0]) diff --git a/src/tests/integration/kprove/test_print_prove_rewrite.py b/src/tests/integration/kprove/test_print_prove_rewrite.py index 244175283..24e9cdb4c 100644 --- a/src/tests/integration/kprove/test_print_prove_rewrite.py +++ b/src/tests/integration/kprove/test_print_prove_rewrite.py @@ -6,7 +6,6 @@ from pyk.kast.inner import KApply, KRewrite, KVariable from pyk.kast.manip import push_down_rewrites from pyk.kast.outer import KClaim -from pyk.prelude.ml import mlOr from pyk.testing import KProveTest from ..utils import K_FILES @@ -47,4 +46,5 @@ def test_print_prove_rewrite(self, kprove: KProve) -> None: # Then assert actual == expected - assert CTerm._is_top(mlOr([res.kast for res in result])) + assert len(result) == 1 + assert CTerm.is_top(result[0]) diff --git a/src/tests/integration/kprove/test_prove_claim_with_lemmas.py b/src/tests/integration/kprove/test_prove_claim_with_lemmas.py index b8f30b1a7..3633f0687 100644 --- a/src/tests/integration/kprove/test_prove_claim_with_lemmas.py +++ b/src/tests/integration/kprove/test_prove_claim_with_lemmas.py @@ -7,7 +7,6 @@ from pyk.kast.inner import KToken from pyk.kast.outer import KClaim, KRule from pyk.prelude.kbool import BOOL -from pyk.prelude.ml import mlOr from pyk.testing import KProveTest from ..utils import K_FILES @@ -36,5 +35,7 @@ def test_prove_claim_with_lemmas(self, kprove: KProve) -> None: result2 = kprove.prove_claim(claim, 'claim-with-lemma', lemmas=[lemma]) # Then - assert not CTerm._is_top(mlOr([res.kast for res in result1])) - assert CTerm._is_top(mlOr([res.kast for res in result2])) + assert len(result1) == 1 + assert len(result2) == 1 + assert not CTerm.is_top(result1[0]) + assert CTerm.is_top(result2[0]) From 11b941cf3402a97a2253b1720901661281095939 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Mon, 25 Sep 2023 13:43:53 -0500 Subject: [PATCH 8/8] Fix is_top call --- src/tests/integration/kprove/test_emit_json_spec.py | 5 ++--- src/tests/integration/kprove/test_print_prove_rewrite.py | 3 +-- src/tests/integration/kprove/test_prove_claim_with_lemmas.py | 5 ++--- 3 files changed, 5 insertions(+), 8 deletions(-) diff --git a/src/tests/integration/kprove/test_emit_json_spec.py b/src/tests/integration/kprove/test_emit_json_spec.py index 15a01973c..6e75e5986 100644 --- a/src/tests/integration/kprove/test_emit_json_spec.py +++ b/src/tests/integration/kprove/test_emit_json_spec.py @@ -5,7 +5,6 @@ import pytest -from pyk.cterm import CTerm from pyk.kast.kast import EMPTY_ATT from pyk.kast.manip import remove_generated_cells from pyk.kast.outer import KDefinition, KRequire @@ -43,7 +42,7 @@ def test_prove_claim(self, kprove: KProve, spec_module: KFlatModule) -> None: # Then assert len(result) == 1 - assert CTerm.is_top(result[0]) + assert result[0].is_top def test_prove(self, kprove: KProve, spec_module: KFlatModule) -> None: # Given @@ -65,4 +64,4 @@ def test_prove(self, kprove: KProve, spec_module: KFlatModule) -> None: # Then assert len(result) == 1 - assert CTerm.is_top(result[0]) + assert result[0].is_top diff --git a/src/tests/integration/kprove/test_print_prove_rewrite.py b/src/tests/integration/kprove/test_print_prove_rewrite.py index 24e9cdb4c..f0fbe581f 100644 --- a/src/tests/integration/kprove/test_print_prove_rewrite.py +++ b/src/tests/integration/kprove/test_print_prove_rewrite.py @@ -2,7 +2,6 @@ from typing import TYPE_CHECKING -from pyk.cterm import CTerm from pyk.kast.inner import KApply, KRewrite, KVariable from pyk.kast.manip import push_down_rewrites from pyk.kast.outer import KClaim @@ -47,4 +46,4 @@ def test_print_prove_rewrite(self, kprove: KProve) -> None: # Then assert actual == expected assert len(result) == 1 - assert CTerm.is_top(result[0]) + assert result[0].is_top diff --git a/src/tests/integration/kprove/test_prove_claim_with_lemmas.py b/src/tests/integration/kprove/test_prove_claim_with_lemmas.py index 3633f0687..220f5910e 100644 --- a/src/tests/integration/kprove/test_prove_claim_with_lemmas.py +++ b/src/tests/integration/kprove/test_prove_claim_with_lemmas.py @@ -2,7 +2,6 @@ from typing import TYPE_CHECKING -from pyk.cterm import CTerm from pyk.kast import KAtt from pyk.kast.inner import KToken from pyk.kast.outer import KClaim, KRule @@ -37,5 +36,5 @@ def test_prove_claim_with_lemmas(self, kprove: KProve) -> None: # Then assert len(result1) == 1 assert len(result2) == 1 - assert not CTerm.is_top(result1[0]) - assert CTerm.is_top(result2[0]) + assert not result1[0].is_top + assert result2[0].is_top