From 9a777d6c66b42dfa5eaf912957400e967cc6ae76 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Fri, 16 Oct 2026 11:13:25 +0200 Subject: [PATCH] Simplify equality factoring and add extra iteration over potential HOL unifiers --- Indexing/TermSubstitutionTree.hpp | 2 +- Inferences/EqualityFactoring.cpp | 218 ++++++++------------ Inferences/EqualityFactoring.hpp | 10 +- Inferences/EqualityResolution.cpp | 2 +- Inferences/HOL/Cases.cpp | 2 + Inferences/HOL/CasesSimp.cpp | 2 + Kernel/EqHelper.cpp | 8 - Kernel/EqHelper.hpp | 22 -- Kernel/HOL/Unifier.cpp | 8 +- Kernel/HOL/Unifier.hpp | 2 +- UnitTests/HOL/tHOL_Unifier.cpp | 4 +- UnitTests/tInferences_EqualityFactoring.cpp | 20 ++ 12 files changed, 123 insertions(+), 177 deletions(-) diff --git a/Indexing/TermSubstitutionTree.hpp b/Indexing/TermSubstitutionTree.hpp index 7dfab6dff5..f624058a69 100644 --- a/Indexing/TermSubstitutionTree.hpp +++ b/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 qr) { return pvi(pushPairIntoRightIterator(qr, vi(new HOL::AbstractingWrapper(qr.unifier, hoUnifDepth, funcExt)))); }) + .flatMap([hoUnifDepth,funcExt](QueryRes qr) { return pvi(pushPairIntoRightIterator(qr, vi(new HOL::AbstractingWrapper(*qr.unifier, hoUnifDepth, funcExt)))); }) .map([](auto arg) { return queryRes(arg.second, arg.first.data); })); } diff --git a/Inferences/EqualityFactoring.cpp b/Inferences/EqualityFactoring.cpp index 965c580743..f285e2faca 100644 --- a/Inferences/EqualityFactoring.cpp +++ b/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 > > operator() (pair 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 > 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 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 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 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 > 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())); } } diff --git a/Inferences/EqualityFactoring.hpp b/Inferences/EqualityFactoring.hpp index c6bb2f513b..690d5e2b9f 100644 --- a/Inferences/EqualityFactoring.hpp +++ b/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; diff --git a/Inferences/EqualityResolution.cpp b/Inferences/EqualityResolution.cpp index da0bc48ac2..70ce5873cf 100644 --- a/Inferences/EqualityResolution.cpp +++ b/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); })); diff --git a/Inferences/HOL/Cases.cpp b/Inferences/HOL/Cases.cpp index 658f84e4a3..9c105c02e6 100644 --- a/Inferences/HOL/Cases.cpp +++ b/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" diff --git a/Inferences/HOL/CasesSimp.cpp b/Inferences/HOL/CasesSimp.cpp index c7e7b4571d..43d4d4c19a 100644 --- a/Inferences/HOL/CasesSimp.cpp +++ b/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" diff --git a/Kernel/EqHelper.cpp b/Kernel/EqHelper.cpp index 8859866991..89f77f73b9 100644 --- a/Kernel/EqHelper.cpp +++ b/Kernel/EqHelper.cpp @@ -357,12 +357,4 @@ std::pair,bool> EqHelper::getDemodulationLHSItera } } -TermIterator EqHelper::getEqualityArgumentIterator(Literal* lit) -{ - ASS(lit->isEquality()); - - return pvi( iterItems( *lit->nthArgument(0), *lit->nthArgument(1)) ); -} - - } diff --git a/Kernel/EqHelper.hpp b/Kernel/EqHelper.hpp index 66f95d06db..fb01fa2e81 100644 --- a/Kernel/EqHelper.hpp +++ b/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 getLHSIterator(Literal* lit, const Ordering& ord); static VirtualIterator getSuperpositionLHSIterator(Literal* lit, const Ordering& ord, const Options& opt); static std::pair,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 > operator()(Literal* lit) - { - return pvi( pushPairIntoRightIterator(lit, getLHSIterator(lit, _ord)) ); - } - private: - const Ordering& _ord; - }; - - struct EqualityArgumentIteratorFn - { - VirtualIterator > 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)); diff --git a/Kernel/HOL/Unifier.cpp b/Kernel/HOL/Unifier.cpp index 69b3bb39d5..1bffb0a780 100644 --- a/Kernel/HOL/Unifier.cpp +++ b/Kernel/HOL/Unifier.cpp @@ -249,15 +249,15 @@ Stack 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 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()), diff --git a/Kernel/HOL/Unifier.hpp b/Kernel/HOL/Unifier.hpp index f419d0976c..ef6ed144f3 100644 --- a/Kernel/HOL/Unifier.hpp +++ b/Kernel/HOL/Unifier.hpp @@ -82,7 +82,7 @@ class AbstractingWrapper : public IteratorCore { 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; diff --git a/UnitTests/HOL/tHOL_Unifier.cpp b/UnitTests/HOL/tHOL_Unifier.cpp index eb4cd6ed87..a38e3e661d 100644 --- a/UnitTests/HOL/tHOL_Unifier.cpp +++ b/UnitTests/HOL/tHOL_Unifier.cpp @@ -78,7 +78,7 @@ void testUnifySuccess(TermList lhs, TermList rhs, Stack expected) { ASSERTION_VIOLATION; } - HOL::AbstractingWrapper wrapper(&unif, UNIF_DEPTH, funcExt); + HOL::AbstractingWrapper wrapper(unif, UNIF_DEPTH, funcExt); for (unsigned i = 0; i < expected.size(); i++) { if (!wrapper.hasNext()) { std::cout << std::endl; @@ -150,7 +150,7 @@ void testUnifyFail(TermList lhs, TermList rhs) { AbstractingUnifier unif(oracle); if (unif.unify(lhs, LEFT_BANK, rhs, RIGHT_BANK, /*fixedPointIteration=*/true)) { - HOL::AbstractingWrapper wrapper(&unif, UNIF_DEPTH, funcExt); + HOL::AbstractingWrapper wrapper(unif, UNIF_DEPTH, funcExt); if (wrapper.hasNext()) { std::cout << std::endl; std::cout << "expected *not* to HO unify (" << unifToStr(lhs, rhs) << ")" << std::endl; diff --git a/UnitTests/tInferences_EqualityFactoring.cpp b/UnitTests/tInferences_EqualityFactoring.cpp index a1584ea9a4..ce10d5f89f 100644 --- a/UnitTests/tInferences_EqualityFactoring.cpp +++ b/UnitTests/tInferences_EqualityFactoring.cpp @@ -47,4 +47,24 @@ TEST_GENERATION(test02, .expected(none()) ) +#undef MY_SYNTAX_SUGAR +#define MY_SYNTAX_SUGAR \ + DECL_SORT(s) \ + DECL_DEFAULT_VARS \ + DECL_CONST(f, arrow(s, s)) \ + DECL_DE_BRUIJN_INDEX(db0, 0, s) \ + DECL_CONST(a, s) \ + DECL_CONST(b, s) + +// with higher-order unification +TEST_GENERATION(test_hol01, + Generation::AsymmetricTest() + .input(clause({ selected(ap(x.sort(arrow(s, s)), ap(f, a)) == a), ap(f, a) == b, x != f })) + .expected( exactly( + clause({ b == ap(f, a), ap(f, a) != a, lam(s, b) != f() }), + clause({ ap(f, a) == b, b != a, lam(s, db0) != f() }), + clause({ ap(f, a) == b, b != a, lam(s, ap(f, ap(lam(s, a), db0))) != f() }) + )) + ) + } \ No newline at end of file