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

CTerm.match_with_constraint does not return expected CSubst.constraints #4496

Closed
Stevengre opened this issue Jul 3, 2024 · 4 comments · Fixed by #4499
Closed

CTerm.match_with_constraint does not return expected CSubst.constraints #4496

Stevengre opened this issue Jul 3, 2024 · 4 comments · Fixed by #4499
Assignees
@Stevengre

Comments

@Stevengre
Copy link
Contributor

Hi @tothtamas28 !

I am encountering an issue with CTerm.match_with_constraint where it does not provide the expected CSubst that can be used to transform self into other via CSubst.apply. Instead, I am receiving an empty constraint. I suspect there may be an issue with the _ml_impl method.

Here is my test harness:

def test_cterm_match_with_constraint() -> None:
    # Given
    merged_cterm = {
        'config': {
            'args': [{'name': 'X', 'node': 'KVariable'}],
            'arity': 1,
            'label': {'name': '<top>', 'node': 'KLabel', 'params': []},
            'node': 'KApply',
            'variable': False
        },
        'constraints': []
    }
    merged_cterm = CTerm.from_dict(merged_cterm)

    original_cterm = {
        'config': {
            'node': 'KApply',
            'label': {'node': 'KLabel', 'name': '<top>', 'params': []},
            'args': [{'node': 'KVariable', 'name': 'X'}],
            'arity': 1,
            'variable': False
        },
        'constraints': [{
            'node': 'KApply',
            'label': {
                'node': 'KLabel',
                'name': '#Equals',
                'params': [{'node': 'KSort', 'name': 'Bool'}, {'node': 'KSort', 'name': 'GeneratedTopCell'}]
            },
            'args': [
                {'node': 'KToken', 'token': 'true', 'sort': {'node': 'KSort', 'name': 'Bool'}},
                {
                    'node': 'KApply',
                    'label': {'node': 'KLabel', 'name': '_>=Int_', 'params': []},
                    'args': [
                        {'node': 'KVariable', 'name': 'X'},
                        {'node': 'KToken', 'token': '5', 'sort': {'node': 'KSort', 'name': 'Int'}}
                    ],
                    'arity': 2,
                    'variable': False
                }
            ],
            'arity': 2,
            'variable': False
        }]
    }
    original_cterm = CTerm.from_dict(original_cterm)

    # When
    csubst = merged_cterm.match_with_constraint(original_cterm)

    # Then
    assert csubst.apply(merged_cterm) == original_cterm

Could you please help me identify what might be going wrong?

Thank you!
@Stevengre Stevengre self-assigned this Jul 3, 2024
@tothtamas28
Copy link
Contributor

Thanks for reporting this issue.

Let's simplify the example. You can

  • construct the CTerm directly, i.e. CTerm(KApply(...), ...);
  • minimize the CTerm, i.e. reduce the number of sub-terms so that the issue is still reproducible.

Also, please push a branch with the test so that the issue is easy to reproduce.

@Stevengre
Copy link
Contributor Author

Thanks for your suggestion. I’ve already constructed a test in this branch: https://github.com/runtimeverification/k/tree/4496-ctermmatch_with_constraint-does-not-return-expected-csubstconstraints. I hope this can help.

@tothtamas28 tothtamas28 mentioned this issue Jul 4, 2024
Merged
@tothtamas28
Copy link
Contributor

I opened a PR with your test to start the discussion (does not yet fix the issue):

The fix should be straightforward, we just need to figure out what the intended semantics for CTerm.constraint is. For that, all uses need to be inspected.

@tothtamas28 tothtamas28 linked a pull request Jul 4, 2024 that will close this issue
Fix match_with_constraint #4499
Merged
@Stevengre Stevengre mentioned this issue Sep 6, 2024
Closed
@ehildenb
Copy link
Member

ehildenb commented Sep 6, 2024

Hmmm, reading the implementation for CTerm.match_with_constraints, I'm honestly quite surprised it works at all! It seems that it's completely incorrect basically, I think we should probably just try reimplementing it.

@ehildenb ehildenb mentioned this issue Sep 6, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@Stevengre Stevengre

Labels
None yet
Projects
None yet
Milestone
No milestone
3 participants
@tothtamas28 @ehildenb @Stevengre