CTerm.anti_unify doesn't provide expected constraints for CTerm and CSubst.

[Stevengre]

Hi @nwatson22!

I’ve encountered an issue with the Cterm.anti_unify function, which doesn’t behave as expected. Below is a simple example provided by @PetarMax to illustrate the problem.

Given

CTerm1:

<k> X </k> 
<whatever> 5 </whatever>
X > 0

CTerm2:

<k> Y </k>
<whatever> 3 </whatever>
Y > 5

Expected Anti-Unification

Anti-Unified CTerm:

<k> A </k>
<whatever> B </whatever>
{ (A ==Int X #And B ==K 5) #Implies X >Int 0 } #And { (A ==Int Y #And B ==Int 3) #Implies Y >Int 5 }

CSubst1

{A -> X; B -> 5}

CSubst1

{A -> Y; B -> 3}

Actual Result

Anti-Unified CTerm:

<k> A </k>
<whatever> B </whatever>

CSubst1

{A -> X; B -> 5}

CSubst1

{A -> Y; B -> 3}

Additional Information

1. Issue Fix match_with_constraint #4499 is addressing more reasonable constraints for the result of match_with_constraint.
2. Issue Node merging to reduce branching for CSE #4425 is utilizing match_with_constraint to obtain the constraint substitution and anti-unify for merging nodes.

Open Questions

1. The Expected Anti-Unification result may not be optimal depending on the desired KCFG structure. It’s possible to place all constraints in either the CTerm or the CSubst. However, it may be more effective to differentiate constraints: common constraints should remain in the CTerm, while specific constraints should be in the respective CSubst. Consequently, X >Int 0 and Y >Int 5 should be in CSubst1 and CSubst2, respectively.
2. This function might be used for loop invariant generation. While it works well due to anti-unify’s termination properties (transforming specific CTerms into general CTerms with free variables and empty constraints), tightening the generated CTerm constraints could lead to non-termination or delayed termination but better loop-inv. We may need to prove termination for loop invariant generation.

Thank you for your attention to this matter.

[Stevengre]

I wrote a simple test for the issue. Currently, it can pass if match_with_constraint functions as expected. However, what I really want to discuss is the point mentioned in Open Question 1. I’m unsure how to precisely distinguish between common constraints and disjoint constraints without a solver. Can this be handled via RPC?

[Stevengre]

Additionally, as previously mentioned, we need to determine the specification of constraints desired for CTerm and CSubst in the context of KCFG.