Adapt equality factoring for HOL unification

Indexing/TermSubstitutionTree.hpp

@@ -91,7 +91,7 @@ class TermSubstitutionTree
   auto getUwaHOL(TypedTermList t, Options::UnificationWithAbstraction uwa, bool fixedPointIteration, unsigned hoUnifDepth, bool funcExt)
   {
     return pvi(iterTraits(getUwa(t, uwa, fixedPointIteration, funcExt))
-      .flatMap([hoUnifDepth,funcExt](QueryRes<AbstractingUnifier*, LeafData> qr) { return pvi(pushPairIntoRightIterator(qr, vi(new HOL::AbstractingWrapper(qr.unifier, hoUnifDepth, funcExt)))); })
+      .flatMap([hoUnifDepth,funcExt](QueryRes<AbstractingUnifier*, LeafData> qr) { return pvi(pushPairIntoRightIterator(qr, vi(new HOL::AbstractingWrapper(*qr.unifier, hoUnifDepth, funcExt)))); })
       .map([](auto arg) { return queryRes(arg.second, arg.first.data); }));
   }
 

Inferences/EqualityFactoring.cpp

@@ -21,6 +21,7 @@
 
 #include "Kernel/Clause.hpp"
 #include "Kernel/EqHelper.hpp"
+#include "Kernel/HOL/Unifier.hpp"
 #include "Kernel/Inference.hpp"
 #include "Kernel/Ordering.hpp"
 #include "Kernel/RobSubstitution.hpp"
@@ -40,156 +41,113 @@ using namespace Indexing;
 using namespace Saturation;
 using std::pair;
 
-EqualityFactoring::EqualityFactoring(SaturationAlgorithm& salg)
-  : _salg(salg)
-  , _abstractionOracle(_salg.getOptions().unificationWithAbstraction())
-  , _uwaFixedPointIteration(_salg.getOptions().unificationWithAbstractionFixedPointIteration())
-{}
-
-struct EqualityFactoring::IsPositiveEqualityFn
-{
-  bool operator()(Literal* l)
-  { return l->isEquality() && l->isPositive(); }
-};
-struct EqualityFactoring::IsDifferentPositiveEqualityFn
-{
-  IsDifferentPositiveEqualityFn(Literal* lit) : _lit(lit) {}
-  bool operator()(Literal* l2)
-  { return l2->isEquality() && l2->polarity() && l2!=_lit; }
-private:
-  Literal* _lit;
-};
-
-struct EqualityFactoring::FactorablePairsFn
-{
-  FactorablePairsFn(Clause* cl) : _cl(cl) {}
-  VirtualIterator<pair<pair<Literal*,TermList>,pair<Literal*,TermList> > > operator() (pair<Literal*,TermList> arg)
-  {
-    auto it1 = _cl->iterLits();
-
-    auto it2 = getFilteredIterator(it1,IsDifferentPositiveEqualityFn(arg.first));
-
-    auto it3 = getMapAndFlattenIterator(it2,EqHelper::EqualityArgumentIteratorFn());
-
-    auto it4 = pushPairIntoRightIterator(arg,std::move(it3));
+constexpr unsigned kVarBank = 0;
 
-    return pvi( std::move(it4) );
-  }
-private:
-  Clause* _cl;
-};
+namespace {
 
-struct EqualityFactoring::ResultFn
+Clause* unifierToClause(Clause* cl, TermList srt, Literal* sLit, TermList sLHS, Literal* fLit, TermList fLHS, AbstractingUnifier* absUnif, const Ordering& ord, const bool afterCheck)
 {
-  ResultFn(EqualityFactoring& self, Clause* cl, bool afterCheck, Ordering& ordering, bool fixedPointIteration)
-      : _self(self), _cl(cl), _cLen(cl->length()), _afterCheck(afterCheck), _ordering(ordering), _fixedPointIteration(fixedPointIteration) {}
-  Clause* operator() (pair<pair<Literal*,TermList>,pair<Literal*,TermList> > arg)
-  {
-    auto absUnif = AbstractingUnifier::empty(_self._abstractionOracle);
-    Literal* sLit=arg.first.first;  // selected literal ( = factored-out literal )
-    Literal* fLit=arg.second.first; // fairly boring side literal
-    ASS(sLit->isEquality());
-    ASS(fLit->isEquality());
-
-
-    TermList srt = SortHelper::getEqualityArgumentSort(sLit);
-
-    if (!absUnif.unifyOnce(srt, 0, SortHelper::getEqualityArgumentSort(fLit), 0)) {
-      return 0;
-    }
-
+  TermList srtS = absUnif->subs().apply(srt,kVarBank);
+  TermList sLHSS = absUnif->subs().apply(sLHS,kVarBank);
+  TermList sRHSS = absUnif->subs().apply(EqHelper::getOtherEqualitySide(sLit, sLHS),kVarBank);
+  if(Ordering::isGreaterOrEqual(ord.compare(sRHSS,sLHSS))) {
+    return nullptr;
+  }
+  auto fRHS = EqHelper::getOtherEqualitySide(fLit, fLHS);
+  TermList fRHSS = absUnif->subs().apply(fRHS,kVarBank);
+  if(Ordering::isGreaterOrEqual(ord.compare(fRHSS,sLHSS))) {
+    return nullptr;
+  }
+  auto constraints = absUnif->computeConstraintLiterals();
 
-    TermList sLHS=arg.first.second;
-    TermList sRHS=EqHelper::getOtherEqualitySide(sLit, sLHS);
-    TermList fLHS=arg.second.second;
-    TermList fRHS=EqHelper::getOtherEqualitySide(fLit, fLHS);
-    ASS_NEQ(sLit, fLit);
+  RStack<Literal*> resLits;
+  resLits->push(Literal::createEquality(false, sRHSS, fRHSS, srtS));
 
-    if(!absUnif.unifyOnce(sLHS,0,fLHS,0)) {
-      return 0;
-    }
+  Literal* sLitAfter = 0;
+  if (afterCheck && cl->numSelected() > 1) {
+    TIME_TRACE(TimeTrace::LITERAL_ORDER_AFTERCHECK);
+    sLitAfter = absUnif->subs().apply(sLit, kVarBank);
+  }
 
-    if (_fixedPointIteration && !absUnif.fixedPointIteration()) {
-      return nullptr;
+  for (unsigned i = 0; i < cl->length(); i++) {
+    Literal* curr = (*cl)[i];
+    if (curr == sLit) {
+      continue;
     }
+    Literal* currAfter = absUnif->subs().apply(curr, kVarBank);
 
-    TermList srtS = absUnif.subs().apply(srt,0);
-    TermList sLHSS = absUnif.subs().apply(sLHS,0);
-    TermList sRHSS = absUnif.subs().apply(sRHS,0);
-    if(Ordering::isGreaterOrEqual(_ordering.compare(sRHSS,sLHSS))) {
-      return 0;
-    }
-    TermList fRHSS = absUnif.subs().apply(fRHS,0);
-    if(Ordering::isGreaterOrEqual(_ordering.compare(fRHSS,sLHSS))) {
-      return 0;
-    }
-    auto constraints = absUnif.computeConstraintLiterals();
-
-    RStack<Literal*> resLits;
-
-    resLits->push(Literal::createEquality(false, sRHSS, fRHSS, srtS));
-
-    Literal* sLitAfter = 0;
-    if (_afterCheck && _cl->numSelected() > 1) {
+    if (sLitAfter) {
       TIME_TRACE(TimeTrace::LITERAL_ORDER_AFTERCHECK);
-      sLitAfter = absUnif.subs().apply(sLit, 0);
-    }
-
-    for(unsigned i=0;i<_cLen;i++) {
-      Literal* curr=(*_cl)[i];
-      if(curr!=sLit) {
-        Literal* currAfter = absUnif.subs().apply(curr, 0);
-
-        if (sLitAfter) {
-          TIME_TRACE(TimeTrace::LITERAL_ORDER_AFTERCHECK);
-          if (i < _cl->numSelected() && _ordering.compare(currAfter,sLitAfter) == Ordering::GREATER) {
-            env.statistics->inferencesBlockedDueToOrderingAftercheck++;
-            return nullptr;
-          }
-        }
-
-        resLits->push(currAfter);
+      if (i < cl->numSelected() && ord.compare(currAfter,sLitAfter) == Ordering::GREATER) {
+        env.statistics->inferencesBlockedDueToOrderingAftercheck++;
+        return nullptr;
       }
     }
 
-    resLits->loadFromIterator(constraints->iterFifo());
-
-    Clause *cl = Clause::fromStack(*resLits, GeneratingInference1(InferenceRule::EQUALITY_FACTORING, _cl));
-    if(env.options->proofExtra() == Options::ProofExtra::FULL)
-      env.proofExtra.insert(cl, new EqualityFactoringExtra(sLit, fLit, sLHS, fRHS));
-    return cl;
-  }
-private:
-  EqualityFactoring& _self;
-  Clause* _cl;
-  unsigned _cLen;
-  bool _afterCheck;
-  const Ordering& _ordering;
-  bool _fixedPointIteration;
-};
-
-ClauseIterator EqualityFactoring::generateClauses(Clause* premise)
-{
-  if(premise->length()<=1) {
-    return ClauseIterator::getEmpty();
+    resLits->push(currAfter);
   }
-  ASS(premise->numSelected()>0);
 
-  auto it1 = premise->getSelectedLiteralIterator();
+  resLits->loadFromIterator(constraints->iterFifo());
 
-  auto it2 = getFilteredIterator(it1,IsPositiveEqualityFn());
+  auto res = Clause::fromStack(*resLits, GeneratingInference1(InferenceRule::EQUALITY_FACTORING, cl));
+  if(env.options->proofExtra() == Options::ProofExtra::FULL)
+    env.proofExtra.insert(res, new EqualityFactoringExtra(sLit, fLit, sLHS, fRHS));
+  return res;
+}
 
-  auto it3 = getMapAndFlattenIterator(it2,EqHelper::LHSIteratorFn(_salg.getOrdering()));
+}
 
-  auto it4 = getMapAndFlattenIterator(std::move(it3),FactorablePairsFn(premise));
+EqualityFactoring::EqualityFactoring(SaturationAlgorithm& salg)
+  : _salg(salg)
+  , _abstractionOracle(_salg.getOptions().unificationWithAbstraction())
+  , _uwaFixedPointIteration(_salg.getOptions().unificationWithAbstractionFixedPointIteration())
+{}
 
-  auto it5 = getMappingIterator(std::move(it4),ResultFn(*this, premise,
-      _salg.getOptions().literalMaximalityAftercheck() && _salg.getLiteralSelector().isBGComplete(),
-      _salg.getOrdering(), _uwaFixedPointIteration));
+ClauseIterator EqualityFactoring::generateClauses(Clause* premise)
+{
+  static AbstractingUnifier unif;
+  static bool funcExt = _salg.getOptions().functionExtensionality()==Options::FunctionExtensionality::ABSTRACTION;
+
+  return pvi(premise->getSelectedLiteralIterator()
+    .filter([](Literal* l){
+      return l->isEquality() && l->isPositive();
+    })
+    .flatMap([this](Literal* lit) {
+      return pvi( pushPairIntoRightIterator(lit, EqHelper::getLHSIterator(lit, _salg.getOrdering())) );
+    })
+    .flatMap([premise](pair<Literal*,TermList> arg) {
+      return pvi(pushPairIntoRightIterator(arg, premise->iterLits()
+        .filter([arg](Literal* l2){
+          return l2->isEquality() && l2->isPositive() && l2 != arg.first;
+        })
+        .flatMap([](Literal* l2) {
+          auto [lhs,rhs] = l2->eqArgs();
+          return pvi( pushPairIntoRightIterator(l2, iterItems( lhs, rhs ) ) );
+        })));
+    })
+    .flatMap([=,this](pair<pair<Literal*,TermList>,pair<Literal*,TermList> > arg) {
+      auto [p1, p2] = arg;
+      auto [sLit, sLHS] = p1; // selected literal ( = factored-out literal ) and side of equation
+      auto [fLit, fLHS] = p2; // fairly boring side literal and side of equation
+      ASS_NEQ(sLit, fLit);
+
+      TermList srt = SortHelper::getEqualityArgumentSort(sLit);
+
+      unif.init(_abstractionOracle);
+      if (!unif.unifyOnce(srt, kVarBank, SortHelper::getEqualityArgumentSort(fLit), kVarBank)) {
+        return ClauseIterator::getEmpty();
+      }
 
-  auto it6 = getFilteredIterator(std::move(it5),NonzeroFn());
+      if (!unif.unify(sLHS, kVarBank, fLHS, kVarBank, _uwaFixedPointIteration)) {
+        return ClauseIterator::getEmpty();
+      }
 
-  return pvi( std::move(it6) );
+      return pvi(iterTraits(vi(new HOL::AbstractingWrapper(unif, _salg.getOptions().higherOrderUnifDepth(), funcExt)))
+        .map([=,this](AbstractingUnifier* unif) {
+          return unifierToClause(premise, srt, sLit, sLHS, fLit, fLHS, unif, _salg.getOrdering(), _salg.getOptions().literalMaximalityAftercheck() && _salg.getLiteralSelector().isBGComplete());
+        }));
+    })
+    .filter(NonzeroFn()));
 }
 
 }

Inferences/EqualityFactoring.hpp

@@ -37,15 +37,9 @@ class EqualityFactoring
   EqualityFactoring(SaturationAlgorithm& salg);
   ClauseIterator generateClauses(Clause* premise) override;
 private:
-  struct IsPositiveEqualityFn;
-  struct IsDifferentPositiveEqualityFn;
-  struct FactorablePairsFn;
-  struct ResultFn;
-  friend struct ResultFn;
-
   const SaturationAlgorithm& _salg;
-  AbstractionOracle _abstractionOracle;
-  bool _uwaFixedPointIteration;
+  const AbstractionOracle _abstractionOracle;
+  const bool _uwaFixedPointIteration;
 };
 
 using EqualityFactoringExtra = TwoLiteralRewriteInferenceExtra;

Inferences/EqualityResolution.cpp

@@ -110,7 +110,7 @@ ClauseIterator EqualityResolution::generateClauses(Clause* premise)
         return ClauseIterator::getEmpty();
       }
 
-      return pvi(iterTraits(vi(new HOL::AbstractingWrapper(&unif, _salg.getOptions().higherOrderUnifDepth(), funcExt)))
+      return pvi(iterTraits(vi(new HOL::AbstractingWrapper(unif, _salg.getOptions().higherOrderUnifDepth(), funcExt)))
         .map([this,premise,lit](AbstractingUnifier* unif) {
           return unifierToClause(premise, lit, unif, _salg.getOptions().literalMaximalityAftercheck() && _salg.getLiteralSelector().isBGComplete() ? &_salg.getOrdering() : nullptr);
         }));

Inferences/HOL/Cases.cpp

@@ -15,6 +15,8 @@
 
 #include "Debug/TimeProfiling.hpp"
 
+#include "Lib/PairUtils.hpp"
+
 #include "Kernel/Clause.hpp"
 #include "Kernel/EqHelper.hpp"
 #include "Kernel/Inference.hpp"

Inferences/HOL/CasesSimp.cpp

@@ -15,6 +15,8 @@
 
 #include "Debug/TimeProfiling.hpp"
 
+#include "Lib/PairUtils.hpp"
+
 #include "Kernel/Clause.hpp"
 #include "Kernel/EqHelper.hpp"
 #include "Kernel/Inference.hpp"

Kernel/EqHelper.cpp

@@ -357,12 +357,4 @@ std::pair<VirtualIterator<TypedTermList>,bool> EqHelper::getDemodulationLHSItera
   }
 }
 
-TermIterator EqHelper::getEqualityArgumentIterator(Literal* lit)
-{
-  ASS(lit->isEquality());
-
-  return pvi( iterItems( *lit->nthArgument(0), *lit->nthArgument(1)) );
-}
-
-
 }

Kernel/EqHelper.hpp

@@ -19,7 +19,6 @@
 #include "Forwards.hpp"
 
 #include "Lib/VirtualIterator.hpp"
-#include "Lib/PairUtils.hpp"
 #include "Kernel/TypedTermList.hpp"
 
 #include "Term.hpp"
@@ -39,7 +38,6 @@ class EqHelper
   static VirtualIterator<TypedTermList> getLHSIterator(Literal* lit, const Ordering& ord);
   static VirtualIterator<TypedTermList> getSuperpositionLHSIterator(Literal* lit, const Ordering& ord, const Options& opt);
   static std::pair<VirtualIterator<TypedTermList>,bool> getDemodulationLHSIterator(Literal* lit, bool onlyPreordered, const Ordering& ord);
-  static TermIterator getEqualityArgumentIterator(Literal* lit);
 
   //WARNING, this function cannot be used when @param t is a sort.
   static Term* replace(Term* t, TermList what, TermList by);
@@ -50,26 +48,6 @@ class EqHelper
   }
   static Literal* replace(Literal* lit, TermList what, TermList by);
 
-  struct LHSIteratorFn
-  {
-    LHSIteratorFn(const Ordering& ord) : _ord(ord) {}
-
-    VirtualIterator<std::pair<Literal*, TypedTermList> > operator()(Literal* lit)
-    {
-      return pvi( pushPairIntoRightIterator(lit, getLHSIterator(lit, _ord)) );
-    }
-  private:
-    const Ordering& _ord;
-  };
-
-  struct EqualityArgumentIteratorFn
-  {
-    VirtualIterator<std::pair<Literal*, TermList> > operator()(Literal* lit)
-    {
-      return pvi( pushPairIntoRightIterator(lit, getEqualityArgumentIterator(lit)) );
-    }
-  };
-
   static bool isEqTautology(Literal* lit)
   {
     return lit->isEquality() && lit->isPositive() && (*lit->nthArgument(0))==(*lit->nthArgument(1));

Kernel/HOL/Unifier.cpp

@@ -249,15 +249,15 @@ Stack<UnificationNode::Constraint> UnificationNode::decompose(unsigned index, bo
 }
 
 
-AbstractingWrapper::AbstractingWrapper(AbstractingUnifier* unifier, unsigned hoUnifDepth, bool funcExt)
-  : _unifier(new AbstractingUnifier(unifier->_uwa)), _hoUnifDepth(hoUnifDepth)
+AbstractingWrapper::AbstractingWrapper(AbstractingUnifier& unifier, unsigned hoUnifDepth, bool funcExt)
+  : _unifier(new AbstractingUnifier(unifier._uwa)), _hoUnifDepth(hoUnifDepth)
 #if VDEBUG
   , _funcExt(funcExt)
 #endif
 {
-  _unifier->subs().copy(unifier->subs());
+  _unifier->subs().copy(unifier.subs());
   Stack<UnificationNode::Constraint> cons;
-  for (const auto c : unifier->constr().iter()) {
+  for (const auto c : unifier.constr().iter()) {
     cons.emplace(
       c.lhs().toGluedTerm(_unifier->subs()),
       c.rhs().toGluedTerm(_unifier->subs()),

Kernel/HOL/Unifier.hpp

@@ -82,7 +82,7 @@ class AbstractingWrapper
   : public IteratorCore<AbstractingUnifier*>
 {
 public:
-  AbstractingWrapper(AbstractingUnifier* unifier, unsigned hoUnifDepth, bool funcExt);
+  AbstractingWrapper(AbstractingUnifier& unifier, unsigned hoUnifDepth, bool funcExt);
   ~AbstractingWrapper() override;
   AbstractingWrapper(const AbstractingWrapper&) = delete;
   AbstractingWrapper& operator=(const AbstractingWrapper&) = delete;