From c315ca88227f8ed6f7d6f293196d7156a66dfd53 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Wed, 25 Mar 2026 14:08:30 +0100 Subject: [PATCH 1/7] Refactor fresh variable handling in primitive instantiation; add unit tests to see how it works --- Inferences/HOL/PrimitiveInstantiation.hpp | 1 + Test/SyntaxSugar.hpp | 7 +- UnitTests/tInferences_HOL_ArgCong.cpp | 7 +- ...tInferences_HOL_PrimitiveInstantiation.cpp | 71 ++++++++++++++++--- 4 files changed, 73 insertions(+), 13 deletions(-) diff --git a/Inferences/HOL/PrimitiveInstantiation.hpp b/Inferences/HOL/PrimitiveInstantiation.hpp index 2fea814e5..53fe8f662 100644 --- a/Inferences/HOL/PrimitiveInstantiation.hpp +++ b/Inferences/HOL/PrimitiveInstantiation.hpp @@ -32,6 +32,7 @@ class PrimitiveInstantiation ClauseIterator generateClauses(Clause* premise) override; private: const Shell::Options::PISet _piSet; + TermStack _heads; }; }; diff --git a/Test/SyntaxSugar.hpp b/Test/SyntaxSugar.hpp index 1b658428d..50cf50dc5 100644 --- a/Test/SyntaxSugar.hpp +++ b/Test/SyntaxSugar.hpp @@ -60,7 +60,9 @@ #define DECL_NOT_PROXY auto notP = TermSugar(HOL::create::neg()); #define DECL_AND_PROXY auto andP = TermSugar(HOL::create::conj()); #define DECL_OR_PROXY auto orP = TermSugar(HOL::create::disj()); -#define DECL_EQ_PROXY(s) auto eqP = TermSugar(HOL::create::equality(s)); +#define DECL_EQ_PROXY(p) auto p = FuncSugar(env.signature->getEqualityProxy()); +#define DECL_PI_PROXY(p) auto p = FuncSugar(env.signature->getPiSigmaProxy("vPI")); +#define DECL_SIGMA_PROXY(p) auto p = FuncSugar(env.signature->getPiSigmaProxy("vSIGMA")); #define DECL_APP env.signature->getApp(); #define DECL_LAM env.signature->getLam(); #define NEXT_INTRODUCED_PRED(s,offset) auto s = PredSugar(env.signature->predicates()+offset); @@ -435,6 +437,9 @@ inline TermSugar ap(TermList head, TermStack args) inline TermSugar lam(SortSugar varSort, TermSugar body) { return HOL::create::namelessLambda(varSort, body.sort(), body); } +inline TermSugar db(unsigned i, SortSugar srt) +{ return HOL::getDeBruijnIndex(i, srt); } + inline TermSugar operator+(TermSugar lhs, TermSugar rhs) { return syntaxSugarGlobals().add(lhs, rhs); } inline TermSugar operator-(TermSugar lhs, TermSugar rhs) { return lhs + -rhs; } inline TermSugar operator*(TermSugar lhs, TermSugar rhs) { diff --git a/UnitTests/tInferences_HOL_ArgCong.cpp b/UnitTests/tInferences_HOL_ArgCong.cpp index 0a87b38dd..4e9af915f 100644 --- a/UnitTests/tInferences_HOL_ArgCong.cpp +++ b/UnitTests/tInferences_HOL_ArgCong.cpp @@ -16,7 +16,6 @@ using namespace Test; #define MY_SYNTAX_SUGAR \ DECL_SORT(srt) \ - DECL_SORT_VAR(sx, 0) \ DECL_SORT_VAR(sy, 4) \ DECL_SORT_VAR(sz, 5) \ DECL_VAR_SORTED(x, 0, srt) \ @@ -29,8 +28,8 @@ using namespace Test; DECL_PRED(p, { srt }) \ DECL_CONST(f, arrow({srt, srt}, srt)) \ DECL_CONST(g, arrow(srt, srt)) \ - DECL_POLY_CONST(g2, 1, sx) \ - DECL_POLY_CONST(g3, 1, sx) \ + DECL_POLY_CONST(g2, 1, x) \ + DECL_POLY_CONST(g3, 1, x) \ DECL_DE_BRUIJN_INDEX(db0, 0, srt) \ DECL_CONST(a, srt) \ DECL_CONST(b, srt) @@ -80,6 +79,6 @@ TEST_GENERATION(success_2, TEST_GENERATION(success_3, Generation::AsymmetricTest() - .input( clause({ selected(g2(sx) == g3(sx)), y == z })) + .input( clause({ selected(g2(x) == g3(x)), y == z })) .expected(exactly(clause({ ap(g2(arrow(sy, sz)), xs2) == ap(g3(arrow(sy, sz)), xs2), y == z }))) ) diff --git a/UnitTests/tInferences_HOL_PrimitiveInstantiation.cpp b/UnitTests/tInferences_HOL_PrimitiveInstantiation.cpp index 279c696bf..648b3434b 100644 --- a/UnitTests/tInferences_HOL_PrimitiveInstantiation.cpp +++ b/UnitTests/tInferences_HOL_PrimitiveInstantiation.cpp @@ -17,24 +17,27 @@ using namespace Test; #define MY_SYNTAX_SUGAR \ DECL_SORT(srt) \ DECL_SORT_BOOL \ + DECL_DEFAULT_VARS \ + DECL_VAR(u, 3) \ + DECL_VAR(v, 4) \ TROO \ FOLS \ DECL_NOT_PROXY \ DECL_AND_PROXY \ DECL_OR_PROXY \ - DECL_EQ_PROXY(srt) \ + DECL_EQ_PROXY(eqP) \ + DECL_PI_PROXY(piP) \ + DECL_SIGMA_PROXY(sgP) \ DECL_VAR_SORTED(xs, 0, arrow(srt, Bool)) \ DECL_VAR_SORTED(ys, 1, arrow(srt, srt)) \ DECL_VAR_SORTED(zs, 2, arrow(srt, Bool)) \ DECL_VAR_SORTED(zs2, 3, arrow(srt, Bool)) \ - DECL_VAR_SORTED(zs3, 2, arrow(srt, srt)) \ - DECL_VAR_SORTED(zs4, 3, arrow(srt, srt)) \ DECL_VAR_SORTED(us, 3, arrow({srt, srt}, Bool)) \ DECL_VAR_SORTED(vs, 4, arrow(Bool, Bool)) \ DECL_VAR_SORTED(ws, 5, arrow({srt, srt}, Bool)) \ DECL_VAR_SORTED(ws2, 5, arrow(Bool, Bool)) \ DECL_CONST(f, arrow(srt, Bool)) \ - DECL_CONST(f1, arrow(srt, Bool)) \ + DECL_CONST(f1, arrow({srt, srt}, Bool)) \ DECL_CONST(g, arrow(srt, srt)) \ DECL_DE_BRUIJN_INDEX(db0, 0, srt) \ DECL_DE_BRUIJN_INDEX(db0B, 0, Bool) \ @@ -63,14 +66,14 @@ TEST_GENERATION(fail_2, // not done for non-applied variables TEST_GENERATION(fail_3, Generation::AsymmetricTest() - .input( clause({ selected(f == xs) })) + .input( clause({ selected(f == x) })) .expected(none()) ) // not done for rigid-rigid literals TEST_GENERATION(fail_4, Generation::AsymmetricTest() - .input( clause({ selected(ap(f,b) == ap(f1,c)) })) + .input( clause({ selected(ap(f,b) == ap(f1, {c,x})) })) .expected(none()) ) @@ -98,8 +101,8 @@ TEST_GENERATION(success_2, clause({ ap(f,c) == ap(lam(srt, lam(srt, troo)), {c, b}) }), clause({ ap(f,c) == ap(lam(srt, lam(srt, fols)), {c, b}) }), clause({ ap(f,c) == ap(lam(srt, lam(srt, ap(notP, ap(ap(ws,db1),db0)))), {c, b}) }), - clause({ ap(f,c) == ap(lam(srt, lam(srt, ap(eqP,{db1,db0}))), {c, b}) }), - clause({ ap(f,c) == ap(lam(srt, lam(srt, ap(notP, ap(eqP,{db1,db0})))), {c, b}) }) + clause({ ap(f,c) == ap(lam(srt, lam(srt, ap(eqP(srt),{db1,db0}))), {c, b}) }), + clause({ ap(f,c) == ap(lam(srt, lam(srt, ap(notP, ap(eqP(srt),{db1,db0})))), {c, b}) }) )) ) @@ -136,3 +139,55 @@ TEST_GENERATION(success_5, )) ) +TEST_GENERATION(success_6, + Generation::AsymmetricTest() + .input( clause({ selected(ap(f1, {x,y}) == ap(arrow(srt,Bool),z,c)) })) + .options({ { "prim_inst_set", "pi_sigma" } }) + .expected(exactly( + clause({ ap(f1, {x,y}) == ap(lam(srt,troo),c) }), + clause({ ap(f1, {x,y}) == ap(lam(srt,fols),c) }), + clause({ ap(f1, {x,y}) == ap(lam(srt,ap(piP(z), ap(arrow({srt,z},Bool),u,db0))),c) }), + clause({ ap(f1, {x,y}) == ap(lam(srt,ap(sgP(z), ap(arrow({srt,z},Bool),u,db0))),c) }) + )) + ) + +TEST_GENERATION(success_7, + Generation::AsymmetricTest() + .input( clause({ selected(ap(f1, {x,z}) == ap(arrow(srt,Bool),y,c)) })) + .options({ { "prim_inst_set", "equals" } }) + .expected(exactly( + clause({ ap(f1, {x,z}) == ap(lam(srt,troo),c) }), + clause({ ap(f1, {x,z}) == ap(lam(srt,fols),c) }), + clause({ ap(f1, {x,z}) == ap(lam(srt,ap(eqP(y), { ap(arrow(srt,y),u,db0), ap(arrow(srt,y),v,db0) })),c) }) + )) + ) + +TEST_GENERATION(success_8, + Generation::AsymmetricTest() + .input( clause({ selected(ap(f1, {x,z}) == ap(arrow(srt,Bool),y,c)) })) + .options({ { "prim_inst_set", "small_set" } }) + .expected(exactly( + clause({ ap(f1, {x,z}) == ap(lam(srt,troo),c) }), + clause({ ap(f1, {x,z}) == ap(lam(srt,fols),c) }), + clause({ ap(f1, {x,z}) == ap(lam(srt,ap(eqP(y), { ap(arrow(srt,y),u,db0), ap(arrow(srt,y),v,db0) })),c) }), + clause({ ap(f1, {x,z}) == ap(lam(srt,ap(notP, ap(arrow(srt,Bool),u,db0))),c) }), + clause({ ap(f1, {x,z}) == ap(lam(srt, ap(notP, ap(eqP(y), { ap(arrow(srt,y),u,db0), ap(arrow(srt,y),v,db0) }))),c) }) + )) + ) + +TEST_GENERATION(success_9, + Generation::AsymmetricTest() + .input( clause({ selected(ap(f1, {x,z}) == ap(arrow(srt,Bool),y,c)) })) + .options({ { "prim_inst_set", "all" } }) + .expected(exactly( + clause({ ap(f1, {x,z}) == ap(lam(srt,troo),c) }), + clause({ ap(f1, {x,z}) == ap(lam(srt,fols),c) }), + clause({ ap(f1, {x,z}) == ap(lam(srt,ap(eqP(y), { ap(arrow(srt,y),u,db0), ap(arrow(srt,y),v,db0) })),c) }), + clause({ ap(f1, {x,z}) == ap(lam(srt,ap(notP, ap(arrow(srt,Bool),u,db0))),c) }), + clause({ ap(f1, {x,z}) == ap(lam(srt, ap(notP, ap(eqP(y), { ap(arrow(srt,y),u,db0), ap(arrow(srt,y),v,db0) }))),c) }), + clause({ ap(f1, {x,z}) == ap(lam(srt,ap(piP(y), ap(arrow({srt,y},Bool),u,db0))),c) }), + clause({ ap(f1, {x,z}) == ap(lam(srt,ap(sgP(y), ap(arrow({srt,y},Bool),u,db0))),c) }), + clause({ ap(f1, {x,z}) == ap(lam(srt,ap(andP, {ap(arrow(srt,Bool),u,db0), ap(arrow(srt,Bool),v,db0)})),c) }), + clause({ ap(f1, {x,z}) == ap(lam(srt,ap(orP, {ap(arrow(srt,Bool),u,db0), ap(arrow(srt,Bool),v,db0)})),c) }) + )) + ) From 196da67926da04a0048bd7970b4eb574f0d68dcc Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Wed, 25 Mar 2026 15:42:43 +0100 Subject: [PATCH 2/7] Basic adaption of code trees for higher-order matching by not binding to terms with loose DB indices --- Indexing/ClauseCodeTree.cpp | 99 ++++++++++++------- Indexing/ClauseCodeTree.hpp | 15 ++- Indexing/CodeTree.cpp | 57 ++++++----- Indexing/CodeTree.hpp | 11 ++- Indexing/CodeTreeInterfaces.cpp | 28 +++--- Indexing/CodeTreeInterfaces.hpp | 9 +- Indexing/IndexManager.cpp | 8 +- Indexing/TermCodeTree.cpp | 71 +++++++------ Indexing/TermCodeTree.hpp | 13 ++- Indexing/TermIndex.cpp | 11 ++- Indexing/TermIndex.hpp | 1 + ...odeTreeForwardSubsumptionAndResolution.cpp | 13 ++- ...odeTreeForwardSubsumptionAndResolution.hpp | 5 +- Inferences/ForwardDemodulation.cpp | 2 +- Inferences/ForwardDemodulation.hpp | 2 +- Inferences/ForwardGroundJoinability.cpp | 20 ++-- Inferences/ForwardGroundJoinability.hpp | 3 +- Kernel/Clause.cpp | 6 ++ Kernel/TermOrderingDiagram.hpp | 4 +- Lib/Vector.hpp | 4 +- Saturation/SaturationAlgorithm.cpp | 12 ++- Shell/FunctionDefinitionHandler.cpp | 2 +- Shell/FunctionDefinitionHandler.hpp | 2 +- Shell/PartialRedundancyHandler.cpp | 4 +- ...ences_CodeTreeSubsumptionAndResolution.cpp | 2 +- .../tInferences_ForwardGroundJoinability.cpp | 2 +- 26 files changed, 251 insertions(+), 155 deletions(-) diff --git a/Indexing/ClauseCodeTree.cpp b/Indexing/ClauseCodeTree.cpp index b820f4e3e..a2023edee 100644 --- a/Indexing/ClauseCodeTree.cpp +++ b/Indexing/ClauseCodeTree.cpp @@ -36,14 +36,16 @@ using namespace std; using namespace Lib; using namespace Kernel; -void ClauseCodeTree::onCodeOpDestroying(CodeOp* op) +template +void ClauseCodeTree::onCodeOpDestroying(CodeOp* op) { if (op->isLitEnd()) { delete op->getILS(); } } -ClauseCodeTree::ClauseCodeTree() +template +ClauseCodeTree::ClauseCodeTree() { _clauseCodeTree=true; _onCodeOpDestroying = onCodeOpDestroying; @@ -54,7 +56,8 @@ ClauseCodeTree::ClauseCodeTree() //////////////// insertion //////////////////// -void ClauseCodeTree::insert(Clause* cl) +template +void ClauseCodeTree::insert(Clause* cl) { unsigned clen=cl->length(); static DArray lits; @@ -77,7 +80,8 @@ void ClauseCodeTree::insert(Clause* cl) ASS(code.isEmpty()); } -struct ClauseCodeTree::InitialLiteralOrderingComparator +template +struct ClauseCodeTree::InitialLiteralOrderingComparator { Comparison compare(Literal* l1, Literal* l2) { @@ -88,7 +92,8 @@ struct ClauseCodeTree::InitialLiteralOrderingComparator } }; -void ClauseCodeTree::optimizeLiteralOrder(DArray& lits) +template +void ClauseCodeTree::optimizeLiteralOrder(DArray& lits) { unsigned clen=lits.size(); if(isEmpty() || clen<=1) { @@ -139,7 +144,8 @@ void ClauseCodeTree::optimizeLiteralOrder(DArray& lits) } } -void ClauseCodeTree::evalSharing(Literal* lit, CodeOp* startOp, size_t& sharedLen, size_t& unsharedLen, CodeOp*& nextOp) +template +void ClauseCodeTree::evalSharing(Literal* lit, CodeOp* startOp, size_t& sharedLen, size_t& unsharedLen, CodeOp*& nextOp) { CodeStack code; LitCompiler compiler(code); @@ -163,7 +169,8 @@ void ClauseCodeTree::evalSharing(Literal* lit, CodeOp* startOp, size_t& sharedLe * it is the first operation on which mismatch occurred and there was no alternative to * proceed to (in this case it therefore holds that @b lastAttemptedOp->alternative==0 ). */ -void ClauseCodeTree::matchCode(CodeStack& code, CodeOp* startOp, size_t& matchedCnt, CodeOp*& nextOp) +template +void ClauseCodeTree::matchCode(CodeStack& code, CodeOp* startOp, size_t& matchedCnt, CodeOp*& nextOp) { size_t clen=code.length(); CodeOp* treeOp=startOp; @@ -207,7 +214,8 @@ void ClauseCodeTree::matchCode(CodeStack& code, CodeOp* startOp, size_t& matched //////////////// removal //////////////////// -void ClauseCodeTree::remove(Clause* cl) +template +void ClauseCodeTree::remove(Clause* cl) { static DArray lInfos; Recycled> firstsInBlocks; @@ -283,19 +291,21 @@ void ClauseCodeTree::remove(Clause* cl) } } -void ClauseCodeTree::RemovingLiteralMatcher::init(CodeOp* entry_, LitInfo* linfos_, +template +void ClauseCodeTree::RemovingLiteralMatcher::init(CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, ClauseCodeTree* tree_, Stack* firstsInBlocks_) { - Matcher::init(tree_, entry_, linfos_, linfoCnt_, firstsInBlocks_); + Base::init(tree_, entry_, linfos_, linfoCnt_, firstsInBlocks_); - ALWAYS(prepareLiteral()); + ALWAYS(Base::prepareLiteral()); } /** * The first operation of the CodeBlock containing @b op * must already be on the @b firstsInBlocks stack. */ -bool ClauseCodeTree::removeOneOfAlternatives(CodeOp* op, Clause* cl, Stack* firstsInBlocks) +template +bool ClauseCodeTree::removeOneOfAlternatives(CodeOp* op, Clause* cl, Stack* firstsInBlocks) { unsigned initDepth=firstsInBlocks->size(); @@ -320,13 +330,14 @@ bool ClauseCodeTree::removeOneOfAlternatives(CodeOp* op, Clause* cl, Stack +void ClauseCodeTree::LiteralMatcher::init(CodeTree* tree_, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, bool seekOnlySuccess) { ASS_G(linfoCnt_,0); - Matcher::init(tree_,entry_,linfos_,linfoCnt_); + Base::init(tree_,entry_,linfos_,linfoCnt_); _eagerlyMatched=false; eagerResults.reset(); @@ -338,24 +349,25 @@ void ClauseCodeTree::LiteralMatcher::init(CodeTree* tree_, CodeOp* entry_, //(and those must be at the entry point or its alternatives) _eagerlyMatched=true; - fresh=false; - CodeOp* sop=entry; + Base::fresh=false; + CodeOp* sop=Base::entry; while(sop) { if(sop->isSuccess()) { - eagerResults.push(sop); + eagerResults.push(sop); } sop=sop->alternative(); } return; } - ALWAYS(prepareLiteral()); + ALWAYS(Base::prepareLiteral()); } /** * Try to find a match, and if one is found, return true */ -bool ClauseCodeTree::LiteralMatcher::next() +template +bool ClauseCodeTree::LiteralMatcher::next() { if(eagerlyMatched()) { _matched=!eagerResults.isEmpty(); @@ -386,7 +398,8 @@ bool ClauseCodeTree::LiteralMatcher::next() /** * Perform eager matching and return true iff new matches were found */ -bool ClauseCodeTree::LiteralMatcher::doEagerMatching() +template +bool ClauseCodeTree::LiteralMatcher::doEagerMatching() { ASS(!eagerlyMatched()); //eager matching can be done only once ASS(eagerResults.isEmpty()); @@ -430,21 +443,22 @@ bool ClauseCodeTree::LiteralMatcher::doEagerMatching() return eagerResults.isNonEmpty(); } -void ClauseCodeTree::LiteralMatcher::recordMatch() +template +void ClauseCodeTree::LiteralMatcher::recordMatch() { - ASS(matched()); + ASS(_matched); ILStruct* ils=op->getILS(); - ils->ensureFreshness(tree->_curTimeStamp); + ils->ensureFreshness(Base::tree->_curTimeStamp); if(ils->finished) { //no need to record matches which we already know will not lead to anything return; } - if(!ils->matchCnt && linfos[curLInfo].opposite) { + if(!ils->matchCnt && Base::linfos[Base::curLInfo].opposite) { //if we're matching opposite matches, we have already tried all non-opposite ones ils->noNonOppositeMatches=true; } - ils->addMatch(linfos[curLInfo].liIndex, bindings); + ils->addMatch(Base::linfos[Base::curLInfo].liIndex, Base::bindings); } @@ -455,7 +469,8 @@ void ClauseCodeTree::LiteralMatcher::recordMatch() * of the @b query_ clause. * If @b sres_ if true, we perform subsumption resolution */ -void ClauseCodeTree::ClauseMatcher::init(ClauseCodeTree* tree_, Clause* query_, bool sres_) +template +void ClauseCodeTree::ClauseMatcher::init(ClauseCodeTree* tree_, Clause* query_, bool sres_) { ASS(!tree_->isEmpty()); @@ -521,7 +536,8 @@ void ClauseCodeTree::ClauseMatcher::init(ClauseCodeTree* tree_, Clause* query_, enterLiteral(tree->getEntryPoint(), clen==0); } -void ClauseCodeTree::ClauseMatcher::reset() +template +void ClauseCodeTree::ClauseMatcher::reset() { unsigned liCnt=lInfos.size(); for(unsigned i=0;i +Clause* ClauseCodeTree::ClauseMatcher::next(int& resolvedQueryLit) { if(lms.isEmpty()) { return 0; @@ -558,7 +575,7 @@ Clause* ClauseCodeTree::ClauseMatcher::next(int& resolvedQueryLit) } } else if(lm->op->isSuccess()) { - Clause* candidate=lm->op->getSuccessResult(); + Clause* candidate=lm->op->template getSuccessResult(); RSTAT_MCTR_INC("candidates", lms.size()-1); if(checkCandidate(candidate, resolvedQueryLit)) { RSTAT_MCTR_INC("candidates (success)", lms.size()-1); @@ -589,7 +606,8 @@ Clause* ClauseCodeTree::ClauseMatcher::next(int& resolvedQueryLit) } } -inline bool ClauseCodeTree::ClauseMatcher::canEnterLiteral(CodeOp* op) +template +inline bool ClauseCodeTree::ClauseMatcher::canEnterLiteral(CodeOp* op) { ASS(op->isLitEnd()); ASS_EQ(lms.top()->op, op); @@ -638,7 +656,8 @@ inline bool ClauseCodeTree::ClauseMatcher::canEnterLiteral(CodeOp* op) * (this is to be used when all literals are matched so we want * to see just clauses that end at this point). */ -void ClauseCodeTree::ClauseMatcher::enterLiteral(CodeOp* entry, bool seekOnlySuccess) +template +void ClauseCodeTree::ClauseMatcher::enterLiteral(CodeOp* entry, bool seekOnlySuccess) { if(!seekOnlySuccess) { RSTAT_MCTR_INC("enterLiteral levels (non-sos)", lms.size()); @@ -669,7 +688,8 @@ void ClauseCodeTree::ClauseMatcher::enterLiteral(CodeOp* entry, bool seekOnlySuc lms.push(std::move(lm)); } -void ClauseCodeTree::ClauseMatcher::leaveLiteral() +template +void ClauseCodeTree::ClauseMatcher::leaveLiteral() { ASS(lms.isNonEmpty()); @@ -697,7 +717,8 @@ void ClauseCodeTree::ClauseMatcher::leaveLiteral() //////////////// Multi-literal matching -bool ClauseCodeTree::ClauseMatcher::checkCandidate(Clause* cl, int& resolvedQueryLit) +template +bool ClauseCodeTree::ClauseMatcher::checkCandidate(Clause* cl, int& resolvedQueryLit) { unsigned clen=cl->length(); //the last matcher in mls is the one that yielded the SUCCESS operation @@ -752,7 +773,8 @@ bool ClauseCodeTree::ClauseMatcher::checkCandidate(Clause* cl, int& resolvedQuer // return newMatches && matchGlobalVars(resolvedQueryLit); } -bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQueryLit) +template +bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQueryLit) { //TODO: perform _set_, not _multiset_ subsumption for subsumption resolution @@ -849,7 +871,8 @@ bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQueryLit) return true; } -bool ClauseCodeTree::ClauseMatcher::compatible(ILStruct* bi, MatchInfo* bq, ILStruct* ni, MatchInfo* nq) +template +bool ClauseCodeTree::ClauseMatcher::compatible(ILStruct* bi, MatchInfo* bq, ILStruct* ni, MatchInfo* nq) { if( lInfos[bq->liIndex].litIndex==lInfos[nq->liIndex].litIndex || (lInfos[bq->liIndex].opposite && lInfos[nq->liIndex].opposite) ) { @@ -894,7 +917,8 @@ bool ClauseCodeTree::ClauseMatcher::compatible(ILStruct* bi, MatchInfo* bq, ILSt return true; } -bool ClauseCodeTree::ClauseMatcher::existsCompatibleMatch(ILStruct* si, MatchInfo* sq, ILStruct* targets) +template +bool ClauseCodeTree::ClauseMatcher::existsCompatibleMatch(ILStruct* si, MatchInfo* sq, ILStruct* targets) { size_t tcnt=targets->matchCnt; for(size_t i=0;i; +template class ClauseCodeTree; + } diff --git a/Indexing/ClauseCodeTree.hpp b/Indexing/ClauseCodeTree.hpp index a6eb6298a..8aed172fc 100644 --- a/Indexing/ClauseCodeTree.hpp +++ b/Indexing/ClauseCodeTree.hpp @@ -29,6 +29,7 @@ namespace Indexing { using namespace Lib; using namespace Kernel; +template class ClauseCodeTree : public CodeTree { protected: @@ -55,8 +56,10 @@ class ClauseCodeTree : public CodeTree bool removeOneOfAlternatives(CodeOp* op, Clause* cl, Stack* firstsInBlocks); struct RemovingLiteralMatcher - : public Matcher + : public Matcher { + using Base = Matcher; + void init(CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, ClauseCodeTree* tree_, Stack* firstsInBlocks_); @@ -69,15 +72,21 @@ class ClauseCodeTree : public CodeTree * * Here the actual execution of the code of the tree takes place */ struct LiteralMatcher - : public Matcher + : public Matcher { + using Base = Matcher; + using Base::op; + using Base::_matched; + using Base::finished; + using Base::execute; + void init(CodeTree* tree, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, bool seekOnlySuccess=false); bool next(); bool doEagerMatching(); inline bool eagerlyMatched() const { return _eagerlyMatched; } - inline ILStruct* getILS() { ASS(matched()); return op->getILS(); } + inline ILStruct* getILS() { ASS(Base::matched()); return op->getILS(); } USE_ALLOCATOR(LiteralMatcher); diff --git a/Indexing/CodeTree.cpp b/Indexing/CodeTree.cpp index 64deb82d2..99331ce53 100644 --- a/Indexing/CodeTree.cpp +++ b/Indexing/CodeTree.cpp @@ -522,8 +522,8 @@ CodeTree::CodeOp*& CodeTree::SearchStructImpl::targetOp(const T& val) //////////////// Matcher //////////////////// -template -bool CodeTree::Matcher::execute() +template +bool CodeTree::Matcher::execute() { if(fresh) { fresh=false; @@ -582,11 +582,7 @@ bool CodeTree::Matcher::execute() shouldBacktrack=!doCheckFun(); break; case ASSIGN_VAR: - if constexpr (removing) { - shouldBacktrack=!doAssignVar(); - } else { - doAssignVar(); - } + shouldBacktrack=!doAssignVar(); break; case CHECK_VAR: shouldBacktrack=!doCheckVar(); @@ -621,8 +617,8 @@ bool CodeTree::Matcher::execute() } } -template -void CodeTree::Matcher::init(CodeTree* tree_, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, Stack* firstsInBlocks_) +template +void CodeTree::Matcher::init(CodeTree* tree_, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, Stack* firstsInBlocks_) { tree=tree_; entry=entry_; @@ -651,8 +647,8 @@ void CodeTree::Matcher::init(CodeTree* tree_, CodeOp* entr * entry point and starts evaluating new literal info (if there * is some left). */ -template -bool CodeTree::Matcher::backtrack() +template +bool CodeTree::Matcher::backtrack() { if(btStack.isEmpty()) { curLInfo++; @@ -668,8 +664,8 @@ bool CodeTree::Matcher::backtrack() return true; } -template -bool CodeTree::Matcher::prepareLiteral() +template +bool CodeTree::Matcher::prepareLiteral() { if constexpr (removing) { RemovingBase::firstsInBlocks->truncate(RemovingBase::initFIBDepth); @@ -683,8 +679,8 @@ bool CodeTree::Matcher::prepareLiteral() return true; } -template -inline bool CodeTree::Matcher::doAssignVar() +template +inline bool CodeTree::Matcher::doAssignVar() { ASS_EQ(op->_instruction(), ASSIGN_VAR); @@ -709,6 +705,13 @@ inline bool CodeTree::Matcher::doAssignVar() fte++; ASS_EQ(fte->_tag(), FlatTerm::FUN_TERM_PTR); ASS(fte->_term()); + if constexpr (higherOrder) { + // When dealing with HOL we want to avoid binding to + // any terms that contain loose DB indices. + if (TermList(fte->_term()).containsLooseDBIndex()) { + return false; + } + } bindings[var]=TermList(fte->_term()); fte++; ASS_EQ(fte->_tag(), FlatTerm::FUN_RIGHT_OFS); @@ -717,8 +720,8 @@ inline bool CodeTree::Matcher::doAssignVar() return true; } -template -inline bool CodeTree::Matcher::doCheckVar() +template +inline bool CodeTree::Matcher::doCheckVar() { ASS_EQ(op->_instruction(), CHECK_VAR); @@ -749,8 +752,8 @@ inline bool CodeTree::Matcher::doCheckVar() return true; } -template -inline bool CodeTree::Matcher::doCheckFun() +template +inline bool CodeTree::Matcher::doCheckFun() { ASS_EQ(op->_instruction(), CHECK_FUN); @@ -764,8 +767,8 @@ inline bool CodeTree::Matcher::doCheckFun() return true; } -template -inline bool CodeTree::Matcher::doCheckGroundTerm() +template +inline bool CodeTree::Matcher::doCheckGroundTerm() { ASS_EQ(op->_instruction(), CHECK_GROUND_TERM); @@ -788,8 +791,8 @@ inline bool CodeTree::Matcher::doCheckGroundTerm() return true; } -template -inline bool CodeTree::Matcher::doSearchStruct() +template +inline bool CodeTree::Matcher::doSearchStruct() { ASS_EQ(op->_instruction(), SEARCH_STRUCT); @@ -805,9 +808,11 @@ inline bool CodeTree::Matcher::doSearchStruct() return true; } -template struct CodeTree::Matcher; -template struct CodeTree::Matcher; -template struct CodeTree::Matcher; +template struct CodeTree::Matcher; +template struct CodeTree::Matcher; +template struct CodeTree::Matcher; +template struct CodeTree::Matcher; +template struct CodeTree::Matcher; //////////////// auxiliary //////////////////// diff --git a/Indexing/CodeTree.hpp b/Indexing/CodeTree.hpp index 58ab1e56c..7f60a86a6 100644 --- a/Indexing/CodeTree.hpp +++ b/Indexing/CodeTree.hpp @@ -20,6 +20,7 @@ #include "Lib/Allocator.hpp" #include "Lib/DArray.hpp" #include "Lib/DHMap.hpp" +#include "Lib/Environment.hpp" #include "Lib/Stack.hpp" #include "Lib/Vector.hpp" @@ -326,7 +327,7 @@ class CodeTree * this one. After use, the @b deinit function should be called (if * present). This allows for reuse of a single object. */ - template + template struct Matcher : public std::conditional::type { @@ -334,6 +335,14 @@ class CodeTree // removing, which works on variables static_assert(removing || !checkRange); + Matcher() { + if constexpr (higherOrder) { + ASS(env.higherOrder()); + } else { + ASS(!env.higherOrder()); + } + } + /** * Backtracking point for the interpretation of the code tree. */ diff --git a/Indexing/CodeTreeInterfaces.cpp b/Indexing/CodeTreeInterfaces.cpp index ce73a9048..0e973033f 100644 --- a/Indexing/CodeTreeInterfaces.cpp +++ b/Indexing/CodeTreeInterfaces.cpp @@ -86,8 +86,8 @@ class CodeTreeSubstitution /////////////////////////////////////// -template -class CodeTreeTIS::ResultIterator +template +class CodeTreeTIS::ResultIterator : public IteratorCore> { public: @@ -150,11 +150,11 @@ class CodeTreeTIS::ResultIterator Data* _found; bool _finished; CodeTreeTIS* _tree; - Recycled::TermMatcher> _matcher; + Recycled::TermMatcher> _matcher; }; -template -VirtualIterator> CodeTreeTIS::getGeneralizations(TypedTermList t, bool retrieveSubstitutions) +template +VirtualIterator> CodeTreeTIS::getGeneralizations(TypedTermList t, bool retrieveSubstitutions) { if(_ct.isEmpty()) { return VirtualIterator>::getEmpty(); @@ -163,14 +163,14 @@ VirtualIterator> CodeTreeTIS::getGene return vi( new ResultIterator(this, t, retrieveSubstitutions) ); } -template -bool CodeTreeTIS::generalizationExists(TermList t) +template +bool CodeTreeTIS::generalizationExists(TermList t) { if(_ct.isEmpty()) { return false; } - static typename TermCodeTree::TermMatcher tm; + static typename TermCodeTree::TermMatcher tm; tm.init(&_ct, t); bool res=tm.next(); @@ -179,12 +179,15 @@ bool CodeTreeTIS::generalizationExists(TermList t) return res; } -template class CodeTreeTIS; -template class CodeTreeTIS; +template class CodeTreeTIS; +template class CodeTreeTIS; +template class CodeTreeTIS; +template class CodeTreeTIS; ///////////////// CodeTreeSubsumptionIndex ////////////////////// -void CodeTreeSubsumptionIndex::handleClause(Clause* cl, bool adding) +template +void CodeTreeSubsumptionIndex::handleClause(Clause* cl, bool adding) { TIME_TRACE("codetree subsumption index maintenance"); @@ -196,4 +199,7 @@ void CodeTreeSubsumptionIndex::handleClause(Clause* cl, bool adding) } } +template class CodeTreeSubsumptionIndex; +template class CodeTreeSubsumptionIndex; + } diff --git a/Indexing/CodeTreeInterfaces.hpp b/Indexing/CodeTreeInterfaces.hpp index aecf1a733..db5b25fd0 100644 --- a/Indexing/CodeTreeInterfaces.hpp +++ b/Indexing/CodeTreeInterfaces.hpp @@ -34,7 +34,7 @@ using namespace Lib; * Term indexing structure using code trees to retrieve generalizations */ -template +template class CodeTreeTIS : public TermIndexingStructure { public: @@ -60,20 +60,21 @@ class CodeTreeTIS : public TermIndexingStructure private: class ResultIterator; - TermCodeTree _ct; + TermCodeTree _ct; }; +template class CodeTreeSubsumptionIndex : public Index { public: CodeTreeSubsumptionIndex(SaturationAlgorithm&) {} - ClauseCodeTree* getClauseCodeTree() { return &_ct; } + ClauseCodeTree* getClauseCodeTree() { return &_ct; } protected: void handleClause(Clause* c, bool adding) override; private: - ClauseCodeTree _ct; + ClauseCodeTree _ct; }; }; diff --git a/Indexing/IndexManager.cpp b/Indexing/IndexManager.cpp index d6b2d70f2..8e3b38249 100644 --- a/Indexing/IndexManager.cpp +++ b/Indexing/IndexManager.cpp @@ -33,14 +33,16 @@ using namespace Indexing; SIMP_INDEX_IMPL(AlascaIndex) SIMP_INDEX_IMPL(AlascaIndex) -SIMP_INDEX_IMPL(DemodulationLHSIndex) -SIMP_INDEX_IMPL(CodeTreeSubsumptionIndex) +SIMP_INDEX_IMPL(DemodulationLHSIndex) +SIMP_INDEX_IMPL(DemodulationLHSIndex) +SIMP_INDEX_IMPL(CodeTreeSubsumptionIndex) +SIMP_INDEX_IMPL(CodeTreeSubsumptionIndex) SIMP_INDEX_IMPL(BackwardSubsumptionIndex) SIMP_INDEX_IMPL(FwSubsSimplifyingLiteralIndex) SIMP_INDEX_IMPL(RewriteRuleIndex) SIMP_INDEX_IMPL(UnitClauseLiteralIndex) -SIMP_INDEX_IMPL(DemodulationSubtermIndex) SIMP_INDEX_IMPL(DemodulationSubtermIndex) +SIMP_INDEX_IMPL(DemodulationSubtermIndex) SIMP_INDEX_IMPL(SkolemisingFormulaIndex) SIMP_INDEX_IMPL(FSDLiteralIndex) diff --git a/Indexing/TermCodeTree.cpp b/Indexing/TermCodeTree.cpp index b4822683b..e16ce5de8 100644 --- a/Indexing/TermCodeTree.cpp +++ b/Indexing/TermCodeTree.cpp @@ -25,23 +25,23 @@ namespace Indexing using namespace Lib; using namespace Kernel; -template -void TermCodeTree::onCodeOpDestroying(CodeOp* op) +template +void TermCodeTree::onCodeOpDestroying(CodeOp* op) { if (op->isSuccess()) { delete op->getSuccessResult(); } } -template -TermCodeTree::TermCodeTree() +template +TermCodeTree::TermCodeTree() { _clauseCodeTree=false; _onCodeOpDestroying = onCodeOpDestroying; } -template -void TermCodeTree::insert(Data* data) +template +void TermCodeTree::insert(Data* data) { static CodeStack code; code.reset(); @@ -66,8 +66,8 @@ void TermCodeTree::insert(Data* data) //////////////// removal //////////////////// -template -void TermCodeTree::remove(const Data& data) +template +void TermCodeTree::remove(const Data& data) { static RemovingTermMatcher rtm; static Stack firstsInBlocks; @@ -118,46 +118,43 @@ void TermCodeTree::remove(const Data& data) */ } // TermCodeTree::remove -template -void TermCodeTree::RemovingTermMatcher::init(FlatTerm* ft_, +template +void TermCodeTree::RemovingTermMatcher::init(FlatTerm* ft_, TermCodeTree* tree_, Stack* firstsInBlocks_) { - Matcher::init(tree_, tree_->getEntryPoint(), 0, 0, firstsInBlocks_); + Base::init(tree_, tree_->getEntryPoint(), /*linfos_=*/0, /*linfoCnt_=*/0, firstsInBlocks_); - firstsInBlocks->push(entry); + Base::firstsInBlocks->push(Base::entry); - ft=ft_; - tp=0; - op=entry; + Base::ft=ft_; + Base::tp=0; + Base::op=Base::entry; } //////////////// retrieval //////////////////// -template -TermCodeTree::TermMatcher::TermMatcher() +template +TermCodeTree::TermMatcher::TermMatcher() { #if VDEBUG ft=0; #endif } -template -void TermCodeTree::TermMatcher::init(CodeTree* tree, TermList t) +template +void TermCodeTree::TermMatcher::init(CodeTree* tree, TermList t) { - Matcher::init(tree,tree->getEntryPoint()); - - linfos=0; - linfoCnt=0; + Base::init(tree,tree->getEntryPoint(),/*linfos_=*/0,/*linfoCnt_=*/0); ASS(!ft); ft = FlatTerm::createUnexpanded(t); - op=entry; - tp=0; + Base::op=Base::entry; + Base::tp=0; } -template -void TermCodeTree::TermMatcher::reset() +template +void TermCodeTree::TermMatcher::reset() { ft->destroy(); #if VDEBUG @@ -165,24 +162,26 @@ void TermCodeTree::TermMatcher::reset() #endif } -template -Data* TermCodeTree::TermMatcher::next() +template +Data* TermCodeTree::TermMatcher::next() { - if (finished()) { + if (Base::finished()) { //all possible matches are exhausted return 0; } - _matched=execute(); - if (!_matched) { + Base::_matched=Base::execute(); + if (!Base::_matched) { return 0; } - ASS(op->isSuccess()); - return op->getSuccessResult(); + ASS(Base::op->isSuccess()); + return Base::op->template getSuccessResult(); } -template class TermCodeTree; -template class TermCodeTree; +template class TermCodeTree; +template class TermCodeTree; +template class TermCodeTree; +template class TermCodeTree; }; diff --git a/Indexing/TermCodeTree.hpp b/Indexing/TermCodeTree.hpp index 75aa8f790..1119a2b6f 100644 --- a/Indexing/TermCodeTree.hpp +++ b/Indexing/TermCodeTree.hpp @@ -19,7 +19,6 @@ #include "Lib/Allocator.hpp" #include "Lib/Stack.hpp" -#include "Lib/Vector.hpp" #include "CodeTree.hpp" @@ -29,7 +28,7 @@ namespace Indexing { using namespace Lib; using namespace Kernel; -template +template class TermCodeTree : public CodeTree { protected: @@ -43,19 +42,23 @@ class TermCodeTree : public CodeTree private: struct RemovingTermMatcher - : public Matcher + : public Matcher { public: - void init(FlatTerm* ft_, TermCodeTree* tree_, Stack* firstsInBlocks_); + using Base = Matcher; + void init(FlatTerm* ft_, TermCodeTree* tree_, Stack* firstsInBlocks_); }; public: struct TermMatcher - : public Matcher + : public Matcher { TermMatcher(); + using Base = Matcher; + using Base::ft; + void init(CodeTree* tree, TermList t); void reset(); diff --git a/Indexing/TermIndex.cpp b/Indexing/TermIndex.cpp index 1afbe03d5..f46774570 100644 --- a/Indexing/TermIndex.cpp +++ b/Indexing/TermIndex.cpp @@ -112,11 +112,13 @@ void DemodulationSubtermIndex::handleClause(Clause* c, bool adding) template class DemodulationSubtermIndex; template class DemodulationSubtermIndex; -DemodulationLHSIndex::DemodulationLHSIndex(SaturationAlgorithm& salg) -: TermIndex(new CodeTreeTIS()), _ord(salg.getOrdering()), +template +DemodulationLHSIndex::DemodulationLHSIndex(SaturationAlgorithm& salg) +: TermIndex(new CodeTreeTIS()), _ord(salg.getOrdering()), _preordered(salg.getOptions().forwardDemodulation()==Options::Demodulation::PREORDERED) {}; -void DemodulationLHSIndex::handleClause(Clause* c, bool adding) +template +void DemodulationLHSIndex::handleClause(Clause* c, bool adding) { if (c->length()!=1) { return; @@ -143,6 +145,9 @@ void DemodulationLHSIndex::handleClause(Clause* c, bool adding) } } +template class DemodulationLHSIndex; +template class DemodulationLHSIndex; + InductionTermIndex::InductionTermIndex(SaturationAlgorithm& salg) : TermIndex(new TermSubstitutionTree()), _inductionGroundOnly(salg.getOptions().inductionGroundOnly()) {} diff --git a/Indexing/TermIndex.hpp b/Indexing/TermIndex.hpp index 549268f9e..95a0ad57e 100644 --- a/Indexing/TermIndex.hpp +++ b/Indexing/TermIndex.hpp @@ -90,6 +90,7 @@ class DemodulationSubtermIndex /** * Term index for forward demodulation */ +template class DemodulationLHSIndex : public TermIndex { diff --git a/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp b/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp index b02902943..c030aba22 100644 --- a/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp +++ b/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp @@ -19,19 +19,21 @@ namespace Inferences { -CodeTreeForwardSubsumptionAndResolution::CodeTreeForwardSubsumptionAndResolution(SaturationAlgorithm& salg) +template +CodeTreeForwardSubsumptionAndResolution::CodeTreeForwardSubsumptionAndResolution(SaturationAlgorithm& salg) : _subsumptionResolution(salg.getOptions().forwardSubsumptionResolution()), - _index(salg.getSimplifyingIndex()), + _index(salg.getSimplifyingIndex>()), _ct(_index->getClauseCodeTree()) {} -bool CodeTreeForwardSubsumptionAndResolution::perform(Clause *cl, Clause *&replacement, ClauseIterator &premises) +template +bool CodeTreeForwardSubsumptionAndResolution::perform(Clause *cl, Clause *&replacement, ClauseIterator &premises) { if (_ct->isEmpty()) { return false; } - static ClauseCodeTree::ClauseMatcher cm; + static typename ClauseCodeTree::ClauseMatcher cm; cm.init(_ct, cl, _subsumptionResolution); @@ -67,4 +69,7 @@ bool CodeTreeForwardSubsumptionAndResolution::perform(Clause *cl, Clause *&repla return false; } +template class CodeTreeForwardSubsumptionAndResolution; +template class CodeTreeForwardSubsumptionAndResolution; + } // namespace Inferences diff --git a/Inferences/CodeTreeForwardSubsumptionAndResolution.hpp b/Inferences/CodeTreeForwardSubsumptionAndResolution.hpp index d3c892b53..5a3048937 100644 --- a/Inferences/CodeTreeForwardSubsumptionAndResolution.hpp +++ b/Inferences/CodeTreeForwardSubsumptionAndResolution.hpp @@ -23,6 +23,7 @@ namespace Inferences { +template class CodeTreeForwardSubsumptionAndResolution : public ForwardSimplificationEngine { @@ -35,8 +36,8 @@ class CodeTreeForwardSubsumptionAndResolution private: const bool _subsumptionResolution; - std::shared_ptr _index; - Indexing::ClauseCodeTree* _ct; + std::shared_ptr> _index; + Indexing::ClauseCodeTree* _ct; #if VDEBUG SATSubsumption::SATSubsumptionAndResolution satSubs; #endif diff --git a/Inferences/ForwardDemodulation.cpp b/Inferences/ForwardDemodulation.cpp index a02d1a8f2..dc27c6905 100644 --- a/Inferences/ForwardDemodulation.cpp +++ b/Inferences/ForwardDemodulation.cpp @@ -76,7 +76,7 @@ ForwardDemodulation::ForwardDemodulation(SaturationAlgorithm& salg) _skipNonequationalLiterals(salg.getOptions().demodulationOnlyEquational()), _helper(DemodulationHelper(salg.getOptions(), &salg.getOrdering())), _ord(salg.getOrdering()), - _index(salg.getSimplifyingIndex()) + _index(salg.getSimplifyingIndex>()) {} template diff --git a/Inferences/ForwardDemodulation.hpp b/Inferences/ForwardDemodulation.hpp index 83da1e613..6f07f58e0 100644 --- a/Inferences/ForwardDemodulation.hpp +++ b/Inferences/ForwardDemodulation.hpp @@ -44,7 +44,7 @@ class ForwardDemodulation const bool _skipNonequationalLiterals; const DemodulationHelper _helper; const Ordering& _ord; - std::shared_ptr _index; + std::shared_ptr> _index; }; using ForwardDemodulationExtra = RewriteInferenceExtra; diff --git a/Inferences/ForwardGroundJoinability.cpp b/Inferences/ForwardGroundJoinability.cpp index 07bfb709c..ea7e0af65 100644 --- a/Inferences/ForwardGroundJoinability.cpp +++ b/Inferences/ForwardGroundJoinability.cpp @@ -48,14 +48,16 @@ struct Applicator : SubstApplicator { } // end namespace -ForwardGroundJoinability::ForwardGroundJoinability(SaturationAlgorithm& salg) +template +ForwardGroundJoinability::ForwardGroundJoinability(SaturationAlgorithm& salg) : _ord(salg.getOrdering()), - _index(salg.getSimplifyingIndex()) + _index(salg.getSimplifyingIndex>()) {} #define ITERATION_LIMIT 500 -bool ForwardGroundJoinability::perform(Clause* cl, Clause*& replacement, ClauseIterator& premises) +template +bool ForwardGroundJoinability::perform(Clause* cl, Clause*& replacement, ClauseIterator& premises) { // cout << "trying " << *cl << endl; @@ -182,7 +184,8 @@ bool ForwardGroundJoinability::perform(Clause* cl, Clause*& replacement, ClauseI return true; } -ForwardGroundJoinability::RedundancyCheck::RedundancyCheck(const Ordering& ord, Literal* data) +template +ForwardGroundJoinability::RedundancyCheck::RedundancyCheck(const Ordering& ord, Literal* data) : tod(ord.createTermOrderingDiagram(/*ground=*/true)), traversal(tod.get(), nullptr) { tod->_source = Branch(data, tod->_sink); @@ -191,7 +194,8 @@ ForwardGroundJoinability::RedundancyCheck::RedundancyCheck(const Ordering& ord, ASS_EQ(_curr,&tod->_source); } -std::pair ForwardGroundJoinability::RedundancyCheck::next( +template +std::pair ForwardGroundJoinability::RedundancyCheck::next( Stack ordCons, Literal* data) { static Ordering::Result ordVals[] = { Ordering::EQUAL, Ordering::GREATER, Ordering::INCOMPARABLE }; @@ -250,7 +254,8 @@ std::pair ForwardGroundJoinability::Redunda return { nullptr, nullptr }; } -bool ForwardGroundJoinability::makeEqual(Literal* lit, Stack& res) +template +bool ForwardGroundJoinability::makeEqual(Literal* lit, Stack& res) { ASS(lit->isEquality()); ASS(lit->isPositive()); @@ -291,4 +296,7 @@ bool ForwardGroundJoinability::makeEqual(Literal* lit, Stack; +template class ForwardGroundJoinability; + } diff --git a/Inferences/ForwardGroundJoinability.hpp b/Inferences/ForwardGroundJoinability.hpp index c549882d7..1a3e29f0e 100644 --- a/Inferences/ForwardGroundJoinability.hpp +++ b/Inferences/ForwardGroundJoinability.hpp @@ -27,6 +27,7 @@ using namespace Kernel; using namespace Indexing; using namespace Saturation; +template class ForwardGroundJoinability : public ForwardSimplificationEngine { @@ -54,7 +55,7 @@ class ForwardGroundJoinability }; const Ordering& _ord; - std::shared_ptr _index; + std::shared_ptr> _index; }; }; diff --git a/Kernel/Clause.cpp b/Kernel/Clause.cpp index 792fd5563..1ebcb556e 100644 --- a/Kernel/Clause.cpp +++ b/Kernel/Clause.cpp @@ -82,6 +82,12 @@ Clause::Clause(Literal* const* lits, unsigned length, Inference inf) (*this)[i] = lits[i]; } +#if VDEBUG + // check that the variable sorts are consistent + DHMap temp; + SortHelper::collectVariableSorts(this, temp); +#endif + doUnitTracing(); } diff --git a/Kernel/TermOrderingDiagram.hpp b/Kernel/TermOrderingDiagram.hpp index f6830cf25..2f864deb7 100644 --- a/Kernel/TermOrderingDiagram.hpp +++ b/Kernel/TermOrderingDiagram.hpp @@ -21,7 +21,7 @@ #include "Ordering.hpp" namespace Inferences { - class ForwardGroundJoinability; + template class ForwardGroundJoinability; } namespace Kernel { @@ -195,7 +195,7 @@ struct TermOrderingDiagram const SubstApplicator* _appl; bool _ground; - friend class Inferences::ForwardGroundJoinability; + template friend class Inferences::ForwardGroundJoinability; public: template diff --git a/Lib/Vector.hpp b/Lib/Vector.hpp index 8a6c4f625..4eab9000d 100644 --- a/Lib/Vector.hpp +++ b/Lib/Vector.hpp @@ -25,7 +25,7 @@ namespace Indexing { class CodeTree; - class ClauseCodeTree; + template class ClauseCodeTree; } namespace Lib { @@ -117,7 +117,7 @@ class Vector } // toString friend class Indexing::CodeTree; - friend class Indexing::ClauseCodeTree; + template friend class Indexing::ClauseCodeTree; /** * Iterator that deallocates the vector when it yields the last value. diff --git a/Saturation/SaturationAlgorithm.cpp b/Saturation/SaturationAlgorithm.cpp index 88c6ebc69..b6558aacd 100644 --- a/Saturation/SaturationAlgorithm.cpp +++ b/Saturation/SaturationAlgorithm.cpp @@ -1597,7 +1597,11 @@ SaturationAlgorithm *SaturationAlgorithm::createFromOptions(Problem& prb, const } if (mayHaveEquality) { if (opt.forwardGroundJoinability()) { - res->addExpensiveForwardSimplifierToFront(); + if (prb.isHigherOrder()) { + res->addExpensiveForwardSimplifierToFront>(); + } else { + res->addExpensiveForwardSimplifierToFront>(); + } } switch (opt.forwardDemodulation()) { case Options::Demodulation::ALL: @@ -1619,7 +1623,11 @@ SaturationAlgorithm *SaturationAlgorithm::createFromOptions(Problem& prb, const if (opt.forwardSubsumption()) { if (opt.codeTreeSubsumption()) { - res->addForwardSimplifierToFront(); + if (prb.isHigherOrder()) { + res->addForwardSimplifierToFront>(); + } else { + res->addForwardSimplifierToFront>(); + } } else { res->addForwardSimplifierToFront(); } diff --git a/Shell/FunctionDefinitionHandler.cpp b/Shell/FunctionDefinitionHandler.cpp index a2a3d2026..12f725df5 100644 --- a/Shell/FunctionDefinitionHandler.cpp +++ b/Shell/FunctionDefinitionHandler.cpp @@ -88,7 +88,7 @@ void FunctionDefinitionHandler::initAndPreprocessEarly(Problem& prb) void FunctionDefinitionHandler::initAndPreprocessLate(Problem& prb,const Options& opts) { // reset state - _is = new CodeTreeTIS(); + _is = new CodeTreeTIS(); _templates.reset(); UnitList::DelIterator it(prb.units()); diff --git a/Shell/FunctionDefinitionHandler.hpp b/Shell/FunctionDefinitionHandler.hpp index 104a0b86e..0ecf8b946 100644 --- a/Shell/FunctionDefinitionHandler.hpp +++ b/Shell/FunctionDefinitionHandler.hpp @@ -111,7 +111,7 @@ class FunctionDefinitionHandler const InductionTemplate* matchesTerm(Term* t, Stack& inductionTerms) const; private: - ScopedPtr> _is; + ScopedPtr> _is; DHMap, RecursionTemplate> _templates; }; diff --git a/Shell/PartialRedundancyHandler.cpp b/Shell/PartialRedundancyHandler.cpp index 8a76779bd..8e470681a 100644 --- a/Shell/PartialRedundancyHandler.cpp +++ b/Shell/PartialRedundancyHandler.cpp @@ -246,7 +246,7 @@ class PartialRedundancyHandler::ConstraintIndex } struct SubstMatcher - : public Matcher + : public Matcher { void init(CodeTree* tree, const TermStack& ts) { @@ -281,7 +281,7 @@ class PartialRedundancyHandler::ConstraintIndex }; struct VariantMatcher - : public Matcher + : public Matcher { public: void init(FlatTerm* ft_, CodeTree* tree_, Stack* firstsInBlocks_) { diff --git a/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp b/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp index 351432a28..34b0c605b 100644 --- a/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp +++ b/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp @@ -61,7 +61,7 @@ using namespace Test; namespace { inline auto tester() { - return FwdBwdSimplification::TestCase() + return FwdBwdSimplification::TestCase, BackwardSubsumptionAndResolution>() .options({ { "backward_subsumption", "on" }, { "backward_subsumption_resolution", "on" } diff --git a/UnitTests/tInferences_ForwardGroundJoinability.cpp b/UnitTests/tInferences_ForwardGroundJoinability.cpp index 8e1c5fb0c..bb8bb5b4b 100644 --- a/UnitTests/tInferences_ForwardGroundJoinability.cpp +++ b/UnitTests/tInferences_ForwardGroundJoinability.cpp @@ -71,7 +71,7 @@ void joinabilityTest(ClauseStack axioms, Clause* cl, bool joinable, bool useKbo) env.options->set("term_ordering", useKbo ? "kbo" : "lpo"); Test::MockedSaturationAlgorithm salg(p, o); - ForwardGroundJoinability fgj(salg); + ForwardGroundJoinability fgj(salg); auto container = salg.getSimplifyingClauseContainer(); From e16d95ea50501de515163b53ff0eaa86b3954252 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Wed, 25 Mar 2026 17:03:28 +0100 Subject: [PATCH 3/7] Fix some errors --- Saturation/ProvingHelper.cpp | 2 ++ Shell/TweeGoalTransformation.cpp | 4 ++++ UnitTests/tALASCA_Superposition.cpp | 2 +- UnitTests/tFunctionDefinitionHandler.cpp | 4 ++-- UnitTests/tInferences_TheoryInstAndSimp.cpp | 21 +++++++++++---------- 5 files changed, 20 insertions(+), 13 deletions(-) diff --git a/Saturation/ProvingHelper.cpp b/Saturation/ProvingHelper.cpp index 89d47d9f8..a58413fb3 100644 --- a/Saturation/ProvingHelper.cpp +++ b/Saturation/ProvingHelper.cpp @@ -132,6 +132,8 @@ void ProvingHelper::runVampire(Problem& prb, const Options& opt) //decide whether to use poly or mono well-typedness test //after options have been read. Equality Proxy can introduce poly in mono. env.sharing->setPoly(); + // Preprocessing can alter whether a problem is HO, update it here. + env.setHigherOrder(env.getMainProblem()->isHigherOrder()); env.options->resolveAwayAutoValues(prb); diff --git a/Shell/TweeGoalTransformation.cpp b/Shell/TweeGoalTransformation.cpp index 290dc67ea..9bc624246 100644 --- a/Shell/TweeGoalTransformation.cpp +++ b/Shell/TweeGoalTransformation.cpp @@ -115,6 +115,10 @@ class Definizator : public BottomUpTermTransformer { Term* t = trm.term(); if (t->isSort() || t->arity() == 0 || (!t->ground() && _groundOnly)) return trm; + if (env.higherOrder() && trm.containsLooseDBIndex()) { + return trm; + } + Term* key = t; if (!t->ground()) { // as we go bottom up, t is never too big (well, it could be wide, but at least not deep) diff --git a/UnitTests/tALASCA_Superposition.cpp b/UnitTests/tALASCA_Superposition.cpp index 6cd5c71f6..36e1a1d9c 100644 --- a/UnitTests/tALASCA_Superposition.cpp +++ b/UnitTests/tALASCA_Superposition.cpp @@ -548,7 +548,7 @@ TEST_GENERATION(bug03, alascaSymmetricTest() .inputs ({ clause({ pa(aa) }) - , clause({ x == sorted(y, alpha), fa(x) != fa(y) }) + , clause({ x == sorted(y, Rat), fa(x) != fa(y) }) }) .expected(exactly( /* nothing */ diff --git a/UnitTests/tFunctionDefinitionHandler.cpp b/UnitTests/tFunctionDefinitionHandler.cpp index 50f8b1b37..31832220c 100644 --- a/UnitTests/tFunctionDefinitionHandler.cpp +++ b/UnitTests/tFunctionDefinitionHandler.cpp @@ -75,9 +75,9 @@ TEST_FUN(test_01) { clause({ def_s(f(r(x), r(y)), f(f(x, r(r(y))), y)) }), clause({ def_s(g(r(x)), g(f(x,x))) }), clause({ def_u(h(x, y, r1(x, z)), h(y, y, z)) }), - clause({ def_u(h(r(x), y, z), h(x, x, r2(y,z))) }), + clause({ def_u(h(r(x), y, z), h(x, x, r2(z,y))) }), clause({ def_p(r(r(x))), p(y) }), - clause({ def_q(r1(x,y),r(z)), q(y,r(z)), g(b) == b, ~q(z,b) }), + clause({ def_q(r1(x,y),r(z)), q(y,r(z)), g(b) == b, ~q(b1,b) }), }); ASS(!handler.getRecursionTemplate(f(x,y).sugaredExpr().term())); diff --git a/UnitTests/tInferences_TheoryInstAndSimp.cpp b/UnitTests/tInferences_TheoryInstAndSimp.cpp index d3f1e153d..8d2237868 100644 --- a/UnitTests/tInferences_TheoryInstAndSimp.cpp +++ b/UnitTests/tInferences_TheoryInstAndSimp.cpp @@ -120,16 +120,17 @@ TEST_GENERATION(test_02, DECL_CONST(a, alpha) \ DECL_PRED(p, {list}) \ -TEST_GENERATION_WITH_SUGAR(test_03, - MY_GEN_RULE, MY_GEN_TESTER, LIST_ALPHA_SUGAR, - Generation::SymmetricTest() - .options(options("all")) - .inputs({ clause({ cons(a, nil()) != cons(x, nil()), - p(x) }) }) - .expected(exactly( - )) - .premiseRedundant(false) - ) +// TODO fix this test with wrong variable sorts +// TEST_GENERATION_WITH_SUGAR(test_03, +// MY_GEN_RULE, MY_GEN_TESTER, LIST_ALPHA_SUGAR, +// Generation::SymmetricTest() +// .options(options("all")) +// .inputs({ clause({ cons(a, nil()) != cons(x, nil()), +// p(x) }) }) +// .expected(exactly( +// )) +// .premiseRedundant(false) +// ) #define RAT_SYNTAX_SUGAR \ DECL_VARS \ From fb3c402cfb925ac5a20d944a2e16340db47dedc2 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Thu, 26 Mar 2026 09:31:38 +0100 Subject: [PATCH 4/7] Add HOL sampler --- samplers/samplerHOL.smp | 404 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 404 insertions(+) create mode 100644 samplers/samplerHOL.smp diff --git a/samplers/samplerHOL.smp b/samplers/samplerHOL.smp new file mode 100644 index 000000000..908e5895b --- /dev/null +++ b/samplers/samplerHOL.smp @@ -0,0 +1,404 @@ +# MACRO DEFINITIONS + +# set $has_z3 to false, if you want to sample without it +> $has_z3 ~cat true:1 + +# PREPROCESSING + +# blocked_clause_elimination +> bce ~cat off:5,on:1 + +# equality_proxy +intent=unsat > ep ~cat off:70,RST:2,R:3,RSTC:2,RS:3 +# mono_ep +ep!=off > mep ~cat on:10,off:1 + +# equality_resolution_with_deletion +> erd ~cat on:10,off:1 + +# function_definition_elimination +> fde ~cat all:5,none:1,unused:1 + +# general_splitting +> gsp ~cat off:8,on:1 + +# newcnf +> newcnf ~cat on:9,off:25 + +# inline_let -- this is probably irrelevant on TPTP anyway +newcnf=on > ile ~cat off:10,on:1 + +# naming +> $nm ~cat Z:1,NZ:5 +$nm=Z > nm ~cat 0:1 +$nm=NZ > nm ~sgd 0.07,2 + +# inequality_splitting +> $ins ~cat Z:2,NZ:1 +$ins=Z > ins ~cat 0:1 +$ins=NZ > ins ~sgd 0.4,1 + +# random_polarities +> rp ~cat off:3,on:1 + +# twee_goal_transformation +> tgt ~cat off:10,ground:6,full:5 + +# sine_selection +intent=unsat > ss ~cat off:1182,included:135,axioms:392 + +# sine_depth +intent=unsat ss!=off > sd ~cat 0:45,1:13,2:12,3:5,4:4,5:4,7:3,10:2,12:1,15:1 + +# sine_generality_threshold +intent=unsat ss!=off > sgt ~cat 0:7,5:1,10:1,15:1,20:1,30:1,50:1,100:1 + +# sine_tolerance +intent=unsat ss!=off > st ~cat -1.0:50,1.0:150,1.5:37,2.0:60,2.5:20,3.0:70,3.5:15,4.0:60,4.5:15,5.0:50,5.5:10,6.0:30,7.0:20 + +# unused_predicate_definition_removal +> updr ~cat on:16,off:1 + +# SATURATION + +# saturation_algorithms +intent=unsat ep=off > sa ~cat fmb:10,lrs:600,discount:572,otter:236 +intent=unsat ep!=off > sa ~cat lrs:600,discount:572,otter:236 +intent=sat > sa ~cat fmb:22,otter:60,discount:28 + +# set_of_support +intent=unsat sa!=fmb > sos ~cat off:80,on:17,all:10 + +# lrs_first_time_check +> $lftc ~cat N:5,Y:1 +sa=lrs $lftc=Y > lftc ~ui 5,95 + +# literal selection +> $s_pos ~cat Y:4,N:1 +intent=unsat sa!=fmb $s_pos=Y > s ~cat 0:11,1:31,2:52,3:21,4:22,10:300,11:131,20:11,21:66,22:11,30:6,31:14,32:4,33:10,34:3,35:8,666:50,1002:141,1003:14,1004:23,1010:145,1011:357,1666:50 +intent=unsat sa!=fmb $s_pos=N > s ~cat -1:31,-2:52,-3:21,-4:22,-10:300,-11:131,-20:11,-21:66,-22:11,-30:6,-31:14,-32:4,-33:10,-34:3,-35:8,-666:50,-1002:141,-1003:14,-1004:23,-1010:145,-1011:357,-1666:50 + +intent=sat sa!=fmb $s_pos=Y > s ~cat 0:11,1:31,2:52,3:21,4:22,10:300,11:131,20:11,21:66,22:11,30:6,31:14,32:4,33:10,34:3,35:8,666:50 +intent=sat sa!=fmb $s_pos=N > s ~cat -1:31,-2:52,-3:21,-4:22,-10:300,-11:131,-20:11,-21:66,-22:11,-30:6,-31:14,-32:4,-33:10,-34:3,-35:8,-666:50 + +# lookahaed_delay +> $ls ~cat off:1 +sa!=fmb s=11 > $ls ~cat on:1 +sa!=fmb s=-11 > $ls ~cat on:1 +sa!=fmb s=1011 > $ls ~cat on:1 +sa!=fmb s=-1011 > $ls ~cat on:1 + +sa!=fmb $ls=on > lsd ~cat 0:20,1:1,5:1,10:1,20:1,50:1,100:1 + +# age_weight_ratio +sa!=fmb > $awr ~cat A:1,W:1,AW:98 +sa!=fmb $awr=A > awr ~set 1:0 +sa!=fmb $awr=W > awr ~set 0:1 +sa!=fmb $awr=AW > awr ~u2r -10;4;: + +# random_awr +sa!=fmb > rawr ~cat on:4,off:1 + +# lrs_weight_limit_only +sa=lrs > lwlo ~cat off:5,on:1 + +# lrs_retroactive_deletes +sa=lrs > lrd ~cat off:1,on:1 + +# lrs_estimate_correction_coef +# > $lecc ~cat 1:1 +# sa=lrs > $lecc ~cat 1:10,666:1 +# sa=lrs $lecc=1 > lecc ~cat 1.0:1 +# sa=lrs $lecc!=1 > lecc ~uf 0.5,2.0 +# TODO: leaving out weird timing dependent options + +# nongoal_weight_coefficient +sa!=fmb > $nwc ~cat 1:2,666:1 +sa!=fmb $nwc=1 > nwc ~cat 1:1 +sa!=fmb $nwc!=1 > nwc ~uf 0.5,15.0 +# TODO: we will most likely want a new distribution here for ($nwc!=1) just above! + +# restrict_nwc_to_goal_constants +sa!=fmb nwc!=1 > rnwc ~cat off:5,on:1 + +# literal_maximality_aftercheck +sa!=fmb > lma ~cat off:500,on:83 + +# POSITIVE LITERAL SPLIT QUEUE +sa!=fmb > plsq ~cat off:4,on:1 + +# positive_literal_split_queue_layered_arrangement +plsq=on > plsql ~cat on:66,off:162 + +# positive_literal_split_queue_cutoffs +plsq=on > plsqc ~cat 0:117,1:92,2:19,3:5,4:1 + +# positive_literal_split_queue_ratios +plsq=on > plsqr ~u2r -5;7;, + +# INFERENCES + +# superposition (don't turn this off at home!) +intent=unsat sa!=fmb > sup ~cat on:100,off:1 + +# simultaneous_superposition +sa!=fmb sup=on > sims ~cat on:50,off:1 + +# superposition_from_variables +intent=unsat sa!=fmb sup=on > sfv ~cat on:38,off:1 + +# code_tree_subsumption +sa!=fmb > cts ~cat on:3,off:1 + +# forward_subsumption +sa!=fmb > fs ~cat on:500,off:31 + +# forward_subsumption_resolution +sa!=fmb fs=off > fsr ~cat off:1 +sa!=fmb fs=on > fsr ~cat on:500,off:193 + +# forward_subsumption_demodulation +sa!=fmb > fsd ~cat off:500,on:90 + +# forward_subsumption_demodulation_max_matches +sa!=fmb fsd=on > fsdmm ~cat 0:10,1:3,2:2,3:1 + +# backward_demodulation +sa!=fmb > bd ~cat all:500,off:245,preordered:91 + +# backward_subsumption +sa!=fmb fs!=off > bs ~cat off:500,unit_only:74,on:64 + +# backward_subsumption_resolution +sa!=fmb > bsr ~cat off:500,unit_only:118,on:75 + +# backward_subsumption_demodulation +sa!=fmb > bsd ~cat off:500,on:74 + +# backward_subsumption_demodulation_max_matches +sa!=fmb bsd=on > bsdmm ~cat 0:10,1:3,2:2,3:1 + +# condensation +sa!=fmb > cond ~cat off:500,on:89,fast:61 + +# equational_tautology_removal +sa!=fmb > etr ~cat off:500,on:30 + +# extensionality_resolution +sa!=fmb ins=0 > er ~cat off:500,known:25,filter:26 + +# extensionality_allow_pos_eq +sa!=fmb er=filter > eape ~cat off:3,on:1 + +# extensionality_max_length +sa!=fmb er!=off > erml ~cat 0:3,2:1,3:1 + +# fool_paramodulation +sa!=fmb > foolp ~cat off:10,on:1 + +# forward_demodulation +sa!=fmb > fd ~cat all:500,off:41,preordered:168 + +# demodulation_redundancy_check +> $drc ~cat 0:1 +fd!=off > $drc ~cat 1:1 +bd!=off > $drc ~cat 1:1 +intent=unsat sa!=fmb $drc=1 > drc ~cat encompass:500,ordering:500,off:354 +intent=sat sa!=fmb $drc=1 > drc ~cat ordering:643,encompass:554 + +# forward_demodulation_term_ordering_diagrams +sa!=fmb fd!=off > fdtod ~cat on:1,off:1 + +# demodulation_only_equational +sa!=fmb $drc=1 > doe ~cat on:1,off:1 + +# forward_ground_joinability +sa!=fmb > fgj ~cat on:1,off:1 + +# forward_literal_rewriting +intent=unsat sa!=fmb > flr ~cat off:8,on:1 + +# function_definition_introduction +# TODO fix this +# sa!=fmb > fdi ~cat 0:100,2:1,4:1,8:1,16:1,32:1,64:1,128:1,256:1,512:1,1024:1 + +# inner_rewriting +sa!=fmb > irw ~cat off:165,on:6 + +# SINE LEVELS and shit + +# sine_to_age +sa!=fmb > s2a ~cat off:2,on:1 + +# sine_level_split_queue +sa!=fmb > slsq ~cat off:5,on:1 + +# sine_level_split_queue_layered_arrangement +sa!=fmb slsq=on > slsql ~cat on:1,off:1 + +# sine_level_split_queue_cutoffs +sa!=fmb slsq=on > slsqc ~cat 0:10,1:10,2:6,3:3,4:1 + +# sine_level_split_queue_ratios +sa!=fmb slsq=on > slsqr ~u2r -5;2;, + +# ORDERING + +# term_ordering +sa!=fmb > to ~cat kbo:13,lpo:4 + +# symbol_precedence +sa!=fmb > sp ~cat arity:100,const_min:72,frequency:130,const_frequency:49,reverse_frequency:55,reverse_arity:72,weighted_frequency:24,unary_first:28,occurrence:82,unary_frequency:14,const_max:18 +# symbol_precedence_boost +sa!=fmb > spb ~cat none:200,units:78,goal:91,goal_then_units:93,non_intro:14,intro:12 + +# kbo_max_zero +sa!=fmb to=kbo > kmz ~cat off:200,on:1 +# kbo_weight_scheme +sa!=fmb to=kbo > kws ~cat const:50,inv_arity_squared:6,precedence:28,arity_squared:1,inv_arity:5,inv_frequency:8,frequency:2 + +# literal_comparison_mode +intent=unsat sa!=fmb > lcm ~cat standard:500,reverse:66,predicate:51 +intent=sat sa!=fmb > lcm ~cat standard:500,reverse:66,predicate:51 + +# sine_to_pred_levels +sa!=fmb lcm=standard > s2pl ~cat off:50,on:2,no:3 + +# SINE LEVELS - configure (must come after sine_to_age & slsq & s2pl) + +# set $s2a as the disjunction: s2a=on | slsq=on | s2pl!=off +> $s2a ~cat off:1 +s2a=on > $s2a ~cat on:1 +slsq=on > $s2a ~cat on:1 +s2pl!=off > $s2a ~cat on:1 + +# now configure (stealing the values from sine proper, which is not ideal, but should do) + +# sine_to_age_generality_threshold +$s2a=on > s2agt ~cat 0:7,5:1,10:1,15:1,20:1,30:1,50:1,100:1 + +# sine_to_age_tolerance +$s2a=on > s2at ~cat -1.0:50,1.0:150,1.5:37,2.0:60,2.5:20,3.0:70,3.5:15,4.0:60,4.5:15,5.0:50,5.5:10,6.0:30,7.0:20 + +# AVATAR +sa!=fmb > av ~cat on:15,off:4 + +# partial_redundancy_check +sa!=fmb > prc ~cat on:3,off:5 + +# partial_redundancy_ordering_constraints +sa!=fmb prc=on > proc ~cat on:1,off:1 + +# partial_redundancy_avatar_constraints +sa!=fmb av=on prc=on > prac ~cat on:1,off:1 + +# partial_redundancy_literal_constraints +sa!=fmb prc=on > prlc ~cat on:1,off:1 + +# sat_solver +sa!=fmb $has_z3=true av=on > sas ~cat minisat:10,cadical:7,z3:3 +sa!=fmb $has_z3!=true av=on > sas ~cat minisat:10,cadical:7 +sa=fmb > sas ~cat minisat:7,cadical:10 + +# avatar_add_complementary +sa!=fmb av=on > aac ~cat none:147,ground:600 + +# avatar_congruence_closure +sa!=fmb sas!=z3 av=on > acc ~cat off:600,on:58 + +# avatar_minimize_model +sa!=fmb av=on > amm ~cat on:600,off:69 + +# avatar_delete_deactivated +sa!=fmb av=on > add ~cat on:300,large:55,off:8 + +# avatar_literal_polarity_advice +sa!=fmb av=on > alpa ~cat none:300,false:13,true:6,random:4 + +# avatar_nonsplittable_components +sa!=fmb av=on > anc ~cat known:300,all_dependent:38,all:45,none:48 + +# avatar_turn_off_time_frac +# sa!=fmb av=on > $atotf ~cat 1:10,666:1 +# sa!=fmb av=on $atotf=1 > atotf ~cat 1:1 +# sa!=fmb av=on $atotf!=1 > atotf ~uf 0.0,0.7 +# TODO: leaving out weird timing dependent options + +# nonliterals_in_clause_weight +sa!=fmb av=on > nicw ~cat off:600,on:76 + +# split_at_activation +sa!=fmb av=on > sac ~cat off:3,on:1 + +# Michael's clause cleaving TODO +# intent=sat av=on > cm ~cat on:1 + +# BACK TO INFERENCES + +# unit_resulting_resolution +sa!=fmb av=on > urr ~cat off:1200,ec_only:162,on:300,full:40 +sa!=fmb av=off > urr ~cat off:1200,ec_only:162,on:340 + +# binary_resolution +intent=unsat sa!=fmb > br ~cat on:8,off:1 +intent=sat sa!=fmb urr=on > br ~cat on:10,off:1 + +# AVATAR SPLIT QUEUE + +# avatar_split_queue +sa!=fmb av=on > avsq ~cat off:5,on:1 + +# avatar_split_queue_layered_arrangement +sa!=fmb avsq=on > avsql ~cat off:4,on:1 + +# avatar_split_queue_cutoffs +sa!=fmb avsq=on > avsqc ~cat 0:80,1:30,2:20,3:20,4:10,5:5 + +# avatar_split_queue_ratios +sa!=fmb avsq=on > avsqr ~u2r -5;3;, + +# GLOBAL SUBSUMPTION +# global_subsumption +sa!=fmb > gs ~cat off:5,on:1 + +# FMB options + +# TODO: a candidate for hardwiring "on" (go an collect the data) +# fmb_use_simplifying_solver +sa=fmb sas=minisat > fmbuss ~cat off:1,on:5 + +# fmb_enumeration_strategy (TODO: in the multi-sorted setting, sbeam makes only sense with intent=sat) +$has_z3=true sa=fmb > fmbes ~cat sbeam:1,smt:1,contour:1 +$has_z3!=true sa=fmb > fmbes ~cat sbeam:1,contour:1 + +# fmb_size_weight_ratio +fmbes=contour > fmbswr ~ui 0,5 + +# fmb_adjust_sorts +sa=fmb fmbes!=contour > fmbas ~cat group:36,predicate:4,expand:4,off:1,function:1 +sa=fmb fmbes=contour > fmbas ~cat group:36,predicate:4,off:1,function:1 + +# fmb_detect_sort_bounds +sa=fmb fmbas!=predicate fmbas!=function > fmbdsb ~cat off:5,on:1 + +# fmb_detect_sort_bounds_time_limit +fmbdsb=on > fmbdsbt ~cat 1:5,2:2,3:1 + +# fmb_keep_sbeam_generators +sa=fmb fmbes=sbeam > fmbksg ~cat off:2,on:1 + +# fmb_start_size - setting this to values > 1 is making things "finite model incomplete" (but could save time for some problems) +intent=sat sa=fmb > $fmbss ~cat 1:5,666:1 +intent=sat sa=fmb $fmbss=1 > fmbss ~cat 1:1 +intent=sat sa=fmb $fmbss=666 > fmbss ~sgd 0.1,1 + +# fmb_symmetry_symbol_order +sa=fmb > fmbsso ~cat occurrence:22,input_usage:1,preprocessed_usage:1 + +# fmb_symmetry_ratio +sa=fmb > fmbsr ~uf 1.0,2.5 + +# MISSING: +# Any theory reasoning options (including term algebras and sa=z3) +# Any induction options +# Any higher-order options (Higher-order options section) From f4f70df1d5bbdc6fad8041a2aaa23603cb590ab4 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Thu, 26 Mar 2026 09:39:12 +0100 Subject: [PATCH 5/7] Add assertion about synced higher-order options to saturation initialization --- Indexing/CodeTree.hpp | 8 -------- Saturation/SaturationAlgorithm.cpp | 3 +++ 2 files changed, 3 insertions(+), 8 deletions(-) diff --git a/Indexing/CodeTree.hpp b/Indexing/CodeTree.hpp index 7f60a86a6..02d7a0aac 100644 --- a/Indexing/CodeTree.hpp +++ b/Indexing/CodeTree.hpp @@ -335,14 +335,6 @@ class CodeTree // removing, which works on variables static_assert(removing || !checkRange); - Matcher() { - if constexpr (higherOrder) { - ASS(env.higherOrder()); - } else { - ASS(!env.higherOrder()); - } - } - /** * Backtracking point for the interpretation of the code tree. */ diff --git a/Saturation/SaturationAlgorithm.cpp b/Saturation/SaturationAlgorithm.cpp index b6558aacd..7d4f9488c 100644 --- a/Saturation/SaturationAlgorithm.cpp +++ b/Saturation/SaturationAlgorithm.cpp @@ -1381,6 +1381,9 @@ SaturationAlgorithm *SaturationAlgorithm::createFromOptions(Problem& prb, const { bool alascaTakesOver = doesAlascaTakeOver(prb, opt); + // For the following part, we want these two values to be synced + ASS_EQ(env.higherOrder(), prb.isHigherOrder()); + SaturationAlgorithm* res; switch(opt.saturationAlgorithm()) { case Shell::Options::SaturationAlgorithm::DISCOUNT: From 4c8d594c2a252ba525a61ad0020a552297b2bfd2 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Thu, 26 Mar 2026 10:10:54 +0100 Subject: [PATCH 6/7] Adapt subsumption demodulation --- .../BackwardSubsumptionDemodulation.cpp | 21 ++++++++++++------- .../BackwardSubsumptionDemodulation.hpp | 1 + Inferences/ForwardSubsumptionDemodulation.cpp | 17 +++++++++++---- Inferences/ForwardSubsumptionDemodulation.hpp | 1 + Saturation/SaturationAlgorithm.cpp | 12 +++++++++-- .../tInferences_SubsumptionDemodulation.cpp | 2 +- 6 files changed, 39 insertions(+), 15 deletions(-) diff --git a/Inferences/BackwardSubsumptionDemodulation.cpp b/Inferences/BackwardSubsumptionDemodulation.cpp index 05d91b609..22ffde897 100644 --- a/Inferences/BackwardSubsumptionDemodulation.cpp +++ b/Inferences/BackwardSubsumptionDemodulation.cpp @@ -48,8 +48,8 @@ using namespace Kernel; using namespace Indexing; using namespace Saturation; - -BackwardSubsumptionDemodulation::BackwardSubsumptionDemodulation(SaturationAlgorithm& salg) +template +BackwardSubsumptionDemodulation::BackwardSubsumptionDemodulation(SaturationAlgorithm& salg) : _ord(salg.getOrdering()) , _index(salg.getSimplifyingIndex()) , _preorderedOnly{false} @@ -61,7 +61,8 @@ BackwardSubsumptionDemodulation::BackwardSubsumptionDemodulation(SaturationAlgor , _backwardSubsumptionDemodulationMaxMatches(salg.getOptions().backwardSubsumptionDemodulationMaxMatches()) { } -void BackwardSubsumptionDemodulation::perform(Clause* sideCl, BwSimplificationRecordIterator& simplifications) +template +void BackwardSubsumptionDemodulation::perform(Clause* sideCl, BwSimplificationRecordIterator& simplifications) { ASSERT_VALID(*sideCl); @@ -118,8 +119,8 @@ void BackwardSubsumptionDemodulation::perform(Clause* sideCl, BwSimplificationRe simplificationsStorage.clear(); } // perform - -void BackwardSubsumptionDemodulation::performWithQueryLit(Clause* sideCl, Literal* candidateQueryLit, std::vector& simplifications) +template +void BackwardSubsumptionDemodulation::performWithQueryLit(Clause* sideCl, Literal* candidateQueryLit, std::vector& simplifications) { // sideCl // vvvvvvvvvv @@ -243,7 +244,8 @@ void BackwardSubsumptionDemodulation::performWithQueryLit(Clause* sideCl, Litera /// Handles the matching part. /// Returns true iff the main premise has been simplified. -bool BackwardSubsumptionDemodulation::simplifyCandidate(Clause* sideCl, Clause* mainCl, std::vector& simplifications) +template +bool BackwardSubsumptionDemodulation::simplifyCandidate(Clause* sideCl, Clause* mainCl, std::vector& simplifications) { static std::vector alts; @@ -337,7 +339,8 @@ bool BackwardSubsumptionDemodulation::simplifyCandidate(Clause* sideCl, Clause* /// Handles the rewriting part. /// Returns true iff the main premise has been simplified. -bool BackwardSubsumptionDemodulation::rewriteCandidate(Clause* sideCl, Clause* mainCl, MLMatcherSD const& matcher, Clause*& replacement) +template +bool BackwardSubsumptionDemodulation::rewriteCandidate(Clause* sideCl, Clause* mainCl, MLMatcherSD const& matcher, Clause*& replacement) { // to see why we use this have a look at the respective line in ForwardSubsumptionDemodulation DEBUG_CODE(static bool isAlascaOrdering = env.options->termOrdering () == Shell::Options::TermOrdering::QKBO @@ -435,7 +438,7 @@ bool BackwardSubsumptionDemodulation::rewriteCandidate(Clause* sideCl, Clause* m continue; } - NonVariableNonTypeIterator nvi(dlit); + RewritableSubtermIterator nvi(dlit); while (nvi.hasNext()) { TypedTermList lhsS = nvi.next(); // named 'lhsS' because it will be matched against 'lhs' @@ -663,5 +666,7 @@ bool BackwardSubsumptionDemodulation::rewriteCandidate(Clause* sideCl, Clause* m return false; } // rewriteCandidate +template class BackwardSubsumptionDemodulation; +template class BackwardSubsumptionDemodulation; } diff --git a/Inferences/BackwardSubsumptionDemodulation.hpp b/Inferences/BackwardSubsumptionDemodulation.hpp index e7e655e02..c84ec33d9 100644 --- a/Inferences/BackwardSubsumptionDemodulation.hpp +++ b/Inferences/BackwardSubsumptionDemodulation.hpp @@ -44,6 +44,7 @@ using namespace Kernel; * * This class implements the backward direction. */ +template class BackwardSubsumptionDemodulation : public BackwardSimplificationEngine { diff --git a/Inferences/ForwardSubsumptionDemodulation.cpp b/Inferences/ForwardSubsumptionDemodulation.cpp index 942369cac..fb71cdb97 100644 --- a/Inferences/ForwardSubsumptionDemodulation.cpp +++ b/Inferences/ForwardSubsumptionDemodulation.cpp @@ -28,10 +28,13 @@ using namespace Kernel; using namespace Lib; -using namespace Inferences; using namespace Saturation; -ForwardSubsumptionDemodulation::ForwardSubsumptionDemodulation(SaturationAlgorithm& salg) +namespace Inferences +{ + +template +ForwardSubsumptionDemodulation::ForwardSubsumptionDemodulation(SaturationAlgorithm& salg) : _preorderedOnly(false), _allowIncompleteness(false), _enableOrderingOptimizations( @@ -43,7 +46,8 @@ ForwardSubsumptionDemodulation::ForwardSubsumptionDemodulation(SaturationAlgorit _index(salg.getSimplifyingIndex()) {} -bool ForwardSubsumptionDemodulation::perform(Clause* cl, Clause*& replacement, ClauseIterator& premises) +template +bool ForwardSubsumptionDemodulation::perform(Clause* cl, Clause*& replacement, ClauseIterator& premises) { // cl // vvvvvvvvvvvvvvvv @@ -361,7 +365,7 @@ bool ForwardSubsumptionDemodulation::perform(Clause* cl, Clause*& replacement, C continue; } - NonVariableNonTypeIterator nvi(dlit); + RewritableSubtermIterator nvi(dlit); while (nvi.hasNext()) { TypedTermList lhsS = nvi.next(); // named 'lhsS' because it will be matched against 'lhs' @@ -637,3 +641,8 @@ bool ForwardSubsumptionDemodulation::perform(Clause* cl, Clause*& replacement, C return false; } + +template class ForwardSubsumptionDemodulation; +template class ForwardSubsumptionDemodulation; + +} \ No newline at end of file diff --git a/Inferences/ForwardSubsumptionDemodulation.hpp b/Inferences/ForwardSubsumptionDemodulation.hpp index 60938de20..0fbea6224 100644 --- a/Inferences/ForwardSubsumptionDemodulation.hpp +++ b/Inferences/ForwardSubsumptionDemodulation.hpp @@ -43,6 +43,7 @@ using namespace Saturation; * * This class implements the forward direction. */ +template class ForwardSubsumptionDemodulation : public ForwardSimplificationEngine { diff --git a/Saturation/SaturationAlgorithm.cpp b/Saturation/SaturationAlgorithm.cpp index 7d4f9488c..4a58305e0 100644 --- a/Saturation/SaturationAlgorithm.cpp +++ b/Saturation/SaturationAlgorithm.cpp @@ -1595,7 +1595,11 @@ SaturationAlgorithm *SaturationAlgorithm::createFromOptions(Problem& prb, const // fsd should be performed after forward subsumption, // because every successful forward subsumption will lead to a (useless) match in fsd. if (opt.forwardSubsumptionDemodulation()) { - res->addForwardSimplifierToFront(); + if (prb.isHigherOrder()) { + res->addForwardSimplifierToFront>(); + } else { + res->addForwardSimplifierToFront>(); + } } } if (mayHaveEquality) { @@ -1660,7 +1664,11 @@ SaturationAlgorithm *SaturationAlgorithm::createFromOptions(Problem& prb, const } if (mayHaveEquality && opt.backwardSubsumptionDemodulation()) { - res->addBackwardSimplifierToFront(); + if (prb.isHigherOrder()) { + res->addBackwardSimplifierToFront>(); + } else { + res->addBackwardSimplifierToFront>(); + } } bool backSubsumption = opt.backwardSubsumption() != Options::Subsumption::OFF; diff --git a/UnitTests/tInferences_SubsumptionDemodulation.cpp b/UnitTests/tInferences_SubsumptionDemodulation.cpp index 00d1649e6..61088f3cd 100644 --- a/UnitTests/tInferences_SubsumptionDemodulation.cpp +++ b/UnitTests/tInferences_SubsumptionDemodulation.cpp @@ -37,7 +37,7 @@ using namespace Test; namespace { inline auto tester() { - return FwdBwdSimplification::TestCase(); + return FwdBwdSimplification::TestCase, BackwardSubsumptionDemodulation>(); } // subsumption demodulation with preordered equation From bbedbb5962adfdfdf520a25b359920696c0ef732 Mon Sep 17 00:00:00 2001 From: Marton Hajdu Date: Fri, 27 Mar 2026 14:58:40 +0100 Subject: [PATCH 7/7] Add todo to potentially lift HO restriction in Twee goal transformation --- Shell/TweeGoalTransformation.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/Shell/TweeGoalTransformation.cpp b/Shell/TweeGoalTransformation.cpp index 9bc624246..93cebf3bf 100644 --- a/Shell/TweeGoalTransformation.cpp +++ b/Shell/TweeGoalTransformation.cpp @@ -115,6 +115,7 @@ class Definizator : public BottomUpTermTransformer { Term* t = trm.term(); if (t->isSort() || t->arity() == 0 || (!t->ground() && _groundOnly)) return trm; + // TODO(HOL): try to lift this restriction if (env.higherOrder() && trm.containsLooseDBIndex()) { return trm; }