Preparation for CASC HOL 2026 #1

Indexing/CodeTreeInterfaces.cpp

@@ -163,22 +163,6 @@ VirtualIterator<QueryRes<ResultSubstitutionSP, Data>> CodeTreeTIS<higherOrder, D
   return vi( new ResultIterator(this, t, retrieveSubstitutions) );
 }
 
-template<bool higherOrder, class Data>
-bool CodeTreeTIS<higherOrder, Data>::generalizationExists(TermList t)
-{
-  if(_ct.isEmpty()) {
-    return false;
-  }
-
-  static typename TermCodeTree<higherOrder, Data>::TermMatcher tm;
-
-  tm.init(&_ct, t);
-  bool res=tm.next();
-  tm.reset();
-
-  return res;
-}
-
 template class CodeTreeTIS<false, TermLiteralClause>;
 template class CodeTreeTIS<true,  TermLiteralClause>;
 template class CodeTreeTIS<false, DemodulatorData>;

Indexing/CodeTreeInterfaces.hpp

@@ -50,8 +50,6 @@ class CodeTreeTIS : public TermIndexingStructure<Data>
   }
 
   VirtualIterator<QueryRes<ResultSubstitutionSP, Data>> getGeneralizations(TypedTermList t, bool retrieveSubstitutions = true) final ;
-  // TODO use TypedTermList here too
-  bool generalizationExists(TermList t) final ;
   // TODO: get rid of NOT_IMPLEMENTED
   VirtualIterator<QueryRes<AbstractingUnifier*, Data>> getUwa(TypedTermList t, Options::UnificationWithAbstraction, bool fixedPointIteration) override { NOT_IMPLEMENTED; }
 

Indexing/LiteralIndex.cpp

@@ -21,7 +21,6 @@
 #include "Kernel/MLVariant.hpp"
 #include "Kernel/Ordering.hpp"
 
-#include "LiteralIndexingStructure.hpp"
 #include "LiteralSubstitutionTree.hpp"
 #include "Saturation/SaturationAlgorithm.hpp"
 
@@ -332,7 +331,7 @@ void UnitIntegerComparisonLiteralIndex::handleClause(Clause* c, bool adding)
   Literal* lit = (*c)[0];
   ASS(lit != nullptr);
 
-  _is->handle(LiteralClause{ lit, c }, adding);
+  _is.handle(LiteralClause{ lit, c }, adding);
 }
 
 }

Indexing/LiteralIndex.hpp

@@ -21,7 +21,6 @@
 #include "Lib/DHMap.hpp"
 
 #include "Index.hpp"
-#include "LiteralIndexingStructure.hpp"
 
 namespace Indexing {
 
@@ -30,34 +29,40 @@ class LiteralIndex
 : public Index
 {
 public:
-  VirtualIterator<LiteralClause> getAll()
-  { return _is->getAll(); }
-
   VirtualIterator<QueryRes<ResultSubstitutionSP, LiteralClause>> getUnifications(Literal* lit, bool complementary, bool retrieveSubstitutions = true)
-  { return _is->getUnifications(lit, complementary, retrieveSubstitutions); }
+  { return _is.getUnifications(lit, complementary, retrieveSubstitutions); }
 
   VirtualIterator<QueryRes<AbstractingUnifier*, Data>> getUwa(Literal* lit, bool complementary, Options::UnificationWithAbstraction uwa, bool fixedPointIteration)
-  { return _is->getUwa(lit, complementary, uwa, fixedPointIteration); }
+  { return _is.getUwa(lit, complementary, uwa, fixedPointIteration); }
 
   VirtualIterator<QueryRes<ResultSubstitutionSP, LiteralClause>> getGeneralizations(Literal* lit, bool complementary, bool retrieveSubstitutions = true)
-  { return _is->getGeneralizations(lit, complementary, retrieveSubstitutions); }
+  { return _is.getGeneralizations(lit, complementary, retrieveSubstitutions); }
 
+  template<bool higherOrder>
   VirtualIterator<QueryRes<ResultSubstitutionSP, LiteralClause>> getInstances(Literal* lit, bool complementary, bool retrieveSubstitutions = true)
-  { return _is->getInstances(lit, complementary, retrieveSubstitutions); }
-
-  size_t getUnificationCount(Literal* lit, bool complementary)
-  { return _is->getUnificationCount(lit, complementary); }
+  {
+    if constexpr (higherOrder) {
+      // TODO(HOL): implement proper higher-order matching here
+      // we override retrieveSubstitutions because we need the substitution for the aftercheck
+      return pvi(iterTraits(_is.getInstances(lit, complementary, /*retrieveSubstitutions=*/true))
+        .filter([lit](auto qr) {
+          return iterTraits(VariableIterator(lit)).all([&qr](TermList var) {
+            return !qr.unifier->applyToBoundQuery(var).containsLooseDBIndex();
+          });
+        }));
+    } else {
+      return _is.getInstances(lit, complementary, retrieveSubstitutions);
+    }
+  }
 
-  friend std::ostream& operator<<(std::ostream& out,                 LiteralIndex const& self) { return out << *self._is; }
-  friend std::ostream& operator<<(std::ostream& out, Output::Multiline<LiteralIndex>const& self) { return out << Output::multiline(*self.self._is, self.indent); }
+  friend std::ostream& operator<<(std::ostream& out,                 LiteralIndex const& self) { return out << self._is; }
+  friend std::ostream& operator<<(std::ostream& out, Output::Multiline<LiteralIndex>const& self) { return out << Output::multiline(self.self._is, self.indent); }
 
 protected:
-  LiteralIndex() : _is(new LiteralSubstitutionTree<LiteralClause>()) {}
-
   void handle(Data data, bool add)
-  { _is->handle(std::move(data), add); }
+  { _is.handle(std::move(data), add); }
 
-  std::unique_ptr<LiteralIndexingStructure<Data>> _is;
+  LiteralSubstitutionTree<LiteralClause> _is;
 };
 
 class BinaryResolutionIndex

Indexing/LiteralSubstitutionTree.hpp

@@ -21,16 +21,14 @@
 #include "Kernel/UnificationWithAbstraction.hpp"
 #include "Lib/Metaiterators.hpp"
 #include "Lib/VirtualIterator.hpp"
-#include "LiteralIndexingStructure.hpp"
 #include "SubstitutionTree.hpp"
 #include "Kernel/Signature.hpp"
 
 namespace Indexing {
 
-/** A wrapper class around SubstitutionTree that makes it usable  as a LiteralIndexingStructure */
+/** A wrapper class around SubstitutionTree that makes it usable a literal index */
 template<class LeafData_>
 class LiteralSubstitutionTree
-: public LiteralIndexingStructure<LeafData_>
 {
   using SubstitutionTree = Indexing::SubstitutionTree<LeafData_>;
   using LeafData         = LeafData_;
@@ -47,30 +45,22 @@ class LiteralSubstitutionTree
     : _trees(env.signature->predicates() * 2)
     { }
 
-  void handle(LeafData ld, bool insert) final
+  void handle(LeafData ld, bool insert)
   { getTree(ld.key(), /* complementary */ false).handle(std::move(ld), insert); }
 
-  VirtualIterator<LeafData> getAll() final
-  {
-    return pvi(
-          iterTraits(getRangeIterator((unsigned long)0, _trees.size()))
-           .flatMap([this](auto i) { return LeafIterator(_trees[i].get()); })
-           .flatMap([](Leaf* l) { return l->allChildren(); })
-           // TODO get rid of copying data here
-           .map([](LeafData const* ld) { return *ld; })
-        );
-  }
+  void insert(LeafData ld) { handle(std::move(ld), /* insert = */ true ); }
+  void remove(LeafData ld) { handle(std::move(ld), /* insert = */ false); }
 
-  VirtualIterator<QueryRes<ResultSubstitutionSP, LeafData_>> getUnifications(Literal* lit, bool complementary, bool retrieveSubstitutions) final
+  VirtualIterator<QueryRes<ResultSubstitutionSP, LeafData_>> getUnifications(Literal* lit, bool complementary, bool retrieveSubstitutions)
   { return pvi(getResultIterator<typename SubstitutionTree::template Iterator<RetrievalAlgorithms::RobUnification<RetrievalAlgorithms::DefaultVarBanks>>>(lit, complementary, retrieveSubstitutions)); }
 
-  VirtualIterator<QueryRes<ResultSubstitutionSP, LeafData>> getGeneralizations(Literal* lit, bool complementary, bool retrieveSubstitutions) final
+  VirtualIterator<QueryRes<ResultSubstitutionSP, LeafData>> getGeneralizations(Literal* lit, bool complementary, bool retrieveSubstitutions)
   { return pvi(getResultIterator<FastGeneralizationsIterator>(lit, complementary, retrieveSubstitutions)); }
 
-  VirtualIterator<QueryRes<ResultSubstitutionSP, LeafData>> getInstances(Literal* lit, bool complementary, bool retrieveSubstitutions) final
+  VirtualIterator<QueryRes<ResultSubstitutionSP, LeafData>> getInstances(Literal* lit, bool complementary, bool retrieveSubstitutions)
   { return pvi(getResultIterator<FastInstancesIterator>(lit, complementary, retrieveSubstitutions)); }
 
-  VirtualIterator<QueryRes<ResultSubstitutionSP, LeafData>> getVariants(Literal* query, bool complementary, bool retrieveSubstitutions) final
+  VirtualIterator<QueryRes<ResultSubstitutionSP, LeafData>> getVariants(Literal* query, bool complementary, bool retrieveSubstitutions)
   {
     return pvi(iterTraits(getTree(query, complementary).getVariants(query, retrieveSubstitutions)));
   }
@@ -104,7 +94,7 @@ class LiteralSubstitutionTree
 
 public:
 
-  VirtualIterator<QueryRes<AbstractingUnifier*, LeafData>> getUwa(Literal* lit, bool complementary, Options::UnificationWithAbstraction uwa, bool fixedPointIteration) final
+  VirtualIterator<QueryRes<AbstractingUnifier*, LeafData>> getUwa(Literal* lit, bool complementary, Options::UnificationWithAbstraction uwa, bool fixedPointIteration)
   { 
     auto unif = Lib::make_shared(AbstractingUnifier::empty(AbstractionOracle(uwa)));
     return pvi(getResultIterator<typename SubstitutionTree::template Iterator<RetrievalAlgorithms::UnificationWithAbstraction<AbstractingUnifier*, RetrievalAlgorithms::DefaultVarBanks>>>(lit, complementary, /* retrieveSubstitutions */ true,  unif.get(), AbstractionOracle(uwa), fixedPointIteration)
@@ -143,15 +133,14 @@ class LiteralSubstitutionTree
     return out << "} ";
   }
 
-  void output(std::ostream& out, Option<unsigned> multilineIndent) const override {
+  void output(std::ostream& out, Option<unsigned> multilineIndent) const {
     if (multilineIndent) {
       out << Output::multiline(*this, *multilineIndent);
     } else {
       out << *this;
     }
   }
 
-
 private:
   SubstitutionTree& getTree(Literal* lit, bool complementary)
   {

Indexing/SubstitutionTree.hpp

@@ -620,14 +620,6 @@ class SubstitutionTree final
       { out << "{ _query: " << _query << ", _result: " << _result << " }"; }
     };
 
-    template<class Query>
-    bool generalizationExists(Query query)
-    {
-      return _root == nullptr 
-        ? false
-        : FastGeneralizationsIterator(this, _root, query, /* retrieveSubstitutions */ false, /* reversed */ false).hasNext();
-    }
-
     template<class Query>
     VirtualIterator<QueryRes<ResultSubstitutionSP, LeafData>> getVariants(Query query, bool retrieveSubstitutions)
     {

Indexing/TermIndex.hpp

@@ -26,8 +26,6 @@ class TermIndex
 : public Index
 {
 public:
-  ~TermIndex() override {}
-
   VirtualIterator<QueryRes<AbstractingUnifier*, Data>> getUwa(TypedTermList t, Options::UnificationWithAbstraction uwa, bool fixedPointIteration)
   { return _is->getUwa(t, uwa, fixedPointIteration); }
 
@@ -37,8 +35,22 @@ class TermIndex
   VirtualIterator<QueryRes<ResultSubstitutionSP, Data>> getGeneralizations(TypedTermList t, bool retrieveSubstitutions = true)
   { return _is->getGeneralizations(t, retrieveSubstitutions); }
 
+  template<bool higherOrder>
   VirtualIterator<QueryRes<ResultSubstitutionSP, Data>> getInstances(TypedTermList t, bool retrieveSubstitutions = true)
-  { return _is->getInstances(t, retrieveSubstitutions); }
+  {
+    if constexpr (higherOrder) {
+      // TODO(HOL): implement proper higher-order matching here
+      // we override retrieveSubstitutions because we need the substitution for the aftercheck
+      return pvi(iterTraits(_is->getInstances(t, /*retrieveSubstitutions=*/true))
+        .filter([t](auto qr) {
+          return iterTraits(VariableIterator(t)).all([&qr](TermList var) {
+            return !qr.unifier->applyToBoundQuery(var).containsLooseDBIndex();
+          });
+        }));
+    } else {
+      return _is->getInstances(t, retrieveSubstitutions);
+    }
+  }
 
   friend std::ostream& operator<<(std::ostream& out, TermIndex const& self)
   { return out << *self._is; }

Indexing/TermIndexingStructure.hpp

@@ -35,8 +35,6 @@ class TermIndexingStructure {
   virtual VirtualIterator<QueryRes<ResultSubstitutionSP, Data>> getGeneralizations(TypedTermList t, bool retrieveSubstitutions = true) { NOT_IMPLEMENTED; }
   virtual VirtualIterator<QueryRes<ResultSubstitutionSP, Data>> getInstances(TypedTermList t, bool retrieveSubstitutions = true) { NOT_IMPLEMENTED; }
 
-  virtual bool generalizationExists(TermList t) { NOT_IMPLEMENTED; }
-
   virtual void output(std::ostream& output) const = 0;
 
   friend std::ostream& operator<<(std::ostream& out, TermIndexingStructure const& self)

Indexing/TermSharing.cpp

@@ -133,6 +133,8 @@ void TermSharing::computeAndSetSharedTermData(Term* t)
     t->setHasLambda(hasLambda);
     t->setInterpretedConstantsPresence(hasInterpretedConstants);
 
+    ASS_REP(!env.higherOrder() || t->isApplication() || t->isLambdaTerm() || !t->numTermArguments(), "HO term " + t->toString() + " is not appified");
+
     //poly function works for mono as well, but is slow
     //it is fine to use for debug
     ASS_REP(_wellSortednessCheckingDisabled || SortHelper::areImmediateSortsValidPoly(t), t->toString());

Indexing/TermSubstitutionTree.hpp

@@ -67,9 +67,6 @@ class TermSubstitutionTree
   { return iterTraits(_inner.template iterator<Iterator>(query, retrieveSubstitutions, /* reversed */  false, std::move(args)...))
       ; }
 
-  bool generalizationExists(TermList t) override
-  { return t.isVar() ? false : _inner.generalizationExists(TypedTermList(t.term())); }
-
   void output(std::ostream& out) const final { out << *this; }
 
   friend std::ostream& operator<<(std::ostream& out, TermSubstitutionTree<LeafData_> const& self)

Inferences/BackwardDemodulation.cpp

@@ -178,7 +178,8 @@ void BackwardDemodulation<higherOrder>::perform(Clause* cl,
 	    getMappingIterator(
 		    getMapAndFlattenIterator(
 			    EqHelper::getDemodulationLHSIterator(lit, _preordered, _ord).first,
-			    [this](TypedTermList lhs){ return pvi( pushPairIntoRightIterator(lhs, _index->getInstances(lhs, true)) ); }),
+			    [this](TypedTermList lhs)
+          { return pvi( pushPairIntoRightIterator(lhs, _index->template getInstances<higherOrder>(lhs, true)) ); }),
 		    ResultFn(cl, *this, _helper)),
  	      [](BwSimplificationRecord arg){ return arg.toRemove!=0; }));