Reverse pyk match operator

[ehildenb]

I was trying to explain the algorithm behind summarization to @xc93 and realized that on this line:

https://github.com/runtimeverification/erc20-verification/blob/master/ksummarize/src/ksummarize/kevm_summarize.py#L211

we are saying term.match(pattern). I would much prefer for us to say pattern.match(term), it matches the same direction as match(pattern, term) that I'm used to for a long time and makes more sense in my head. I can't provide a better justification for it than this, but I did confirm that this is the only use that needs to change.

[ehildenb]

Also, pattern.match(term) matches better the python way of defining match as:

class CTerm:
    def match(self, other):
        return match(self.config, other.config)

[tothtamas28]

A previous discussion we had on this topic: #2470 (comment).

To sum up. my take on the issue is the following.

1. Both "pattern matches term" and "term matches pattern" are in use.
2. Both map(patterm.match, iterable) and map(term.match, iterable) have natural use cases.
3. term.match(pattern) is not None corresponds to "the set of models of term is a subset of the set of models of pattern". Notice that the order of operands is the same in both the code and its logical interpretation. This is also the direction we draw our abstraction edges in KCFG.

But I do not have a strong opinion on this one, so I'm fine with pattern.match(term).

[ehildenb]

Yeah, I remember being unsure what the correct direction was before, but I think the fact that I spent an hour being baffled at how the summarization algorithm was working was a strong enough indicator of what I naturally expected while working with the library.