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

Add ability to pass in custom function to KCFGExplore for modifying new nodes#498

Merged
rv-jenkins merged 19 commits into
masterfrom
noah/node-postprocessing
Jun 19, 2023
Merged

Add ability to pass in custom function to KCFGExplore for modifying new nodes#498
rv-jenkins merged 19 commits into
masterfrom
noah/node-postprocessing

Conversation

@nwatson22

@nwatson22 nwatson22 commented Jun 15, 2023

Copy link
Copy Markdown
Contributor

This PR adds the ability to pass in a function simplify_node: CTerm->CTerm to KCFGExplore() which modifies new nodes as they are added during exploration. This is intended to be used to accomplish runtimeverification/evm-semantics#1909.

@nwatson22 nwatson22 self-assigned this Jun 15, 2023
@ehildenb

Copy link
Copy Markdown
Member

Let's call it abstract_node instead of simplify_node, and make it an argument to APRProver instead of KCFGExplore.

We have have another block like _check_subsume or _check_terminal, which is _check_abstract. https://github.com/runtimeverification/pyk/blob/master/src/pyk/proof/reachability.py#L316. It should:

  • See if auto_abstraction exists, if it does, try applying it.
  • If applying it changes the cterm, then insert the new cterm into the KCFG, and also insert a cover from the old node to the new one. Then skip the rest of advance_proof (return true from _check_abstract so that it can continue just like the other _check* methods).
  • If auto_bastraction doesn't exist, or doesn't result in a change in the cterm, continue with checking extract_branches.
  • Make sure to thread through the new argument to the APRBMCProver too.

Comment thread src/pyk/proof/reachability.py
@ehildenb ehildenb marked this pull request as ready for review June 19, 2023 17:45
@rv-jenkins rv-jenkins merged commit be26278 into master Jun 19, 2023
@rv-jenkins rv-jenkins deleted the noah/node-postprocessing branch June 19, 2023 20:49
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 9, 2024
…ew nodes (runtimeverification/pyk#498)

This PR adds the ability to pass in a function simplify_node:
CTerm->CTerm to `KCFGExplore()` which modifies new nodes as they are
added during exploration. This is intended to be used to accomplish
runtimeverification/evm-semantics#1909.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 9, 2024
…ew nodes (runtimeverification/pyk#498)

This PR adds the ability to pass in a function simplify_node:
CTerm->CTerm to `KCFGExplore()` which modifies new nodes as they are
added during exploration. This is intended to be used to accomplish
runtimeverification/evm-semantics#1909.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 10, 2024
…ew nodes (runtimeverification/pyk#498)

This PR adds the ability to pass in a function simplify_node:
CTerm->CTerm to `KCFGExplore()` which modifies new nodes as they are
added during exploration. This is intended to be used to accomplish
runtimeverification/evm-semantics#1909.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 10, 2024
…ew nodes (runtimeverification/pyk#498)

This PR adds the ability to pass in a function simplify_node:
CTerm->CTerm to `KCFGExplore()` which modifies new nodes as they are
added during exploration. This is intended to be used to accomplish
runtimeverification/evm-semantics#1909.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants