CTerm.match_with_constraint does not return expected CSubst.constraints

[Stevengre]

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!

[tothtamas28]

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]

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]

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

• Fix match_with_constraint #4499

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.

[ehildenb]

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.