From eb23e73af1c12fee62c6b6c01ce8f0fb80dfe21c Mon Sep 17 00:00:00 2001
From: franfran <fgg67@hotmail.fr>
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 <fgg67@hotmail.fr>
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 <fgg67@hotmail.fr>
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 <devops@runtimeverification.com>
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. <contact@runtimeverification.com>",
From 71095a60dc3e763612690ee43a9456d69d255392 Mon Sep 17 00:00:00 2001
From: franfran <fgg67@hotmail.fr>
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 <devops@runtimeverification.com>
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. <contact@runtimeverification.com>",
From ca6064d74c9c380a75faf8434ce2baf5882d5691 Mon Sep 17 00:00:00 2001
From: Noah Watson <noah@nwatson.xyz>
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 <noah@nwatson.xyz>
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