Merge remote-tracking branch 'origin/master' into anvacaru/vacuous-2

Author: anvacaru

deps/k_release

@@ -1 +1 @@
-6.0.58
+6.0.69

package/version

@@ -1 +1 @@
-0.1.416
+0.1.431

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.416"
+version = "0.1.431"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-K_VERSION: Final = '6.0.58'
+K_VERSION: Final = '6.0.69'

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.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}')
 
 

src/pyk/cli/args.py

@@ -5,7 +5,7 @@
 from typing import TYPE_CHECKING
 
 from ..utils import ensure_dir_path
-from .utils import dir_path, file_path
+from .utils import bug_report_arg, dir_path, file_path
 
 if TYPE_CHECKING:
     from typing import TypeVar
@@ -27,6 +27,16 @@ def parallel_args(self) -> ArgumentParser:
         args.add_argument('--workers', '-j', default=1, type=int, help='Number of processes to run in parallel.')
         return args
 
+    @cached_property
+    def bug_report_args(self) -> ArgumentParser:
+        args = ArgumentParser(add_help=False)
+        args.add_argument(
+            '--bug-report',
+            type=bug_report_arg,
+            help='Generate bug report with given name',
+        )
+        return args
+
     @cached_property
     def kompile_args(self) -> ArgumentParser:
         args = ArgumentParser(add_help=False)
@@ -81,6 +91,18 @@ def kompile_args(self) -> ArgumentParser:
         args.add_argument('-O3', dest='o3', default=False, action='store_true', help='Optimization level 3.')
         return args
 
+    @cached_property
+    def smt_args(self) -> ArgumentParser:
+        args = ArgumentParser(add_help=False)
+        args.add_argument('--smt-timeout', dest='smt_timeout', type=int, help='Timeout in ms to use for SMT queries.')
+        args.add_argument(
+            '--smt-retry-limit',
+            dest='smt_retry_limit',
+            type=int,
+            help='Number of times to retry SMT queries with scaling timeouts.',
+        )
+        return args
+
     @cached_property
     def display_args(self) -> ArgumentParser:
         args = ArgumentParser(add_help=False)

src/pyk/cli/utils.py

@@ -4,7 +4,7 @@
 from pathlib import Path
 from typing import TYPE_CHECKING
 
-from ..utils import check_dir_path, check_file_path, check_relative_path
+from ..utils import BugReport, check_dir_path, check_file_path, check_relative_path, ensure_dir_path
 
 if TYPE_CHECKING:
     from argparse import Namespace
@@ -73,3 +73,9 @@ def parse(s: str) -> tuple[T1, T2]:
         return fst_type(elems[0]), snd_type(elems[1])
 
     return parse
+
+
+def bug_report_arg(path: str | Path) -> BugReport:
+    path = Path(path)
+    ensure_dir_path(path.parent)
+    return BugReport(path)

src/pyk/cterm.py

@@ -5,9 +5,10 @@
 from itertools import chain
 from typing import TYPE_CHECKING
 
-from .kast.inner import KApply, KInner, KRewrite, KVariable, Subst
+from .kast.inner import KApply, KInner, KRewrite, KToken, KVariable, Subst, bottom_up
 from .kast.kast import KAtt
 from .kast.manip import (
+    abstract_term_safely,
     apply_existential_substitutions,
     count_vars,
     flatten_label,
@@ -22,41 +23,64 @@
 )
 from .kast.outer import KClaim, KRule
 from .prelude.k import GENERATED_TOP_CELL
-from .prelude.ml import is_top, mlAnd, mlImplies, mlTop
-from .utils import unique
+from .prelude.kbool import orBool
+from .prelude.ml import is_bottom, is_top, mlAnd, mlBottom, mlEqualsTrue, mlImplies, mlTop
+from .utils import single, unique
 
 if TYPE_CHECKING:
     from collections.abc import Iterable, Iterator
     from typing import Any
 
+    from .kast.outer import KDefinition
+
 
 @dataclass(frozen=True, order=True)
 class CTerm:
     config: KInner  # TODO Optional?
     constraints: tuple[KInner, ...]
 
     def __init__(self, config: KInner, constraints: Iterable[KInner] = ()) -> None:
-        self._check_config(config)
-        constraints = self._normalize_constraints(constraints)
+        if CTerm._is_top(config):
+            config = mlTop()
+            constraints = ()
+        elif CTerm._is_bottom(config):
+            config = mlBottom()
+            constraints = ()
+        else:
+            self._check_config(config)
+            constraints = self._normalize_constraints(constraints)
         object.__setattr__(self, 'config', config)
         object.__setattr__(self, 'constraints', constraints)
 
     @staticmethod
     def from_kast(kast: KInner) -> CTerm:
-        config, constraint = split_config_and_constraints(kast)
-        constraints = flatten_label('#And', constraint)
-        return CTerm(config, constraints)
+        if CTerm._is_top(kast):
+            return CTerm.top()
+        elif CTerm._is_bottom(kast):
+            return CTerm.bottom()
+        else:
+            config, constraint = split_config_and_constraints(kast)
+            constraints = flatten_label('#And', constraint)
+            return CTerm(config, constraints)
 
     @staticmethod
     def from_dict(dct: dict[str, Any]) -> CTerm:
         config = KInner.from_dict(dct['config'])
         constraints = [KInner.from_dict(c) for c in dct['constraints']]
         return CTerm(config, constraints)
 
+    @staticmethod
+    def top() -> CTerm:
+        return CTerm(mlTop(), ())
+
+    @staticmethod
+    def bottom() -> CTerm:
+        return CTerm(mlBottom(), ())
+
     @staticmethod
     def _check_config(config: KInner) -> None:
         if not isinstance(config, KApply) or not config.is_cell:
-            raise ValueError('Expected cell label, found: {config.label.name}')
+            raise ValueError(f'Expected cell label, found: {config}')
 
     @staticmethod
     def _normalize_constraints(constraints: Iterable[KInner]) -> tuple[KInner, ...]:
@@ -74,6 +98,20 @@ def _is_spurious_constraint(term: KInner) -> bool:
             return True
         return False
 
+    @staticmethod
+    def _is_top(kast: KInner) -> bool:
+        flat = flatten_label('#And', kast)
+        if len(flat) == 1:
+            return is_top(single(flat))
+        return all(CTerm._is_top(term) for term in flat)
+
+    @staticmethod
+    def _is_bottom(kast: KInner) -> bool:
+        flat = flatten_label('#And', kast)
+        if len(flat) == 1:
+            return is_bottom(single(flat))
+        return all(CTerm._is_bottom(term) for term in flat)
+
     @staticmethod
     def _constraint_sort_key(term: KInner) -> tuple[int, str]:
         term_str = str(term)
@@ -104,6 +142,9 @@ def cells(self) -> Subst:
     def cell(self, cell: str) -> KInner:
         return self.cells[cell]
 
+    def try_cell(self, cell: str) -> KInner | None:
+        return self.cells.get(cell)
+
     def match(self, cterm: CTerm) -> Subst | None:
         csubst = self.match_with_constraint(cterm)
 
@@ -138,6 +179,59 @@ def _ml_impl(antecedents: Iterable[KInner], consequents: Iterable[KInner]) -> KI
     def add_constraint(self, new_constraint: KInner) -> CTerm:
         return CTerm(self.config, [new_constraint] + list(self.constraints))
 
+    def anti_unify(
+        self, other: CTerm, keep_values: bool = False, kdef: KDefinition | None = None
+    ) -> tuple[CTerm, CSubst, CSubst]:
+        def disjunction_from_substs(subst1: Subst, subst2: Subst) -> KInner:
+            if KToken('true', 'Bool') in [subst1.pred, subst2.pred]:
+                return mlTop()
+            return mlEqualsTrue(orBool([subst1.pred, subst2.pred]))
+
+        new_config, self_subst, other_subst = anti_unify(self.config, other.config, kdef=kdef)
+        common_constraints = [constraint for constraint in self.constraints if constraint in other.constraints]
+
+        new_cterm = CTerm(
+            config=new_config, constraints=([disjunction_from_substs(self_subst, other_subst)] if keep_values else [])
+        )
+
+        new_constraints = []
+        fvs = free_vars(new_cterm.kast)
+        len_fvs = 0
+        while len_fvs < len(fvs):
+            len_fvs = len(fvs)
+            for constraint in common_constraints:
+                if constraint not in new_constraints:
+                    constraint_fvs = free_vars(constraint)
+                    if any(fv in fvs for fv in constraint_fvs):
+                        new_constraints.append(constraint)
+                        fvs.extend(constraint_fvs)
+
+        for constraint in new_constraints:
+            new_cterm = new_cterm.add_constraint(constraint)
+        self_csubst = new_cterm.match_with_constraint(self)
+        other_csubst = new_cterm.match_with_constraint(other)
+        if self_csubst is None or other_csubst is None:
+            raise ValueError(
+                f'Anti-unification failed to produce a more general state: {(new_cterm, (self, self_csubst), (other, other_csubst))}'
+            )
+        return (new_cterm, self_csubst, other_csubst)
+
+
+def anti_unify(state1: KInner, state2: KInner, kdef: KDefinition | None = None) -> tuple[KInner, Subst, Subst]:
+    def _rewrites_to_abstractions(_kast: KInner) -> KInner:
+        if type(_kast) is KRewrite:
+            sort = kdef.sort(_kast) if kdef else None
+            return abstract_term_safely(_kast, sort=sort)
+        return _kast
+
+    minimized_rewrite = push_down_rewrites(KRewrite(state1, state2))
+    abstracted_state = bottom_up(_rewrites_to_abstractions, minimized_rewrite)
+    subst1 = abstracted_state.match(state1)
+    subst2 = abstracted_state.match(state2)
+    if subst1 is None or subst2 is None:
+        raise ValueError('Anti-unification failed to produce a more general state!')
+    return (abstracted_state, subst1, subst2)
+
 
 @dataclass(frozen=True, order=True)
 class CSubst: