Storing Custom Data in SubstitutionTree and friends

[joe-hauns]

This PR refactors substitution trees (and the respective Index interfaces) so we can store arbitrary data in the leaves.

A substitution tree can be thought of a special map Map<Key,Value> with Key being something we can decompose into substitutions, and then perform unification with (i.e. currently in vampire we have Key in { Literal*, TypedTermList}). Up to this PR Value used to be fixed: a tuple (TermList, Literal*, Clause*) (called LeafData). This makes sense for some use cases (i.e. some inference rules), but not for all of them. This lead to the fact that e.g. in many inference rules the data (TermList(t), nullptr, nullptr) was being inserted which is a waste of memory, and leads to bugs as we always have to check whether there are null values present or not. Further always having this fixed Value data was rather unflexible, as we cannot store more (or different) information than (TermList, Literal*, Clause*) to compute an inference. An examples where more/different data needs to be stored are

• the Fourier Motzkin Rule from the ALASCA caluclus (PR coming some time after this)
• the data TermList _extra that has been added for some higher-order inferences
• if i remember correctly there was also the need for something like this from @mezpusz in his work on induction.

This PR introduces a type parameter LeafData to Substitution, Index and friends which makes the changes described above possible, and at the same time simplifies the SubstitutionTree interface quite a bit. The default old leaf data class is still exists as Indexing::TermLiteralClause for term indices and Indexing::LiteralClause for Literal indices. Further I introduced Indexing::TermWithValue<V> which can be used if you want to have a term as a key, and some other value associated with it. Additionally there is Indexing::TermWithoutValue if you want to consider the SubstitutionTree as a set and not a map.

[MichaelRawson]

@mezpusz and @RobCoutel - I think you have demodulation/induction and SAT subsumption branches respectively that might benefit from this and/or need some modification. You might want to keep an eye on this PR's progress.

[MichaelRawson]

I think merging @mezpusz's branch broke this one, sorry @joe-hauns - are we ready to go otherwise?

[joe-hauns]

merged master again! Everthing's clear from my side.

[quickbeam123]

Hey hey, just warming up on this:

In file included from SAT/MinisatInterfacing.cpp:15:
In file included from SAT/MinisatInterfacing.hpp:17:
In file included from SAT/SATSolver.hpp:18:
In file included from SAT/SATLiteral.hpp:21:
In file included from ./Shell/Options.hpp:43:
In file included from ./Forwards.hpp:18:
In file included from ./Lib/VString.hpp:26:
In file included from ./Lib/STLAllocator.hpp:27:
In file included from ./Lib/Allocator.hpp:26:
./Debug/Assertion.hpp:269:36: error: call to function 'operator<<' that is neither visible in the template definition nor found by argument-dependent lookup
              << val1Str << " == " << val1 << "\n"
                                   ^
./Kernel/Term.hpp:376:37: note: in instantiation of function template specialization 'Debug::Assertion::violatedEquality<Kernel::Term::SpecialFunctor, Kernel::Term::SpecialFunctor>' requested here
    Formula* getCondition() const { ASS_EQ(specialFunctor(), SpecialFunctor::ITE); return _iteData.condition; }
                                    ^
./Debug/Assertion.hpp:87:25: note: expanded from macro 'ASS_EQ'
      Debug::Assertion::violatedEquality(__FILE__, __LINE__, #VAL1, #VAL2, VAL1, VAL2); \
                        ^
./Kernel/Term.hpp:1159:15: note: 'operator<<' should be declared prior to the call site or in namespace 'Kernel'
std::ostream& operator<<(std::ostream& out, Kernel::Term::SpecialFunctor const& self);

[joe-hauns]

How are you compiling this? I'm not getting the warning using clang, or gcc, in either release or debug mode.

[quickbeam123]

Sorry, a false alarm. Something must have been not up to date in my repo.