Refactoring and Extending Unification with Abstraction

[joe-hauns]

Main motivation for this PR was implementing our LPAR23 paper "Refining Unification With Abstraction". In this paper we introduced a new algorithm for unification with abstraction that generalizes the original unification with abstraction (UWA) algorithm, and gives us more control over how and when to perform UWA. For example in the old algorithm when unifying f(a + x + y) with f(b + a) we were only introduce a constraint a + x + y != b + a, while the new algorithm allows introducing the simplified constraint x + y != b straight away. Another example is unifying f(a + x + b) with f(b + a), where we now can straight derive the substitution { x -> 0 }, instead of introducing the constraint a + x + b != b + a. More examples motivation and explanation can be found in the paper.

In order to implement this new algorithm without compromising the performance of ordinary unification there are now two distinct unification algorithms:

• RobSubstition::unify classic Rob unification algorithm as we had before the first introduction of unification with abstraction
• AbstractingUnifier::unify the new unification with abstraction algorithm that we introduced in our LPAR23 paper

Additionally to do unification with abstraction as introduced in the paper we need to be able to create TermSpecs in unification that contain variables of two different variable banks: Say we want to unify x + f(y) <- var bank 0 and
f(y) <- var bank 1 Then an mgu is x -> -f(y/0) + f(y/1) This cannot be directly represented in vampire as our TermSpec can only hold 1 variable bank per term, and not multiple per subterm. So what we want to do instead is introduce two new glue variables varibles G0, G1

G0 -> -f(y)/0
G1 ->  f(y)/1

and return as mgu {x -> G0 + G1, G0 -> -f(y)/0, G1 -> f(y)/1} For this in RobSubstition we introduced a new constant GLUE_INDEX, and helper functions createTerm, and introGlueVariable.

Further quite a lot of tidying/refactoring around substitution trees and how they interface with UWA as well as some library code (e.g. Metaiterators that is being used there) has been done. The main changes are:

• Query Results: Whenevery we called unify on a substitution tree we used to get a SLQueryResult or a TermQueryResult which contains some data (TermList, Literal, Clause), as well as a unifier. The unifier used to always be a pair (Constraints, Substitution), no matter what query we used to make on the index. This means most of the time (e.g. when we didn't use unification with abstraction but normal unificatio, generalization, or instantiation we would get a nullpointer constraints). This means functions that deal with a {Term,Literal}QueryResult had to check with assertions whether the constraints are non-null and had callers of the functions had to know whether the functions can actually deal with constraints and so on. I moved this to be dealt with the typesystem now. Now TermQueryResult is parametrized by the unifier:

  • TQueryRes<AbstractingUnifier*> for unification with abstraction
  • TQueryRes<ResultSubstititionSP> for instantiation and generalization Same for `LiteralQueryResult. In the future I also want to split ResultSubstitution into UnifyingSubstitution, and GeneralizingSubstitution, as both of them have very different behaviour but use the same interface and just throw exceptions when the wrong function is called which is very hard to work with if you don't know the codebase well. Parametrizing The results will also allow for such a refactor.

  We have now different functions to query unfication with and without abstraction:

  VirtualIterator<          ResultSubstititionSP> getUnifications(TypedTermList lit, bool complementary, bool retrieveSubstitutions = true);
  VirtualIterator<TQueryRes<AbstractingUnifier*>> getUwa(TypedTermList t, Options::UnificationWithAbstraction uwa, bool fixedPointIteration);

• removal of various not needed fields and parameters in substitution tree that were associated with unification with abstraction but that are not needed anymore (e.g. useC that enabled making it possible to use unifiacion with abstraction with the related SubstitutionTree; we can now use UWA with and substitution tree hence we don't need the flag, rfSubs (this was related to very special variables which i got rid of all along), ...)

• shortened the RobSubstition code for apply and getApplicationResultWeight using BottomUpEvaluation instead of manual bottom up traversal. A performance bottlekneck that came from this change was how term sharing used to work: We create allocate term, then check if it already exists, and if so we deallocate it again and return the other one. In order to get rid of this unnecessary allocation i added functionality to Set to check whether an element exists before actually allocating it the relevant function is Set::rawFindOrInsert, and is documented in the hpp file.

• replaced VirtualIterator<void> by VirtualIterator<tuple<>>, in LookaheadLiteralSelector as this allows for it being usable in combination with IterTraits. I do not remember if/why this was needed and can change it back if anyone opposes for some reason.

• extended and optimized general functionality Coproduct.hpp & Option.hpp

• improved Recycler

• added macros to automatically implement Hash, Equals, and Comparison operators for custom types to Lib/Reflection.hpp

• added unit tests to UnitTests/tUnificationWithAbstraction.cpp (this is where +1000 lines comes from which makes the PR seem like it's adding loads of lines of code). The test in there also test UWA in the context of substition trees

[quickbeam123]

Some randomized testing with discount10 on TPTP:

Master: Expect 8746.846343722325 +/- 11.23557282358998
Branch: Expect 8763.348315603816 +/- 11.218682373124999

So some nice performance improvement!

[MichaelRawson]

Merge conflicts are probably due to my crude USE_ALLOCATOR deletion spree. Thinking about it I should have waited with that until this was in. Oh well - it's probably quite easy to fix @joe-hauns, if I've deleted a USE_ALLOCATOR it can probably go on this branch too unless you have some reason to believe it's worthwhile.

[joe-hauns]

Merge conflicts are probably due to my crude USE_ALLOCATOR deletion spree. Thinking about it I should have waited with that until this was in. Oh well - it's probably quite easy to fix @joe-hauns, if I've deleted a USE_ALLOCATOR it can probably go on this branch too unless you have some reason to believe it's worthwhile.

From my side all USE_ALLOCATOR calls can go. I just put them there to satisfy the old allocator and not get any assertion violations because of that.

[quickbeam123]

I tried to merge master in, to start a new round of tests (some bugs got fixed in master), but the merge felt tricky. Could you please do the merge when you have time?

[MichaelRawson]

From my side all USE_ALLOCATOR calls can go. I just put them there to satisfy the old allocator and not get any assertion violations because of that.

OK - my last deletion round was just the "obviously useless" ones - if you have any objects that are small and frequently allocated you might want to keep it for now otherwise you might dent performance on this branch without meaning to. Of course, the rest can go!