Performance on First Order Problems

[hargoniX]

I was playing around with the latest version of duper today and gave it this problem (pb34.p from the Pelletier Problem set mined in zipperposition) which is quite hard even for high end tools like E:

% Andrew`s Challenge

fof(goal, conjecture,
  ((? [X] : ! [Y] : (p(X) <=> p(Y))) <=>
   ((? [X] : q(X)) <=> ! [Y] : p(Y)))
  <=>
  ((? [X] : ! [Y] : (q(X) <=> q(Y))) <=>
   ((? [X] : p(X)) <=> ! [Y] : q(Y)))
).

duper wasn't able to solve it (which is fine) but I saw something interesting in the profile that came from this:

as you can see this is quite bound on subsumption checks and particular litsMatch. within litsMatch there is a call to betaEtaReduceInstMVars that takes up a lot of the time here. However this call is a noop (though an O(n) one as we still traverse the entire term) for this problem as no lambdas are actually syntactically present (I checked this by instrumenting the call sites). So we could in principle skip this check if we knew about this a priori.

Naively looking at the issue I would suggest to cache two flags in Lit that tells you whether the lhs/rhs might be beta/eta reducible by checking for the presence of lambdas on creation once and then only performing the reduction if this flag says yes we might need to do some work.

Implementing this change is a bit non trivial as there is a lot of locations in the code base that just blindly reach into literals using with notation so I believe the easiest way to go here would be to make the Lit constructor private, expose a new function that has the same signature as the old constructor but computes the flags on the fly and finally replace all calls to with notation with functions on Lit that take care of fixing up the flag. In addition to that it might make sense to try and persist the flag from one literal to a new one instead of re-computing it once upon creation (even though just doing this should already provide a speedup as it will be computed once per literal in the active set and not thousands or even more times).