RobSubstitution::match is unsound

[ibnyusuf]

Just discovered an unsoundness in RobSubstitution::match

vampire/Kernel/RobSubstitution.cpp

Line 470 in e979a7e

bool RobSubstitution::match(TermSpec base, TermSpec instance)

Function claims to successfully matc term f(g(x), x) with f(g(x),g(x)) when of course they are not matchable. To see this, please insert the following unit test into tUnificationWithAbstraction and see the result:

TEST_FUN(matching_test)
{
  RobSubstitution sub;
 
  unsigned f = function_symbol("f",2,AtomicSort::defaultSort()); 
  unsigned g = function_symbol("g",1,AtomicSort::defaultSort()); 

  TermList x = var(0);

  TermList gx = TermList(Term::create1(g,x));
  TermList fgxx = TermList(Term::create2(f,gx,x));  // f(g(x),x)
  TermList fgxgx = TermList(Term::create2(f,gx,gx)); // f(g(x),g(x))

  ASS(!sub.match(fgxx,0,fgxgx,0));
}

The issue is caused by the code ignoring pairs of terms with the same content. This is unsound when it comes to matching.

[joe-hauns]

Interesting. That's a good point to reimplement the function I guess, because it's quite long and messy.
I'll have a look as I wanted to do this at some point anyways.
It is to note that this doesn't make any of rules that rely on instantiation or generalization unsound/incomplete, as they use the Fast*Iterators which have their own way of generalizing that is not linked to RobSubstitution.

[MichaelRawson]

Awesome, thanks @joe-hauns ! If you don't get to it lmk and I'll do something (if only assert and crash), this seems quite critical to fix otherwise it will trip somebody up in future.

[ibnyusuf]

If we are re-implementing, we may want to consider introducing the same weight() check, that we have in Matcher::matchArgs(...)

vampire/Kernel/Matcher.hpp

Line 319 in e979a7e

if(base->weight() > instance->weight()) {

vampire/Kernel/Matcher.hpp

Line 362 in e979a7e

if(s->weight() > t->weight()) {

Why we have so many different matching routines is another topic for discussion!

[MichaelRawson]

@joe-hauns does #508 fix this, perhaps?