Skip to content
This repository has been archived by the owner on Apr 25, 2024. It is now read-only.

Make branch extraction more intelligent #652

Merged
merged 14 commits into from
Sep 18, 2023
Merged

Make branch extraction more intelligent #652

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
d259f23
Make branch extraction more intelligent
nwatson22 Sep 13, 2023
51d7729
Merge d259f23fe282348402f9fd018d567959460004d0 into d19598b275c2ee741…
nwatson22 Sep 13, 2023
2863769
Set Version: 0.1.440
Sep 13, 2023
2826395
Do not immediately apply simplifications, only count non-bottom nodes
nwatson22 Sep 13, 2023
6de4680
Merge branch 'noah/extract-branches-fix' of https://github.com/runtim…
nwatson22 Sep 13, 2023
07574aa
Use kast_simplify
nwatson22 Sep 13, 2023
229ed7a
Merge 07574aa687bd10f4c62dbb1647126ac2cd949d18 into 26443bfcb4c36189e…
nwatson22 Sep 13, 2023
9967e07
Set Version: 0.1.441
Sep 13, 2023
21b44fa
Merge master into branch
nwatson22 Sep 15, 2023
c142928
Merge 21b44fae194c425b934f868d6c4e47a5c05b9541 into da0e4eae92248661b…
nwatson22 Sep 15, 2023
08aa799
Set Version: 0.1.443
Sep 15, 2023
848713c
Merge branch 'master' into noah/extract-branches-fix
PetarMax Sep 18, 2023
3658a3c
Merge 848713cc92a575fd422feb200fb148a9e0fe1148 into 31ca5378c8cb2109c…
nwatson22 Sep 18, 2023
849773d
Set Version: 0.1.444
Sep 18, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion package/version
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.443
0.1.444
2 changes: 1 addition & 1 deletion pyproject.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "pyk"
version = "0.1.443"
version = "0.1.444"
description = ""
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
21 changes: 13 additions & 8 deletions src/pyk/kcfg/explore.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -377,14 +377,19 @@ def extend(
if self._check_abstract(node, kcfg):
return

if not kcfg.splits(target_id=node.id):
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This check is no longer relevant?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, as I understand, it was the check preventing us from branching over and over again. But by simplifying before branching when it tries to branch a second time without having made an execution step, one of the branches will now simplify to bottom and it won't branch.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What do you mean by 'over and over again', when can that happen? As part of looping code?

branches = self.kcfg_semantics.extract_branches(node.cterm)
if branches:
kcfg.split_on_constraints(node.id, branches)
_LOGGER.info(
f'Found {len(branches)} branches using heuristic for node {node.id}: {shorten_hashes(node.id)}: {[self.kprint.pretty_print(bc) for bc in branches]}'
)
return
_branches = self.kcfg_semantics.extract_branches(node.cterm)
branches = []
for constraint in _branches:
kast = mlAnd(list(node.cterm.constraints) + [constraint])
kast, _ = self.kast_simplify(kast)
if not CTerm._is_bottom(kast):
branches.append(constraint)
if len(branches) > 1:
kcfg.split_on_constraints(node.id, branches)
_LOGGER.info(
f'Found {len(branches)} branches using heuristic for node {node.id}: {shorten_hashes(node.id)}: {[self.kprint.pretty_print(bc) for bc in branches]}'
)
return
Comment on lines +387 to +392
Copy link
Contributor

@PetarMax PetarMax Sep 18, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In this case, will the unsimplified constraint be added to the configuration or will the Haskell backend simplify it? The problem that we had was that the booster was not able to simplify a given constraint. Perhaps just checking for #Bottom will be enough.

I will try to run this on an appropriate test from the engagement in question.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The unsimplified contsraint will be added, but that should be enough to make it only take the one branch on subsequent execute call.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If the backend can't simplify a constraint, then it needs more lemmas to do so, or is a bug in the backend.


_LOGGER.info(f'Extending KCFG from node {self.id}: {shorten_hashes(node.id)}')
_is_vacuous, depth, cterm, next_cterms, next_node_logs = self.cterm_execute(
Expand Down