Separate generalizing term index and use code trees

Indexing/CodeTree.cpp

@@ -638,7 +638,7 @@ bool CodeTree::Matcher<removing, checkRange, higherOrder>::execute()
 }
 
 template<bool removing, bool checkRange, bool higherOrder>
-void CodeTree::Matcher<removing, checkRange, higherOrder>::init(CodeTree* tree_, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, Stack<CodeOp*>* firstsInBlocks_)
+void CodeTree::Matcher<removing, checkRange, higherOrder>::init(CodeTree const* tree_, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, Stack<CodeOp*>* firstsInBlocks_)
 {
   tree=tree_;
   entry=entry_;

Indexing/CodeTree.hpp

@@ -382,7 +382,7 @@ class CodeTree
     }
 
   protected:
-    void init(CodeTree* tree_, CodeOp* entry_, LitInfo* linfos_ = 0,
+    void init(CodeTree const* tree_, CodeOp* entry_, LitInfo* linfos_ = 0,
       size_t linfoCnt_ = 0, Stack<CodeOp*>* firstsInBlocks_ = 0);
 
     bool backtrack();
@@ -416,7 +416,7 @@ class CodeTree
     Stack<std::conditional_t<removing,BTPointRemoving,BTPoint>> btStack;
 
     CodeOp* entry;
-    CodeTree* tree;
+    CodeTree const* tree;
 
     /**
      * Array of alternative LitInfo objects

Indexing/CodeTreeInterfaces.cpp

@@ -14,14 +14,13 @@
  */
 
 #include "Indexing/Index.hpp"
-#include "Indexing/ResultSubstitution.hpp"
+#include "Inferences/ALASCA/Demodulation.hpp"
 #include "Lib/Allocator.hpp"
 #include "Lib/Recycled.hpp"
 #include "Debug/TimeProfiling.hpp"
 #include "Lib/VirtualIterator.hpp"
 
 #include "Kernel/Renaming.hpp"
-#include "Kernel/SubstHelper.hpp"
 #include "Kernel/Term.hpp"
 
 #include "ClauseCodeTree.hpp"
@@ -35,70 +34,19 @@ namespace Indexing
 using namespace Lib;
 using namespace Kernel;
 
-template<class Data>
-class CodeTreeSubstitution
-: public ResultSubstitution
-{
-public:
-  CodeTreeSubstitution(CodeTree::BindingArray* bindings, Renaming* resultNormalizer)
-  : _bindings(bindings), _resultNormalizer(resultNormalizer)
-  {}
-
-  USE_ALLOCATOR(CodeTreeSubstitution);
-
-  TermList apply(unsigned var)
-  {
-    if constexpr (is_indexed_data_normalized<Data>::value) {
-      return (*_bindings)[var];
-    } else {
-      ASS(_resultNormalizer->contains(var));
-      unsigned nvar=_resultNormalizer->get(var);
-      TermList res=(*_bindings)[nvar];
-      ASS(res.isTerm()||res.isOrdinaryVar());
-      ASSERT_VALID(res);
-      return res;
-    }
-  }
-
-  TermList applyToBoundResult(unsigned v) override
-  {
-    return apply(v);
-  }
-
-  TermList applyToBoundResult(TermList t) override
-  {
-    return SubstHelper::apply(t, *this);
-  }
-
-  Literal* applyToBoundResult(Literal* lit) override
-  {
-    return SubstHelper::apply(lit, *this);
-  }
-
-  bool isIdentityOnQueryWhenResultBound() override {return true;}
-private:
-  void output(std::ostream& out) const final
-  { out << "CodeTreeSubstitution(<output unimplemented>)"; }
-
-  CodeTree::BindingArray* _bindings;
-  Renaming* _resultNormalizer;
-};
-
-///////////////////////////////////////
-
 template<bool higherOrder, class Data>
 class CodeTreeTIS<higherOrder, Data>::ResultIterator
-: public IteratorCore<QueryRes<ResultSubstitutionSP, Data>>
+: public IteratorCore<QueryRes<const GenSubstitution<Data>*, Data>>
 {
 public:
-  ResultIterator(CodeTreeTIS* tree, TermList t, bool retrieveSubstitutions)
+  ResultIterator(const CodeTreeTIS& tree, TypedTermList t, bool retrieveSubstitutions)
   : _retrieveSubstitutions(retrieveSubstitutions),
     _found(0), _finished(false), _tree(tree)
   {
-    _matcher->init(&_tree->_ct, t);
+    _matcher->init(&_tree._ct, t);
 
     if(_retrieveSubstitutions) {
-      _subst = new CodeTreeSubstitution<Data>(&_matcher->bindings, &*_resultNormalizer);
+      _subst = new GenSubstitution<Data>(&_matcher->bindings, &*_resultNormalizer);
     }
   }
 
@@ -126,47 +74,45 @@ class CodeTreeTIS<higherOrder, Data>::ResultIterator
     return _found;
   }
 
-  QueryRes<ResultSubstitutionSP, Data> next() override
+  QueryRes<const GenSubstitution<Data>*, Data> next() override
   {
     ASS(_found);
 
-    ResultSubstitutionSP subs;
     if (_retrieveSubstitutions) {
       if constexpr (!is_indexed_data_normalized<Data>::value) {
         _resultNormalizer->reset();
-        _resultNormalizer->normalizeVariables(_found->term);
+        _resultNormalizer->normalizeVariables(_found->key());
       }
-      subs = ResultSubstitutionSP(_subst, /* nondisposable */ true);
     }
-    auto out = QueryRes<ResultSubstitutionSP, Data>(subs, _found);
+    auto out = QueryRes<const GenSubstitution<Data>*, Data>(_subst, _found);
     _found=0;
     return out;
   }
 private:
-
-  CodeTreeSubstitution<Data>* _subst;
+  GenSubstitution<Data>* _subst = nullptr;
   Recycled<Renaming> _resultNormalizer;
   bool _retrieveSubstitutions;
   Data* _found;
   bool _finished;
-  CodeTreeTIS* _tree;
+  const CodeTreeTIS& _tree;
   Recycled<typename TermCodeTree<higherOrder, Data>::TermMatcher> _matcher;
 };
 
 template<bool higherOrder, class Data>
-VirtualIterator<QueryRes<ResultSubstitutionSP, Data>> CodeTreeTIS<higherOrder, Data>::getGeneralizations(TypedTermList t, bool retrieveSubstitutions)
+VirtualIterator<QueryRes<const GenSubstitution<Data>*, Data>> CodeTreeTIS<higherOrder, Data>::getGeneralizations(TypedTermList t, bool retrieveSubstitutions) const
 {
   if(_ct.isEmpty()) {
-    return VirtualIterator<QueryRes<ResultSubstitutionSP, Data>>::getEmpty();
+    return VirtualIterator<QueryRes<const GenSubstitution<Data>*, Data>>::getEmpty();
   }
 
-  return vi( new ResultIterator(this, t, retrieveSubstitutions) );
+  return vi( new ResultIterator(*this, t, retrieveSubstitutions) );
 }
 
 template class CodeTreeTIS<false, TermLiteralClause>;
 template class CodeTreeTIS<true,  TermLiteralClause>;
 template class CodeTreeTIS<false, DemodulatorData>;
 template class CodeTreeTIS<true,  DemodulatorData>;
+template class CodeTreeTIS<false, Inferences::ALASCA::Demodulation::Lhs>;
 template class CodeTreeTIS<true,  TermWithValue<TermList>>;
 
 /////////////////   CodeTreeSubsumptionIndex   //////////////////////

Indexing/CodeTreeInterfaces.hpp

@@ -21,25 +21,57 @@
 #include "ClauseCodeTree.hpp"
 
 #include "Index.hpp"
-#include "TermIndexingStructure.hpp"
 
 namespace Indexing
 {
 
 using namespace Kernel;
 using namespace Lib;
 
+template<class Data>
+class GenSubstitution
+  : public SubstApplicator
+{
+public:
+  GenSubstitution(CodeTree::BindingArray* bindings, Renaming* resultNormalizer)
+  : _bindings(bindings), _resultNormalizer(resultNormalizer) {}
+
+  USE_ALLOCATOR(GenSubstitution);
+
+  TermList apply(unsigned var) const override {
+    if constexpr (is_indexed_data_normalized<Data>::value) {
+      return (*_bindings)[var];
+    } else {
+      ASS(_resultNormalizer->contains(var));
+      unsigned nvar=_resultNormalizer->get(var);
+      TermList res=(*_bindings)[nvar];
+      ASS(res.isTerm()||res.isOrdinaryVar());
+      ASSERT_VALID(res);
+      return res;
+    }
+  }
+
+  TermList apply(TermList t) const {
+    return SubstHelper::apply(t, *this);
+  }
+
+  Literal* apply(Literal* lit) const {
+    return SubstHelper::apply(lit, *this);
+  }
+private:
+  CodeTree::BindingArray* _bindings;
+  Renaming* _resultNormalizer;
+};
 
 /**
  * Term indexing structure using code trees to retrieve generalizations
  */
-
 template<bool higherOrder, class Data>
-class CodeTreeTIS : public TermIndexingStructure<Data>
+class CodeTreeTIS
 {
 public:
   /* INFO: we ignore unifying the sort of the keys here */
-  void handle(Data data, bool insert) final
+  void handle(Data data, bool insert)
   {
     if (insert) {
       auto ti = new Data(std::move(data));
@@ -49,12 +81,9 @@ class CodeTreeTIS : public TermIndexingStructure<Data>
     }
   }
 
-  VirtualIterator<QueryRes<ResultSubstitutionSP, Data>> getGeneralizations(TypedTermList t, bool retrieveSubstitutions = true) final ;
-  // TODO: get rid of NOT_IMPLEMENTED
-  VirtualIterator<QueryRes<AbstractingUnifier*, Data>> getUwa(TypedTermList t, Options::UnificationWithAbstraction, bool fixedPointIteration, bool funcExt) override { NOT_IMPLEMENTED; }
-  VirtualIterator<QueryRes<AbstractingUnifier*, Data>> getUwaHOL(TypedTermList t, Options::UnificationWithAbstraction, bool fixedPointIteration, unsigned hoUnifDepth, bool funcExt) override { NOT_IMPLEMENTED; }
+  VirtualIterator<QueryRes<const GenSubstitution<Data>*, Data>> getGeneralizations(TypedTermList t, bool retrieveSubstitutions = true) const;
 
-  void output(std::ostream& out) const final { out << _ct; }
+  void output(std::ostream& out) const { out << _ct; }
 
 private:
   class ResultIterator;

Indexing/Index.hpp

@@ -95,7 +95,7 @@ struct TermLiteralClause
   Literal* literal = nullptr;
   Clause* clause = nullptr;
 
-  TypedTermList const& key() const { return term; }
+  TypedTermList key() const { return term; }
 
   auto  asTuple() const
   { return std::make_tuple(clause->number(), literal->getId(), term); }
@@ -114,7 +114,7 @@ struct TermLiteralClause
  * left- and right-hand side normalized and cache preorderedness. */
 struct DemodulatorData
 {
-  DemodulatorData(TypedTermList term, TermList rhs, Clause* clause, bool preordered, const Ordering& ord)
+  DemodulatorData(TypedTermList term, TypedTermList rhs, Clause* clause, bool preordered, const Ordering& ord)
     : term(term), rhs(rhs), clause(clause), preordered(preordered), tod(ord.createTermOrderingDiagram())
   {
     // insert pointer to owner as non-null value representing success

Indexing/IndexManager.cpp

@@ -31,7 +31,7 @@
 using namespace Lib;
 using namespace Indexing;
 
-SIMP_INDEX_IMPL(AlascaIndex<ALASCA::Demodulation::Lhs>)
+SIMP_INDEX_IMPL(GeneralizingAlascaIndex<ALASCA::Demodulation::Lhs>)
 SIMP_INDEX_IMPL(AlascaIndex<ALASCA::Demodulation::Rhs>)
 SIMP_INDEX_IMPL(DemodulationLHSIndex<false>)
 SIMP_INDEX_IMPL(DemodulationLHSIndex<true>)