Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Mergeable heuristic in KCFGSemantics for merging node #4612

Closed
wants to merge 2 commits into from
Closed

Mergeable heuristic in KCFGSemantics for merging node #4612

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a6019eb
add is_mergeable heuristics for KCFGSemantics
Stevengre Aug 28, 2024
41db87f
KCFGSemantics to DefaultSemantics for testing
Stevengre Aug 30, 2024
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
8 changes: 8 additions & 0 deletions pyk/src/pyk/kcfg/semantics.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,11 @@ def custom_step(self, c: CTerm) -> KCFGExtendResult | None: ...

"""Implement a custom semantic step."""

@abstractmethod
def is_mergeable(self, c1: CTerm, c2: CTerm) -> bool: ...
Copy link
Contributor Author

Choose a reason for hiding this comment

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

This PR only introduces an interface. Its semantics will be determined by the merge_node function, which will be provided in another PR.


"""Check whether or not the two given ``CTerm``s are mergeable. Must be transitive, commutative, and reflexive."""


class DefaultSemantics(KCFGSemantics):
def is_terminal(self, c: CTerm) -> bool:
Expand All @@ -50,3 +55,6 @@ def can_make_custom_step(self, c: CTerm) -> bool:

def custom_step(self, c: CTerm) -> KCFGExtendResult | None:
return None

def is_mergeable(self, c1: CTerm, c2: CTerm) -> bool:
return False
5 changes: 3 additions & 2 deletions pyk/src/tests/integration/ktool/test_imp.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@

from pyk.cli.pyk import ProveOptions
from pyk.kast.inner import KApply, KSequence, KVariable
from pyk.kcfg.semantics import KCFGSemantics
from pyk.kcfg.semantics import DefaultSemantics
from pyk.ktool.prove_rpc import ProveRpc
from pyk.proof import ProofStatus
from pyk.testing import KCFGExploreTest, KProveTest
Expand All @@ -25,12 +25,13 @@
from pyk.kast.outer import KDefinition
from pyk.kcfg import KCFGExplore
from pyk.kcfg.kcfg import KCFGExtendResult
from pyk.kcfg.semantics import KCFGSemantics
from pyk.ktool.kprove import KProve

_LOGGER: Final = logging.getLogger(__name__)


class ImpSemantics(KCFGSemantics):
class ImpSemantics(DefaultSemantics):
definition: KDefinition | None

def __init__(self, definition: KDefinition | None = None):
Expand Down
5 changes: 3 additions & 2 deletions pyk/src/tests/integration/proof/test_custom_step.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@
from pyk.kast.manip import set_cell
from pyk.kcfg import KCFGExplore
from pyk.kcfg.kcfg import Step
from pyk.kcfg.semantics import KCFGSemantics
from pyk.kcfg.semantics import DefaultSemantics
from pyk.kcfg.show import KCFGShow
from pyk.proof import APRProof, APRProver, ProofStatus
from pyk.proof.show import APRProofNodePrinter
Expand All @@ -26,6 +26,7 @@
from pyk.cterm import CTermSymbolic
from pyk.kast.outer import KClaim
from pyk.kcfg.kcfg import KCFGExtendResult
from pyk.kcfg.semantics import KCFGSemantics
from pyk.ktool.kprove import KProve
from pyk.utils import BugReport

Expand All @@ -46,7 +47,7 @@
)


class CustomStepSemanticsWithoutStep(KCFGSemantics):
class CustomStepSemanticsWithoutStep(DefaultSemantics):
def is_terminal(self, c: CTerm) -> bool:
k_cell = c.cell('K_CELL')
if (
Expand Down
5 changes: 3 additions & 2 deletions pyk/src/tests/integration/proof/test_goto.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
import pytest

from pyk.kast.inner import KApply, KSequence
from pyk.kcfg.semantics import KCFGSemantics
from pyk.kcfg.semantics import DefaultSemantics
from pyk.kcfg.show import KCFGShow
from pyk.proof import APRProof, APRProver, ProofStatus
from pyk.proof.show import APRProofNodePrinter
Expand All @@ -24,12 +24,13 @@
from pyk.kast.outer import KDefinition
from pyk.kcfg import KCFGExplore
from pyk.kcfg.kcfg import KCFGExtendResult
from pyk.kcfg.semantics import KCFGSemantics
from pyk.ktool.kprove import KProve

_LOGGER: Final = logging.getLogger(__name__)


class GotoSemantics(KCFGSemantics):
class GotoSemantics(DefaultSemantics):
def is_terminal(self, c: CTerm) -> bool:
return False

Expand Down
5 changes: 3 additions & 2 deletions pyk/src/tests/integration/proof/test_imp.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@
from pyk.cterm import CSubst, CTerm
from pyk.kast.inner import KApply, KSequence, KSort, KToken, KVariable, Subst
from pyk.kast.manip import minimize_term, sort_ac_collections
from pyk.kcfg.semantics import KCFGSemantics
from pyk.kcfg.semantics import DefaultSemantics
from pyk.kcfg.show import KCFGShow
from pyk.prelude.kbool import FALSE, andBool, orBool
from pyk.prelude.kint import intToken
Expand All @@ -34,6 +34,7 @@
from pyk.kast.outer import KDefinition
from pyk.kcfg import KCFGExplore
from pyk.kcfg.kcfg import KCFGExtendResult
from pyk.kcfg.semantics import KCFGSemantics
from pyk.ktool.kprint import KPrint, SymbolTable
from pyk.ktool.kprove import KProve
from pyk.proof import Prover
Expand All @@ -46,7 +47,7 @@ def proof_dir(tmp_path_factory: TempPathFactory) -> Path:
return tmp_path_factory.mktemp('proofs')


class ImpSemantics(KCFGSemantics):
class ImpSemantics(DefaultSemantics):
definition: KDefinition | None

def __init__(self, definition: KDefinition | None = None):
Expand Down
5 changes: 3 additions & 2 deletions pyk/src/tests/integration/proof/test_refute_node.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@
from pyk.kast.outer import KClaim
from pyk.kcfg import KCFG
from pyk.kcfg.minimize import KCFGMinimizer
from pyk.kcfg.semantics import KCFGSemantics
from pyk.kcfg.semantics import DefaultSemantics
from pyk.prelude.kint import gtInt, intToken, leInt
from pyk.prelude.ml import is_top, mlEqualsTrue
from pyk.proof import APRProof, APRProver, ImpliesProver, ProofStatus, RefutationProof
Expand All @@ -31,12 +31,13 @@
from pyk.kast.outer import KDefinition
from pyk.kcfg import KCFGExplore
from pyk.kcfg.kcfg import KCFGExtendResult
from pyk.kcfg.semantics import KCFGSemantics
from pyk.ktool.kprove import KProve

STATE = Union[tuple[str, str], tuple[str, str, str]]


class RefuteSemantics(KCFGSemantics):
class RefuteSemantics(DefaultSemantics):
def is_terminal(self, c: CTerm) -> bool:
k_cell = c.cell('K_CELL')
if type(k_cell) is KSequence:
Expand Down
5 changes: 3 additions & 2 deletions pyk/src/tests/integration/proof/test_simple.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
from typing import TYPE_CHECKING

from pyk.kast.inner import KApply, KSequence
from pyk.kcfg.semantics import KCFGSemantics
from pyk.kcfg.semantics import DefaultSemantics
from pyk.proof import APRProof, APRProver
from pyk.testing import KCFGExploreTest, KProveTest
from pyk.utils import single
Expand All @@ -18,12 +18,13 @@
from pyk.kast.outer import KDefinition
from pyk.kcfg import KCFGExplore
from pyk.kcfg.kcfg import KCFGExtendResult
from pyk.kcfg.semantics import KCFGSemantics
from pyk.ktool.kprove import KProve

_LOGGER: Final = logging.getLogger(__name__)


class SimpleSemantics(KCFGSemantics):
class SimpleSemantics(DefaultSemantics):
def is_terminal(self, c: CTerm) -> bool:
k_cell = c.cell('K_CELL')
if type(k_cell) is KSequence and type(k_cell[0]) is KApply and k_cell[0].label.name == 'f_SIMPLE-PROOFS_Step':
Expand Down
Loading