From deaea59e913d6a834a79866d95b404037e66a047 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 1 Jul 2023 16:59:17 +0000 Subject: [PATCH 01/12] cterm: add CTerm.anti_unify(cterm) -> tuple[CTerm, CSubst, CSubst] --- src/pyk/cterm.py | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/src/pyk/cterm.py b/src/pyk/cterm.py index ad16cb2c6..bce1efca8 100644 --- a/src/pyk/cterm.py +++ b/src/pyk/cterm.py @@ -7,6 +7,7 @@ from .kast.inner import KApply, KAtt, KInner, KRewrite, KVariable, Subst from .kast.manip import ( + anti_unify, apply_existential_substitutions, count_vars, flatten_label, @@ -137,6 +138,29 @@ 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) -> tuple[CTerm, CSubst, CSubst]: + new_config, _, _ = anti_unify(self.config, other.config) + common_constraints = [constraint for constraint in self.constraints if constraint in other.constraints] + 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) + @dataclass(frozen=True, order=True) class CSubst: From 2939fa1f958929c0bc9bb90ea2091ade667056ea Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 1 Jul 2023 16:59:53 +0000 Subject: [PATCH 02/12] kcfg/kcfg: add KCFG.create_merge for merging several nodes in a graph --- src/pyk/kcfg/kcfg.py | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/pyk/kcfg/kcfg.py b/src/pyk/kcfg/kcfg.py index e09f60352..94f1320d5 100644 --- a/src/pyk/kcfg/kcfg.py +++ b/src/pyk/kcfg/kcfg.py @@ -646,6 +646,19 @@ def create_split(self, source_id: NodeIdLike, splits: Iterable[tuple[NodeIdLike, split = KCFG.Split(self.node(source_id), tuple((self.node(nid), csubst) for nid, csubst in splits)) self._splits[source_id] = split + def create_merge(self, node_ids: Iterable[NodeIdLike]) -> NodeIdLike: + node_ids = list(node_ids) + if len(node_ids) < 2: + raise ValueError(f'Cannot create merge node with less than 2 input nodes: {node_ids}') + cterms = [self.node(nid).cterm for nid in node_ids] + new_cterm = cterms[0] + for cterm in cterms[1:]: + new_cterm, _, _ = new_cterm.anti_unify(cterm) + new_node = self.create_node(new_cterm) + for nid in node_ids: + self.create_cover(nid, new_node.id) + return new_node.id + def ndbranches(self, *, source_id: NodeIdLike | None = None, target_id: NodeIdLike | None = None) -> list[NDBranch]: source_id = self._resolve(source_id) if source_id is not None else None target_id = self._resolve(target_id) if target_id is not None else None From 44a105bc721ca2c1c49c05497248a27321abe09b Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 1 Jul 2023 17:16:09 +0000 Subject: [PATCH 03/12] proof/reachability: add APRProver.specialize_target_node routine for factoring out specialized proofs --- src/pyk/proof/reachability.py | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 6eacfd0e7..9561a54ae 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -587,6 +587,28 @@ def construct_node_refutation(self, node: KCFG.Node) -> RefutationProof | None: self.proof.add_subproof(refutation) return refutation + def specialize_target_node(self) -> None: + target_subsumed = self.proof.kcfg.predecessors(self.proof.target) + if len(target_subsumed) < 2: + _LOGGER.info( + f'Found less than 2 nodes subsumed into target, not specializing target node {self.proof.id}: {target_subsumed}' + ) + return + target_subsumed_covers: list[KCFG.Cover] = [] + for ts in target_subsumed: + if type(ts) is KCFG.Cover: + target_subsumed_covers.append(ts) + else: + _LOGGER.info( + f'Found non-cover predecessor into target node, not specializing target node {self.proof.id}: {ts}' + ) + return + for tsc in target_subsumed_covers: + self.proof.kcfg.remove_cover(tsc.source.id, tsc.target.id) + merge_id = self.proof.kcfg.create_merge([cover.source.id for cover in target_subsumed_covers]) + self.proof.kcfg.create_cover(merge_id, self.proof.target) + _LOGGER.info(f'Created specialized target subsumed node {self.proof.id}: {merge_id}') + class APRBMCProver(APRProver): proof: APRBMCProof From 89ce40fc1d83cd7e50527b3afe4b1044aba40dc4 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 1 Jul 2023 17:18:05 +0000 Subject: [PATCH 04/12] cterm: add CSubst.ml_pred --- src/pyk/cterm.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/pyk/cterm.py b/src/pyk/cterm.py index bce1efca8..32dfb320d 100644 --- a/src/pyk/cterm.py +++ b/src/pyk/cterm.py @@ -197,6 +197,10 @@ def apply(self, cterm: CTerm) -> CTerm: _kast = self.subst(cterm.kast) return CTerm(_kast, [self.constraint]) + @property + def ml_pred(self) -> KInner: + return mlAnd(flatten_label('#And', self.subst.ml_pred) + list(self.constraints)) + def remove_useless_constraints(cterm: CTerm, keep_vars: Iterable[str] = ()) -> CTerm: used_vars = free_vars(cterm.config) + list(keep_vars) From 312cc6751e59a03d75eb7a6a4b0f394d9757525c Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 18 Jul 2023 15:21:57 +0000 Subject: [PATCH 05/12] proof/reachability: move APRProver.specialize_target_node => APRProof.specialize_target_node --- src/pyk/proof/reachability.py | 44 +++++++++++++++++------------------ 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 3bad93133..746015dc0 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -253,6 +253,28 @@ def summary(self) -> Iterable[str]: def get_refutation_id(self, node_id: int) -> str: return f'{self.id}.node-infeasible-{node_id}' + def specialize_target_node(self) -> None: + target_subsumed = self.kcfg.predecessors(self.target) + if len(target_subsumed) < 2: + _LOGGER.info( + f'Found less than 2 nodes subsumed into target, not specializing target node {self.id}: {target_subsumed}' + ) + return + target_subsumed_covers: list[KCFG.Cover] = [] + for ts in target_subsumed: + if type(ts) is KCFG.Cover: + target_subsumed_covers.append(ts) + else: + _LOGGER.info( + f'Found non-cover predecessor into target node, not specializing target node {self.id}: {ts}' + ) + return + for tsc in target_subsumed_covers: + self.kcfg.remove_cover(tsc.source.id, tsc.target.id) + merge_id = self.kcfg.create_merge([cover.source.id for cover in target_subsumed_covers]) + self.kcfg.create_cover(merge_id, self.target) + _LOGGER.info(f'Created specialized target subsumed node {self.id}: {merge_id}') + class APRBMCProof(APRProof): """APRBMCProof and APRBMCProver perform bounded model-checking of an all-path reachability logic claim.""" @@ -588,28 +610,6 @@ def construct_node_refutation(self, node: KCFG.Node) -> RefutationProof | None: self.proof.add_subproof(refutation) return refutation - def specialize_target_node(self) -> None: - target_subsumed = self.proof.kcfg.predecessors(self.proof.target) - if len(target_subsumed) < 2: - _LOGGER.info( - f'Found less than 2 nodes subsumed into target, not specializing target node {self.proof.id}: {target_subsumed}' - ) - return - target_subsumed_covers: list[KCFG.Cover] = [] - for ts in target_subsumed: - if type(ts) is KCFG.Cover: - target_subsumed_covers.append(ts) - else: - _LOGGER.info( - f'Found non-cover predecessor into target node, not specializing target node {self.proof.id}: {ts}' - ) - return - for tsc in target_subsumed_covers: - self.proof.kcfg.remove_cover(tsc.source.id, tsc.target.id) - merge_id = self.proof.kcfg.create_merge([cover.source.id for cover in target_subsumed_covers]) - self.proof.kcfg.create_cover(merge_id, self.proof.target) - _LOGGER.info(f'Created specialized target subsumed node {self.proof.id}: {merge_id}') - def failure_info(self) -> APRFailureInfo: return APRFailureInfo.from_proof(self.proof, self.kcfg_explore) From 2a28e9fe8e1499087a64c93e3216d2d0a791a322 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 18 Jul 2023 15:27:26 +0000 Subject: [PATCH 06/12] kcfg/kcfg: implement KCFG.pullback_covers which minimizes covers --- src/pyk/kcfg/kcfg.py | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/pyk/kcfg/kcfg.py b/src/pyk/kcfg/kcfg.py index 94f1320d5..677b1ee50 100644 --- a/src/pyk/kcfg/kcfg.py +++ b/src/pyk/kcfg/kcfg.py @@ -659,6 +659,18 @@ def create_merge(self, node_ids: Iterable[NodeIdLike]) -> NodeIdLike: self.create_cover(nid, new_node.id) return new_node.id + def pullback_covers(self, target_id: NodeIdLike) -> tuple[list[NodeIdLike], NodeIdLike] | None: + covers = self.covers(target_id=target_id) + source_ids: list[NodeIdLike] = [cover.source.id for cover in covers] + if len(source_ids) < 2: + return None + merge_id = self.create_merge(source_ids) + for cover in covers: + self.remove_cover(cover.source.id, target_id) + self.create_cover(cover.source.id, merge_id) + self.create_cover(merge_id, target_id) + return source_ids, merge_id + def ndbranches(self, *, source_id: NodeIdLike | None = None, target_id: NodeIdLike | None = None) -> list[NDBranch]: source_id = self._resolve(source_id) if source_id is not None else None target_id = self._resolve(target_id) if target_id is not None else None From e065729f09b077822fe06d1045595b359e7fee0b Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 18 Jul 2023 15:39:43 +0000 Subject: [PATCH 07/12] proof/reachability: implement simpler APRProof.specialize_target_node with KCFG.pullback_covers --- src/pyk/proof/reachability.py | 26 ++++++-------------------- 1 file changed, 6 insertions(+), 20 deletions(-) diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 746015dc0..2304c421d 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -254,26 +254,12 @@ def get_refutation_id(self, node_id: int) -> str: return f'{self.id}.node-infeasible-{node_id}' def specialize_target_node(self) -> None: - target_subsumed = self.kcfg.predecessors(self.target) - if len(target_subsumed) < 2: - _LOGGER.info( - f'Found less than 2 nodes subsumed into target, not specializing target node {self.id}: {target_subsumed}' - ) - return - target_subsumed_covers: list[KCFG.Cover] = [] - for ts in target_subsumed: - if type(ts) is KCFG.Cover: - target_subsumed_covers.append(ts) - else: - _LOGGER.info( - f'Found non-cover predecessor into target node, not specializing target node {self.id}: {ts}' - ) - return - for tsc in target_subsumed_covers: - self.kcfg.remove_cover(tsc.source.id, tsc.target.id) - merge_id = self.kcfg.create_merge([cover.source.id for cover in target_subsumed_covers]) - self.kcfg.create_cover(merge_id, self.target) - _LOGGER.info(f'Created specialized target subsumed node {self.id}: {merge_id}') + pullback = self.kcfg.pullback_covers(self.target) + if pullback is None: + _LOGGER.warning(f'Could not make a cover pullback for target node: {self.target}') + else: + merge_id, source_ids = pullback + _LOGGER.info(f'Created specialized target subsumed node {self.id}: {pullback}') class APRBMCProof(APRProof): From a56d4b04be40cedc7c321c0505b30e24a8650e7a Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 19 Jul 2023 09:06:49 +0000 Subject: [PATCH 08/12] Set Version: 0.1.372 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 0dc706225..df263c054 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.371 +0.1.372 diff --git a/pyproject.toml b/pyproject.toml index 283502769..66fbe3f9f 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.371" +version = "0.1.372" description = "" authors = [ "Runtime Verification, Inc. ", From 221798629d6d4694398b79d386776880c1e1eb50 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 26 Jul 2023 21:07:18 +0000 Subject: [PATCH 09/12] Set Version: 0.1.385 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 9ff5c75dc..280197c3c 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.384 +0.1.385 diff --git a/pyproject.toml b/pyproject.toml index f45441df1..3fcd3346f 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.384" +version = "0.1.385" description = "" authors = [ "Runtime Verification, Inc. ", From f33865e655a5b4bfd15c45174d29e4eb3f8eb1ba Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 26 Jul 2023 21:24:22 +0000 Subject: [PATCH 10/12] src/tests/unit/{kast,test_manip,test_cterm}: make unit test harness for cterm antiunification --- src/tests/unit/kast/test_manip.py | 99 +------------------------------ src/tests/unit/test_cterm.py | 94 +++++++++++++++++++++++++++-- 2 files changed, 93 insertions(+), 100 deletions(-) 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 diff --git a/src/tests/unit/test_cterm.py b/src/tests/unit/test_cterm.py index 51bb1de9a..18ae0638b 100644 --- a/src/tests/unit/test_cterm.py +++ b/src/tests/unit/test_cterm.py @@ -5,13 +5,14 @@ import pytest -from pyk.cterm import CTerm, build_claim, build_rule +from pyk.cterm import CSubst, CTerm, build_claim, build_rule from pyk.kast import KAtt -from pyk.kast.inner import KApply, KLabel, KRewrite, KSequence, KVariable +from pyk.kast.inner import KApply, KLabel, KRewrite, KSequence, KToken, KVariable, Subst from pyk.kast.outer import KClaim from pyk.prelude.k import GENERATED_TOP_CELL -from pyk.prelude.kint import INT, intToken +from pyk.prelude.kint import INT from pyk.prelude.ml import mlAnd, mlEqualsTrue +from pyk.prelude.utils import token from .utils import a, b, c, f, g, h, k, x, y, z @@ -106,7 +107,7 @@ def test_build_rule(lhs: KInner, rhs: KInner, keep_vars: list[str], expected: KI def constraint(v: KVariable) -> KInner: - return KApply('_<=Int_', intToken(0), v) + return KApply('_<=Int_', token(0), v) # ( V1 #And { true #Equals 0 <=Int V2}) => V2 expected: _V1 => V2 requires 0 <=Int V2 @@ -156,3 +157,88 @@ def test_build_claim(test_id: str, init: KInner, target: KInner, expected: KClai # Then assert actual == expected + + +ANTI_UNIFY_TEST_DATA: list[tuple[str, CTerm, CTerm, tuple[CTerm, CSubst, CSubst] | None]] = [ + ( + 'empty-subst', + CTerm( + KApply( + '', + [ + KApply('', KToken('1', 'Int')), + ], + ), + [], + ), + CTerm( + KApply( + '', + [ + KApply('', KToken('1', 'Int')), + ], + ), + [], + ), + ( + CTerm( + KApply( + '', + [ + KApply('', [KToken('1', 'Int')]), + ], + ), + [], + ), + CSubst(Subst({}), []), + CSubst(Subst({}), []), + ), + ), + ( + 'same-constraints', + CTerm( + KApply( + '', + [ + KApply('', KToken('1', 'Int')), + KApply('', KVariable('GENERATEDCOUNTER_CELL')), + ], + ), + [mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')]))], + ), + CTerm( + KApply( + '', + [ + KApply('', KToken('2', 'Int')), + KApply('', KVariable('GENERATEDCOUNTER_CELL')), + ], + ), + [mlEqualsTrue(KApply('_==K_', [KToken('1', 'Int'), KToken('1', 'Int')]))], + ), + ( + CTerm( + KApply( + '', + [ + KApply('', [KVariable('V_93d8c352')]), + KApply('', KVariable('GENERATEDCOUNTER_CELL')), + ], + ), + [], + ), + CSubst(Subst({'V_93d8c352': token(1), 'GENERATEDCOUNTER_CELL': KVariable('GENERATEDCOUNTER_CELL')}), []), + CSubst(Subst({'V_93d8c352': token(2), 'GENERATEDCOUNTER_CELL': KVariable('GENERATEDCOUNTER_CELL')}), []), + ), + ), +] + + +@pytest.mark.parametrize( + 'test_id,cterm1,cterm2,expected', + ANTI_UNIFY_TEST_DATA, + ids=[test_id for test_id, *_ in ANTI_UNIFY_TEST_DATA], +) +def test_anti_unify(test_id: str, cterm1: CTerm, cterm2: CTerm, expected: tuple[CTerm, CSubst, CSubst] | None) -> None: + actual = cterm1.anti_unify(cterm2) + assert actual == expected From 260b6b260f017e824338e2421e5aaa7fcd645836 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 26 Jul 2023 21:25:06 +0000 Subject: [PATCH 11/12] kast/manip: remove now unused anti_unify_with_constraints --- src/pyk/kast/manip.py | 39 +-------------------------------------- 1 file changed, 1 insertion(+), 38 deletions(-) diff --git a/src/pyk/kast/manip.py b/src/pyk/kast/manip.py index e5fc13446..25e211652 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 @@ -597,43 +597,6 @@ def _rewrites_to_abstractions(_kast: KInner) -> KInner: 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) From 90f665e365a303d8985f53856ec9c7538c195a44 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 26 Jul 2023 21:42:07 +0000 Subject: [PATCH 12/12] kcfg/kcfg: avoid duplicate covers being created --- src/pyk/kcfg/kcfg.py | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/pyk/kcfg/kcfg.py b/src/pyk/kcfg/kcfg.py index 9f427ad4d..e67fd36b8 100644 --- a/src/pyk/kcfg/kcfg.py +++ b/src/pyk/kcfg/kcfg.py @@ -682,8 +682,6 @@ def create_merge(self, node_ids: Iterable[NodeIdLike]) -> NodeIdLike: for cterm in cterms[1:]: new_cterm, _, _ = new_cterm.anti_unify(cterm) new_node = self.create_node(new_cterm) - for nid in node_ids: - self.create_cover(nid, new_node.id) return new_node.id def pullback_covers(self, target_id: NodeIdLike) -> tuple[list[NodeIdLike], NodeIdLike] | None: