Make anti-unification more sort-aware

[nwatson22]

• Changed anti_unify and anti_unify_with_constraints to require a KDefinition which they use to grab the tightest sort for the terms they are abstracting
• Since these actions are now associated with a specific K definition, moved them into KDefinition as methods.
• Adds KDefinition.least_common_supersort which returns the most specific sort that will cover two terms (as long as one sort is a subsort of the other).
• Uses this function in KDefinition.sort to determine the sort of a KRewrite.
• Rewrote the tests for anti_unify and anti_unify_with_constraints to use KDefinition and test that the abstracted variables are now more tightly typed based on the original terms.

This is an attempt to fix an issue in runtimeverification/evm-semantics#1934 where the looser sort bound is preventing simplification after the merging (anti-unification) of two nodes.

[ehildenb]

I think this problem can also be solved without creating a circular dependency by just calling KDefinition.sort_vars on the resulting anti-unifier after it's produced (wherever we are calling this routine).

[nwatson22]

I think this problem can also be solved without creating a circular dependency by just calling KDefinition.sort_vars on the resulting anti-unifier after it's produced (wherever we are calling this routine).

@ehildenb That might work in some cases if a tight enough sort is able to be inferred based on the position of the new variable, but in general it doesn't (e.g. in this case it is appearing as the value of a Map, and ==K is not sort parametric).

[ehildenb]

Introducing circular imports like this feels like pretty bad coding practice, and I think we sholud avoid it when possible. It also is making this routine more complicated than it needs to be perhaps.

I think we need to explore alternative solutions to this.

One option may be to change where anti_unify lives, this PR moves it to cterm.py: #544

[nwatson22]

Introducing circular imports like this feels like pretty bad coding practice, and I think we sholud avoid it when possible. It also is making this routine more complicated than it needs to be perhaps.

I think we need to explore alternative solutions to this.

One option may be to change where anti_unify lives, this PR moves it to cterm.py: #544

@ehildenb I looked at #544 and moved both the anti_unification functions into cterm.py to avoid the circular imports. It looks like #544 gets rid of the flags we currently have for anti_unify_with_constraints but is always including the implications. I don't know all what we are trying to do with anti-unification besides my use case so I don't understand the thought process behind these flags/variants.

[nwatson22]

I added the code from #544 that removes constraints from no longer used variables and integrated it with the system that produces the disjunction, so now those constraints on variables getting abstracted during the merge will no longer be removed, unless the option to include the disjunction is disabled.

[ehildenb]

@nwatson22 it would be good to add some tests of the sort inference algorithm at this point.

You can do it by adding tests of kast_to_kore that have rewrites in them, because those invoke the sort inference directly.

[nwatson22]

@nwatson22 it would be good to add some tests of the sort inference algorithm at this point.

You can do it by adding tests of kast_to_kore that have rewrites in them, because those invoke the sort inference directly.

@ehildenb kast_to_kore does not support rewrites currently. Also, it does not call the KDefinition.sort(KInner) function that this new logic is being added under, so as I understand it there are two separate sort inference algorithms here, sort_vars() which does what I guess you could call "top-down" sort inference and sort() which does "bottom-up" sort inference, and these are being used in disjoint cases. Currently the only uses of sort() are in anti_unify() and EqualityProof.from_claim(), and sort_vars() only operates on variables which have no constituent parts to do bottom-up inference on anyway.

So, I've added tests for sort() under a separate test.