From 28157b53dac3a613c8681df13907b5cbd9458d9d Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Thu, 10 Aug 2023 15:32:55 -0500 Subject: [PATCH 01/10] Add least_common_supersort(), use in sort(), use sort() in anti_unify, move anti_unify to KDefinition --- src/pyk/kast/manip.py | 54 +------------- src/pyk/kast/outer.py | 77 ++++++++++++++++++-- src/tests/integration/kcfg/test_imp.py | 71 +++++++++++++++++- src/tests/unit/kast/test_manip.py | 99 +------------------------- 4 files changed, 146 insertions(+), 155 deletions(-) diff --git a/src/pyk/kast/manip.py b/src/pyk/kast/manip.py index e5fc13446..126cc201c 100644 --- a/src/pyk/kast/manip.py +++ b/src/pyk/kast/manip.py @@ -6,7 +6,7 @@ from ..prelude.k import DOTS, GENERATED_TOP_CELL from ..prelude.kbool import FALSE, TRUE, andBool, impliesBool, notBool, orBool -from ..prelude.ml import mlAnd, mlEqualsTrue, mlImplies, mlOr, mlTop +from ..prelude.ml import mlAnd, mlEqualsTrue, mlOr from ..utils import find_common_items, hash_str from .inner import KApply, KRewrite, KSequence, KToken, KVariable, Subst, bottom_up, top_down, var_occurrences from .kast import EMPTY_ATT, KAtt, WithKAtt @@ -582,58 +582,6 @@ def _abstract(k: KInner) -> KVariable: return new_var -def anti_unify(state1: KInner, state2: KInner) -> tuple[KInner, Subst, Subst]: - def _rewrites_to_abstractions(_kast: KInner) -> KInner: - if type(_kast) is KRewrite: - return abstract_term_safely(_kast) - 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) - - -def anti_unify_with_constraints( - constrained_term_1: KInner, - constrained_term_2: KInner, - implications: bool = False, - constraint_disjunct: bool = False, - abstracted_disjunct: bool = False, -) -> KInner: - 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])) - - state1, constraint1 = split_config_and_constraints(constrained_term_1) - state2, constraint2 = split_config_and_constraints(constrained_term_2) - constraints1 = flatten_label('#And', constraint1) - constraints2 = flatten_label('#And', constraint2) - state, subst1, subst2 = anti_unify(state1, state2) - - constraints = [c for c in constraints1 if c in constraints2] - constraint1 = mlAnd([c for c in constraints1 if c not in constraints]) - constraint2 = mlAnd([c for c in constraints2 if c not in constraints]) - implication1 = mlImplies(constraint1, subst1.ml_pred) - implication2 = mlImplies(constraint2, subst2.ml_pred) - - if abstracted_disjunct: - constraints.append(disjunction_from_substs(subst1, subst2)) - - if implications: - constraints.append(implication1) - constraints.append(implication2) - - if constraint_disjunct: - constraints.append(mlOr([constraint1, constraint2])) - - return mlAnd([state] + constraints) - - def apply_existential_substitutions(constrained_term: KInner) -> KInner: state, constraint = split_config_and_constraints(constrained_term) constraints = flatten_label('#And', constraint) diff --git a/src/pyk/kast/outer.py b/src/pyk/kast/outer.py index 1f04a7b68..a3144ed00 100644 --- a/src/pyk/kast/outer.py +++ b/src/pyk/kast/outer.py @@ -10,8 +10,8 @@ from functools import cached_property from typing import TYPE_CHECKING, final -from ..prelude.kbool import TRUE -from ..prelude.ml import ML_QUANTIFIERS +from ..prelude.kbool import TRUE, orBool +from ..prelude.ml import ML_QUANTIFIERS, mlAnd, mlEqualsTrue, mlImplies, mlOr, mlTop from ..utils import filter_none, single, unique from .inner import ( KApply, @@ -35,6 +35,8 @@ from os import PathLike from typing import Any, Final, TypeVar + from ..cterm import CTerm + RL = TypeVar('RL', bound='KRuleLike') _LOGGER: Final = logging.getLogger(__name__) @@ -1057,6 +1059,61 @@ def production_for_klabel(self, klabel: KLabel) -> KProduction: raise ValueError(f'Expected a single production for label {klabel}, not: {prods}') from err return self._production_for_klabel[klabel] + def anti_unify(self, state1: KInner, state2: KInner) -> tuple[KInner, Subst, Subst]: + from .manip import abstract_term_safely, push_down_rewrites + + def _rewrites_to_abstractions(_kast: KInner) -> KInner: + if type(_kast) is KRewrite: + return abstract_term_safely(_kast, sort=self.sort(_kast)) + 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) + + def anti_unify_with_constraints( + self, + constrained_term_1: CTerm, + constrained_term_2: CTerm, + implications: bool = False, + constraint_disjunct: bool = False, + abstracted_disjunct: bool = False, + ) -> KInner: + from .manip import flatten_label, split_config_and_constraints + + 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])) + + state1, constraint1 = split_config_and_constraints(constrained_term_1.kast) + state2, constraint2 = split_config_and_constraints(constrained_term_2.kast) + constraints1 = flatten_label('#And', constraint1) + constraints2 = flatten_label('#And', constraint2) + state, subst1, subst2 = self.anti_unify(state1, state2) + + constraints = [c for c in constraints1 if c in constraints2] + constraint1 = mlAnd([c for c in constraints1 if c not in constraints]) + constraint2 = mlAnd([c for c in constraints2 if c not in constraints]) + implication1 = mlImplies(constraint1, subst1.ml_pred) + implication2 = mlImplies(constraint2, subst2.ml_pred) + + if abstracted_disjunct: + constraints.append(disjunction_from_substs(subst1, subst2)) + + if implications: + constraints.append(implication1) + constraints.append(implication2) + + if constraint_disjunct: + constraints.append(mlOr([constraint1, constraint2])) + + return mlAnd([state] + constraints) + def production_for_cell_sort(self, sort: KSort) -> KProduction: # Typical cell production has 3 productions: # syntax KCell ::= "project:KCell" "(" K ")" [function, projection] @@ -1101,8 +1158,11 @@ def sort(self, kast: KInner) -> KSort | None: case KToken(_, sort) | KVariable(_, sort): return sort case KRewrite(lhs, rhs): - sort = self.sort(lhs) - return sort if sort == self.sort(rhs) else None + lhs_sort = self.sort(lhs) + rhs_sort = self.sort(rhs) + if lhs_sort and rhs_sort: + return self.least_common_supersort(lhs_sort, rhs_sort) + return None case KSequence(_): return KSort('K') case KApply(label, _): @@ -1128,6 +1188,15 @@ def sort_strict(self, kast: KInner) -> KSort: raise ValueError(f'Could not determine sort of term: {kast}') return sort + def least_common_supersort(self, sort1: KSort, sort2: KSort) -> KSort | None: + if sort1 == sort2: + return sort1 + if sort1 in self.subsorts(sort2): + return sort2 + if sort2 in self.subsorts(sort1): + return sort1 + return None + def greatest_common_subsort(self, sort1: KSort, sort2: KSort) -> KSort | None: if sort1 == sort2: return sort1 diff --git a/src/tests/integration/kcfg/test_imp.py b/src/tests/integration/kcfg/test_imp.py index 06034e208..e9638bea1 100644 --- a/src/tests/integration/kcfg/test_imp.py +++ b/src/tests/integration/kcfg/test_imp.py @@ -8,10 +8,10 @@ from pyk.cterm import CSubst, CTerm from pyk.kast.inner import KApply, KSequence, KSort, KToken, KVariable, Subst -from pyk.kast.manip import minimize_term +from pyk.kast.manip import get_cell, minimize_term from pyk.kcfg.semantics import KCFGSemantics from pyk.kcfg.show import KCFGShow -from pyk.prelude.kbool import BOOL, notBool +from pyk.prelude.kbool import BOOL, notBool, orBool from pyk.prelude.kint import intToken from pyk.prelude.ml import mlAnd, mlBottom, mlEqualsFalse, mlEqualsTrue, mlTop from pyk.proof import APRBMCProof, APRBMCProver, APRProof, APRProver, ProofStatus @@ -1147,3 +1147,70 @@ def test_fail_fast( assert len(proof.pending) == 1 assert len(proof.terminal) == 1 assert len(proof.failing) == 1 + + def test_anti_unify_with_constraints( + self, + kprint: KPrint, + ) -> None: + cterm1 = self.config( + kprint=kprint, + k='int $n ; { }', + state='$s |-> 0', + constraint=KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')]), + ) + cterm2 = self.config( + kprint=kprint, + k='int $n ; { }', + state='$s |-> 1', + constraint=KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')]), + ) + + anti_unifier = kprint.definition.anti_unify_with_constraints(cterm1, cterm2, abstracted_disjunct=True) + + k_cell = get_cell(anti_unifier, 'STATE_CELL') + assert type(k_cell) is KApply + assert k_cell.label.name == '_|->_' + assert type(k_cell.args[1]) is KVariable + abstracted_var: KVariable = k_cell.args[1] + + expected_anti_unifier = self.config( + kprint=kprint, + k='int $n ; { }', + state=f'$s |-> {abstracted_var.name}:Int', + constraint=mlAnd( + [ + KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')]), + mlEqualsTrue( + orBool( + [ + KApply('_==K_', [KVariable(name=abstracted_var.name), intToken(0)]), + KApply('_==K_', [KVariable(name=abstracted_var.name), intToken(1)]), + ] + ) + ), + ] + ), + ).kast + + assert anti_unifier == expected_anti_unifier + + def test_anti_unify_with_constraints_subst_true( + self, + kprint: KPrint, + ) -> None: + cterm1 = self.config( + kprint=kprint, + k='int $n ; { }', + state='$s |-> 0', + constraint=KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')]), + ) + cterm2 = self.config( + kprint=kprint, + k='int $n ; { }', + state='$s |-> 0', + constraint=KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')]), + ) + + anti_unifier = kprint.definition.anti_unify_with_constraints(cterm1, cterm2, abstracted_disjunct=True) + + assert anti_unifier == cterm1.kast diff --git a/src/tests/unit/kast/test_manip.py b/src/tests/unit/kast/test_manip.py index 175c9370a..d898d19ed 100644 --- a/src/tests/unit/kast/test_manip.py +++ b/src/tests/unit/kast/test_manip.py @@ -5,9 +5,8 @@ import pytest -from pyk.kast.inner import KApply, KLabel, KRewrite, KSequence, KSort, KToken, KVariable, Subst +from pyk.kast.inner import KApply, KLabel, KRewrite, KSequence, KSort, KVariable, Subst from pyk.kast.manip import ( - anti_unify_with_constraints, bool_to_ml_pred, collapse_dots, minimize_term, @@ -16,13 +15,12 @@ remove_generated_cells, rename_generated_vars, simplify_bool, - split_config_and_constraints, split_config_from, ) from pyk.prelude.k import DOTS, GENERATED_TOP_CELL -from pyk.prelude.kbool import BOOL, FALSE, TRUE, andBool, notBool, orBool +from pyk.prelude.kbool import BOOL, FALSE, TRUE, andBool, notBool from pyk.prelude.kint import INT, intToken -from pyk.prelude.ml import mlAnd, mlEqualsTrue, mlTop +from pyk.prelude.ml import mlEqualsTrue, mlTop from ..utils import a, b, c, f, k, x @@ -341,94 +339,3 @@ def test_split_config_from(term: KInner, expected_config: KInner, expected_subst # Then assert actual_config == expected_config assert actual_subst == expected_subst - - -def test_anti_unify_with_constraints() -> None: - cterm1 = mlAnd( - [ - KApply( - '', - [ - KApply('', KToken('1', 'Int')), - KApply('', KVariable('GENERATEDCOUNTER_CELL')), - ], - ), - mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])), - ] - ) - cterm2 = mlAnd( - [ - KApply( - '', - [ - KApply('', KToken('2', 'Int')), - KApply('', KVariable('GENERATEDCOUNTER_CELL')), - ], - ), - mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])), - ] - ) - - anti_unifier = anti_unify_with_constraints(cterm1, cterm2, abstracted_disjunct=True) - - config, constraints = split_config_and_constraints(anti_unifier) - - assert type(config) is KApply - assert type(config.args[0]) is KApply - assert type(config.args[0].args[0]) is KVariable - var_name = config.args[0].args[0].name - - expected = mlAnd( - [ - mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])), - mlEqualsTrue( - orBool( - [ - KApply('_==K_', [KVariable(var_name), KToken('1', 'Int')]), - KApply('_==K_', [KVariable(var_name), KToken('2', 'Int')]), - ] - ) - ), - ] - ) - - assert expected == constraints - - -def test_anti_unify_with_constraints_subst_true() -> None: - cterm1 = mlAnd( - [ - KApply( - '', - [ - KApply('', KToken('1', 'Int')), - KApply('', KVariable('GENERATEDCOUNTER_CELL')), - ], - ), - mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])), - ] - ) - cterm2 = mlAnd( - [ - KApply( - '', - [ - KApply('', KToken('1', 'Int')), - KApply('', KVariable('GENERATEDCOUNTER_CELL')), - ], - ), - mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])), - ] - ) - - anti_unifier = anti_unify_with_constraints(cterm1, cterm2, abstracted_disjunct=True) - - config, constraints = split_config_and_constraints(anti_unifier) - - expected = mlAnd( - [ - mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])), - ] - ) - - assert expected == constraints From a8222ac6a888ec6a06f71a771bcf6b3f7c8e738e Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 10 Aug 2023 20:40:42 +0000 Subject: [PATCH 02/10] Set Version: 0.1.412 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 759f8fc7d..d10f1fedc 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.411 +0.1.412 diff --git a/pyproject.toml b/pyproject.toml index 9b8fc36a8..564f79bc2 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.411" +version = "0.1.412" description = "" authors = [ "Runtime Verification, Inc. ", From b2ad5574483f7caa409bfd08bf2dda5f419aaed5 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Fri, 11 Aug 2023 12:40:24 -0500 Subject: [PATCH 03/10] Move anti-unification into cterm.py and make anti-unification of cterms a method of CTerm, improve test --- src/pyk/cterm.py | 35 ++++++++++++++- src/pyk/kast/outer.py | 61 +------------------------- src/tests/integration/kcfg/test_imp.py | 18 ++++---- 3 files changed, 44 insertions(+), 70 deletions(-) diff --git a/src/pyk/cterm.py b/src/pyk/cterm.py index b51f18384..f112994b4 100644 --- a/src/pyk/cterm.py +++ b/src/pyk/cterm.py @@ -5,8 +5,9 @@ from itertools import chain from typing import TYPE_CHECKING -from .kast.inner import KApply, KAtt, KInner, KRewrite, KVariable, Subst +from .kast.inner import KApply, KAtt, KInner, KRewrite, KToken, KVariable, Subst, bottom_up from .kast.manip import ( + abstract_term_safely, apply_existential_substitutions, count_vars, flatten_label, @@ -21,13 +22,16 @@ ) from .kast.outer import KClaim, KRule from .prelude.k import GENERATED_TOP_CELL -from .prelude.ml import is_top, mlAnd, mlImplies, mlTop +from .prelude.kbool import orBool +from .prelude.ml import is_top, mlAnd, mlEqualsTrue, mlImplies, mlTop from .utils import 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: @@ -137,6 +141,33 @@ 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_term: CTerm, kdef: KDefinition | None = None) -> KInner: + 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_term.config, kdef) + constraints = [c for c in self.constraints if c in other_term.constraints] + constraints.append(disjunction_from_substs(self_subst, other_subst)) + return mlAnd([new_config] + constraints) + + +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: diff --git a/src/pyk/kast/outer.py b/src/pyk/kast/outer.py index a3144ed00..f2725c3b3 100644 --- a/src/pyk/kast/outer.py +++ b/src/pyk/kast/outer.py @@ -10,8 +10,8 @@ from functools import cached_property from typing import TYPE_CHECKING, final -from ..prelude.kbool import TRUE, orBool -from ..prelude.ml import ML_QUANTIFIERS, mlAnd, mlEqualsTrue, mlImplies, mlOr, mlTop +from ..prelude.kbool import TRUE +from ..prelude.ml import ML_QUANTIFIERS from ..utils import filter_none, single, unique from .inner import ( KApply, @@ -35,8 +35,6 @@ from os import PathLike from typing import Any, Final, TypeVar - from ..cterm import CTerm - RL = TypeVar('RL', bound='KRuleLike') _LOGGER: Final = logging.getLogger(__name__) @@ -1059,61 +1057,6 @@ def production_for_klabel(self, klabel: KLabel) -> KProduction: raise ValueError(f'Expected a single production for label {klabel}, not: {prods}') from err return self._production_for_klabel[klabel] - def anti_unify(self, state1: KInner, state2: KInner) -> tuple[KInner, Subst, Subst]: - from .manip import abstract_term_safely, push_down_rewrites - - def _rewrites_to_abstractions(_kast: KInner) -> KInner: - if type(_kast) is KRewrite: - return abstract_term_safely(_kast, sort=self.sort(_kast)) - 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) - - def anti_unify_with_constraints( - self, - constrained_term_1: CTerm, - constrained_term_2: CTerm, - implications: bool = False, - constraint_disjunct: bool = False, - abstracted_disjunct: bool = False, - ) -> KInner: - from .manip import flatten_label, split_config_and_constraints - - 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])) - - state1, constraint1 = split_config_and_constraints(constrained_term_1.kast) - state2, constraint2 = split_config_and_constraints(constrained_term_2.kast) - constraints1 = flatten_label('#And', constraint1) - constraints2 = flatten_label('#And', constraint2) - state, subst1, subst2 = self.anti_unify(state1, state2) - - constraints = [c for c in constraints1 if c in constraints2] - constraint1 = mlAnd([c for c in constraints1 if c not in constraints]) - constraint2 = mlAnd([c for c in constraints2 if c not in constraints]) - implication1 = mlImplies(constraint1, subst1.ml_pred) - implication2 = mlImplies(constraint2, subst2.ml_pred) - - if abstracted_disjunct: - constraints.append(disjunction_from_substs(subst1, subst2)) - - if implications: - constraints.append(implication1) - constraints.append(implication2) - - if constraint_disjunct: - constraints.append(mlOr([constraint1, constraint2])) - - return mlAnd([state] + constraints) - def production_for_cell_sort(self, sort: KSort) -> KProduction: # Typical cell production has 3 productions: # syntax KCell ::= "project:KCell" "(" K ")" [function, projection] diff --git a/src/tests/integration/kcfg/test_imp.py b/src/tests/integration/kcfg/test_imp.py index e9638bea1..bbdb7a631 100644 --- a/src/tests/integration/kcfg/test_imp.py +++ b/src/tests/integration/kcfg/test_imp.py @@ -1148,7 +1148,7 @@ def test_fail_fast( assert len(proof.terminal) == 1 assert len(proof.failing) == 1 - def test_anti_unify_with_constraints( + def test_anti_unify( self, kprint: KPrint, ) -> None: @@ -1156,16 +1156,16 @@ def test_anti_unify_with_constraints( kprint=kprint, k='int $n ; { }', state='$s |-> 0', - constraint=KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')]), + constraint=mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])), ) cterm2 = self.config( kprint=kprint, k='int $n ; { }', state='$s |-> 1', - constraint=KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')]), + constraint=mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])), ) - anti_unifier = kprint.definition.anti_unify_with_constraints(cterm1, cterm2, abstracted_disjunct=True) + anti_unifier = cterm1.anti_unify(cterm2, kprint.definition) k_cell = get_cell(anti_unifier, 'STATE_CELL') assert type(k_cell) is KApply @@ -1179,7 +1179,7 @@ def test_anti_unify_with_constraints( state=f'$s |-> {abstracted_var.name}:Int', constraint=mlAnd( [ - KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')]), + mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])), mlEqualsTrue( orBool( [ @@ -1194,7 +1194,7 @@ def test_anti_unify_with_constraints( assert anti_unifier == expected_anti_unifier - def test_anti_unify_with_constraints_subst_true( + def test_anti_unify_subst_true( self, kprint: KPrint, ) -> None: @@ -1202,15 +1202,15 @@ def test_anti_unify_with_constraints_subst_true( kprint=kprint, k='int $n ; { }', state='$s |-> 0', - constraint=KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')]), + constraint=mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])), ) cterm2 = self.config( kprint=kprint, k='int $n ; { }', state='$s |-> 0', - constraint=KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')]), + constraint=mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])), ) - anti_unifier = kprint.definition.anti_unify_with_constraints(cterm1, cterm2, abstracted_disjunct=True) + anti_unifier = cterm1.anti_unify(cterm2, kprint.definition) assert anti_unifier == cterm1.kast From 3fcf774a8334b04c8d1d214e03cedbdc87dcffa7 Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 14 Aug 2023 18:40:50 +0000 Subject: [PATCH 04/10] Set Version: 0.1.414 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index f94afd37e..0cb3afc5f 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.413 +0.1.414 diff --git a/pyproject.toml b/pyproject.toml index 6c35ce325..9c1f5d531 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.413" +version = "0.1.414" description = "" authors = [ "Runtime Verification, Inc. ", From 34f35cfe8292954ca431b4ae3f04f2ac364b2586 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Mon, 14 Aug 2023 16:36:26 -0500 Subject: [PATCH 05/10] Incorporarte code from #544 which removes constraints for variables that no longer appear after abstraction during merge --- src/pyk/cterm.py | 35 +++++++-- src/tests/integration/kcfg/test_imp.py | 101 ++++++++++++++++++++----- 2 files changed, 112 insertions(+), 24 deletions(-) diff --git a/src/pyk/cterm.py b/src/pyk/cterm.py index f02e9795e..26c34c1c3 100644 --- a/src/pyk/cterm.py +++ b/src/pyk/cterm.py @@ -142,16 +142,41 @@ 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_term: CTerm, kdef: KDefinition | None = None) -> KInner: + 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_term.config, kdef) - constraints = [c for c in self.constraints if c in other_term.constraints] - constraints.append(disjunction_from_substs(self_subst, other_subst)) - return mlAnd([new_config] + constraints) + 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] + + if keep_values: + new_constraints = common_constraints + new_constraints.append(disjunction_from_substs(self_subst, other_subst)) + else: + new_constraints = [] + fvs = free_vars(new_config) + 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) + + new_cterm = CTerm(config=new_config, constraints=new_constraints) + 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]: diff --git a/src/tests/integration/kcfg/test_imp.py b/src/tests/integration/kcfg/test_imp.py index bbdb7a631..79093239c 100644 --- a/src/tests/integration/kcfg/test_imp.py +++ b/src/tests/integration/kcfg/test_imp.py @@ -1148,26 +1148,86 @@ def test_fail_fast( assert len(proof.terminal) == 1 assert len(proof.failing) == 1 - def test_anti_unify( + def test_anti_unify_forget_values( self, + kcfg_explore: KCFGExplore, + kprint: KPrint, + ) -> None: + cterm1 = self.config( + kprint=kprint, + k='int $n ; { }', + state='N |-> X:Int', + constraint=mlAnd( + [ + mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])), + ] + ), + ) + cterm2 = self.config( + kprint=kprint, + k='int $n ; { }', + state='N |-> Y:Int', + constraint=mlAnd( + [ + mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])), + ] + ), + ) + + anti_unifier, subst1, subst2 = cterm1.anti_unify(cterm2, keep_values=False, kdef=kprint.definition) + + k_cell = get_cell(anti_unifier.kast, 'STATE_CELL') + assert type(k_cell) is KApply + assert k_cell.label.name == '_|->_' + assert type(k_cell.args[1]) is KVariable + abstracted_var: KVariable = k_cell.args[1] + + expected_anti_unifier = self.config( + kprint=kprint, + k='int $n ; { }', + state=f'N |-> {abstracted_var.name}:Int', + constraint=mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])), + ) + + assert anti_unifier.kast == expected_anti_unifier.kast + + def test_anti_unify_keep_values( + self, + kcfg_explore: KCFGExplore, kprint: KPrint, ) -> None: cterm1 = self.config( kprint=kprint, k='int $n ; { }', - state='$s |-> 0', - constraint=mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])), + state='N |-> X:Int', + constraint=mlAnd( + [ + mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])), + ] + ), ) cterm2 = self.config( kprint=kprint, k='int $n ; { }', - state='$s |-> 1', - constraint=mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])), + state='N |-> Y:Int', + constraint=mlAnd( + [ + mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])), + ] + ), ) - anti_unifier = cterm1.anti_unify(cterm2, kprint.definition) + anti_unifier, subst1, subst2 = cterm1.anti_unify(cterm2, keep_values=True, kdef=kprint.definition) - k_cell = get_cell(anti_unifier, 'STATE_CELL') + k_cell = get_cell(anti_unifier.kast, 'STATE_CELL') assert type(k_cell) is KApply assert k_cell.label.name == '_|->_' assert type(k_cell.args[1]) is KVariable @@ -1176,41 +1236,44 @@ def test_anti_unify( expected_anti_unifier = self.config( kprint=kprint, k='int $n ; { }', - state=f'$s |-> {abstracted_var.name}:Int', + state=f'N |-> {abstracted_var.name}:Int', constraint=mlAnd( [ - mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])), + mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])), mlEqualsTrue( orBool( [ - KApply('_==K_', [KVariable(name=abstracted_var.name), intToken(0)]), - KApply('_==K_', [KVariable(name=abstracted_var.name), intToken(1)]), + KApply('_==K_', [KVariable(name=abstracted_var.name), KVariable('X', 'Int')]), + KApply('_==K_', [KVariable(name=abstracted_var.name), KVariable('Y', 'Int')]), ] ) ), ] ), - ).kast + ) - assert anti_unifier == expected_anti_unifier + assert anti_unifier.kast == expected_anti_unifier.kast def test_anti_unify_subst_true( self, + kcfg_explore: KCFGExplore, kprint: KPrint, ) -> None: cterm1 = self.config( kprint=kprint, k='int $n ; { }', - state='$s |-> 0', - constraint=mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])), + state='N |-> 0', + constraint=mlEqualsTrue(KApply('_==K_', [KVariable('N', 'Int'), KToken('1', 'Int')])), ) cterm2 = self.config( kprint=kprint, k='int $n ; { }', - state='$s |-> 0', - constraint=mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')])), + state='N |-> 0', + constraint=mlEqualsTrue(KApply('_==K_', [KVariable('N', 'Int'), KToken('1', 'Int')])), ) - anti_unifier = cterm1.anti_unify(cterm2, kprint.definition) + anti_unifier, _, _ = cterm1.anti_unify(cterm2, keep_values=True, kdef=kprint.definition) - assert anti_unifier == cterm1.kast + assert anti_unifier.kast == cterm1.kast From 410d3348d99de107feb695b6dae4536e99672e24 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Mon, 14 Aug 2023 16:48:40 -0500 Subject: [PATCH 06/10] Simplify code, allow pruning of constraints referring to absent variables while still keeping ones that will appear in the disjunction --- src/pyk/cterm.py | 35 +++++++++++++------------- src/tests/integration/kcfg/test_imp.py | 4 +++ 2 files changed, 21 insertions(+), 18 deletions(-) diff --git a/src/pyk/cterm.py b/src/pyk/cterm.py index 26c34c1c3..59c2f971a 100644 --- a/src/pyk/cterm.py +++ b/src/pyk/cterm.py @@ -60,7 +60,7 @@ def from_dict(dct: dict[str, Any]) -> CTerm: @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.label.name}') @staticmethod def _normalize_constraints(constraints: Iterable[KInner]) -> tuple[KInner, ...]: @@ -153,23 +153,22 @@ def disjunction_from_substs(subst1: Subst, subst2: Subst) -> KInner: 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] - if keep_values: - new_constraints = common_constraints - new_constraints.append(disjunction_from_substs(self_subst, other_subst)) - else: - new_constraints = [] - fvs = free_vars(new_config) - 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) - - new_cterm = CTerm(config=new_config, constraints=new_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: diff --git a/src/tests/integration/kcfg/test_imp.py b/src/tests/integration/kcfg/test_imp.py index 79093239c..02eded97d 100644 --- a/src/tests/integration/kcfg/test_imp.py +++ b/src/tests/integration/kcfg/test_imp.py @@ -1159,6 +1159,7 @@ def test_anti_unify_forget_values( state='N |-> X:Int', constraint=mlAnd( [ + mlEqualsTrue(KApply('_>Int_', [KVariable('K', 'Int'), KToken('1', 'Int')])), mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])), mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])), mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])), @@ -1171,6 +1172,7 @@ def test_anti_unify_forget_values( state='N |-> Y:Int', constraint=mlAnd( [ + mlEqualsTrue(KApply('_>Int_', [KVariable('K', 'Int'), KToken('1', 'Int')])), mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])), mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])), mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])), @@ -1206,6 +1208,7 @@ def test_anti_unify_keep_values( state='N |-> X:Int', constraint=mlAnd( [ + mlEqualsTrue(KApply('_>Int_', [KVariable('K', 'Int'), KToken('1', 'Int')])), mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])), mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])), mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])), @@ -1218,6 +1221,7 @@ def test_anti_unify_keep_values( state='N |-> Y:Int', constraint=mlAnd( [ + mlEqualsTrue(KApply('_>Int_', [KVariable('K', 'Int'), KToken('1', 'Int')])), mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])), mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])), mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])), From c782d0fd3a6dbd3828e8ac4546d02d25ab50536d Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Mon, 14 Aug 2023 16:52:21 -0500 Subject: [PATCH 07/10] Fix formatting and error message typing --- src/pyk/cterm.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/pyk/cterm.py b/src/pyk/cterm.py index 59c2f971a..2b5b3aff0 100644 --- a/src/pyk/cterm.py +++ b/src/pyk/cterm.py @@ -60,7 +60,7 @@ def from_dict(dct: dict[str, Any]) -> CTerm: @staticmethod def _check_config(config: KInner) -> None: if not isinstance(config, KApply) or not config.is_cell: - raise ValueError(f'Expected cell label, found: {config.label.name}') + raise ValueError(f'Expected cell label, found: {config}') @staticmethod def _normalize_constraints(constraints: Iterable[KInner]) -> tuple[KInner, ...]: @@ -153,7 +153,9 @@ def disjunction_from_substs(subst1: Subst, subst2: Subst) -> KInner: 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_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) From 3a1c459f17fa3815e2a256a4fca51dadbc5ffe85 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 16 Aug 2023 00:05:48 +0000 Subject: [PATCH 08/10] Set Version: 0.1.415 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 0cb3afc5f..5bb6eae1e 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.414 +0.1.415 diff --git a/pyproject.toml b/pyproject.toml index 9c1f5d531..6272a7533 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.414" +version = "0.1.415" description = "" authors = [ "Runtime Verification, Inc. ", From 9153ffb5aebcffc308a39b84ebd8f87d16fba03b Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Tue, 15 Aug 2023 19:06:48 -0500 Subject: [PATCH 09/10] Add tests for KDefinition.sort() --- src/pyk/kast/outer.py | 4 + .../integration/konvert/test_simple_proofs.py | 87 +++++++++++++++++++ 2 files changed, 91 insertions(+) diff --git a/src/pyk/kast/outer.py b/src/pyk/kast/outer.py index f2725c3b3..dc1ec0b96 100644 --- a/src/pyk/kast/outer.py +++ b/src/pyk/kast/outer.py @@ -1138,6 +1138,8 @@ def least_common_supersort(self, sort1: KSort, sort2: KSort) -> KSort | None: return sort2 if sort2 in self.subsorts(sort1): return sort1 + # Computing least common supersort is not currently supported if sort1 is not a subsort of sort2 or + # vice versa. In that case there may be more than one LCS. return None def greatest_common_subsort(self, sort1: KSort, sort2: KSort) -> KSort | None: @@ -1147,6 +1149,8 @@ def greatest_common_subsort(self, sort1: KSort, sort2: KSort) -> KSort | None: return sort1 if sort2 in self.subsorts(sort1): return sort2 + # Computing greatest common subsort is not currently supported if sort1 is not a subsort of sort2 or + # vice versa. In that case there may be more than one GCS. return None # Sorts like Int cannot be injected directly into sort K so they are embedded in a KSequence. diff --git a/src/tests/integration/konvert/test_simple_proofs.py b/src/tests/integration/konvert/test_simple_proofs.py index dd9b05125..a40df4543 100644 --- a/src/tests/integration/konvert/test_simple_proofs.py +++ b/src/tests/integration/konvert/test_simple_proofs.py @@ -547,6 +547,75 @@ ), ) +SORT_TERM_DATA: Final = ( + ( + 'variable-int', + KVariable('X', 'Int'), + KSort('Int'), + ), + ( + 'variable-bool', + KVariable('X', 'Bool'), + KSort('Bool'), + ), + ( + 'variable-k', + KVariable('X', 'K'), + KSort('K'), + ), + ( + 'variable-kitem', + KVariable('X', 'KItem'), + KSort('KItem'), + ), + ( + 'int-token', + intToken(1), + KSort('Int'), + ), + ( + 'bool-token', + KToken('true', 'Bool'), + KSort('Bool'), + ), + ( + 'ksequence', + KSequence((intToken(0), intToken(1), intToken(2))), + KSort('K'), + ), + ( + 'krewrite-same-sort', + KRewrite(lhs=intToken(0), rhs=intToken(1)), + KSort('Int'), + ), + ( + 'krewrite-direct-supersort-lhs', + KRewrite(lhs=intToken(0), rhs=KVariable('X', 'KItem')), + KSort('KItem'), + ), + ( + 'krewrite-direct-supersort-rhs', + KRewrite(rhs=intToken(0), lhs=KVariable('X', 'KItem')), + KSort('KItem'), + ), + ( + 'sort-parametric-int', + KApply( + KLabel('#if_#then_#else_#fi_K-EQUAL-SYNTAX_Sort_Bool_Sort_Sort', [KSort('Int')]), + [KToken('true', 'Bool'), intToken(1), intToken(2)], + ), + KSort('Int'), + ), + ( + 'sort-parametric-bool', + KApply( + KLabel('#if_#then_#else_#fi_K-EQUAL-SYNTAX_Sort_Bool_Sort_Sort', [KSort('Bool')]), + [KToken('true', 'Bool'), KToken('true', 'Bool'), KToken('false', 'Bool')], + ), + KSort('Bool'), + ), +) + class TestKonvertSimpleProofs(KompiledTest): KOMPILE_MAIN_FILE = K_FILES / 'simple-proofs.k' @@ -639,3 +708,21 @@ def test_explicit_krule_to_kore( # Then assert actual_kore_text == kore_text + + @pytest.mark.parametrize( + 'test_id,kast,expected_sort', + SORT_TERM_DATA, + ids=[test_id for test_id, *_ in SORT_TERM_DATA], + ) + def test_sort_term( + self, + definition: KDefinition, + test_id: str, + kast: KInner, + expected_sort: KSort, + ) -> None: + # When + actual_sort = definition.sort(kast) + + # Then + assert actual_sort == expected_sort From 4b7472e33bd7f012c452226374729e6a18783a99 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 16 Aug 2023 14:42:42 +0000 Subject: [PATCH 10/10] Set Version: 0.1.416 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 5bb6eae1e..0892550dd 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.415 +0.1.416 diff --git a/pyproject.toml b/pyproject.toml index 6272a7533..5c06d1e5b 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.415" +version = "0.1.416" description = "" authors = [ "Runtime Verification, Inc. ",