Merge master into branch

Author: nwatson22

deps/k_release

@@ -1 +1 @@
-6.0.69
+6.0.87

package/version

@@ -1 +1 @@
-0.1.432
+0.1.448

pyproject.toml

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

src/pyk/__init__.py

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

src/pyk/cli/args.py

@@ -101,6 +101,12 @@ def smt_args(self) -> ArgumentParser:
             type=int,
             help='Number of times to retry SMT queries with scaling timeouts.',
         )
+        args.add_argument(
+            '--smt-tactic',
+            dest='smt_tactic',
+            type=str,
+            help='Z3 tactic to use when checking satisfiability. Example: (check-sat-using smt)',
+        )
         return args
 
     @cached_property

src/pyk/cterm.py

@@ -23,7 +23,7 @@
 )
 from .kast.outer import KClaim, KRule
 from .prelude.k import GENERATED_TOP_CELL
-from .prelude.kbool import orBool
+from .prelude.kbool import andBool, orBool
 from .prelude.ml import is_bottom, is_top, mlAnd, mlBottom, mlEqualsTrue, mlImplies, mlTop
 from .utils import single, unique
 
@@ -118,7 +118,11 @@ 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)
+        return any(CTerm._is_bottom(term) for term in flat)
+
+    @property
+    def is_bottom(self) -> bool:
+        return CTerm._is_bottom(self.config) or any(CTerm._is_bottom(cterm) for cterm in self.constraints)
 
     @staticmethod
     def _constraint_sort_key(term: KInner) -> tuple[int, str]:
@@ -190,17 +194,21 @@ def add_constraint(self, new_constraint: KInner) -> CTerm:
     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 [])
-        )
+        self_unique_constraints = [
+            ml_pred_to_bool(constraint) for constraint in self.constraints if constraint not in other.constraints
+        ]
+        other_unique_constraints = [
+            ml_pred_to_bool(constraint) for constraint in other.constraints if constraint not in self.constraints
+        ]
+
+        new_cterm = CTerm(config=new_config, constraints=())
+        if keep_values:
+            disjunct_lhs = andBool([self_subst.pred] + self_unique_constraints)
+            disjunct_rhs = andBool([other_subst.pred] + other_unique_constraints)
+            if KToken('true', 'Bool') not in [disjunct_lhs, disjunct_rhs]:
+                new_cterm = new_cterm.add_constraint(mlEqualsTrue(orBool([disjunct_lhs, disjunct_rhs])))
 
         new_constraints = []
         fvs = free_vars(new_cterm.kast)

src/pyk/kast/inner.py

@@ -577,10 +577,10 @@ def __init__(self, *args: Any, **kwargs: Any):
         else:
             items = args
 
-        _items = []
+        _items: list[KInner] = []
         for i in items:
             if type(i) is KSequence:
-                _items.extend(list(i.items))
+                _items.extend(i.items)
             else:
                 _items.append(i)
         items = tuple(_items)

src/pyk/kast/outer.py

@@ -1154,14 +1154,21 @@ def greatest_common_subsort(self, sort1: KSort, sort2: KSort) -> KSort | None:
         return None
 
     # Sorts like Int cannot be injected directly into sort K so they are embedded in a KSequence.
-    def add_ksequence_under_kequal(self, kast: KInner) -> KInner:
-        def _add_ksequence_under_kequal(kast: KInner) -> KInner:
-            if type(kast) is KApply and kast.label.name == '_==K_':
-                return KApply('_==K_', [KSequence(arg) for arg in kast.args])
-            else:
+    def add_ksequence_under_k_productions(self, kast: KInner) -> KInner:
+        def _add_ksequence_under_k_productions(kast: KInner) -> KInner:
+            if type(kast) is not KApply:
                 return kast
 
-        return top_down(_add_ksequence_under_kequal, kast)
+            prod = self.production_for_klabel(kast.label)
+            return KApply(
+                kast.label,
+                [
+                    KSequence(arg) if sort.name == 'K' and not self.sort(arg) == KSort('K') else arg
+                    for arg, sort in zip(kast.args, prod.argument_sorts, strict=True)
+                ],
+            )
+
+        return top_down(_add_ksequence_under_k_productions, kast)
 
     def sort_vars(self, kast: KInner, sort: KSort | None = None) -> KInner:
         if type(kast) is KVariable and kast.sort is None and sort is not None:

src/pyk/kbuild/__init__.py

@@ -1,3 +1,2 @@
 from .kbuild import KBuild
-from .package import Package
 from .project import Project

src/pyk/kbuild/__main__.py

@@ -1,23 +1,19 @@
-import shutil
 import sys
 from argparse import ArgumentParser
 from pathlib import Path
 from typing import Any
 
 from ..cli.utils import check_dir_path, dir_path
-from .config import KBUILD_DIR, PROJECT_FILE_NAME
+from .config import DIST_DIR_NAME, PROJECT_FILE_NAME
 from .kbuild import KBuild
-from .package import Package
+from .project import Project
 from .utils import find_file_upwards
 
 
 def main() -> None:
     args = vars(_argument_parser().parse_args())
     command = args['command']
 
-    if command == 'clean':
-        return do_clean(**args)
-
     if command == 'kompile':
         return do_kompile(**args)
 
@@ -35,38 +31,52 @@ def _argument_parser() -> ArgumentParser:
 
     command_parser = parser.add_subparsers(dest='command', metavar='COMMAND', required=True)
 
-    command_parser.add_parser('clean', help='clean build cache')
-
     kompile_parser = command_parser.add_parser('kompile', help='kompile target')
     kompile_parser.add_argument('target_name', metavar='TARGET', help='target to build')
+    kompile_parser.add_argument(
+        '-o',
+        '--output',
+        dest='output_dir',
+        metavar='OUTPUT',
+        type=Path,
+        help='output directory',
+    )
 
     which_parser = command_parser.add_parser('which', help='print definition directory for target')
     which_parser.add_argument('target_name', metavar='TARGET', help='target to print definition directory for')
+    which_parser.add_argument(
+        '-o',
+        '--output',
+        dest='output_dir',
+        metavar='OUTPUT',
+        type=Path,
+        help='output directory',
+    )
 
     return parser
 
 
-def _package(start_dir: Path) -> Package:
-    project_file = find_file_upwards(PROJECT_FILE_NAME, start_dir)
-    return Package.create(project_file)
-
+def _project_file(start_dir: Path) -> Path:
+    return find_file_upwards(PROJECT_FILE_NAME, start_dir)
 
-def do_clean(**kwargs: Any) -> None:
-    shutil.rmtree(KBUILD_DIR, ignore_errors=True)
 
+def do_kompile(start_dir: Path, target_name: str, output_dir: Path | None, **kwargs: Any) -> None:
+    project_file = _project_file(start_dir)
+    project = Project.load(project_file)
+    kdist_dir = output_dir or project_file.parent / DIST_DIR_NAME
+    kbuild = KBuild(kdist_dir)
 
-def do_kompile(start_dir: Path, target_name: str, **kwargs: Any) -> None:
-    package = _package(start_dir)
-    kbuild = KBuild()
-    definition_dir = kbuild.kompile(package, target_name)
+    definition_dir = kbuild.kompile(project, target_name)
     print(definition_dir)
 
 
-def do_which(start_dir: Path, target_name: str, **kwargs: Any) -> None:
-    package = _package(start_dir)
-    kbuild = KBuild()
-    definition_dir = kbuild.definition_dir(package, target_name)
+def do_which(start_dir: Path, target_name: str, output_dir: Path | None, **kwargs: Any) -> None:
+    project_file = _project_file(start_dir)
+    project = Project.load(project_file)
+    kdist_dir = output_dir or project_file.parent / DIST_DIR_NAME
+    kbuild = KBuild(kdist_dir)
 
+    definition_dir = kbuild.definition_dir(project, target_name)
     try:
         check_dir_path(definition_dir)
     except ValueError as e: