From fc6487954699f8575b8f45b26fa39d7f5eeb177d Mon Sep 17 00:00:00 2001 From: Synrom Date: Fri, 10 Jul 2026 17:04:38 +0200 Subject: [PATCH 01/15] Add opposite pruning --- Indexing/ClauseCodeTree.cpp | 79 ++++++++++++------- Indexing/ClauseCodeTree.hpp | 6 +- Indexing/CodeTree.cpp | 26 +++--- Indexing/CodeTree.hpp | 36 ++++++++- Indexing/CodeTreeInterfaces.cpp | 2 + Indexing/TermCodeTree.cpp | 2 +- ...odeTreeForwardSubsumptionAndResolution.cpp | 1 + Kernel/Clause.cpp | 70 ++++++++++++++++ Kernel/Clause.hpp | 1 + Kernel/FlatTerm.hpp | 1 + Shell/PartialRedundancyHandler.cpp | 4 +- 11 files changed, 181 insertions(+), 47 deletions(-) diff --git a/Indexing/ClauseCodeTree.cpp b/Indexing/ClauseCodeTree.cpp index d0f8c689f..51f4b71b4 100644 --- a/Indexing/ClauseCodeTree.cpp +++ b/Indexing/ClauseCodeTree.cpp @@ -300,7 +300,7 @@ template void ClauseCodeTree::RemovingLiteralMatcher::init(CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, ClauseCodeTree* tree_, Stack* firstsInBlocks_) { - Base::init(tree_, entry_, linfos_, linfoCnt_, firstsInBlocks_); + Base::init(tree_, entry_, false, linfos_, linfoCnt_, firstsInBlocks_); ALWAYS(Base::prepareLiteral()); } @@ -338,14 +338,15 @@ bool ClauseCodeTree::removeOneOfAlternatives(CodeOp* op, Clause* cl template void ClauseCodeTree::LiteralMatcher::init(CodeTree* tree_, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, - bool seekOnlySuccess) + bool canEnterOpposites, bool seekOnlySuccess) { ASS_G(linfoCnt_,0); - Base::init(tree_,entry_,linfos_,linfoCnt_); + Base::init(tree_,entry_,canEnterOpposites, linfos_,linfoCnt_); _eagerlyMatched=false; eagerResults.reset(); + oppositeResults.reset(); RSTAT_CTR_INC("LiteralMatcher::init"); if(seekOnlySuccess) { @@ -375,10 +376,15 @@ template bool ClauseCodeTree::LiteralMatcher::next() { if(eagerlyMatched()) { - _matched=!eagerResults.isEmpty(); - if(!_matched) { - return false; + if (eagerResults.isEmpty()) { + if (oppositeResults.isEmpty()) { + _matched = false; + return false; + } + op = oppositeResults.pop(); + return true; } + _matched=true; op=eagerResults.pop(); return true; } @@ -388,16 +394,23 @@ bool ClauseCodeTree::LiteralMatcher::next() return false; } - _matched=execute(); - if(!_matched) { - return false; + while ((_matched = execute())) { + ASS(op->isLitEnd() || op->isSuccess()); + if(op->isLitEnd()) { + recordMatch(); + } + if (opposite) { + oppositeResults.push(op); + continue; + } + return true; } - - ASS(op->isLitEnd() || op->isSuccess()); - if(op->isLitEnd()) { - recordMatch(); + if (oppositeResults.isNonEmpty()) { + op = oppositeResults.pop(); + _matched = true; + return true; } - return true; + return false; } /** @@ -459,11 +472,13 @@ void ClauseCodeTree::LiteralMatcher::recordMatch() //no need to record matches which we already know will not lead to anything return; } - if(!ils->matchCnt && Base::linfos[Base::curLInfo].opposite) { + if(!ils->matchCnt && opposite) { //if we're matching opposite matches, we have already tried all non-opposite ones ils->noNonOppositeMatches=true; + } else if (ils->noNonOppositeMatches && !opposite) { + ils->noNonOppositeMatches=false; } - ils->addMatch(Base::linfos[Base::curLInfo].liIndex, Base::bindings); + ils->addMatch(Base::linfos[Base::curLInfo].liIndex, Base::bindings, opposite); } @@ -497,7 +512,7 @@ void ClauseCodeTree::ClauseMatcher::init(ClauseCodeTree* tree_, Cla baseLICnt++; } } - unsigned liCnt=sres ? (baseLICnt*2) : baseLICnt; + unsigned liCnt=baseLICnt; lInfos.ensure(liCnt); //we put ground literals first @@ -529,16 +544,18 @@ void ClauseCodeTree::ClauseMatcher::init(ClauseCodeTree* tree_, Cla } } if(sres) { + /* for(unsigned i=0;iincTimeStamp(); - enterLiteral(tree->getEntryPoint(), clen==0); + enterLiteral(tree->getEntryPoint(), clen==0, sres); } template @@ -562,6 +579,7 @@ void ClauseCodeTree::ClauseMatcher::reset() template Clause* ClauseCodeTree::ClauseMatcher::next(int& resolvedQueryLit) { + TIME_TRACE("Optimized Clause Matcher next"); if(lms.isEmpty()) { return 0; } @@ -606,7 +624,8 @@ Clause* ClauseCodeTree::ClauseMatcher::next(int& resolvedQueryLit) } bool seekOnlySuccess=lms.size()==query->length(); - enterLiteral(newLitEntry, seekOnlySuccess); + bool canEnterOpposites=sres && sresLiteral == sresNoLiteral; + enterLiteral(newLitEntry, seekOnlySuccess, canEnterOpposites); } } } @@ -662,7 +681,7 @@ inline bool ClauseCodeTree::ClauseMatcher::canEnterLiteral(CodeOp* * to see just clauses that end at this point). */ template -void ClauseCodeTree::ClauseMatcher::enterLiteral(CodeOp* entry, bool seekOnlySuccess) +void ClauseCodeTree::ClauseMatcher::enterLiteral(CodeOp* entry, bool seekOnlySuccess, bool canEnterOpposites) { if(!seekOnlySuccess) { RSTAT_MCTR_INC("enterLiteral levels (non-sos)", lms.size()); @@ -678,6 +697,7 @@ void ClauseCodeTree::ClauseMatcher::enterLiteral(CodeOp* entry, boo } size_t linfoCnt=lInfos.size(); + /* if(sres && sresLiteral!=sresNoLiteral) { ASS_L(sresLiteral,lms.size()); //we do not need to match index literals with opposite query @@ -687,9 +707,10 @@ void ClauseCodeTree::ClauseMatcher::enterLiteral(CodeOp* entry, boo ASS_EQ(linfoCnt%2,0); linfoCnt/=2; } + */ Recycled lm; - lm->init(tree, entry, lInfos.array(), linfoCnt, seekOnlySuccess); + lm->init(tree, entry, lInfos.array(), linfoCnt, canEnterOpposites, seekOnlySuccess); lms.push(std::move(lm)); } @@ -738,8 +759,8 @@ bool ClauseCodeTree::ClauseMatcher::checkCandidate(Clause* cl, int& size_t matchCnt=lms[0]->getILS()->matchCnt; for(size_t i=0;igetILS()->getMatch(i); - if(lInfos[mi->liIndex].opposite) { - resolvedQueryLit=lInfos[mi->liIndex].litIndex; + if(mi->opposite()) { + resolvedQueryLit=lInfos[mi->getLiIndex()].litIndex; } else { //we prefer subsumption to subsumption resolution @@ -866,8 +887,8 @@ bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQu for(unsigned i=0;igetILS(); MatchInfo* mi=ils->getMatch(matchIndex[i]); - if(lInfos[mi->liIndex].opposite) { - resolvedQueryLit=lInfos[mi->liIndex].litIndex; + if(mi->opposite()) { + resolvedQueryLit=lInfos[mi->getLiIndex()].litIndex; break; } } @@ -879,18 +900,18 @@ bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQu 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) ) { + if( lInfos[bq->getLiIndex()].litIndex==lInfos[nq->getLiIndex()].litIndex || + (bq->opposite() && nq->opposite()) ) { return false; } unsigned bvars=bi->varCnt; unsigned* bgvn=bi->sortedGlobalVarNumbers; - TermList* bb=bq->bindings; + TermList* bb=bq->getBindings(); unsigned nvars=ni->varCnt; unsigned* ngvn=ni->sortedGlobalVarNumbers; - TermList* nb=nq->bindings; + TermList* nb=nq->getBindings(); while(bvars && nvars) { while(bvars && *bgvn<*ngvn) { diff --git a/Indexing/ClauseCodeTree.hpp b/Indexing/ClauseCodeTree.hpp index 97ac078e4..e4809c70c 100644 --- a/Indexing/ClauseCodeTree.hpp +++ b/Indexing/ClauseCodeTree.hpp @@ -79,9 +79,10 @@ class ClauseCodeTree : public CodeTree using Base::op; using Base::_matched; using Base::finished; + using Base::opposite; using Base::execute; - void init(CodeTree* tree, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, bool seekOnlySuccess=false); + void init(CodeTree* tree, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, bool canEnterOpposites, bool seekOnlySuccess); bool next(); bool doEagerMatching(); @@ -95,6 +96,7 @@ class ClauseCodeTree : public CodeTree bool _eagerlyMatched; Stack eagerResults; + Stack oppositeResults; void recordMatch(); }; @@ -114,7 +116,7 @@ class ClauseCodeTree : public CodeTree USE_ALLOCATOR(ClauseMatcher); private: - void enterLiteral(CodeOp* entry, bool seekOnlySuccess); + void enterLiteral(CodeOp* entry, bool seekOnlySuccess, bool canEnterOpposites); void leaveLiteral(); bool canEnterLiteral(CodeOp* op); diff --git a/Indexing/CodeTree.cpp b/Indexing/CodeTree.cpp index b4464dc9c..9e8855c75 100644 --- a/Indexing/CodeTree.cpp +++ b/Indexing/CodeTree.cpp @@ -132,9 +132,9 @@ void CodeTree::MatchInfo::destroy(unsigned bindCnt) } -void CodeTree::MatchInfo::init(ILStruct* ils, unsigned liIndex_, DArray& bindingArray) +void CodeTree::MatchInfo::init(ILStruct* ils, unsigned liIndex_, DArray& bindingArray, bool opposite) { - liIndex=liIndex_; + liIndex=opposite ? liIndex_ | leftmost_bit : liIndex_; size_t bindCnt=ils->varCnt; if(bindCnt) { unsigned* perm=ils->globalVarPermutation; @@ -264,7 +264,7 @@ void CodeTree::ILStruct::ensureFreshness(unsigned globalTimestamp) } } -void CodeTree::ILStruct::addMatch(unsigned liIndex, DArray& bindingArray) +void CodeTree::ILStruct::addMatch(unsigned liIndex, DArray& bindingArray, bool opposite) { if(matchCnt==matches.size()) { matches.expand(matchCnt ? (matchCnt*2) : 4); @@ -277,7 +277,7 @@ void CodeTree::ILStruct::addMatch(unsigned liIndex, DArray& bindingArr if(!matches[matchCnt]) { matches[matchCnt]=MatchInfo::alloc(varCnt); } - matches[matchCnt]->init(this, liIndex, bindingArray); + matches[matchCnt]->init(this, liIndex, bindingArray, opposite); matchCnt++; } @@ -559,9 +559,9 @@ bool CodeTree::Matcher::execute() for(;;) { if(op->alternative()) { if constexpr (removing) { - btStack.push(BTPointRemoving(tp, op->alternative(), RemovingBase::firstsInBlocks->size())); + btStack.push(BTPointRemoving(tp, markOp(op->alternative()), RemovingBase::firstsInBlocks->size())); } else { - btStack.push(BTPoint(tp, op->alternative())); + btStack.push(BTPoint(tp, markOp(op->alternative()))); } } switch(op->_instruction()) { @@ -638,10 +638,12 @@ bool CodeTree::Matcher::execute() } template -void CodeTree::Matcher::init(CodeTree* tree_, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, Stack* firstsInBlocks_) +void CodeTree::Matcher::init(CodeTree* tree_, CodeOp* entry_, bool canEnterOpposites_, LitInfo* linfos_, size_t linfoCnt_, Stack* firstsInBlocks_) { + canEnterOpposites=canEnterOpposites_; tree=tree_; entry=entry_; + opposite=false; linfos=linfos_; linfoCnt=linfoCnt_; @@ -676,7 +678,8 @@ bool CodeTree::Matcher::backtrack() } auto bp=btStack.pop(); tp=bp.tp; - op=bp.op; + op=unmarkOp(bp.op); + opposite=getMark(bp.op); if constexpr (removing) { RemovingBase::firstsInBlocks->truncate(bp.fibDepth); RemovingBase::firstsInBlocks->push(op); @@ -696,6 +699,7 @@ bool CodeTree::Matcher::prepareLiteral() ft=linfos[curLInfo].ft; tp=0; op=entry; + opposite=false; return true; } @@ -780,7 +784,11 @@ inline bool CodeTree::Matcher::doCheckFun() unsigned functor=op->_arg(); FlatTerm::Entry& fte=(*ft)[tp]; if(!fte.isFun(functor)) { - return false; + if (canEnterOpposites && tp == 0 && fte.isOppositeFun(functor)) { + opposite=true; + } else { + return false; + } } fte.expand(); tp+=FlatTerm::FUNCTION_ENTRY_COUNT; diff --git a/Indexing/CodeTree.hpp b/Indexing/CodeTree.hpp index 7184abfff..725eb912b 100644 --- a/Indexing/CodeTree.hpp +++ b/Indexing/CodeTree.hpp @@ -74,13 +74,19 @@ class CodeTree struct MatchInfo { + unsigned getLiIndex() const { return liIndex & ~leftmost_bit; } + TermList* getBindings() { return &bindings[0]; } + bool opposite() const { return liIndex & leftmost_bit; } + + private: /** Index of the matched LitInfo in the EContext */ unsigned liIndex; /** array of bindings */ TermList bindings[1]; - private: - void init(ILStruct* ils, unsigned liIndex, DArray& bindingArray); + static constexpr unsigned int leftmost_bit = 1u << (sizeof(unsigned int) * CHAR_BIT - 1); + + void init(ILStruct* ils, unsigned liIndex, DArray& bindingArray, bool opposite); static MatchInfo* alloc(unsigned bindCnt); @@ -130,7 +136,7 @@ class CodeTree unsigned timestamp; //from here on, the values are valid only if the timestamp is current - void addMatch(unsigned liIndex, DArray& bindingArray); + void addMatch(unsigned liIndex, DArray& bindingArray, bool opposite); void deleteMatch(unsigned matchIndex); MatchInfo*& getMatch(unsigned matchIndex); @@ -382,7 +388,7 @@ class CodeTree } protected: - void init(CodeTree* tree_, CodeOp* entry_, LitInfo* linfos_ = 0, + void init(CodeTree* tree_, CodeOp* entry_, bool canEnterOpposites, LitInfo* linfos_ = 0, size_t linfoCnt_ = 0, Stack* firstsInBlocks_ = 0); bool backtrack(); @@ -393,6 +399,25 @@ class CodeTree bool doCheckGroundTerm(); bool doSearchStruct(); + inline CodeOp* markOp(CodeOp* op) const + { + return reinterpret_cast( + reinterpret_cast(op) | opposite + ); + } + + inline bool getMark(CodeOp* op) const + { + return (reinterpret_cast(op) & 1u) != 0; + } + + inline CodeOp* unmarkOp(CodeOp* op) const + { + return reinterpret_cast( + reinterpret_cast(op) & ~std::uintptr_t{1} + ); + } + /** * Position in the flat term * @@ -418,6 +443,9 @@ class CodeTree CodeOp* entry; CodeTree* tree; + bool opposite; + bool canEnterOpposites; + /** * Array of alternative LitInfo objects * diff --git a/Indexing/CodeTreeInterfaces.cpp b/Indexing/CodeTreeInterfaces.cpp index b430bed46..9fecef156 100644 --- a/Indexing/CodeTreeInterfaces.cpp +++ b/Indexing/CodeTreeInterfaces.cpp @@ -177,9 +177,11 @@ void CodeTreeSubsumptionIndex::handleClause(Clause* cl, bool adding TIME_TRACE("codetree subsumption index maintenance"); if(adding) { + //std::cout << "wtree.insert(clause({" << cl->toReproducerString() << "}));" << std::endl; _ct.insert(cl); } else { + //std::cout << "wtree.remove(clause({" << cl->toReproducerString() << "}));" << std::endl; _ct.remove(cl); } } diff --git a/Indexing/TermCodeTree.cpp b/Indexing/TermCodeTree.cpp index 4d82cd42c..a191c9e71 100644 --- a/Indexing/TermCodeTree.cpp +++ b/Indexing/TermCodeTree.cpp @@ -107,7 +107,7 @@ template void TermCodeTree::RemovingTermMatcher::init(FlatTerm* ft_, TermCodeTree* tree_, Stack* firstsInBlocks_) { - Base::init(tree_, tree_->getEntryPoint(), /*linfos_=*/0, /*linfoCnt_=*/0, firstsInBlocks_); + Base::init(tree_, tree_->getEntryPoint(), false, /*linfos_=*/0, /*linfoCnt_=*/0, firstsInBlocks_); Base::firstsInBlocks->push(Base::entry); diff --git a/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp b/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp index c030aba22..2e339abcb 100644 --- a/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp +++ b/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp @@ -40,6 +40,7 @@ bool CodeTreeForwardSubsumptionAndResolution::perform(Clause *cl, C Clause* premise; int resolvedQueryLit; + //std::cout << "Execute on " << cl->toReproducerString() << std::endl; while ((premise = cm.next(resolvedQueryLit))) { if (resolvedQueryLit == -1) { ASS(satSubs.checkSubsumption(premise, cl)); diff --git a/Kernel/Clause.cpp b/Kernel/Clause.cpp index 441965245..412e256b8 100644 --- a/Kernel/Clause.cpp +++ b/Kernel/Clause.cpp @@ -14,6 +14,7 @@ * @since 18/05/2007 Manchester */ +#include #include #include "Debug/RuntimeStatistics.hpp" @@ -337,6 +338,75 @@ std::string Clause::toNiceString() const return result; } +std::string Clause::toReproducerString() const +{ + auto literalStringToReproducerString = [](const std::string& input) { + std::string output; + output.reserve(input.size()); + + for (size_t i = 0; i < input.size();) { + const unsigned char ch = static_cast(input[i]); + if (std::isalpha(ch)) { + size_t j = i + 1; + while (j < input.size()) { + const unsigned char c = static_cast(input[j]); + if (!std::isalnum(c) && c != '_') { + break; + } + j++; + } + + const std::string tok = input.substr(i, j - i); + if (tok == "i") { + output += "f2"; + } else if (tok == "a") { + output += "c"; + } else if (tok == "b") { + output += "d"; + } else if (tok == "c") { + output += "e"; + } else if (tok.size() >= 2 && tok[0] == 'X') { + bool allDigits = true; + for (size_t k = 1; k < tok.size(); k++) { + const unsigned char d = static_cast(tok[k]); + if (!std::isdigit(d)) { + allDigits = false; + break; + } + } + if (allDigits) { + output += "x"; + output += Int::toString(std::stoul(tok.substr(1)) + 1); + } else { + output += tok; + } + } else { + output += tok; + } + + i = j; + } else { + output += input[i]; + i++; + } + } + + return output; + }; + + std::string result; + if (size() == 0) { + return "$false"; + } else { + result += literalStringToReproducerString(_literals[0]->toString()); + for (unsigned i = 1; i < size(); i++) { + result += ", "; + result += literalStringToReproducerString(_literals[i]->toString()); + } + } + return result; +} + std::ostream& operator<<(std::ostream& out, Clause const& self) { if (self.size() == 0) { diff --git a/Kernel/Clause.hpp b/Kernel/Clause.hpp index 21dc55adb..8917060ba 100644 --- a/Kernel/Clause.hpp +++ b/Kernel/Clause.hpp @@ -148,6 +148,7 @@ class Clause void destroy(); void destroyExceptInferenceObject(); std::string literalsOnlyToString() const; + std::string toReproducerString() const; std::string toString() const; std::string toTPTPString() const; std::string toNiceString() const; diff --git a/Kernel/FlatTerm.hpp b/Kernel/FlatTerm.hpp index 8afa86b12..d2688ce97 100644 --- a/Kernel/FlatTerm.hpp +++ b/Kernel/FlatTerm.hpp @@ -61,6 +61,7 @@ class FlatTerm inline bool isVar(unsigned num) const { return isVar() && _number()==num; } inline bool isFun() const { return _tag()==FUN || _tag()==FUN_UNEXPANDED; } inline bool isFun(unsigned num) const { return isFun() && _number()==num; } + inline bool isOppositeFun(unsigned num) const { return isFun() && (_number()^1)==num; } /** * Should be called when @b isFun() is true. * If @b tag()==FUN_UNEXPANDED, it fills out entries for the functions diff --git a/Shell/PartialRedundancyHandler.cpp b/Shell/PartialRedundancyHandler.cpp index 772539e36..89f578460 100644 --- a/Shell/PartialRedundancyHandler.cpp +++ b/Shell/PartialRedundancyHandler.cpp @@ -250,7 +250,7 @@ class PartialRedundancyHandler::ConstraintIndex { void init(CodeTree* tree, const TermStack& ts) { - Matcher::init(tree,tree->getEntryPoint()); + Matcher::init(tree,tree->getEntryPoint(), false); ft = FlatTerm::create(ts); @@ -285,7 +285,7 @@ class PartialRedundancyHandler::ConstraintIndex { public: void init(FlatTerm* ft_, CodeTree* tree_, Stack* firstsInBlocks_) { - Matcher::init(tree_, tree_->getEntryPoint(), 0, 0, firstsInBlocks_); + Matcher::init(tree_, tree_->getEntryPoint(), false, 0, 0, firstsInBlocks_); ft=ft_; tp=0; op=entry; From 698b5f03e54e2b61602ece2f9cd648a57e3c06f9 Mon Sep 17 00:00:00 2001 From: Synrom Date: Fri, 10 Jul 2026 17:18:32 +0200 Subject: [PATCH 02/15] Incorporate oppositeResult into eagerResults --- Indexing/ClauseCodeTree.cpp | 25 +++++++++++-------------- Indexing/ClauseCodeTree.hpp | 1 - 2 files changed, 11 insertions(+), 15 deletions(-) diff --git a/Indexing/ClauseCodeTree.cpp b/Indexing/ClauseCodeTree.cpp index 51f4b71b4..14c89ea73 100644 --- a/Indexing/ClauseCodeTree.cpp +++ b/Indexing/ClauseCodeTree.cpp @@ -346,7 +346,6 @@ void ClauseCodeTree::LiteralMatcher::init(CodeTree* tree_, CodeOp* _eagerlyMatched=false; eagerResults.reset(); - oppositeResults.reset(); RSTAT_CTR_INC("LiteralMatcher::init"); if(seekOnlySuccess) { @@ -376,15 +375,10 @@ template bool ClauseCodeTree::LiteralMatcher::next() { if(eagerlyMatched()) { - if (eagerResults.isEmpty()) { - if (oppositeResults.isEmpty()) { - _matched = false; - return false; - } - op = oppositeResults.pop(); - return true; + _matched = eagerResults.isNonEmpty(); + if (!_matched) { + return false; } - _matched=true; op=eagerResults.pop(); return true; } @@ -400,13 +394,13 @@ bool ClauseCodeTree::LiteralMatcher::next() recordMatch(); } if (opposite) { - oppositeResults.push(op); + eagerResults.push(op); continue; } return true; } - if (oppositeResults.isNonEmpty()) { - op = oppositeResults.pop(); + if (eagerResults.isNonEmpty()) { + op = eagerResults.pop(); _matched = true; return true; } @@ -420,7 +414,6 @@ template bool ClauseCodeTree::LiteralMatcher::doEagerMatching() { ASS(!eagerlyMatched()); //eager matching can be done only once - ASS(eagerResults.isEmpty()); ASS(!finished()); //backup the current op @@ -434,7 +427,11 @@ bool ClauseCodeTree::LiteralMatcher::doEagerMatching() while(execute()) { if(op->isLitEnd()) { recordMatch(); - eagerResultsRevOrder.push(op); + if (opposite) { + eagerResults.push(op); + } else { + eagerResultsRevOrder.push(op); + } } else { ASS(op->isSuccess()); diff --git a/Indexing/ClauseCodeTree.hpp b/Indexing/ClauseCodeTree.hpp index e4809c70c..a6a42179a 100644 --- a/Indexing/ClauseCodeTree.hpp +++ b/Indexing/ClauseCodeTree.hpp @@ -96,7 +96,6 @@ class ClauseCodeTree : public CodeTree bool _eagerlyMatched; Stack eagerResults; - Stack oppositeResults; void recordMatch(); }; From 88ed9bf12a30b75be77df911b1e0b903954ef57d Mon Sep 17 00:00:00 2001 From: Synrom Date: Thu, 16 Jul 2026 10:56:16 +0200 Subject: [PATCH 03/15] Sort Matches of ILStruct's --- Indexing/CodeTree.cpp | 23 +++++++++++++++++++++-- Indexing/CodeTree.hpp | 1 + 2 files changed, 22 insertions(+), 2 deletions(-) diff --git a/Indexing/CodeTree.cpp b/Indexing/CodeTree.cpp index 9e8855c75..edf1da2aa 100644 --- a/Indexing/CodeTree.cpp +++ b/Indexing/CodeTree.cpp @@ -261,6 +261,7 @@ void CodeTree::ILStruct::ensureFreshness(unsigned globalTimestamp) finished=false; noNonOppositeMatches=false; matchCnt=0; + nonOppositeMatchCnt=0; } } @@ -277,7 +278,16 @@ void CodeTree::ILStruct::addMatch(unsigned liIndex, DArray& bindingArr if(!matches[matchCnt]) { matches[matchCnt]=MatchInfo::alloc(varCnt); } - matches[matchCnt]->init(this, liIndex, bindingArray, opposite); + if(opposite) { + matches[matchCnt]->init(this, liIndex, bindingArray, true); + } + else { + if(nonOppositeMatchCnt!=matchCnt) { + swap(matches[nonOppositeMatchCnt], matches[matchCnt]); + } + matches[nonOppositeMatchCnt]->init(this, liIndex, bindingArray, false); + nonOppositeMatchCnt++; + } matchCnt++; } @@ -294,7 +304,16 @@ void CodeTree::ILStruct::deleteMatch(unsigned matchIndex) ASS_L(matchIndex, matchCnt); matchCnt--; - swap(matches[matchIndex], matches[matchCnt]); + if(matchIndex Date: Thu, 16 Jul 2026 12:42:01 +0200 Subject: [PATCH 04/15] Fix Search Structs bug --- Indexing/CodeTree.cpp | 22 ++++++++++++++++++++-- Indexing/CodeTree.hpp | 9 ++++++++- 2 files changed, 28 insertions(+), 3 deletions(-) diff --git a/Indexing/CodeTree.cpp b/Indexing/CodeTree.cpp index edf1da2aa..d9ec3b010 100644 --- a/Indexing/CodeTree.cpp +++ b/Indexing/CodeTree.cpp @@ -501,14 +501,18 @@ bool CodeTree::SearchStruct::getTargetOpPtr(const CodeOp& insertedOp, CodeOp**& // expose for ClauseCodeTree.cpp template bool CodeTree::SearchStruct::getTargetOpPtr(const CodeOp&, CodeOp**&); -CodeTree::CodeOp* CodeTree::SearchStruct::getTargetOp(const FlatTerm::Entry* ftPos) +CodeTree::CodeOp* CodeTree::SearchStruct::getTargetOp(const FlatTerm::Entry* ftPos, bool opposite) { if(!ftPos->isFun()) { return 0; } switch(kind) { case FN_STRUCT: + if (opposite) { + return static_cast(this)->targetOp(ftPos->_number() ^ 1); + } return static_cast(this)->targetOp(ftPos->_number()); case GROUND_TERM_STRUCT: ftPos++; + ASS(!opposite); ASS_EQ(ftPos->_tag(), FlatTerm::FUN_TERM_PTR); return static_cast(this)->targetOp(ftPos->_term()); default: @@ -844,7 +848,21 @@ inline bool CodeTree::Matcher::doSearchStruct ASS_EQ(op->_instruction(), SEARCH_STRUCT); const FlatTerm::Entry* fte=&(*ft)[tp]; - CodeOp* target=op->getSearchStruct()->getTargetOp(fte); + CodeOp* target=op->getSearchStruct()->getTargetOp(fte, false); + if (tp == 0 && op->getSearchStruct()->kind == SearchStruct::FN_STRUCT) { + if (!target) { + target = op->getSearchStruct()->getTargetOp(fte, true); + } else { + CodeOp* alt = op->getSearchStruct()->getTargetOp(fte, true); + if (alt) { + if constexpr (removing) { + btStack.push(BTPointRemoving(tp, markOp(alt, true), RemovingBase::firstsInBlocks->size())); + } else { + btStack.push(BTPoint(tp, markOp(alt, true))); + } + } + } + } if(!target) { return false; } diff --git a/Indexing/CodeTree.hpp b/Indexing/CodeTree.hpp index f8cba1e89..66fea76ff 100644 --- a/Indexing/CodeTree.hpp +++ b/Indexing/CodeTree.hpp @@ -262,7 +262,7 @@ class CodeTree * Returns code op in the structure matching the content * of flat term entry @b ftPos. */ - CodeOp* getTargetOp(const FlatTerm::Entry* ftPos); + CodeOp* getTargetOp(const FlatTerm::Entry* ftPos, bool opposite); inline size_t length() const { return targets.size(); } enum Kind @@ -407,6 +407,13 @@ class CodeTree ); } + inline CodeOp* markOp(CodeOp* op, bool value) const + { + return reinterpret_cast( + reinterpret_cast(op) | value + ); + } + inline bool getMark(CodeOp* op) const { return (reinterpret_cast(op) & 1u) != 0; From 08ea5b9c18e482fece17ed5bf79d7f45928e8a03 Mon Sep 17 00:00:00 2001 From: Synrom Date: Thu, 16 Jul 2026 13:50:04 +0200 Subject: [PATCH 05/15] matchGlobalVars optimization --- .gitignore | 4 ++++ Indexing/ClauseCodeTree.cpp | 33 +++++++++++++++------------------ 2 files changed, 19 insertions(+), 18 deletions(-) diff --git a/.gitignore b/.gitignore index e51a37e42..f4eb2573a 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,10 @@ # ignore common build directories /cmake-build /build +/build** +/profiles +/output +/scripts/__pycache__ /coverage-build # ignore TPTP directories/symlinks at the top level diff --git a/Indexing/ClauseCodeTree.cpp b/Indexing/ClauseCodeTree.cpp index 14c89ea73..3fbb46987 100644 --- a/Indexing/ClauseCodeTree.cpp +++ b/Indexing/ClauseCodeTree.cpp @@ -814,29 +814,22 @@ bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQu // when we get to binding j-th literal // Matches in ILStruct::matches are reordered, so that we always try // the _first_ remaining[j,j] literals + // ILStruct::addMatch/deleteMatch maintain non-opposite matches in the + // prefix [0, nonOppositeMatchCnt). Try that prefix first to prefer + // subsumption over subsumption resolution. static TriangularArray remaining(10); + + static DArray matchIndex; + matchIndex.ensure(clen); + + bool allowOpposites=false; +search_again: remaining.setSide(clen); for(unsigned j=0;jgetILS(); - remaining.set(j,0,ils->matchCnt); - -// VERB_OUT("matches "<matches.size()<<" index:"<varCnt<<" linfos:"<matches.size();y++) { -// LitInfo* linf=&lInfos[ils->matches[y]->liIndex]; -// VERB_OUT(" match "<matches[y]->liIndex<<" op: "<opposite); -// VERB_OUT(" hdr: "<<(*linf->ft)[0].number()); -// } -// for(unsigned x=0;xvarCnt;x++) { -// VERB_OUT(" glob var: "<sortedGlobalVarNumbers[x]); -// for(unsigned y=0;ymatches.size();y++) { -// VERB_OUT(" match "<matches[y]->bindings[x]); -// } -// } - } -// VERB_OUT("secOp:"<<(lms[1]->op-1)->instr()<<" "<<(lms[1]->op-1)->arg()); + remaining.set(j,0,allowOpposites ? ils->matchCnt : ils->nonOppositeMatchCnt); + } - static DArray matchIndex; - matchIndex.ensure(clen); unsigned failLev=0; for(unsigned i=0;i::ClauseMatcher::matchGlobalVars(int& resolvedQu //no more choices at this level, so try going up if(i==0) { RSTAT_MCTR_INC("zero level fails at", failLev); + if(sres && !allowOpposites) { + allowOpposites=true; + goto search_again; + } return false; } i--; From 51193b0065af34e1b5af4224f2da52d17a6c00fc Mon Sep 17 00:00:00 2001 From: Synrom Date: Wed, 22 Jul 2026 16:39:44 +0200 Subject: [PATCH 06/15] Add debugging and testcase --- Indexing/CodeTreeInterfaces.cpp | 12 +- ...odeTreeForwardSubsumptionAndResolution.cpp | 33 +- .../tInferences_SubsumptionAndResolution.cpp | 1079 ++++++++++++++++- 3 files changed, 1107 insertions(+), 17 deletions(-) diff --git a/Indexing/CodeTreeInterfaces.cpp b/Indexing/CodeTreeInterfaces.cpp index 9fecef156..a9db23c3e 100644 --- a/Indexing/CodeTreeInterfaces.cpp +++ b/Indexing/CodeTreeInterfaces.cpp @@ -13,6 +13,8 @@ * */ +#include + #include "Indexing/Index.hpp" #include "Indexing/ResultSubstitution.hpp" #include "Lib/Allocator.hpp" @@ -35,6 +37,12 @@ namespace Indexing using namespace Lib; using namespace Kernel; +std::ostream& codeTreeDebugLog() +{ + static std::ofstream out("wtree.log"); + return out; +} + template class CodeTreeSubstitution : public ResultSubstitution @@ -177,11 +185,11 @@ void CodeTreeSubsumptionIndex::handleClause(Clause* cl, bool adding TIME_TRACE("codetree subsumption index maintenance"); if(adding) { - //std::cout << "wtree.insert(clause({" << cl->toReproducerString() << "}));" << std::endl; + codeTreeDebugLog() << "wtree.insert(clause({" << cl->toReproducerString() << "}));" << std::endl; _ct.insert(cl); } else { - //std::cout << "wtree.remove(clause({" << cl->toReproducerString() << "}));" << std::endl; + codeTreeDebugLog() << "wtree.remove(clause({" << cl->toReproducerString() << "}));" << std::endl; _ct.remove(cl); } } diff --git a/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp b/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp index 2e339abcb..790cb0fc2 100644 --- a/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp +++ b/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp @@ -12,11 +12,17 @@ * Implements class CodeTreeForwardSubsumptionAndResolution. */ +#include + #include "Saturation/SaturationAlgorithm.hpp" #include "ProofExtra.hpp" #include "CodeTreeForwardSubsumptionAndResolution.hpp" +namespace Indexing { +std::ostream& codeTreeDebugLog(); +} + namespace Inferences { template @@ -36,6 +42,15 @@ bool CodeTreeForwardSubsumptionAndResolution::perform(Clause *cl, C static typename ClauseCodeTree::ClauseMatcher cm; cm.init(_ct, cl, _subsumptionResolution); + Indexing::codeTreeDebugLog() << "D = clause({" << cl->toReproducerString() << "});" << std::endl; + Indexing::codeTreeDebugLog() << "m.init(&wtree, D, "; + if (_subsumptionResolution) { + Indexing::codeTreeDebugLog() << "true);" << std::endl; + } else { + Indexing::codeTreeDebugLog() << "false);" << std::endl; + } + Indexing::codeTreeDebugLog() << "m.next(resolvedQueryLit);" << std::endl; + Indexing::codeTreeDebugLog() << "m.reset();" << std::endl; Clause* premise; int resolvedQueryLit; @@ -49,7 +64,23 @@ bool CodeTreeForwardSubsumptionAndResolution::perform(Clause *cl, C cm.reset(); return true; } - ASS(satSubs.checkSubsumptionResolutionWithLiteral(premise, cl, resolvedQueryLit)); +#if VDEBUG + bool subsumptionResolutionChecks = + satSubs.checkSubsumptionResolutionWithLiteral(premise, cl, resolvedQueryLit); + if(!subsumptionResolutionChecks) { + Indexing::codeTreeDebugLog() << "Tree is:" << std::endl; + Indexing::codeTreeDebugLog() << *_ct << std::endl; + Indexing::codeTreeDebugLog() << "Executed on " << cl->toReproducerString() << std::endl; + Indexing::codeTreeDebugLog() << "ResolvedQueryLit " << resolvedQueryLit<< std::endl; + Indexing::codeTreeDebugLog() << "_subsumptionResolution is " << _subsumptionResolution << std::endl; + if constexpr (higherOrder) { + Indexing::codeTreeDebugLog() << "higherOrder is true" << std::endl; + } else { + Indexing::codeTreeDebugLog() << "higherOrder is false" << std::endl; + } + } + ASS(subsumptionResolutionChecks); +#endif LiteralStack res; for (unsigned i = 0; i < cl->length(); i++) { diff --git a/UnitTests/tInferences_SubsumptionAndResolution.cpp b/UnitTests/tInferences_SubsumptionAndResolution.cpp index f77e028f5..2f94b73c5 100644 --- a/UnitTests/tInferences_SubsumptionAndResolution.cpp +++ b/UnitTests/tInferences_SubsumptionAndResolution.cpp @@ -7,36 +7,44 @@ * https://vprover.github.io/license.html * and in the source directory */ +#include #include "Test/SyntaxSugar.hpp" #include "Inferences/ForwardSubsumptionAndResolution.hpp" #include "Inferences/BackwardSubsumptionAndResolution.hpp" +#include "Indexing/ClauseCodeTree.hpp" #include "Test/FwdBwdSimplificationTester.hpp" using namespace std; using namespace Kernel; using namespace Inferences; +using namespace Indexing; using namespace Test; #define MY_SYNTAX_SUGAR \ __ALLOW_UNUSED( \ DECL_DEFAULT_VARS \ - DECL_VAR(x1, 1) \ - DECL_VAR(x2, 2) \ - DECL_VAR(x3, 3) \ - DECL_VAR(x4, 4) \ - DECL_VAR(x5, 5) \ - DECL_VAR(x6, 6) \ - DECL_VAR(x7, 7) \ - DECL_VAR(y1, 11) \ - DECL_VAR(y2, 12) \ - DECL_VAR(y3, 13) \ - DECL_VAR(y4, 14) \ - DECL_VAR(y5, 15) \ - DECL_VAR(y6, 16) \ - DECL_VAR(y7, 17) \ DECL_SORT(s) \ + DECL_VAR_SORTED(x1, 1, s) \ + DECL_VAR_SORTED(x2, 2, s) \ + DECL_VAR_SORTED(x3, 3, s) \ + DECL_VAR_SORTED(x4, 4, s) \ + DECL_VAR_SORTED(x5, 5, s) \ + DECL_VAR_SORTED(x6, 6, s) \ + DECL_VAR_SORTED(x7, 7, s) \ + DECL_VAR_SORTED(x8, 8, s) \ + DECL_VAR_SORTED(x9, 9, s) \ + DECL_VAR_SORTED(x10, 10, s) \ + DECL_VAR_SORTED(x11, 11, s) \ + DECL_VAR_SORTED(x12, 12, s) \ + DECL_VAR_SORTED(y1, 21, s) \ + DECL_VAR_SORTED(y2, 22, s) \ + DECL_VAR_SORTED(y3, 23, s) \ + DECL_VAR_SORTED(y4, 24, s) \ + DECL_VAR_SORTED(y5, 25, s) \ + DECL_VAR_SORTED(y6, 26, s) \ + DECL_VAR_SORTED(y7, 27, s) \ DECL_CONST(c, s) \ DECL_CONST(d, s) \ DECL_CONST(e, s) \ @@ -49,6 +57,44 @@ using namespace Test; DECL_FUNC(h2, {s, s}, s) \ DECL_FUNC(i, {s}, s) \ DECL_FUNC(i2, {s, s}, s) \ + DECL_FUNC(sum, {s, s}, s) \ + DECL_FUNC(underlying_curve, {s}, s) \ + DECL_FUNC(sK1, {s, s}, s) \ + DECL_FUNC(sK2, {s, s}, s) \ + DECL_FUNC(sK3, {s, s}, s) \ + DECL_FUNC(sK4, {s, s}, s) \ + DECL_FUNC(sK5, {s, s, s, s}, s) \ + DECL_FUNC(sK6, {s, s}, s) \ + DECL_FUNC(sK7, {s}, s) \ + DECL_FUNC(sK8, {s, s, s, s}, s) \ + DECL_CONST(sK9, s) \ + DECL_CONST(sK10, s) \ + DECL_CONST(sK11, s) \ + DECL_CONST(sK12, s) \ + DECL_CONST(sK13, s) \ + DECL_CONST(skc8, s) \ + DECL_CONST(skc9, s) \ + DECL_CONST(skc10, s) \ + DECL_CONST(skc11, s) \ + DECL_CONST(skc12, s) \ + DECL_CONST(skc13, s) \ + DECL_CONST(skc14, s) \ + DECL_CONST(skc15, s) \ + DECL_FUNC(sK14, {s}, s) \ + DECL_FUNC(sK15, {s}, s) \ + DECL_FUNC(sK16, {s, s}, s) \ + DECL_FUNC(sK17, {s, s}, s) \ + DECL_FUNC(sK18, {s, s, s}, s) \ + DECL_FUNC(sK19, {s, s}, s) \ + DECL_FUNC(sK20, {s, s}, s) \ + DECL_FUNC(sK21, {s, s}, s) \ + DECL_FUNC(sK22, {s, s}, s) \ + DECL_FUNC(sK23, {s, s}, s) \ + DECL_FUNC(sK24, {s}, s) \ + DECL_FUNC(sK25, {s, s, s}, s) \ + DECL_FUNC(sK26, {s, s}, s) \ + DECL_FUNC(sK27, {s}, s) \ + DECL_FUNC(skf1, {s}, s) \ DECL_PRED(p, {s}) \ DECL_PRED(p2, {s, s}) \ DECL_PRED(p3, {s, s, s}) \ @@ -56,6 +102,56 @@ using namespace Test; DECL_PRED(q2, {s, s}) \ DECL_PRED(r, {s}) \ DECL_PRED(r2, {s, s}) \ + DECL_PRED(between, {s, s, s, s}) \ + DECL_PRED(between_c, {s, s, s, s}) \ + DECL_PRED(between_o, {s, s, s, s}) \ + DECL_PRED(closed, {s}) \ + DECL_PRED(end_point, {s, s}) \ + DECL_PRED(finish_point, {s, s}) \ + DECL_PRED(incident_c, {s, s}) \ + DECL_PRED(incident_o, {s, s}) \ + DECL_PRED(inner_point, {s, s}) \ + DECL_PRED(meet, {s, s, s}) \ + DECL_PRED(open, {s}) \ + DECL_PRED(ordered_by, {s, s, s}) \ + DECL_PRED(part_of, {s, s}) \ + DECL_PRED(sP0, {s, s, s, s, s}) \ + DECL_PRED(start_point, {s, s}) \ + DECL_PRED(abstraction, {s, s}) \ + DECL_PRED(accessible_world, {s, s}) \ + DECL_PRED(agent, {s, s, s}) \ + DECL_PRED(animate, {s, s}) \ + DECL_PRED(be, {s, s, s, s}) \ + DECL_PRED(entity, {s, s}) \ + DECL_PRED(event, {s, s}) \ + DECL_PRED(eventuality, {s, s}) \ + DECL_PRED(existent, {s, s}) \ + DECL_PRED(forename, {s, s}) \ + DECL_PRED(general, {s, s}) \ + DECL_PRED(human, {s, s}) \ + DECL_PRED(human_person, {s, s}) \ + DECL_PRED(impartial, {s, s}) \ + DECL_PRED(jules_forename, {s, s}) \ + DECL_PRED(living, {s, s}) \ + DECL_PRED(male, {s, s}) \ + DECL_PRED(man, {s, s}) \ + DECL_PRED(nonexistent, {s, s}) \ + DECL_PRED(nonhuman, {s, s}) \ + DECL_PRED(of, {s, s, s}) \ + DECL_PRED(organism, {s, s}) \ + DECL_PRED(present, {s, s}) \ + DECL_PRED(proposition, {s, s}) \ + DECL_PRED(relation, {s, s}) \ + DECL_PRED(relname, {s, s}) \ + DECL_PRED(singleton, {s, s}) \ + DECL_PRED(smoke, {s, s}) \ + DECL_PRED(specific, {s, s}) \ + DECL_PRED(state, {s, s}) \ + DECL_PRED(theme, {s, s, s}) \ + DECL_PRED(thing, {s, s}) \ + DECL_PRED(think_believe_consider, {s, s}) \ + DECL_PRED(unisex, {s, s}) \ + DECL_PRED(vincent_forename, {s, s}) \ ) namespace { @@ -324,4 +420,959 @@ TEST_SIMPLIFICATION(neg_sub_res_test12, .justifications({ /* nothing */ }) ) +TEST_FUN(reproducer) +{ + MY_SYNTAX_SUGAR + ClauseCodeTree wtree; + ClauseCodeTree::ClauseMatcher m; + Kernel::Clause* D; + int resolvedQueryLit; + + + Kernel::Clause* C1 = clause({~man(skc12,x1), ~agent(skc12,skf1(x1),x1)}); + wtree.insert(C1); + D = clause({human_person(x1,x2), organism(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C2 = clause({human_person(x1,x2), organism(x1,x2)}); + wtree.insert(C2); + D = clause({human(x1,x3), ~human(x2,x3), accessible_world(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C3 = clause({human(x1,x3), ~human(x2,x3), accessible_world(x1,x2)}); + wtree.insert(C3); + D = clause({general(x1,x3), ~general(x2,x3), accessible_world(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C4 = clause({general(x1,x3), ~general(x2,x3), accessible_world(x1,x2)}); + wtree.insert(C4); + D = clause({state(x1,x2), ~eventuality(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C5 = clause({state(x1,x2), ~eventuality(x1,x2)}); + wtree.insert(C5); + D = clause({~state(skc8,skc9)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C6 = clause({~state(skc8,skc9)}); + wtree.insert(C6); + D = clause({human(x1,x2), ~nonhuman(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C7 = clause({human(x1,x2), ~nonhuman(x1,x2)}); + wtree.insert(C7); + D = clause({human_person(x1,x3), accessible_world(x1,x2), ~human_person(x2,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C8 = clause({human_person(x1,x3), accessible_world(x1,x2), ~human_person(x2,x3)}); + wtree.insert(C8); + D = clause({~relname(x1,x2), relation(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C9 = clause({~relname(x1,x2), relation(x1,x2)}); + wtree.insert(C9); + D = clause({~think_believe_consider(skc8,skc13)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C10 = clause({~think_believe_consider(skc8,skc13)}); + wtree.insert(C10); + D = clause({~existent(x2,x3), existent(x1,x3), accessible_world(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C11 = clause({~existent(x2,x3), existent(x1,x3), accessible_world(x1,x2)}); + wtree.insert(C11); + D = clause({~jules_forename(x1,x2), forename(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C12 = clause({~jules_forename(x1,x2), forename(x1,x2)}); + wtree.insert(C12); + D = clause({forename(skc8,skc14)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C13 = clause({forename(skc8,skc14)}); + wtree.insert(C13); + D = clause({man(skc8,skc15)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C14 = clause({man(skc8,skc15)}); + wtree.insert(C14); + D = clause({~man(x1,x2), ~human_person(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C15 = clause({~man(x1,x2), ~human_person(x1,x2)}); + wtree.insert(C15); + D = clause({~animate(x1,x3), accessible_world(x1,x2), animate(x2,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C16 = clause({~animate(x1,x3), accessible_world(x1,x2), animate(x2,x3)}); + wtree.insert(C16); + D = clause({proposition(x1,x2), relation(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C17 = clause({proposition(x1,x2), relation(x1,x2)}); + wtree.insert(C17); + D = clause({~organism(x1,x2), entity(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C18 = clause({~organism(x1,x2), entity(x1,x2)}); + wtree.insert(C18); + D = clause({x2 == x3, think_believe_consider(x1,x4), agent(x1,x4,x6), agent(x1,x5,x6), proposition(x1,x2), proposition(x1,x3), theme(x1,x5,x3), theme(x1,x4,x2), think_believe_consider(x1,x5)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C19 = clause({x2 == x3, think_believe_consider(x1,x4), agent(x1,x4,x6), agent(x1,x5,x6), proposition(x1,x2), proposition(x1,x3), theme(x1,x5,x3), theme(x1,x4,x2), think_believe_consider(x1,x5)}); + wtree.insert(C19); + D = clause({vincent_forename(skc8,skc14)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C20 = clause({vincent_forename(skc8,skc14)}); + wtree.insert(C20); + D = clause({~agent(skc8,skc13,skc15)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C21 = clause({~agent(skc8,skc13,skc15)}); + wtree.insert(C21); + D = clause({~man(x1,x2), male(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C22 = clause({~man(x1,x2), male(x1,x2)}); + wtree.insert(C22); + D = clause({of(skc8,skc14,skc15)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C23 = clause({of(skc8,skc14,skc15)}); + wtree.insert(C23); + D = clause({~relname(x1,x3), relname(x2,x3), accessible_world(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C24 = clause({~relname(x1,x3), relname(x2,x3), accessible_world(x1,x2)}); + wtree.insert(C24); + D = clause({~eventuality(x1,x2), event(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C25 = clause({~eventuality(x1,x2), event(x1,x2)}); + wtree.insert(C25); + D = clause({forename(skc8,skc11)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C26 = clause({forename(skc8,skc11)}); + wtree.insert(C26); + D = clause({~event(skc12,skf1(x2)), ~man(skc12,x1)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C27 = clause({~event(skc12,skf1(x2)), ~man(skc12,x1)}); + wtree.insert(C27); + D = clause({~proposition(skc8,skc12)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C28 = clause({~proposition(skc8,skc12)}); + wtree.insert(C28); + D = clause({~forename(x1,x3), accessible_world(x1,x2), forename(x2,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C29 = clause({~forename(x1,x3), accessible_world(x1,x2), forename(x2,x3)}); + wtree.insert(C29); + D = clause({~general(x1,x2), ~abstraction(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C30 = clause({~general(x1,x2), ~abstraction(x1,x2)}); + wtree.insert(C30); + D = clause({accessible_world(x1,x2), ~unisex(x1,x3), unisex(x2,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C31 = clause({accessible_world(x1,x2), ~unisex(x1,x3), unisex(x2,x3)}); + wtree.insert(C31); + D = clause({state(x1,x2), ~event(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C32 = clause({state(x1,x2), ~event(x1,x2)}); + wtree.insert(C32); + D = clause({human_person(x1,x2), animate(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C33 = clause({human_person(x1,x2), animate(x1,x2)}); + wtree.insert(C33); + D = clause({vincent_forename(x2,x3), ~vincent_forename(x1,x3), accessible_world(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C34 = clause({vincent_forename(x2,x3), ~vincent_forename(x1,x3), accessible_world(x1,x2)}); + wtree.insert(C34); + D = clause({eventuality(x1,x2), thing(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C35 = clause({eventuality(x1,x2), thing(x1,x2)}); + wtree.insert(C35); + D = clause({~accessible_world(skc8,skc12)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C36 = clause({~accessible_world(skc8,skc12)}); + wtree.insert(C36); + D = clause({~present(skc8,skc13)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C37 = clause({~present(skc8,skc13)}); + wtree.insert(C37); + D = clause({accessible_world(x1,x2), ~impartial(x2,x3), impartial(x1,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C38 = clause({accessible_world(x1,x2), ~impartial(x2,x3), impartial(x1,x3)}); + wtree.insert(C38); + D = clause({~forename(x1,x2), relname(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C39 = clause({~forename(x1,x2), relname(x1,x2)}); + wtree.insert(C39); + D = clause({~relation(x1,x2), abstraction(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C40 = clause({~relation(x1,x2), abstraction(x1,x2)}); + wtree.insert(C40); + D = clause({x2 == x3, ~forename(x1,x3), ~of(x1,x3,x4), ~of(x1,x2,x4), ~forename(x1,x2), ~entity(x1,x4)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C41 = clause({x2 == x3, ~forename(x1,x3), ~of(x1,x3,x4), ~of(x1,x2,x4), ~forename(x1,x2), ~entity(x1,x4)}); + wtree.insert(C41); + D = clause({general(x1,x2), ~specific(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C42 = clause({general(x1,x2), ~specific(x1,x2)}); + wtree.insert(C42); + D = clause({~singleton(x2,x3), singleton(x1,x3), accessible_world(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C43 = clause({~singleton(x2,x3), singleton(x1,x3), accessible_world(x1,x2)}); + wtree.insert(C43); + D = clause({specific(x1,x2), ~entity(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C44 = clause({specific(x1,x2), ~entity(x1,x2)}); + wtree.insert(C44); + D = clause({jules_forename(skc8,skc11)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C45 = clause({jules_forename(skc8,skc11)}); + wtree.insert(C45); + D = clause({~unisex(x1,x2), ~male(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C46 = clause({~unisex(x1,x2), ~male(x1,x2)}); + wtree.insert(C46); + D = clause({~human(x1,x2), human_person(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C47 = clause({~human(x1,x2), human_person(x1,x2)}); + wtree.insert(C47); + D = clause({~agent(x2,x3,x4), agent(x1,x3,x4), accessible_world(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C48 = clause({~agent(x2,x3,x4), agent(x1,x3,x4), accessible_world(x1,x2)}); + wtree.insert(C48); + D = clause({accessible_world(x1,x2), ~eventuality(x2,x3), eventuality(x1,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C49 = clause({accessible_world(x1,x2), ~eventuality(x2,x3), eventuality(x1,x3)}); + wtree.insert(C49); + D = clause({accessible_world(x1,x2), be(x1,x3,x4,x5), ~be(x2,x3,x4,x5)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C50 = clause({accessible_world(x1,x2), be(x1,x3,x4,x5), ~be(x2,x3,x4,x5)}); + wtree.insert(C50); + D = clause({~impartial(x1,x2), ~organism(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C51 = clause({~impartial(x1,x2), ~organism(x1,x2)}); + wtree.insert(C51); + D = clause({think_believe_consider(x1,x3), ~think_believe_consider(x2,x3), accessible_world(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C52 = clause({think_believe_consider(x1,x3), ~think_believe_consider(x2,x3), accessible_world(x1,x2)}); + wtree.insert(C52); + D = clause({theme(x1,x3,x4), ~theme(x2,x3,x4), accessible_world(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C53 = clause({theme(x1,x3,x4), ~theme(x2,x3,x4), accessible_world(x1,x2)}); + wtree.insert(C53); + D = clause({man(skc8,skc10)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C54 = clause({man(skc8,skc10)}); + wtree.insert(C54); + D = clause({relation(x2,x3), accessible_world(x1,x2), ~relation(x1,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C55 = clause({relation(x2,x3), accessible_world(x1,x2), ~relation(x1,x3)}); + wtree.insert(C55); + D = clause({~specific(x1,x3), specific(x2,x3), accessible_world(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C56 = clause({~specific(x1,x3), specific(x2,x3), accessible_world(x1,x2)}); + wtree.insert(C56); + D = clause({accessible_world(x1,x2), thing(x2,x3), ~thing(x1,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C57 = clause({accessible_world(x1,x2), thing(x2,x3), ~thing(x1,x3)}); + wtree.insert(C57); + D = clause({~present(skc12,skf1(x2)), ~man(skc12,x1)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C58 = clause({~present(skc12,skf1(x2)), ~man(skc12,x1)}); + wtree.insert(C58); + D = clause({entity(x2,x3), accessible_world(x1,x2), ~entity(x1,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C59 = clause({entity(x2,x3), accessible_world(x1,x2), ~entity(x1,x3)}); + wtree.insert(C59); + D = clause({abstraction(x2,x3), accessible_world(x1,x2), ~abstraction(x1,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C60 = clause({abstraction(x2,x3), accessible_world(x1,x2), ~abstraction(x1,x3)}); + wtree.insert(C60); + D = clause({~theme(skc8,skc13,skc12)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C61 = clause({~theme(skc8,skc13,skc12)}); + wtree.insert(C61); + D = clause({~existent(x1,x2), ~entity(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C62 = clause({~existent(x1,x2), ~entity(x1,x2)}); + wtree.insert(C62); + D = clause({living(x1,x3), ~living(x2,x3), accessible_world(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C63 = clause({living(x1,x3), ~living(x2,x3), accessible_world(x1,x2)}); + wtree.insert(C63); + D = clause({~abstraction(x1,x2), thing(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C64 = clause({~abstraction(x1,x2), thing(x1,x2)}); + wtree.insert(C64); + D = clause({of(skc8,skc11,skc10)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C65 = clause({of(skc8,skc11,skc10)}); + wtree.insert(C65); + D = clause({~living(x1,x2), ~organism(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C66 = clause({~living(x1,x2), ~organism(x1,x2)}); + wtree.insert(C66); + D = clause({accessible_world(x1,x2), ~proposition(x2,x3), proposition(x1,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C67 = clause({accessible_world(x1,x2), ~proposition(x2,x3), proposition(x1,x3)}); + wtree.insert(C67); + D = clause({thing(x1,x2), ~entity(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C68 = clause({thing(x1,x2), ~entity(x1,x2)}); + wtree.insert(C68); + D = clause({eventuality(x1,x2), ~nonexistent(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C69 = clause({eventuality(x1,x2), ~nonexistent(x1,x2)}); + wtree.insert(C69); + D = clause({~event(skc8,skc13)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C70 = clause({~event(skc8,skc13)}); + wtree.insert(C70); + D = clause({forename(x1,x2), ~vincent_forename(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C71 = clause({forename(x1,x2), ~vincent_forename(x1,x2)}); + wtree.insert(C71); + D = clause({accessible_world(x1,x2), organism(x2,x3), ~organism(x1,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C72 = clause({accessible_world(x1,x2), organism(x2,x3), ~organism(x1,x3)}); + wtree.insert(C72); + D = clause({~abstraction(x1,x2), unisex(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C73 = clause({~abstraction(x1,x2), unisex(x1,x2)}); + wtree.insert(C73); + D = clause({nonhuman(x1,x2), ~abstraction(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C74 = clause({nonhuman(x1,x2), ~abstraction(x1,x2)}); + wtree.insert(C74); + D = clause({~state(x2,x3), accessible_world(x1,x2), state(x1,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C75 = clause({~state(x2,x3), accessible_world(x1,x2), state(x1,x3)}); + wtree.insert(C75); + D = clause({accessible_world(x1,x2), ~smoke(x2,x3), smoke(x1,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C76 = clause({accessible_world(x1,x2), ~smoke(x2,x3), smoke(x1,x3)}); + wtree.insert(C76); + D = clause({~event(x1,x2), smoke(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C77 = clause({~event(x1,x2), smoke(x1,x2)}); + wtree.insert(C77); + D = clause({unisex(x1,x2), eventuality(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C78 = clause({unisex(x1,x2), eventuality(x1,x2)}); + wtree.insert(C78); + D = clause({~event(x2,x3), event(x1,x3), accessible_world(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C79 = clause({~event(x2,x3), event(x1,x3), accessible_world(x1,x2)}); + wtree.insert(C79); + D = clause({~be(skc8,skc9,skc10,skc10)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C80 = clause({~be(skc8,skc9,skc10,skc10)}); + wtree.insert(C80); + D = clause({man(x2,x3), ~man(x1,x3), accessible_world(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C81 = clause({man(x2,x3), ~man(x1,x3), accessible_world(x1,x2)}); + wtree.insert(C81); + D = clause({~jules_forename(x1,x3), jules_forename(x2,x3), accessible_world(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C82 = clause({~jules_forename(x1,x3), jules_forename(x2,x3), accessible_world(x1,x2)}); + wtree.insert(C82); + D = clause({specific(x1,x2), eventuality(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C83 = clause({specific(x1,x2), eventuality(x1,x2)}); + wtree.insert(C83); + D = clause({~smoke(skc12,skf1(x2)), ~man(skc12,x1)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C84 = clause({~smoke(skc12,skf1(x2)), ~man(skc12,x1)}); + wtree.insert(C84); + D = clause({existent(x1,x2), nonexistent(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C85 = clause({existent(x1,x2), nonexistent(x1,x2)}); + wtree.insert(C85); + D = clause({accessible_world(x1,x2), nonhuman(x2,x3), ~nonhuman(x1,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C86 = clause({accessible_world(x1,x2), nonhuman(x2,x3), ~nonhuman(x1,x3)}); + wtree.insert(C86); + D = clause({be(x1,x2,x3,x4), x3 == x4}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C87 = clause({be(x1,x2,x3,x4), x3 == x4}); + wtree.insert(C87); + D = clause({nonexistent(x1,x3), accessible_world(x1,x2), ~nonexistent(x2,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C88 = clause({nonexistent(x1,x3), accessible_world(x1,x2), ~nonexistent(x2,x3)}); + wtree.insert(C88); + D = clause({~singleton(x1,x2), ~thing(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C89 = clause({~singleton(x1,x2), ~thing(x1,x2)}); + wtree.insert(C89); + D = clause({~male(x1,x3), male(x2,x3), accessible_world(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C90 = clause({~male(x1,x3), male(x2,x3), accessible_world(x1,x2)}); + wtree.insert(C90); + D = clause({~present(x2,x3), accessible_world(x1,x2), present(x1,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C91 = clause({~present(x2,x3), accessible_world(x1,x2), present(x1,x3)}); + wtree.insert(C91); + D = clause({of(x2,x3,x4), ~of(x1,x3,x4), accessible_world(x1,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C92 = clause({of(x2,x3,x4), ~of(x1,x3,x4), accessible_world(x1,x2)}); + wtree.insert(C92); + wtree.remove(C14); + D = clause({man(skc8,skc15)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C93 = clause({man(skc8,skc15)}); + wtree.insert(C93); + wtree.remove(C13); + D = clause({forename(skc8,skc14)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C94 = clause({forename(skc8,skc14)}); + wtree.insert(C94); + wtree.remove(C20); + D = clause({vincent_forename(skc8,skc14)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C95 = clause({vincent_forename(skc8,skc14)}); + wtree.insert(C95); + wtree.remove(C45); + D = clause({jules_forename(skc8,skc11)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C96 = clause({jules_forename(skc8,skc11)}); + wtree.insert(C96); + wtree.remove(C26); + D = clause({forename(skc8,skc11)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C97 = clause({forename(skc8,skc11)}); + wtree.insert(C97); + wtree.remove(C54); + D = clause({man(skc8,skc10)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C98 = clause({man(skc8,skc10)}); + wtree.insert(C98); + wtree.remove(C70); + D = clause({~event(skc8,skc13)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C99 = clause({~event(skc8,skc13)}); + wtree.insert(C99); + wtree.remove(C37); + D = clause({~present(skc8,skc13)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C100 = clause({~present(skc8,skc13)}); + wtree.insert(C100); + wtree.remove(C36); + D = clause({~accessible_world(skc8,skc12)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C101 = clause({~accessible_world(skc8,skc12)}); + wtree.insert(C101); + wtree.remove(C28); + D = clause({~proposition(skc8,skc12)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C102 = clause({~proposition(skc8,skc12)}); + wtree.insert(C102); + wtree.remove(C10); + D = clause({~think_believe_consider(skc8,skc13)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C103 = clause({~think_believe_consider(skc8,skc13)}); + wtree.insert(C103); + wtree.remove(C6); + D = clause({~state(skc8,skc9)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C104 = clause({~state(skc8,skc9)}); + wtree.insert(C104); + wtree.remove(C23); + D = clause({of(skc8,skc14,skc15)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C105 = clause({of(skc8,skc14,skc15)}); + wtree.insert(C105); + wtree.remove(C65); + D = clause({of(skc8,skc11,skc10)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C106 = clause({of(skc8,skc11,skc10)}); + wtree.insert(C106); + wtree.remove(C61); + D = clause({~theme(skc8,skc13,skc12)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C107 = clause({~theme(skc8,skc13,skc12)}); + wtree.insert(C107); + wtree.remove(C21); + D = clause({~agent(skc8,skc13,skc15)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C108 = clause({~agent(skc8,skc13,skc15)}); + wtree.insert(C108); + wtree.remove(C80); + D = clause({~be(skc8,skc9,skc10,skc10)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C109 = clause({~be(skc8,skc9,skc10,skc10)}); + wtree.insert(C109); + wtree.remove(C84); + D = clause({~smoke(skc12,skf1(x2))}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C110 = clause({~smoke(skc12,skf1(x2))}); + wtree.insert(C110); + wtree.remove(C58); + D = clause({~man(skc12,x1)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C111 = clause({~man(skc12,x1)}); + wtree.insert(C111); + wtree.remove(C27); + D = clause({forename(skc8,skc11)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + D = clause({forename(skc8,skc14)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + D = clause({~event(skc12,skf1(x1))}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C112 = clause({~event(skc12,skf1(x1))}); + wtree.insert(C112); + D = clause({~event(skc8,skc9)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C113 = clause({~event(skc8,skc9)}); + wtree.insert(C113); + D = clause({~eventuality(skc8,skc13)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C114 = clause({~eventuality(skc8,skc13)}); + wtree.insert(C114); + D = clause({~eventuality(skc8,skc9)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C115 = clause({~eventuality(skc8,skc9)}); + wtree.insert(C115); + D = clause({~present(x1,x2), accessible_world(x3,x1), present(x4,x2), accessible_world(x4,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C116 = clause({~present(x1,x2), accessible_world(x3,x1), present(x4,x2), accessible_world(x4,x3)}); + wtree.insert(C116); + D = clause({~present(x1,skc13), accessible_world(skc8,x1)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C117 = clause({~present(x1,skc13), accessible_world(skc8,x1)}); + wtree.insert(C117); + D = clause({present(x1,x2), accessible_world(x1,x3), ~present(x4,x2), accessible_world(x3,x4)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + D = clause({~jules_forename(x1,x2), accessible_world(x1,x3), forename(x3,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C118 = clause({~jules_forename(x1,x2), accessible_world(x1,x3), forename(x3,x2)}); + wtree.insert(C118); + D = clause({~jules_forename(x1,x2), accessible_world(x1,x3), jules_forename(x4,x2), accessible_world(x3,x4)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C119 = clause({~jules_forename(x1,x2), accessible_world(x1,x3), jules_forename(x4,x2), accessible_world(x3,x4)}); + wtree.insert(C119); + D = clause({jules_forename(x1,x2), accessible_world(x3,x1), ~jules_forename(x4,x2), accessible_world(x4,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + D = clause({jules_forename(x1,skc11), accessible_world(skc8,x1)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C120 = clause({jules_forename(x1,skc11), accessible_world(skc8,x1)}); + wtree.insert(C120); + D = clause({man(x1,x2), accessible_world(x3,x1), ~man(x4,x2), accessible_world(x4,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C121 = clause({man(x1,x2), accessible_world(x3,x1), ~man(x4,x2), accessible_world(x4,x3)}); + wtree.insert(C121); + D = clause({man(x1,skc10), accessible_world(skc8,x1)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C122 = clause({man(x1,skc10), accessible_world(skc8,x1)}); + wtree.insert(C122); + D = clause({man(x1,skc15), accessible_world(skc8,x1)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C123 = clause({man(x1,skc15), accessible_world(skc8,x1)}); + wtree.insert(C123); + D = clause({~man(x1,x2), accessible_world(x1,x3), man(x4,x2), accessible_world(x3,x4)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + D = clause({~man(x1,x2), accessible_world(x1,skc12)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C124 = clause({~man(x1,x2), accessible_world(x1,skc12)}); + wtree.insert(C124); + D = clause({~event(x1,x2), accessible_world(x3,x1), event(x4,x2), accessible_world(x4,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C125 = clause({~event(x1,x2), accessible_world(x3,x1), event(x4,x2), accessible_world(x4,x3)}); + wtree.insert(C125); + D = clause({~event(x1,skc13), accessible_world(skc8,x1)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C126 = clause({~event(x1,skc13), accessible_world(skc8,x1)}); + wtree.insert(C126); + D = clause({event(x1,x2), accessible_world(x1,x3), ~eventuality(x3,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C127 = clause({event(x1,x2), accessible_world(x1,x3), ~eventuality(x3,x2)}); + wtree.insert(C127); + D = clause({event(x1,x2), accessible_world(x1,x3), ~event(x4,x2), accessible_world(x3,x4)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + D = clause({~smoke(x1,x2), accessible_world(x3,x1), smoke(x4,x2), accessible_world(x4,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C128 = clause({~smoke(x1,x2), accessible_world(x3,x1), smoke(x4,x2), accessible_world(x4,x3)}); + wtree.insert(C128); + D = clause({~smoke(x1,skf1(x2)), accessible_world(skc12,x1)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C129 = clause({~smoke(x1,skf1(x2)), accessible_world(skc12,x1)}); + wtree.insert(C129); + D = clause({smoke(x1,x2), accessible_world(x1,x3), ~event(x3,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C130 = clause({smoke(x1,x2), accessible_world(x1,x3), ~event(x3,x2)}); + wtree.insert(C130); + D = clause({smoke(x1,x2), accessible_world(x1,x3), ~smoke(x4,x2), accessible_world(x3,x4)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + D = clause({~state(x1,x2), accessible_world(x3,x1), state(x4,x2), accessible_world(x4,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C131 = clause({~state(x1,x2), accessible_world(x3,x1), state(x4,x2), accessible_world(x4,x3)}); + wtree.insert(C131); + D = clause({~state(x1,skc9), accessible_world(skc8,x1)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C132 = clause({~state(x1,skc9), accessible_world(skc8,x1)}); + wtree.insert(C132); + D = clause({state(x1,x2), accessible_world(x1,x3), ~event(x3,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C133 = clause({state(x1,x2), accessible_world(x1,x3), ~event(x3,x2)}); + wtree.insert(C133); + D = clause({state(x1,x2), accessible_world(x1,x3), ~eventuality(x3,x2)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C134 = clause({state(x1,x2), accessible_world(x1,x3), ~eventuality(x3,x2)}); + wtree.insert(C134); + D = clause({state(x1,x2), accessible_world(x1,x3), ~state(x4,x2), accessible_world(x3,x4)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + D = clause({~proposition(x1,x2), accessible_world(x3,x1), proposition(x4,x2), accessible_world(x4,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C135 = clause({~proposition(x1,x2), accessible_world(x3,x1), proposition(x4,x2), accessible_world(x4,x3)}); + wtree.insert(C135); + D = clause({~proposition(x1,skc12), accessible_world(skc8,x1)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C136 = clause({~proposition(x1,skc12), accessible_world(skc8,x1)}); + wtree.insert(C136); + D = clause({proposition(x1,x2), accessible_world(x1,x3), ~proposition(x4,x2), accessible_world(x3,x4)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + wtree.remove(C113); + D = clause({~event(skc8,skc9)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C137 = clause({~event(skc8,skc9)}); + wtree.insert(C137); + D = clause({think_believe_consider(x1,x2), accessible_world(x1,x3), ~think_believe_consider(x4,x2), accessible_world(x3,x4)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + Kernel::Clause* C138 = clause({think_believe_consider(x1,x2), accessible_world(x1,x3), ~think_believe_consider(x4,x2), accessible_world(x3,x4)}); + wtree.insert(C138); + D = clause({~think_believe_consider(x1,x2), accessible_world(x3,x1), think_believe_consider(x4,x2), accessible_world(x4,x3)}); + m.init(&wtree, D, true); + m.next(resolvedQueryLit); + m.reset(); + + D = clause({~think_believe_consider(x1,x2), accessible_world(x3,x1), think_believe_consider(x4,x2), accessible_world(x4,x3)}); + m.init(&wtree, D, true); + Kernel::Clause* premise; + SATSubsumption::SATSubsumptionAndResolution satSubs; + + //std::ofstream out("test.log"); + //out << "Tree is:" << std::endl; + //out << wtree << std::endl; + + premise = m.next(resolvedQueryLit); + std::cout << resolvedQueryLit << std::endl; + ASS_NEQ(resolvedQueryLit, -1); + ASS(satSubs.checkSubsumptionResolutionWithLiteral(premise, D, resolvedQueryLit)); +} + +TEST_FUN(reproducerMinimized) +{ + MY_SYNTAX_SUGAR + ClauseCodeTree wtree; + + ClauseCodeTree::ClauseMatcher m; + Kernel::Clause* D; + int resolvedQueryLit; + + + Kernel::Clause* C8 = clause({ accessible_world(x1,x2), ~human_person(x2,x3) }); + wtree.insert(C8); + Kernel::Clause* C50 = clause({ accessible_world(x1,x2), ~be(x2,x3,x4,x5) }); + wtree.insert(C50); + Kernel::Clause* C52 = clause({ think_believe_consider(x1,x3), ~think_believe_consider(x2,x3), accessible_world(x1,x2) }); + wtree.insert(C52); + Kernel::Clause* C67 = clause({ accessible_world(x1,x2), proposition(x1,x3) }); + wtree.insert(C67); + Kernel::Clause* C75 = clause({ ~state(x2,x3), accessible_world(x1,x2) }); + wtree.insert(C75); + Kernel::Clause* C130 = clause({ smoke(x1,x2), accessible_world(x1,x3) }); + wtree.insert(C130); + Kernel::Clause* C133 = clause({ accessible_world(x1,x3), ~event(x3,x2) }); + wtree.insert(C133); + Kernel::Clause* C134 = clause({ accessible_world(x1,x3), ~eventuality(x3,x2) }); + wtree.insert(C134); + Kernel::Clause* C138 = clause({ think_believe_consider(x1,x2), accessible_world(x1,x3) }); + wtree.insert(C138); + + std::cout << wtree << std::endl; + + D = clause({~think_believe_consider(x1,x2), accessible_world(x3,x1), think_believe_consider(x4,x2), accessible_world(x4,x3)}); + m.init(&wtree, D, true); + Kernel::Clause* premise; + SATSubsumption::SATSubsumptionAndResolution satSubs; + + //std::ofstream out("test.log"); + //out << "Tree is:" << std::endl; + //out << wtree << std::endl; + + premise = m.next(resolvedQueryLit); + std::cout << resolvedQueryLit << std::endl; + ASS_NEQ(resolvedQueryLit, -1); + ASS(satSubs.checkSubsumptionResolutionWithLiteral(premise, D, resolvedQueryLit)); +} } From 3f2e04c8f00c19728b0439594dc9433ee735c5e6 Mon Sep 17 00:00:00 2001 From: Synrom Date: Sat, 25 Jul 2026 14:33:02 +0100 Subject: [PATCH 07/15] Fix search struct bug and remove debugging logs --- Indexing/CodeTree.cpp | 18 +- Indexing/CodeTreeInterfaces.cpp | 10 - ...odeTreeForwardSubsumptionAndResolution.cpp | 33 +- ...ences_CodeTreeSubsumptionAndResolution.cpp | 82 ++ .../tInferences_SubsumptionAndResolution.cpp | 1079 +---------------- 5 files changed, 104 insertions(+), 1118 deletions(-) diff --git a/Indexing/CodeTree.cpp b/Indexing/CodeTree.cpp index d9ec3b010..09afa372b 100644 --- a/Indexing/CodeTree.cpp +++ b/Indexing/CodeTree.cpp @@ -849,17 +849,13 @@ inline bool CodeTree::Matcher::doSearchStruct const FlatTerm::Entry* fte=&(*ft)[tp]; CodeOp* target=op->getSearchStruct()->getTargetOp(fte, false); - if (tp == 0 && op->getSearchStruct()->kind == SearchStruct::FN_STRUCT) { - if (!target) { - target = op->getSearchStruct()->getTargetOp(fte, true); - } else { - CodeOp* alt = op->getSearchStruct()->getTargetOp(fte, true); - if (alt) { - if constexpr (removing) { - btStack.push(BTPointRemoving(tp, markOp(alt, true), RemovingBase::firstsInBlocks->size())); - } else { - btStack.push(BTPoint(tp, markOp(alt, true))); - } + if (canEnterOpposites && tp == 0 && op->getSearchStruct()->kind == SearchStruct::FN_STRUCT) { + CodeOp* alt = op->getSearchStruct()->getTargetOp(fte, true); + if (alt && target != alt) { + if constexpr (removing) { + btStack.push(BTPointRemoving(tp, markOp(alt, false), RemovingBase::firstsInBlocks->size())); + } else { + btStack.push(BTPoint(tp, markOp(alt, false))); } } } diff --git a/Indexing/CodeTreeInterfaces.cpp b/Indexing/CodeTreeInterfaces.cpp index a9db23c3e..b430bed46 100644 --- a/Indexing/CodeTreeInterfaces.cpp +++ b/Indexing/CodeTreeInterfaces.cpp @@ -13,8 +13,6 @@ * */ -#include - #include "Indexing/Index.hpp" #include "Indexing/ResultSubstitution.hpp" #include "Lib/Allocator.hpp" @@ -37,12 +35,6 @@ namespace Indexing using namespace Lib; using namespace Kernel; -std::ostream& codeTreeDebugLog() -{ - static std::ofstream out("wtree.log"); - return out; -} - template class CodeTreeSubstitution : public ResultSubstitution @@ -185,11 +177,9 @@ void CodeTreeSubsumptionIndex::handleClause(Clause* cl, bool adding TIME_TRACE("codetree subsumption index maintenance"); if(adding) { - codeTreeDebugLog() << "wtree.insert(clause({" << cl->toReproducerString() << "}));" << std::endl; _ct.insert(cl); } else { - codeTreeDebugLog() << "wtree.remove(clause({" << cl->toReproducerString() << "}));" << std::endl; _ct.remove(cl); } } diff --git a/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp b/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp index 790cb0fc2..2e339abcb 100644 --- a/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp +++ b/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp @@ -12,17 +12,11 @@ * Implements class CodeTreeForwardSubsumptionAndResolution. */ -#include - #include "Saturation/SaturationAlgorithm.hpp" #include "ProofExtra.hpp" #include "CodeTreeForwardSubsumptionAndResolution.hpp" -namespace Indexing { -std::ostream& codeTreeDebugLog(); -} - namespace Inferences { template @@ -42,15 +36,6 @@ bool CodeTreeForwardSubsumptionAndResolution::perform(Clause *cl, C static typename ClauseCodeTree::ClauseMatcher cm; cm.init(_ct, cl, _subsumptionResolution); - Indexing::codeTreeDebugLog() << "D = clause({" << cl->toReproducerString() << "});" << std::endl; - Indexing::codeTreeDebugLog() << "m.init(&wtree, D, "; - if (_subsumptionResolution) { - Indexing::codeTreeDebugLog() << "true);" << std::endl; - } else { - Indexing::codeTreeDebugLog() << "false);" << std::endl; - } - Indexing::codeTreeDebugLog() << "m.next(resolvedQueryLit);" << std::endl; - Indexing::codeTreeDebugLog() << "m.reset();" << std::endl; Clause* premise; int resolvedQueryLit; @@ -64,23 +49,7 @@ bool CodeTreeForwardSubsumptionAndResolution::perform(Clause *cl, C cm.reset(); return true; } -#if VDEBUG - bool subsumptionResolutionChecks = - satSubs.checkSubsumptionResolutionWithLiteral(premise, cl, resolvedQueryLit); - if(!subsumptionResolutionChecks) { - Indexing::codeTreeDebugLog() << "Tree is:" << std::endl; - Indexing::codeTreeDebugLog() << *_ct << std::endl; - Indexing::codeTreeDebugLog() << "Executed on " << cl->toReproducerString() << std::endl; - Indexing::codeTreeDebugLog() << "ResolvedQueryLit " << resolvedQueryLit<< std::endl; - Indexing::codeTreeDebugLog() << "_subsumptionResolution is " << _subsumptionResolution << std::endl; - if constexpr (higherOrder) { - Indexing::codeTreeDebugLog() << "higherOrder is true" << std::endl; - } else { - Indexing::codeTreeDebugLog() << "higherOrder is false" << std::endl; - } - } - ASS(subsumptionResolutionChecks); -#endif + ASS(satSubs.checkSubsumptionResolutionWithLiteral(premise, cl, resolvedQueryLit)); LiteralStack res; for (unsigned i = 0; i < cl->length(); i++) { diff --git a/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp b/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp index d526e67db..cd44dd399 100644 --- a/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp +++ b/UnitTests/tInferences_CodeTreeSubsumptionAndResolution.cpp @@ -50,12 +50,28 @@ using namespace Test; DECL_FUNC(i, {s}, s) \ DECL_FUNC(i2, {s, s}, s) \ DECL_PRED(p, {s}) \ + DECL_PRED(p1, {s}) \ DECL_PRED(p2, {s, s}) \ + DECL_PRED(p2u, {s}) \ DECL_PRED(p3, {s, s, s}) \ + DECL_PRED(p3u, {s}) \ + DECL_PRED(p4, {s}) \ + DECL_PRED(p5, {s}) \ DECL_PRED(q, {s}) \ + DECL_PRED(q0, {s}) \ + DECL_PRED(q1, {s}) \ DECL_PRED(q2, {s, s}) \ DECL_PRED(r, {s}) \ DECL_PRED(r2, {s, s}) \ + DECL_PRED(accessible_world, {s, s}) \ + DECL_PRED(be, {s, s, s, s}) \ + DECL_PRED(event, {s, s}) \ + DECL_PRED(eventuality, {s, s}) \ + DECL_PRED(human_person, {s, s}) \ + DECL_PRED(proposition, {s, s}) \ + DECL_PRED(smoke, {s, s}) \ + DECL_PRED(state, {s, s}) \ + DECL_PRED(think_believe_consider, {s, s}) \ ) namespace { @@ -324,4 +340,70 @@ TEST_SIMPLIFICATION(neg_sub_res_test12, .justifications({ /* nothing */ }) ) +TEST_SIMPLIFICATION(opposite_optimization_search_struct_1, + tester() + .simplifyWith({ + clause({ accessible_world(x1, x2), ~human_person(x2, x3) }), + clause({ accessible_world(x1, x2), ~be(x2, x3, x4, x5) }), + clause({ think_believe_consider(x1, x3), ~think_believe_consider(x2, x3), accessible_world(x1, x2) }), + clause({ accessible_world(x1, x2), proposition(x1, x3) }), + clause({ ~state(x2, x3), accessible_world(x1, x2) }), + clause({ smoke(x1, x2), accessible_world(x1, x3) }), + clause({ accessible_world(x1, x3), ~event(x3, x2) }), + clause({ accessible_world(x1, x3), ~eventuality(x3, x2) }), + clause({ think_believe_consider(x1, x2), accessible_world(x1, x3) }) + }) + .toSimplify({ + clause({ + ~think_believe_consider(x1, x2), + accessible_world(x3, x1), + think_believe_consider(x4, x2), + accessible_world(x4, x3) + }) + }) + .expected({ /* nothing */ }) + .justifications({ + clause({ + think_believe_consider(x1, x2), + accessible_world(x1, x3) + }) + }) +) + +TEST_SIMPLIFICATION(opposite_optimization_search_struct_2, + tester() + .simplifyWith({ + clause({ q0(f(x1)) }), + clause({ ~p1(x2) }), + clause({ ~p5(f(x1)) }), + clause({ ~r2(x1, x3), ~q1(x3) }), + clause({ ~p4(x2) }), + clause({ ~q1(d) }), + clause({ r2(x3, x1), ~p3u(x3) }), + clause({ r2(x3, x1), ~p1(x3) }) + }) + .toSimplify({ + clause({ + ~q0(x1), + ~q0(x4), + r2(x3, x2), + r2(x3, x1), + ~r2(x2, x4), + ~p2u(x3), + ~p3u(x2) + }) + }) + .expected({ + clause({ + ~q0(x1), + ~q0(x4), + r2(x3, x2), + r2(x3, x1), + ~p2u(x3), + ~p3u(x2) + }) + }) + .justifications({ clause({ r2(x3, x1), ~p3u(x3) }) }) +) + } diff --git a/UnitTests/tInferences_SubsumptionAndResolution.cpp b/UnitTests/tInferences_SubsumptionAndResolution.cpp index 2f94b73c5..f77e028f5 100644 --- a/UnitTests/tInferences_SubsumptionAndResolution.cpp +++ b/UnitTests/tInferences_SubsumptionAndResolution.cpp @@ -7,44 +7,36 @@ * https://vprover.github.io/license.html * and in the source directory */ -#include #include "Test/SyntaxSugar.hpp" #include "Inferences/ForwardSubsumptionAndResolution.hpp" #include "Inferences/BackwardSubsumptionAndResolution.hpp" -#include "Indexing/ClauseCodeTree.hpp" #include "Test/FwdBwdSimplificationTester.hpp" using namespace std; using namespace Kernel; using namespace Inferences; -using namespace Indexing; using namespace Test; #define MY_SYNTAX_SUGAR \ __ALLOW_UNUSED( \ DECL_DEFAULT_VARS \ + DECL_VAR(x1, 1) \ + DECL_VAR(x2, 2) \ + DECL_VAR(x3, 3) \ + DECL_VAR(x4, 4) \ + DECL_VAR(x5, 5) \ + DECL_VAR(x6, 6) \ + DECL_VAR(x7, 7) \ + DECL_VAR(y1, 11) \ + DECL_VAR(y2, 12) \ + DECL_VAR(y3, 13) \ + DECL_VAR(y4, 14) \ + DECL_VAR(y5, 15) \ + DECL_VAR(y6, 16) \ + DECL_VAR(y7, 17) \ DECL_SORT(s) \ - DECL_VAR_SORTED(x1, 1, s) \ - DECL_VAR_SORTED(x2, 2, s) \ - DECL_VAR_SORTED(x3, 3, s) \ - DECL_VAR_SORTED(x4, 4, s) \ - DECL_VAR_SORTED(x5, 5, s) \ - DECL_VAR_SORTED(x6, 6, s) \ - DECL_VAR_SORTED(x7, 7, s) \ - DECL_VAR_SORTED(x8, 8, s) \ - DECL_VAR_SORTED(x9, 9, s) \ - DECL_VAR_SORTED(x10, 10, s) \ - DECL_VAR_SORTED(x11, 11, s) \ - DECL_VAR_SORTED(x12, 12, s) \ - DECL_VAR_SORTED(y1, 21, s) \ - DECL_VAR_SORTED(y2, 22, s) \ - DECL_VAR_SORTED(y3, 23, s) \ - DECL_VAR_SORTED(y4, 24, s) \ - DECL_VAR_SORTED(y5, 25, s) \ - DECL_VAR_SORTED(y6, 26, s) \ - DECL_VAR_SORTED(y7, 27, s) \ DECL_CONST(c, s) \ DECL_CONST(d, s) \ DECL_CONST(e, s) \ @@ -57,44 +49,6 @@ using namespace Test; DECL_FUNC(h2, {s, s}, s) \ DECL_FUNC(i, {s}, s) \ DECL_FUNC(i2, {s, s}, s) \ - DECL_FUNC(sum, {s, s}, s) \ - DECL_FUNC(underlying_curve, {s}, s) \ - DECL_FUNC(sK1, {s, s}, s) \ - DECL_FUNC(sK2, {s, s}, s) \ - DECL_FUNC(sK3, {s, s}, s) \ - DECL_FUNC(sK4, {s, s}, s) \ - DECL_FUNC(sK5, {s, s, s, s}, s) \ - DECL_FUNC(sK6, {s, s}, s) \ - DECL_FUNC(sK7, {s}, s) \ - DECL_FUNC(sK8, {s, s, s, s}, s) \ - DECL_CONST(sK9, s) \ - DECL_CONST(sK10, s) \ - DECL_CONST(sK11, s) \ - DECL_CONST(sK12, s) \ - DECL_CONST(sK13, s) \ - DECL_CONST(skc8, s) \ - DECL_CONST(skc9, s) \ - DECL_CONST(skc10, s) \ - DECL_CONST(skc11, s) \ - DECL_CONST(skc12, s) \ - DECL_CONST(skc13, s) \ - DECL_CONST(skc14, s) \ - DECL_CONST(skc15, s) \ - DECL_FUNC(sK14, {s}, s) \ - DECL_FUNC(sK15, {s}, s) \ - DECL_FUNC(sK16, {s, s}, s) \ - DECL_FUNC(sK17, {s, s}, s) \ - DECL_FUNC(sK18, {s, s, s}, s) \ - DECL_FUNC(sK19, {s, s}, s) \ - DECL_FUNC(sK20, {s, s}, s) \ - DECL_FUNC(sK21, {s, s}, s) \ - DECL_FUNC(sK22, {s, s}, s) \ - DECL_FUNC(sK23, {s, s}, s) \ - DECL_FUNC(sK24, {s}, s) \ - DECL_FUNC(sK25, {s, s, s}, s) \ - DECL_FUNC(sK26, {s, s}, s) \ - DECL_FUNC(sK27, {s}, s) \ - DECL_FUNC(skf1, {s}, s) \ DECL_PRED(p, {s}) \ DECL_PRED(p2, {s, s}) \ DECL_PRED(p3, {s, s, s}) \ @@ -102,56 +56,6 @@ using namespace Test; DECL_PRED(q2, {s, s}) \ DECL_PRED(r, {s}) \ DECL_PRED(r2, {s, s}) \ - DECL_PRED(between, {s, s, s, s}) \ - DECL_PRED(between_c, {s, s, s, s}) \ - DECL_PRED(between_o, {s, s, s, s}) \ - DECL_PRED(closed, {s}) \ - DECL_PRED(end_point, {s, s}) \ - DECL_PRED(finish_point, {s, s}) \ - DECL_PRED(incident_c, {s, s}) \ - DECL_PRED(incident_o, {s, s}) \ - DECL_PRED(inner_point, {s, s}) \ - DECL_PRED(meet, {s, s, s}) \ - DECL_PRED(open, {s}) \ - DECL_PRED(ordered_by, {s, s, s}) \ - DECL_PRED(part_of, {s, s}) \ - DECL_PRED(sP0, {s, s, s, s, s}) \ - DECL_PRED(start_point, {s, s}) \ - DECL_PRED(abstraction, {s, s}) \ - DECL_PRED(accessible_world, {s, s}) \ - DECL_PRED(agent, {s, s, s}) \ - DECL_PRED(animate, {s, s}) \ - DECL_PRED(be, {s, s, s, s}) \ - DECL_PRED(entity, {s, s}) \ - DECL_PRED(event, {s, s}) \ - DECL_PRED(eventuality, {s, s}) \ - DECL_PRED(existent, {s, s}) \ - DECL_PRED(forename, {s, s}) \ - DECL_PRED(general, {s, s}) \ - DECL_PRED(human, {s, s}) \ - DECL_PRED(human_person, {s, s}) \ - DECL_PRED(impartial, {s, s}) \ - DECL_PRED(jules_forename, {s, s}) \ - DECL_PRED(living, {s, s}) \ - DECL_PRED(male, {s, s}) \ - DECL_PRED(man, {s, s}) \ - DECL_PRED(nonexistent, {s, s}) \ - DECL_PRED(nonhuman, {s, s}) \ - DECL_PRED(of, {s, s, s}) \ - DECL_PRED(organism, {s, s}) \ - DECL_PRED(present, {s, s}) \ - DECL_PRED(proposition, {s, s}) \ - DECL_PRED(relation, {s, s}) \ - DECL_PRED(relname, {s, s}) \ - DECL_PRED(singleton, {s, s}) \ - DECL_PRED(smoke, {s, s}) \ - DECL_PRED(specific, {s, s}) \ - DECL_PRED(state, {s, s}) \ - DECL_PRED(theme, {s, s, s}) \ - DECL_PRED(thing, {s, s}) \ - DECL_PRED(think_believe_consider, {s, s}) \ - DECL_PRED(unisex, {s, s}) \ - DECL_PRED(vincent_forename, {s, s}) \ ) namespace { @@ -420,959 +324,4 @@ TEST_SIMPLIFICATION(neg_sub_res_test12, .justifications({ /* nothing */ }) ) -TEST_FUN(reproducer) -{ - MY_SYNTAX_SUGAR - ClauseCodeTree wtree; - ClauseCodeTree::ClauseMatcher m; - Kernel::Clause* D; - int resolvedQueryLit; - - - Kernel::Clause* C1 = clause({~man(skc12,x1), ~agent(skc12,skf1(x1),x1)}); - wtree.insert(C1); - D = clause({human_person(x1,x2), organism(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C2 = clause({human_person(x1,x2), organism(x1,x2)}); - wtree.insert(C2); - D = clause({human(x1,x3), ~human(x2,x3), accessible_world(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C3 = clause({human(x1,x3), ~human(x2,x3), accessible_world(x1,x2)}); - wtree.insert(C3); - D = clause({general(x1,x3), ~general(x2,x3), accessible_world(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C4 = clause({general(x1,x3), ~general(x2,x3), accessible_world(x1,x2)}); - wtree.insert(C4); - D = clause({state(x1,x2), ~eventuality(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C5 = clause({state(x1,x2), ~eventuality(x1,x2)}); - wtree.insert(C5); - D = clause({~state(skc8,skc9)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C6 = clause({~state(skc8,skc9)}); - wtree.insert(C6); - D = clause({human(x1,x2), ~nonhuman(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C7 = clause({human(x1,x2), ~nonhuman(x1,x2)}); - wtree.insert(C7); - D = clause({human_person(x1,x3), accessible_world(x1,x2), ~human_person(x2,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C8 = clause({human_person(x1,x3), accessible_world(x1,x2), ~human_person(x2,x3)}); - wtree.insert(C8); - D = clause({~relname(x1,x2), relation(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C9 = clause({~relname(x1,x2), relation(x1,x2)}); - wtree.insert(C9); - D = clause({~think_believe_consider(skc8,skc13)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C10 = clause({~think_believe_consider(skc8,skc13)}); - wtree.insert(C10); - D = clause({~existent(x2,x3), existent(x1,x3), accessible_world(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C11 = clause({~existent(x2,x3), existent(x1,x3), accessible_world(x1,x2)}); - wtree.insert(C11); - D = clause({~jules_forename(x1,x2), forename(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C12 = clause({~jules_forename(x1,x2), forename(x1,x2)}); - wtree.insert(C12); - D = clause({forename(skc8,skc14)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C13 = clause({forename(skc8,skc14)}); - wtree.insert(C13); - D = clause({man(skc8,skc15)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C14 = clause({man(skc8,skc15)}); - wtree.insert(C14); - D = clause({~man(x1,x2), ~human_person(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C15 = clause({~man(x1,x2), ~human_person(x1,x2)}); - wtree.insert(C15); - D = clause({~animate(x1,x3), accessible_world(x1,x2), animate(x2,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C16 = clause({~animate(x1,x3), accessible_world(x1,x2), animate(x2,x3)}); - wtree.insert(C16); - D = clause({proposition(x1,x2), relation(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C17 = clause({proposition(x1,x2), relation(x1,x2)}); - wtree.insert(C17); - D = clause({~organism(x1,x2), entity(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C18 = clause({~organism(x1,x2), entity(x1,x2)}); - wtree.insert(C18); - D = clause({x2 == x3, think_believe_consider(x1,x4), agent(x1,x4,x6), agent(x1,x5,x6), proposition(x1,x2), proposition(x1,x3), theme(x1,x5,x3), theme(x1,x4,x2), think_believe_consider(x1,x5)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C19 = clause({x2 == x3, think_believe_consider(x1,x4), agent(x1,x4,x6), agent(x1,x5,x6), proposition(x1,x2), proposition(x1,x3), theme(x1,x5,x3), theme(x1,x4,x2), think_believe_consider(x1,x5)}); - wtree.insert(C19); - D = clause({vincent_forename(skc8,skc14)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C20 = clause({vincent_forename(skc8,skc14)}); - wtree.insert(C20); - D = clause({~agent(skc8,skc13,skc15)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C21 = clause({~agent(skc8,skc13,skc15)}); - wtree.insert(C21); - D = clause({~man(x1,x2), male(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C22 = clause({~man(x1,x2), male(x1,x2)}); - wtree.insert(C22); - D = clause({of(skc8,skc14,skc15)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C23 = clause({of(skc8,skc14,skc15)}); - wtree.insert(C23); - D = clause({~relname(x1,x3), relname(x2,x3), accessible_world(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C24 = clause({~relname(x1,x3), relname(x2,x3), accessible_world(x1,x2)}); - wtree.insert(C24); - D = clause({~eventuality(x1,x2), event(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C25 = clause({~eventuality(x1,x2), event(x1,x2)}); - wtree.insert(C25); - D = clause({forename(skc8,skc11)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C26 = clause({forename(skc8,skc11)}); - wtree.insert(C26); - D = clause({~event(skc12,skf1(x2)), ~man(skc12,x1)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C27 = clause({~event(skc12,skf1(x2)), ~man(skc12,x1)}); - wtree.insert(C27); - D = clause({~proposition(skc8,skc12)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C28 = clause({~proposition(skc8,skc12)}); - wtree.insert(C28); - D = clause({~forename(x1,x3), accessible_world(x1,x2), forename(x2,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C29 = clause({~forename(x1,x3), accessible_world(x1,x2), forename(x2,x3)}); - wtree.insert(C29); - D = clause({~general(x1,x2), ~abstraction(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C30 = clause({~general(x1,x2), ~abstraction(x1,x2)}); - wtree.insert(C30); - D = clause({accessible_world(x1,x2), ~unisex(x1,x3), unisex(x2,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C31 = clause({accessible_world(x1,x2), ~unisex(x1,x3), unisex(x2,x3)}); - wtree.insert(C31); - D = clause({state(x1,x2), ~event(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C32 = clause({state(x1,x2), ~event(x1,x2)}); - wtree.insert(C32); - D = clause({human_person(x1,x2), animate(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C33 = clause({human_person(x1,x2), animate(x1,x2)}); - wtree.insert(C33); - D = clause({vincent_forename(x2,x3), ~vincent_forename(x1,x3), accessible_world(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C34 = clause({vincent_forename(x2,x3), ~vincent_forename(x1,x3), accessible_world(x1,x2)}); - wtree.insert(C34); - D = clause({eventuality(x1,x2), thing(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C35 = clause({eventuality(x1,x2), thing(x1,x2)}); - wtree.insert(C35); - D = clause({~accessible_world(skc8,skc12)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C36 = clause({~accessible_world(skc8,skc12)}); - wtree.insert(C36); - D = clause({~present(skc8,skc13)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C37 = clause({~present(skc8,skc13)}); - wtree.insert(C37); - D = clause({accessible_world(x1,x2), ~impartial(x2,x3), impartial(x1,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C38 = clause({accessible_world(x1,x2), ~impartial(x2,x3), impartial(x1,x3)}); - wtree.insert(C38); - D = clause({~forename(x1,x2), relname(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C39 = clause({~forename(x1,x2), relname(x1,x2)}); - wtree.insert(C39); - D = clause({~relation(x1,x2), abstraction(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C40 = clause({~relation(x1,x2), abstraction(x1,x2)}); - wtree.insert(C40); - D = clause({x2 == x3, ~forename(x1,x3), ~of(x1,x3,x4), ~of(x1,x2,x4), ~forename(x1,x2), ~entity(x1,x4)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C41 = clause({x2 == x3, ~forename(x1,x3), ~of(x1,x3,x4), ~of(x1,x2,x4), ~forename(x1,x2), ~entity(x1,x4)}); - wtree.insert(C41); - D = clause({general(x1,x2), ~specific(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C42 = clause({general(x1,x2), ~specific(x1,x2)}); - wtree.insert(C42); - D = clause({~singleton(x2,x3), singleton(x1,x3), accessible_world(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C43 = clause({~singleton(x2,x3), singleton(x1,x3), accessible_world(x1,x2)}); - wtree.insert(C43); - D = clause({specific(x1,x2), ~entity(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C44 = clause({specific(x1,x2), ~entity(x1,x2)}); - wtree.insert(C44); - D = clause({jules_forename(skc8,skc11)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C45 = clause({jules_forename(skc8,skc11)}); - wtree.insert(C45); - D = clause({~unisex(x1,x2), ~male(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C46 = clause({~unisex(x1,x2), ~male(x1,x2)}); - wtree.insert(C46); - D = clause({~human(x1,x2), human_person(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C47 = clause({~human(x1,x2), human_person(x1,x2)}); - wtree.insert(C47); - D = clause({~agent(x2,x3,x4), agent(x1,x3,x4), accessible_world(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C48 = clause({~agent(x2,x3,x4), agent(x1,x3,x4), accessible_world(x1,x2)}); - wtree.insert(C48); - D = clause({accessible_world(x1,x2), ~eventuality(x2,x3), eventuality(x1,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C49 = clause({accessible_world(x1,x2), ~eventuality(x2,x3), eventuality(x1,x3)}); - wtree.insert(C49); - D = clause({accessible_world(x1,x2), be(x1,x3,x4,x5), ~be(x2,x3,x4,x5)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C50 = clause({accessible_world(x1,x2), be(x1,x3,x4,x5), ~be(x2,x3,x4,x5)}); - wtree.insert(C50); - D = clause({~impartial(x1,x2), ~organism(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C51 = clause({~impartial(x1,x2), ~organism(x1,x2)}); - wtree.insert(C51); - D = clause({think_believe_consider(x1,x3), ~think_believe_consider(x2,x3), accessible_world(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C52 = clause({think_believe_consider(x1,x3), ~think_believe_consider(x2,x3), accessible_world(x1,x2)}); - wtree.insert(C52); - D = clause({theme(x1,x3,x4), ~theme(x2,x3,x4), accessible_world(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C53 = clause({theme(x1,x3,x4), ~theme(x2,x3,x4), accessible_world(x1,x2)}); - wtree.insert(C53); - D = clause({man(skc8,skc10)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C54 = clause({man(skc8,skc10)}); - wtree.insert(C54); - D = clause({relation(x2,x3), accessible_world(x1,x2), ~relation(x1,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C55 = clause({relation(x2,x3), accessible_world(x1,x2), ~relation(x1,x3)}); - wtree.insert(C55); - D = clause({~specific(x1,x3), specific(x2,x3), accessible_world(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C56 = clause({~specific(x1,x3), specific(x2,x3), accessible_world(x1,x2)}); - wtree.insert(C56); - D = clause({accessible_world(x1,x2), thing(x2,x3), ~thing(x1,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C57 = clause({accessible_world(x1,x2), thing(x2,x3), ~thing(x1,x3)}); - wtree.insert(C57); - D = clause({~present(skc12,skf1(x2)), ~man(skc12,x1)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C58 = clause({~present(skc12,skf1(x2)), ~man(skc12,x1)}); - wtree.insert(C58); - D = clause({entity(x2,x3), accessible_world(x1,x2), ~entity(x1,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C59 = clause({entity(x2,x3), accessible_world(x1,x2), ~entity(x1,x3)}); - wtree.insert(C59); - D = clause({abstraction(x2,x3), accessible_world(x1,x2), ~abstraction(x1,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C60 = clause({abstraction(x2,x3), accessible_world(x1,x2), ~abstraction(x1,x3)}); - wtree.insert(C60); - D = clause({~theme(skc8,skc13,skc12)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C61 = clause({~theme(skc8,skc13,skc12)}); - wtree.insert(C61); - D = clause({~existent(x1,x2), ~entity(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C62 = clause({~existent(x1,x2), ~entity(x1,x2)}); - wtree.insert(C62); - D = clause({living(x1,x3), ~living(x2,x3), accessible_world(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C63 = clause({living(x1,x3), ~living(x2,x3), accessible_world(x1,x2)}); - wtree.insert(C63); - D = clause({~abstraction(x1,x2), thing(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C64 = clause({~abstraction(x1,x2), thing(x1,x2)}); - wtree.insert(C64); - D = clause({of(skc8,skc11,skc10)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C65 = clause({of(skc8,skc11,skc10)}); - wtree.insert(C65); - D = clause({~living(x1,x2), ~organism(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C66 = clause({~living(x1,x2), ~organism(x1,x2)}); - wtree.insert(C66); - D = clause({accessible_world(x1,x2), ~proposition(x2,x3), proposition(x1,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C67 = clause({accessible_world(x1,x2), ~proposition(x2,x3), proposition(x1,x3)}); - wtree.insert(C67); - D = clause({thing(x1,x2), ~entity(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C68 = clause({thing(x1,x2), ~entity(x1,x2)}); - wtree.insert(C68); - D = clause({eventuality(x1,x2), ~nonexistent(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C69 = clause({eventuality(x1,x2), ~nonexistent(x1,x2)}); - wtree.insert(C69); - D = clause({~event(skc8,skc13)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C70 = clause({~event(skc8,skc13)}); - wtree.insert(C70); - D = clause({forename(x1,x2), ~vincent_forename(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C71 = clause({forename(x1,x2), ~vincent_forename(x1,x2)}); - wtree.insert(C71); - D = clause({accessible_world(x1,x2), organism(x2,x3), ~organism(x1,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C72 = clause({accessible_world(x1,x2), organism(x2,x3), ~organism(x1,x3)}); - wtree.insert(C72); - D = clause({~abstraction(x1,x2), unisex(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C73 = clause({~abstraction(x1,x2), unisex(x1,x2)}); - wtree.insert(C73); - D = clause({nonhuman(x1,x2), ~abstraction(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C74 = clause({nonhuman(x1,x2), ~abstraction(x1,x2)}); - wtree.insert(C74); - D = clause({~state(x2,x3), accessible_world(x1,x2), state(x1,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C75 = clause({~state(x2,x3), accessible_world(x1,x2), state(x1,x3)}); - wtree.insert(C75); - D = clause({accessible_world(x1,x2), ~smoke(x2,x3), smoke(x1,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C76 = clause({accessible_world(x1,x2), ~smoke(x2,x3), smoke(x1,x3)}); - wtree.insert(C76); - D = clause({~event(x1,x2), smoke(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C77 = clause({~event(x1,x2), smoke(x1,x2)}); - wtree.insert(C77); - D = clause({unisex(x1,x2), eventuality(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C78 = clause({unisex(x1,x2), eventuality(x1,x2)}); - wtree.insert(C78); - D = clause({~event(x2,x3), event(x1,x3), accessible_world(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C79 = clause({~event(x2,x3), event(x1,x3), accessible_world(x1,x2)}); - wtree.insert(C79); - D = clause({~be(skc8,skc9,skc10,skc10)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C80 = clause({~be(skc8,skc9,skc10,skc10)}); - wtree.insert(C80); - D = clause({man(x2,x3), ~man(x1,x3), accessible_world(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C81 = clause({man(x2,x3), ~man(x1,x3), accessible_world(x1,x2)}); - wtree.insert(C81); - D = clause({~jules_forename(x1,x3), jules_forename(x2,x3), accessible_world(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C82 = clause({~jules_forename(x1,x3), jules_forename(x2,x3), accessible_world(x1,x2)}); - wtree.insert(C82); - D = clause({specific(x1,x2), eventuality(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C83 = clause({specific(x1,x2), eventuality(x1,x2)}); - wtree.insert(C83); - D = clause({~smoke(skc12,skf1(x2)), ~man(skc12,x1)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C84 = clause({~smoke(skc12,skf1(x2)), ~man(skc12,x1)}); - wtree.insert(C84); - D = clause({existent(x1,x2), nonexistent(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C85 = clause({existent(x1,x2), nonexistent(x1,x2)}); - wtree.insert(C85); - D = clause({accessible_world(x1,x2), nonhuman(x2,x3), ~nonhuman(x1,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C86 = clause({accessible_world(x1,x2), nonhuman(x2,x3), ~nonhuman(x1,x3)}); - wtree.insert(C86); - D = clause({be(x1,x2,x3,x4), x3 == x4}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C87 = clause({be(x1,x2,x3,x4), x3 == x4}); - wtree.insert(C87); - D = clause({nonexistent(x1,x3), accessible_world(x1,x2), ~nonexistent(x2,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C88 = clause({nonexistent(x1,x3), accessible_world(x1,x2), ~nonexistent(x2,x3)}); - wtree.insert(C88); - D = clause({~singleton(x1,x2), ~thing(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C89 = clause({~singleton(x1,x2), ~thing(x1,x2)}); - wtree.insert(C89); - D = clause({~male(x1,x3), male(x2,x3), accessible_world(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C90 = clause({~male(x1,x3), male(x2,x3), accessible_world(x1,x2)}); - wtree.insert(C90); - D = clause({~present(x2,x3), accessible_world(x1,x2), present(x1,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C91 = clause({~present(x2,x3), accessible_world(x1,x2), present(x1,x3)}); - wtree.insert(C91); - D = clause({of(x2,x3,x4), ~of(x1,x3,x4), accessible_world(x1,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C92 = clause({of(x2,x3,x4), ~of(x1,x3,x4), accessible_world(x1,x2)}); - wtree.insert(C92); - wtree.remove(C14); - D = clause({man(skc8,skc15)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C93 = clause({man(skc8,skc15)}); - wtree.insert(C93); - wtree.remove(C13); - D = clause({forename(skc8,skc14)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C94 = clause({forename(skc8,skc14)}); - wtree.insert(C94); - wtree.remove(C20); - D = clause({vincent_forename(skc8,skc14)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C95 = clause({vincent_forename(skc8,skc14)}); - wtree.insert(C95); - wtree.remove(C45); - D = clause({jules_forename(skc8,skc11)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C96 = clause({jules_forename(skc8,skc11)}); - wtree.insert(C96); - wtree.remove(C26); - D = clause({forename(skc8,skc11)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C97 = clause({forename(skc8,skc11)}); - wtree.insert(C97); - wtree.remove(C54); - D = clause({man(skc8,skc10)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C98 = clause({man(skc8,skc10)}); - wtree.insert(C98); - wtree.remove(C70); - D = clause({~event(skc8,skc13)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C99 = clause({~event(skc8,skc13)}); - wtree.insert(C99); - wtree.remove(C37); - D = clause({~present(skc8,skc13)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C100 = clause({~present(skc8,skc13)}); - wtree.insert(C100); - wtree.remove(C36); - D = clause({~accessible_world(skc8,skc12)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C101 = clause({~accessible_world(skc8,skc12)}); - wtree.insert(C101); - wtree.remove(C28); - D = clause({~proposition(skc8,skc12)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C102 = clause({~proposition(skc8,skc12)}); - wtree.insert(C102); - wtree.remove(C10); - D = clause({~think_believe_consider(skc8,skc13)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C103 = clause({~think_believe_consider(skc8,skc13)}); - wtree.insert(C103); - wtree.remove(C6); - D = clause({~state(skc8,skc9)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C104 = clause({~state(skc8,skc9)}); - wtree.insert(C104); - wtree.remove(C23); - D = clause({of(skc8,skc14,skc15)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C105 = clause({of(skc8,skc14,skc15)}); - wtree.insert(C105); - wtree.remove(C65); - D = clause({of(skc8,skc11,skc10)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C106 = clause({of(skc8,skc11,skc10)}); - wtree.insert(C106); - wtree.remove(C61); - D = clause({~theme(skc8,skc13,skc12)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C107 = clause({~theme(skc8,skc13,skc12)}); - wtree.insert(C107); - wtree.remove(C21); - D = clause({~agent(skc8,skc13,skc15)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C108 = clause({~agent(skc8,skc13,skc15)}); - wtree.insert(C108); - wtree.remove(C80); - D = clause({~be(skc8,skc9,skc10,skc10)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C109 = clause({~be(skc8,skc9,skc10,skc10)}); - wtree.insert(C109); - wtree.remove(C84); - D = clause({~smoke(skc12,skf1(x2))}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C110 = clause({~smoke(skc12,skf1(x2))}); - wtree.insert(C110); - wtree.remove(C58); - D = clause({~man(skc12,x1)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C111 = clause({~man(skc12,x1)}); - wtree.insert(C111); - wtree.remove(C27); - D = clause({forename(skc8,skc11)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - D = clause({forename(skc8,skc14)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - D = clause({~event(skc12,skf1(x1))}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C112 = clause({~event(skc12,skf1(x1))}); - wtree.insert(C112); - D = clause({~event(skc8,skc9)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C113 = clause({~event(skc8,skc9)}); - wtree.insert(C113); - D = clause({~eventuality(skc8,skc13)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C114 = clause({~eventuality(skc8,skc13)}); - wtree.insert(C114); - D = clause({~eventuality(skc8,skc9)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C115 = clause({~eventuality(skc8,skc9)}); - wtree.insert(C115); - D = clause({~present(x1,x2), accessible_world(x3,x1), present(x4,x2), accessible_world(x4,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C116 = clause({~present(x1,x2), accessible_world(x3,x1), present(x4,x2), accessible_world(x4,x3)}); - wtree.insert(C116); - D = clause({~present(x1,skc13), accessible_world(skc8,x1)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C117 = clause({~present(x1,skc13), accessible_world(skc8,x1)}); - wtree.insert(C117); - D = clause({present(x1,x2), accessible_world(x1,x3), ~present(x4,x2), accessible_world(x3,x4)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - D = clause({~jules_forename(x1,x2), accessible_world(x1,x3), forename(x3,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C118 = clause({~jules_forename(x1,x2), accessible_world(x1,x3), forename(x3,x2)}); - wtree.insert(C118); - D = clause({~jules_forename(x1,x2), accessible_world(x1,x3), jules_forename(x4,x2), accessible_world(x3,x4)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C119 = clause({~jules_forename(x1,x2), accessible_world(x1,x3), jules_forename(x4,x2), accessible_world(x3,x4)}); - wtree.insert(C119); - D = clause({jules_forename(x1,x2), accessible_world(x3,x1), ~jules_forename(x4,x2), accessible_world(x4,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - D = clause({jules_forename(x1,skc11), accessible_world(skc8,x1)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C120 = clause({jules_forename(x1,skc11), accessible_world(skc8,x1)}); - wtree.insert(C120); - D = clause({man(x1,x2), accessible_world(x3,x1), ~man(x4,x2), accessible_world(x4,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C121 = clause({man(x1,x2), accessible_world(x3,x1), ~man(x4,x2), accessible_world(x4,x3)}); - wtree.insert(C121); - D = clause({man(x1,skc10), accessible_world(skc8,x1)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C122 = clause({man(x1,skc10), accessible_world(skc8,x1)}); - wtree.insert(C122); - D = clause({man(x1,skc15), accessible_world(skc8,x1)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C123 = clause({man(x1,skc15), accessible_world(skc8,x1)}); - wtree.insert(C123); - D = clause({~man(x1,x2), accessible_world(x1,x3), man(x4,x2), accessible_world(x3,x4)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - D = clause({~man(x1,x2), accessible_world(x1,skc12)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C124 = clause({~man(x1,x2), accessible_world(x1,skc12)}); - wtree.insert(C124); - D = clause({~event(x1,x2), accessible_world(x3,x1), event(x4,x2), accessible_world(x4,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C125 = clause({~event(x1,x2), accessible_world(x3,x1), event(x4,x2), accessible_world(x4,x3)}); - wtree.insert(C125); - D = clause({~event(x1,skc13), accessible_world(skc8,x1)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C126 = clause({~event(x1,skc13), accessible_world(skc8,x1)}); - wtree.insert(C126); - D = clause({event(x1,x2), accessible_world(x1,x3), ~eventuality(x3,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C127 = clause({event(x1,x2), accessible_world(x1,x3), ~eventuality(x3,x2)}); - wtree.insert(C127); - D = clause({event(x1,x2), accessible_world(x1,x3), ~event(x4,x2), accessible_world(x3,x4)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - D = clause({~smoke(x1,x2), accessible_world(x3,x1), smoke(x4,x2), accessible_world(x4,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C128 = clause({~smoke(x1,x2), accessible_world(x3,x1), smoke(x4,x2), accessible_world(x4,x3)}); - wtree.insert(C128); - D = clause({~smoke(x1,skf1(x2)), accessible_world(skc12,x1)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C129 = clause({~smoke(x1,skf1(x2)), accessible_world(skc12,x1)}); - wtree.insert(C129); - D = clause({smoke(x1,x2), accessible_world(x1,x3), ~event(x3,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C130 = clause({smoke(x1,x2), accessible_world(x1,x3), ~event(x3,x2)}); - wtree.insert(C130); - D = clause({smoke(x1,x2), accessible_world(x1,x3), ~smoke(x4,x2), accessible_world(x3,x4)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - D = clause({~state(x1,x2), accessible_world(x3,x1), state(x4,x2), accessible_world(x4,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C131 = clause({~state(x1,x2), accessible_world(x3,x1), state(x4,x2), accessible_world(x4,x3)}); - wtree.insert(C131); - D = clause({~state(x1,skc9), accessible_world(skc8,x1)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C132 = clause({~state(x1,skc9), accessible_world(skc8,x1)}); - wtree.insert(C132); - D = clause({state(x1,x2), accessible_world(x1,x3), ~event(x3,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C133 = clause({state(x1,x2), accessible_world(x1,x3), ~event(x3,x2)}); - wtree.insert(C133); - D = clause({state(x1,x2), accessible_world(x1,x3), ~eventuality(x3,x2)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C134 = clause({state(x1,x2), accessible_world(x1,x3), ~eventuality(x3,x2)}); - wtree.insert(C134); - D = clause({state(x1,x2), accessible_world(x1,x3), ~state(x4,x2), accessible_world(x3,x4)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - D = clause({~proposition(x1,x2), accessible_world(x3,x1), proposition(x4,x2), accessible_world(x4,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C135 = clause({~proposition(x1,x2), accessible_world(x3,x1), proposition(x4,x2), accessible_world(x4,x3)}); - wtree.insert(C135); - D = clause({~proposition(x1,skc12), accessible_world(skc8,x1)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C136 = clause({~proposition(x1,skc12), accessible_world(skc8,x1)}); - wtree.insert(C136); - D = clause({proposition(x1,x2), accessible_world(x1,x3), ~proposition(x4,x2), accessible_world(x3,x4)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - wtree.remove(C113); - D = clause({~event(skc8,skc9)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C137 = clause({~event(skc8,skc9)}); - wtree.insert(C137); - D = clause({think_believe_consider(x1,x2), accessible_world(x1,x3), ~think_believe_consider(x4,x2), accessible_world(x3,x4)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - Kernel::Clause* C138 = clause({think_believe_consider(x1,x2), accessible_world(x1,x3), ~think_believe_consider(x4,x2), accessible_world(x3,x4)}); - wtree.insert(C138); - D = clause({~think_believe_consider(x1,x2), accessible_world(x3,x1), think_believe_consider(x4,x2), accessible_world(x4,x3)}); - m.init(&wtree, D, true); - m.next(resolvedQueryLit); - m.reset(); - - D = clause({~think_believe_consider(x1,x2), accessible_world(x3,x1), think_believe_consider(x4,x2), accessible_world(x4,x3)}); - m.init(&wtree, D, true); - Kernel::Clause* premise; - SATSubsumption::SATSubsumptionAndResolution satSubs; - - //std::ofstream out("test.log"); - //out << "Tree is:" << std::endl; - //out << wtree << std::endl; - - premise = m.next(resolvedQueryLit); - std::cout << resolvedQueryLit << std::endl; - ASS_NEQ(resolvedQueryLit, -1); - ASS(satSubs.checkSubsumptionResolutionWithLiteral(premise, D, resolvedQueryLit)); -} - -TEST_FUN(reproducerMinimized) -{ - MY_SYNTAX_SUGAR - ClauseCodeTree wtree; - - ClauseCodeTree::ClauseMatcher m; - Kernel::Clause* D; - int resolvedQueryLit; - - - Kernel::Clause* C8 = clause({ accessible_world(x1,x2), ~human_person(x2,x3) }); - wtree.insert(C8); - Kernel::Clause* C50 = clause({ accessible_world(x1,x2), ~be(x2,x3,x4,x5) }); - wtree.insert(C50); - Kernel::Clause* C52 = clause({ think_believe_consider(x1,x3), ~think_believe_consider(x2,x3), accessible_world(x1,x2) }); - wtree.insert(C52); - Kernel::Clause* C67 = clause({ accessible_world(x1,x2), proposition(x1,x3) }); - wtree.insert(C67); - Kernel::Clause* C75 = clause({ ~state(x2,x3), accessible_world(x1,x2) }); - wtree.insert(C75); - Kernel::Clause* C130 = clause({ smoke(x1,x2), accessible_world(x1,x3) }); - wtree.insert(C130); - Kernel::Clause* C133 = clause({ accessible_world(x1,x3), ~event(x3,x2) }); - wtree.insert(C133); - Kernel::Clause* C134 = clause({ accessible_world(x1,x3), ~eventuality(x3,x2) }); - wtree.insert(C134); - Kernel::Clause* C138 = clause({ think_believe_consider(x1,x2), accessible_world(x1,x3) }); - wtree.insert(C138); - - std::cout << wtree << std::endl; - - D = clause({~think_believe_consider(x1,x2), accessible_world(x3,x1), think_believe_consider(x4,x2), accessible_world(x4,x3)}); - m.init(&wtree, D, true); - Kernel::Clause* premise; - SATSubsumption::SATSubsumptionAndResolution satSubs; - - //std::ofstream out("test.log"); - //out << "Tree is:" << std::endl; - //out << wtree << std::endl; - - premise = m.next(resolvedQueryLit); - std::cout << resolvedQueryLit << std::endl; - ASS_NEQ(resolvedQueryLit, -1); - ASS(satSubs.checkSubsumptionResolutionWithLiteral(premise, D, resolvedQueryLit)); -} } From e54c4941ddcfccb88deb3ef41618a28ee08d2ae6 Mon Sep 17 00:00:00 2001 From: Synrom Date: Sat, 25 Jul 2026 14:53:55 +0100 Subject: [PATCH 08/15] Some clean ups --- Indexing/ClauseCodeTree.cpp | 1 - ...odeTreeForwardSubsumptionAndResolution.cpp | 1 - Kernel/Clause.cpp | 69 ------------------- Kernel/Clause.hpp | 1 - 4 files changed, 72 deletions(-) diff --git a/Indexing/ClauseCodeTree.cpp b/Indexing/ClauseCodeTree.cpp index 3fbb46987..77534cf0f 100644 --- a/Indexing/ClauseCodeTree.cpp +++ b/Indexing/ClauseCodeTree.cpp @@ -576,7 +576,6 @@ void ClauseCodeTree::ClauseMatcher::reset() template Clause* ClauseCodeTree::ClauseMatcher::next(int& resolvedQueryLit) { - TIME_TRACE("Optimized Clause Matcher next"); if(lms.isEmpty()) { return 0; } diff --git a/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp b/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp index 2e339abcb..c030aba22 100644 --- a/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp +++ b/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp @@ -40,7 +40,6 @@ bool CodeTreeForwardSubsumptionAndResolution::perform(Clause *cl, C Clause* premise; int resolvedQueryLit; - //std::cout << "Execute on " << cl->toReproducerString() << std::endl; while ((premise = cm.next(resolvedQueryLit))) { if (resolvedQueryLit == -1) { ASS(satSubs.checkSubsumption(premise, cl)); diff --git a/Kernel/Clause.cpp b/Kernel/Clause.cpp index 412e256b8..450ca6f68 100644 --- a/Kernel/Clause.cpp +++ b/Kernel/Clause.cpp @@ -14,7 +14,6 @@ * @since 18/05/2007 Manchester */ -#include #include #include "Debug/RuntimeStatistics.hpp" @@ -338,74 +337,6 @@ std::string Clause::toNiceString() const return result; } -std::string Clause::toReproducerString() const -{ - auto literalStringToReproducerString = [](const std::string& input) { - std::string output; - output.reserve(input.size()); - - for (size_t i = 0; i < input.size();) { - const unsigned char ch = static_cast(input[i]); - if (std::isalpha(ch)) { - size_t j = i + 1; - while (j < input.size()) { - const unsigned char c = static_cast(input[j]); - if (!std::isalnum(c) && c != '_') { - break; - } - j++; - } - - const std::string tok = input.substr(i, j - i); - if (tok == "i") { - output += "f2"; - } else if (tok == "a") { - output += "c"; - } else if (tok == "b") { - output += "d"; - } else if (tok == "c") { - output += "e"; - } else if (tok.size() >= 2 && tok[0] == 'X') { - bool allDigits = true; - for (size_t k = 1; k < tok.size(); k++) { - const unsigned char d = static_cast(tok[k]); - if (!std::isdigit(d)) { - allDigits = false; - break; - } - } - if (allDigits) { - output += "x"; - output += Int::toString(std::stoul(tok.substr(1)) + 1); - } else { - output += tok; - } - } else { - output += tok; - } - - i = j; - } else { - output += input[i]; - i++; - } - } - - return output; - }; - - std::string result; - if (size() == 0) { - return "$false"; - } else { - result += literalStringToReproducerString(_literals[0]->toString()); - for (unsigned i = 1; i < size(); i++) { - result += ", "; - result += literalStringToReproducerString(_literals[i]->toString()); - } - } - return result; -} std::ostream& operator<<(std::ostream& out, Clause const& self) { diff --git a/Kernel/Clause.hpp b/Kernel/Clause.hpp index 8917060ba..21dc55adb 100644 --- a/Kernel/Clause.hpp +++ b/Kernel/Clause.hpp @@ -148,7 +148,6 @@ class Clause void destroy(); void destroyExceptInferenceObject(); std::string literalsOnlyToString() const; - std::string toReproducerString() const; std::string toString() const; std::string toTPTPString() const; std::string toNiceString() const; From ab4d2df67b2e5695830605235c8c63e52b382ba2 Mon Sep 17 00:00:00 2001 From: Synrom Date: Sat, 25 Jul 2026 15:02:26 +0100 Subject: [PATCH 09/15] Clean ups --- .gitignore | 4 ---- Kernel/Clause.cpp | 1 - 2 files changed, 5 deletions(-) diff --git a/.gitignore b/.gitignore index f4eb2573a..e51a37e42 100644 --- a/.gitignore +++ b/.gitignore @@ -1,10 +1,6 @@ # ignore common build directories /cmake-build /build -/build** -/profiles -/output -/scripts/__pycache__ /coverage-build # ignore TPTP directories/symlinks at the top level diff --git a/Kernel/Clause.cpp b/Kernel/Clause.cpp index 450ca6f68..441965245 100644 --- a/Kernel/Clause.cpp +++ b/Kernel/Clause.cpp @@ -337,7 +337,6 @@ std::string Clause::toNiceString() const return result; } - std::ostream& operator<<(std::ostream& out, Clause const& self) { if (self.size() == 0) { From 75101d7a1c2af801348ca50a7bc9cdfe09092949 Mon Sep 17 00:00:00 2001 From: Synrom Date: Sun, 16 Aug 2026 21:54:42 +0200 Subject: [PATCH 10/15] Make marked ops more clear and add comments --- Indexing/ClauseCodeTree.cpp | 41 ++++++--------- Indexing/CodeTree.cpp | 29 +++++++++-- Indexing/CodeTree.hpp | 83 +++++++++++++++++------------- Indexing/TermCodeTree.cpp | 2 +- Kernel/FlatTerm.hpp | 2 + Shell/PartialRedundancyHandler.cpp | 4 +- 6 files changed, 91 insertions(+), 70 deletions(-) diff --git a/Indexing/ClauseCodeTree.cpp b/Indexing/ClauseCodeTree.cpp index 77534cf0f..02e77eea6 100644 --- a/Indexing/ClauseCodeTree.cpp +++ b/Indexing/ClauseCodeTree.cpp @@ -300,7 +300,7 @@ template void ClauseCodeTree::RemovingLiteralMatcher::init(CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, ClauseCodeTree* tree_, Stack* firstsInBlocks_) { - Base::init(tree_, entry_, false, linfos_, linfoCnt_, firstsInBlocks_); + Base::init(tree_, entry_, /*canEnterOpposites*/ false, linfos_, linfoCnt_, firstsInBlocks_); ALWAYS(Base::prepareLiteral()); } @@ -393,12 +393,17 @@ bool ClauseCodeTree::LiteralMatcher::next() if(op->isLitEnd()) { recordMatch(); } + + /* Defer opposite matches so that non-opposite matches are always returned first */ if (opposite) { eagerResults.push(op); continue; } + return true; } + + /* No non-opposite matches remain, so fall back to the deferred opposite ones */ if (eagerResults.isNonEmpty()) { op = eagerResults.pop(); _matched = true; @@ -428,6 +433,7 @@ bool ClauseCodeTree::LiteralMatcher::doEagerMatching() if(op->isLitEnd()) { recordMatch(); if (opposite) { + /* push straight to eagerResults so opposite matches end up after all non-opposite ones */ eagerResults.push(op); } else { eagerResultsRevOrder.push(op); @@ -541,13 +547,6 @@ void ClauseCodeTree::ClauseMatcher::init(ClauseCodeTree* tree_, Cla } } if(sres) { - /* - for(unsigned i=0;i::ClauseMatcher::enterLiteral(CodeOp* entry, boo } size_t linfoCnt=lInfos.size(); - /* - if(sres && sresLiteral!=sresNoLiteral) { - ASS_L(sresLiteral,lms.size()); - //we do not need to match index literals with opposite query - //literals, as one of already matched index literals matched only - //to opposite literals (and opposite literals cannot be matched - //on more than one index literal) - ASS_EQ(linfoCnt%2,0); - linfoCnt/=2; - } - */ Recycled lm; lm->init(tree, entry, lInfos.array(), linfoCnt, canEnterOpposites, seekOnlySuccess); @@ -821,6 +809,8 @@ bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQu static DArray matchIndex; matchIndex.ensure(clen); + /* First pass (allowOpposites=false) restricts remaining to non-opposite matches only. + * If that pass fails entirely, we retry allowing opposite matches too. */ bool allowOpposites=false; search_again: remaining.setSide(clen); @@ -838,12 +828,13 @@ bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQu if(matchIndex[i]==remaining.get(i,i)) { //no more choices at this level, so try going up if(i==0) { - RSTAT_MCTR_INC("zero level fails at", failLev); - if(sres && !allowOpposites) { - allowOpposites=true; - goto search_again; - } - return false; + RSTAT_MCTR_INC("zero level fails at", failLev); + if(sres && !allowOpposites) { + /* Non-opposite-only pass failed, retry allowing opposite matches */ + allowOpposites=true; + goto search_again; + } + return false; } i--; goto bind_next_match; diff --git a/Indexing/CodeTree.cpp b/Indexing/CodeTree.cpp index 09afa372b..d2f9a6c78 100644 --- a/Indexing/CodeTree.cpp +++ b/Indexing/CodeTree.cpp @@ -134,7 +134,8 @@ void CodeTree::MatchInfo::destroy(unsigned bindCnt) void CodeTree::MatchInfo::init(ILStruct* ils, unsigned liIndex_, DArray& bindingArray, bool opposite) { - liIndex=opposite ? liIndex_ | leftmost_bit : liIndex_; + /* Pack liIndex and the opposite flag into markedLiIndex (see getLiIndex/opposite) */ + markedLiIndex=opposite ? liIndex_ | leftmost_bit : liIndex_; size_t bindCnt=ils->varCnt; if(bindCnt) { unsigned* perm=ils->globalVarPermutation; @@ -278,6 +279,10 @@ void CodeTree::ILStruct::addMatch(unsigned liIndex, DArray& bindingArr if(!matches[matchCnt]) { matches[matchCnt]=MatchInfo::alloc(varCnt); } + + /* Maintain the invariant that non-opposite matches occupy [0, nonOppositeMatchCnt): + * an opposite match is simply appended, while a non-opposite match is swapped into + * position nonOppositeMatchCnt before that boundary is advanced. */ if(opposite) { matches[matchCnt]->init(this, liIndex, bindingArray, true); } @@ -304,6 +309,7 @@ void CodeTree::ILStruct::deleteMatch(unsigned matchIndex) ASS_L(matchIndex, matchCnt); matchCnt--; + /* Removing a non-opposite match must preserve the [0, nonOppositeMatchCnt) invariant */ if(matchIndexisFun()) { return 0; } switch(kind) { case FN_STRUCT: + /* if opposite is true, look up the negated predicate symbol instead */ if (opposite) { return static_cast(this)->targetOp(ftPos->_number() ^ 1); } @@ -701,8 +708,8 @@ bool CodeTree::Matcher::backtrack() } auto bp=btStack.pop(); tp=bp.tp; - op=unmarkOp(bp.op); - opposite=getMark(bp.op); + op=bp.markedOp.getOp(); + opposite=bp.markedOp.getMark(); if constexpr (removing) { RemovingBase::firstsInBlocks->truncate(bp.fibDepth); RemovingBase::firstsInBlocks->push(op); @@ -807,6 +814,8 @@ inline bool CodeTree::Matcher::doCheckFun() unsigned functor=op->_arg(); FlatTerm::Entry& fte=(*ft)[tp]; if(!fte.isFun(functor)) { + /* the top-level predicate didn't match, so match + * against negation for subsumption resolution */ if (canEnterOpposites && tp == 0 && fte.isOppositeFun(functor)) { opposite=true; } else { @@ -842,6 +851,12 @@ inline bool CodeTree::Matcher::doCheckGroundT return true; } +template +inline typename CodeTree::Matcher::MarkedOp CodeTree::Matcher::markOp(CodeOp *op) +{ + return MarkedOp(op, opposite); +} + template inline bool CodeTree::Matcher::doSearchStruct() { @@ -849,13 +864,17 @@ inline bool CodeTree::Matcher::doSearchStruct const FlatTerm::Entry* fte=&(*ft)[tp]; CodeOp* target=op->getSearchStruct()->getTargetOp(fte, false); + /* look up the branch for the negated predicate, so it + * can be tried on backtracking for subsumption resolution */ if (canEnterOpposites && tp == 0 && op->getSearchStruct()->kind == SearchStruct::FN_STRUCT) { CodeOp* alt = op->getSearchStruct()->getTargetOp(fte, true); if (alt && target != alt) { + /* 'opposite' will be determined by doCheckFun + * when this backtracking point is resumed */ if constexpr (removing) { - btStack.push(BTPointRemoving(tp, markOp(alt, false), RemovingBase::firstsInBlocks->size())); + btStack.push(BTPointRemoving(tp, MarkedOp(alt, false), RemovingBase::firstsInBlocks->size())); } else { - btStack.push(BTPoint(tp, markOp(alt, false))); + btStack.push(BTPoint(tp, MarkedOp(alt, false))); } } } diff --git a/Indexing/CodeTree.hpp b/Indexing/CodeTree.hpp index 66fea76ff..3cf9fed57 100644 --- a/Indexing/CodeTree.hpp +++ b/Indexing/CodeTree.hpp @@ -74,13 +74,15 @@ class CodeTree struct MatchInfo { - unsigned getLiIndex() const { return liIndex & ~leftmost_bit; } - TermList* getBindings() { return &bindings[0]; } - bool opposite() const { return liIndex & leftmost_bit; } + inline unsigned getLiIndex() const { return markedLiIndex & ~leftmost_bit; } + inline TermList* getBindings() { return &bindings[0]; } + inline bool opposite() const { return markedLiIndex & leftmost_bit; } private: - /** Index of the matched LitInfo in the EContext */ - unsigned liIndex; + /** Index of the matched LitInfo in the EContext, with the opposite flag packed + * into the leftmost bit. Use getLiIndex()/opposite() above rather than reading + * this field directly. */ + unsigned markedLiIndex; /** array of bindings */ TermList bindings[1]; @@ -141,6 +143,10 @@ class CodeTree MatchInfo*& getMatch(unsigned matchIndex); unsigned matchCnt; + /** + * non-opposite matches are stored first in [0, nonOppositeMatchCnt) + * opposite matches are stored after in [nonOppositeMatchCnt, matchCnt) + */ unsigned nonOppositeMatchCnt; /** all possible lits were tried to match */ @@ -339,26 +345,48 @@ class CodeTree // removing, which works on variables static_assert(removing || !checkRange); + /** + * A CodeOp* tagged in its lowest bit with the 'opposite' flag + */ + class MarkedOp + { + static_assert(alignof(CodeOp) >= 2, "CodeOp must be at least 2-byte aligned so its lowest bit is free for the mark"); + CodeOp* raw; + public: + MarkedOp(CodeOp* op, bool mark) : + raw(reinterpret_cast(reinterpret_cast(op) | mark)) {} + + inline bool getMark() const { + return (reinterpret_cast(raw) & 1u) != 0; + } + + inline CodeOp* getOp() const { + return reinterpret_cast( + reinterpret_cast(raw) & ~std::uintptr_t{1} + ); + } + }; + /** * Backtracking point for the interpretation of the code tree. */ struct BTPoint { - BTPoint(size_t tp, CodeOp* op) : tp(tp), op(op) {} + BTPoint(size_t tp, MarkedOp markedOp) : tp(tp), markedOp(markedOp) {} /** Position in the flat term */ size_t tp; - /** Pointer to the next operation */ - CodeOp* op; + /** Pointer to the next operation and mark encoding whether this is an opposite branch */ + MarkedOp markedOp; }; struct BTPointRemoving { - BTPointRemoving(size_t tp, CodeOp* op, size_t fibDepth) - : tp(tp), op(op), fibDepth(fibDepth) {} + BTPointRemoving(size_t tp, MarkedOp markedOp, size_t fibDepth) + : tp(tp), markedOp(markedOp), fibDepth(fibDepth) {} size_t tp; - CodeOp* op; + MarkedOp markedOp; size_t fibDepth; }; @@ -399,32 +427,7 @@ class CodeTree bool doCheckFun(); bool doCheckGroundTerm(); bool doSearchStruct(); - - inline CodeOp* markOp(CodeOp* op) const - { - return reinterpret_cast( - reinterpret_cast(op) | opposite - ); - } - - inline CodeOp* markOp(CodeOp* op, bool value) const - { - return reinterpret_cast( - reinterpret_cast(op) | value - ); - } - - inline bool getMark(CodeOp* op) const - { - return (reinterpret_cast(op) & 1u) != 0; - } - - inline CodeOp* unmarkOp(CodeOp* op) const - { - return reinterpret_cast( - reinterpret_cast(op) & ~std::uintptr_t{1} - ); - } + MarkedOp markOp(CodeOp*); /** * Position in the flat term @@ -451,7 +454,13 @@ class CodeTree CodeOp* entry; CodeTree* tree; + /** Whether the current execution branch matched via the opposite (negated) predicate */ bool opposite; + + /** + * Whether this matcher is allowed to match a query literal against its opposite. + * False for e.g. RemovingLiteralMatcher, where subsumption resolution does not apply. + */ bool canEnterOpposites; /** diff --git a/Indexing/TermCodeTree.cpp b/Indexing/TermCodeTree.cpp index a191c9e71..da4d859ba 100644 --- a/Indexing/TermCodeTree.cpp +++ b/Indexing/TermCodeTree.cpp @@ -107,7 +107,7 @@ template void TermCodeTree::RemovingTermMatcher::init(FlatTerm* ft_, TermCodeTree* tree_, Stack* firstsInBlocks_) { - Base::init(tree_, tree_->getEntryPoint(), false, /*linfos_=*/0, /*linfoCnt_=*/0, firstsInBlocks_); + Base::init(tree_, tree_->getEntryPoint(), /*canEnterOpposites_=*/false, /*linfos_=*/0, /*linfoCnt_=*/0, firstsInBlocks_); Base::firstsInBlocks->push(Base::entry); diff --git a/Kernel/FlatTerm.hpp b/Kernel/FlatTerm.hpp index d2688ce97..eaeb8e9eb 100644 --- a/Kernel/FlatTerm.hpp +++ b/Kernel/FlatTerm.hpp @@ -61,6 +61,8 @@ class FlatTerm inline bool isVar(unsigned num) const { return isVar() && _number()==num; } inline bool isFun() const { return _tag()==FUN || _tag()==FUN_UNEXPANDED; } inline bool isFun(unsigned num) const { return isFun() && _number()==num; } + /* Litearl headers encode polarity in their lowest bit, so xor-ing with 1 + * gives the opposite (negated) predicate. Only meaningful for literal predicates. */ inline bool isOppositeFun(unsigned num) const { return isFun() && (_number()^1)==num; } /** * Should be called when @b isFun() is true. diff --git a/Shell/PartialRedundancyHandler.cpp b/Shell/PartialRedundancyHandler.cpp index 89f578460..282835ae8 100644 --- a/Shell/PartialRedundancyHandler.cpp +++ b/Shell/PartialRedundancyHandler.cpp @@ -250,7 +250,7 @@ class PartialRedundancyHandler::ConstraintIndex { void init(CodeTree* tree, const TermStack& ts) { - Matcher::init(tree,tree->getEntryPoint(), false); + Matcher::init(tree,tree->getEntryPoint(), /*canEnterOpposites_=*/false); ft = FlatTerm::create(ts); @@ -285,7 +285,7 @@ class PartialRedundancyHandler::ConstraintIndex { public: void init(FlatTerm* ft_, CodeTree* tree_, Stack* firstsInBlocks_) { - Matcher::init(tree_, tree_->getEntryPoint(), false, 0, 0, firstsInBlocks_); + Matcher::init(tree_, tree_->getEntryPoint(), /*canEnterOpposites_=*/false, 0, 0, firstsInBlocks_); ft=ft_; tp=0; op=entry; From f286e8e2d486c5c9c6e5d8227d18643a0e909bd8 Mon Sep 17 00:00:00 2001 From: Synrom Date: Tue, 25 Aug 2026 13:14:05 +0200 Subject: [PATCH 11/15] Integrate PR feedback --- Indexing/ClauseCodeTree.cpp | 3 +-- Indexing/CodeTree.cpp | 22 ++++++++++--------- Indexing/CodeTree.hpp | 43 ++++++++++++++++++++----------------- Kernel/FlatTerm.hpp | 2 +- 4 files changed, 37 insertions(+), 33 deletions(-) diff --git a/Indexing/ClauseCodeTree.cpp b/Indexing/ClauseCodeTree.cpp index 4ae9d44e9..ee986a939 100644 --- a/Indexing/ClauseCodeTree.cpp +++ b/Indexing/ClauseCodeTree.cpp @@ -476,7 +476,6 @@ void ClauseCodeTree::LiteralMatcher::recordMatch() return; } if(!ils->matchCnt && opposite) { - //if we're matching opposite matches, we have already tried all non-opposite ones ils->noNonOppositeMatches=true; } else if (ils->noNonOppositeMatches && !opposite) { ils->noNonOppositeMatches=false; @@ -619,7 +618,7 @@ Clause* ClauseCodeTree::ClauseMatcher::next(int& resolvedQueryLit) } bool seekOnlySuccess=lms.size()==query->length(); - bool canEnterOpposites=sres && sresLiteral == sresNoLiteral; + bool canEnterOpposites=sres && (sresLiteral == sresNoLiteral); enterLiteral(newLitEntry, seekOnlySuccess, canEnterOpposites); } } diff --git a/Indexing/CodeTree.cpp b/Indexing/CodeTree.cpp index 03af3bbae..049edcd7f 100644 --- a/Indexing/CodeTree.cpp +++ b/Indexing/CodeTree.cpp @@ -134,8 +134,9 @@ void CodeTree::MatchInfo::destroy(unsigned bindCnt) void CodeTree::MatchInfo::init(ILStruct* ils, unsigned liIndex_, DArray& bindingArray, bool opposite) { - /* Pack liIndex and the opposite flag into markedLiIndex (see getLiIndex/opposite) */ - markedLiIndex=opposite ? liIndex_ | leftmost_bit : liIndex_; + /* Pack liIndex and the opposite flag into _content (see getLiIndex/opposite) */ + _setLiIndex(liIndex_); + _setOpposite(opposite); size_t bindCnt=ils->varCnt; if(bindCnt) { unsigned* perm=ils->globalVarPermutation; @@ -284,13 +285,13 @@ void CodeTree::ILStruct::addMatch(unsigned liIndex, DArray& bindingArr * an opposite match is simply appended, while a non-opposite match is swapped into * position nonOppositeMatchCnt before that boundary is advanced. */ if(opposite) { - matches[matchCnt]->init(this, liIndex, bindingArray, true); + matches[matchCnt]->init(this, liIndex, bindingArray, /*opposite=*/true); } else { if(nonOppositeMatchCnt!=matchCnt) { swap(matches[nonOppositeMatchCnt], matches[matchCnt]); } - matches[nonOppositeMatchCnt]->init(this, liIndex, bindingArray, false); + matches[nonOppositeMatchCnt]->init(this, liIndex, bindingArray, /*opposite=*/false); nonOppositeMatchCnt++; } matchCnt++; @@ -587,11 +588,12 @@ bool CodeTree::Matcher::execute() bool shouldBacktrack=false; for(;;) { + /* Note: doSearchStruct() also pushes onto btStack to handle opposite matches */ if(op->alternative()) { if constexpr (removing) { - btStack.push(BTPointRemoving(tp, markOp(op->alternative()), RemovingBase::firstsInBlocks->size())); + btStack.push(BTPointRemoving(tp, MarkedOp(op->alternative(), opposite), RemovingBase::firstsInBlocks->size())); } else { - btStack.push(BTPoint(tp, markOp(op->alternative()))); + btStack.push(BTPoint(tp, MarkedOp(op->alternative(), opposite))); } } switch(op->_instruction()) { @@ -863,18 +865,18 @@ inline bool CodeTree::Matcher::doSearchStruct ASS_EQ(op->_instruction(), SEARCH_STRUCT); const FlatTerm::Entry* fte=&(*ft)[tp]; - CodeOp* target=op->getSearchStruct()->getTargetOp(fte, false); + CodeOp* target=op->getSearchStruct()->getTargetOp(fte, /*opposite=*/false); /* look up the branch for the negated predicate, so it * can be tried on backtracking for subsumption resolution */ if (canEnterOpposites && tp == 0 && op->getSearchStruct()->kind == SearchStruct::FN_STRUCT) { - CodeOp* alt = op->getSearchStruct()->getTargetOp(fte, true); + CodeOp* alt = op->getSearchStruct()->getTargetOp(fte, /*opposite=*/true); if (alt && target != alt) { /* 'opposite' will be determined by doCheckFun * when this backtracking point is resumed */ if constexpr (removing) { - btStack.push(BTPointRemoving(tp, MarkedOp(alt, false), RemovingBase::firstsInBlocks->size())); + btStack.emplace(tp, MarkedOp(alt, /*opposite=*/false), RemovingBase::firstsInBlocks->size()); } else { - btStack.push(BTPoint(tp, MarkedOp(alt, false))); + btStack.emplace(tp, MarkedOp(alt, /*opposite=*/false)); } } } diff --git a/Indexing/CodeTree.hpp b/Indexing/CodeTree.hpp index a79db7142..9a8642c03 100644 --- a/Indexing/CodeTree.hpp +++ b/Indexing/CodeTree.hpp @@ -18,6 +18,7 @@ #include "Forwards.hpp" #include "Lib/Allocator.hpp" +#include "Lib/BitUtils.hpp" #include "Lib/DArray.hpp" #include "Lib/DHMap.hpp" #include "Lib/Stack.hpp" @@ -74,20 +75,22 @@ class CodeTree struct MatchInfo { - inline unsigned getLiIndex() const { return markedLiIndex & ~leftmost_bit; } + inline unsigned getLiIndex() const { return _liIndex(); } inline TermList* getBindings() { return &bindings[0]; } - inline bool opposite() const { return markedLiIndex & leftmost_bit; } + inline bool opposite() const { return _opposite(); } private: + BITFIELD(64, + BITFIELD_MEMBER(bool, _opposite, _setOpposite, 1, + BITFIELD_MEMBER(unsigned, _liIndex, _setLiIndex, CHAR_BIT * sizeof(unsigned) - 1, + END_BITFIELD + ))) /** Index of the matched LitInfo in the EContext, with the opposite flag packed - * into the leftmost bit. Use getLiIndex()/opposite() above rather than reading - * this field directly. */ - unsigned markedLiIndex; + * in alongside it. */ + uint64_t _content = 0; /** array of bindings */ TermList bindings[1]; - static constexpr unsigned int leftmost_bit = 1u << (sizeof(unsigned int) * CHAR_BIT - 1); - void init(ILStruct* ils, unsigned liIndex, DArray& bindingArray, bool opposite); static MatchInfo* alloc(unsigned bindCnt); @@ -351,20 +354,20 @@ class CodeTree class MarkedOp { static_assert(alignof(CodeOp) >= 2, "CodeOp must be at least 2-byte aligned so its lowest bit is free for the mark"); - CodeOp* raw; public: - MarkedOp(CodeOp* op, bool mark) : - raw(reinterpret_cast(reinterpret_cast(op) | mark)) {} - - inline bool getMark() const { - return (reinterpret_cast(raw) & 1u) != 0; - } - - inline CodeOp* getOp() const { - return reinterpret_cast( - reinterpret_cast(raw) & ~std::uintptr_t{1} - ); - } + MarkedOp(CodeOp* op, bool mark) { _setOp(op); _setMark(mark); } + + BITFIELD(64, + BITFIELD_MEMBER(bool, getMark, _setMark, 1, + END_BITFIELD + )) + static_assert(sizeof(void *) <= sizeof(uint64_t), "must be able to fit a pointer into a 64-bit integer"); + BITFIELD_PTR_GET(CodeOp, getOp, 1) + BITFIELD_PTR_SET(CodeOp, _setOp, 1) + + private: + // bitfield + uint64_t _content = 0; }; /** diff --git a/Kernel/FlatTerm.hpp b/Kernel/FlatTerm.hpp index eaeb8e9eb..2010c0cfc 100644 --- a/Kernel/FlatTerm.hpp +++ b/Kernel/FlatTerm.hpp @@ -61,7 +61,7 @@ class FlatTerm inline bool isVar(unsigned num) const { return isVar() && _number()==num; } inline bool isFun() const { return _tag()==FUN || _tag()==FUN_UNEXPANDED; } inline bool isFun(unsigned num) const { return isFun() && _number()==num; } - /* Litearl headers encode polarity in their lowest bit, so xor-ing with 1 + /* Literal headers encode polarity in their lowest bit, so xor-ing with 1 * gives the opposite (negated) predicate. Only meaningful for literal predicates. */ inline bool isOppositeFun(unsigned num) const { return isFun() && (_number()^1)==num; } /** From 2fff4bb1ca77e9e700769c13915f65e6ec7cf046 Mon Sep 17 00:00:00 2001 From: Synrom Date: Tue, 25 Aug 2026 14:38:28 +0200 Subject: [PATCH 12/15] Add GROUND_TERM_CHECK=1 guard and FlatTerm unit test --- Indexing/CodeTree.cpp | 7 ++++++ UnitTests/tFlatTerm.cpp | 53 +++++++++++++++++++++++++++++++++++++++++ cmake/sources.cmake | 1 + 3 files changed, 61 insertions(+) create mode 100644 UnitTests/tFlatTerm.cpp diff --git a/Indexing/CodeTree.cpp b/Indexing/CodeTree.cpp index 049edcd7f..0379679f4 100644 --- a/Indexing/CodeTree.cpp +++ b/Indexing/CodeTree.cpp @@ -39,6 +39,7 @@ #define RED "" #endif +// If re-enabled, see the ASSERTION_VIOLATION in Matcher::init: opposite-literal matching doesn't support it yet. #define GROUND_TERM_CHECK 0 #undef RSTAT_COLLECTION @@ -674,6 +675,12 @@ void CodeTree::Matcher::init(const CodeTree& { tree=&tree_; canEnterOpposites=canEnterOpposites_; +#if GROUND_TERM_CHECK + if (canEnterOpposites) { + // TODO: GROUND_TERM_CHECK is currently incompatible with opposite matching + ASSERTION_VIOLATION; + } +#endif entry=entry_; opposite=false; diff --git a/UnitTests/tFlatTerm.cpp b/UnitTests/tFlatTerm.cpp new file mode 100644 index 000000000..2918818a6 --- /dev/null +++ b/UnitTests/tFlatTerm.cpp @@ -0,0 +1,53 @@ +/* + * This file is part of the source code of the software program + * Vampire. It is protected by applicable + * copyright laws. + * + * This source code is distributed under the licence found here + * https://vprover.github.io/license.html + * and in the source directory + */ + +#include "Test/UnitTesting.hpp" +#include "Test/SyntaxSugar.hpp" +#include "Kernel/FlatTerm.hpp" + +using namespace Kernel; + +/** + * FlatTerm::Entry::isOppositeFun relies on the fact that xor-ing a literal + * header with 1 gives the header of the complementary literal (see + * Literal::header/complementaryHeader in Kernel/Term.hpp). This test checks + * that relationship holds for the header actually stored in a FlatTerm built + * from a literal. + */ +TEST_FUN(isOppositeFun_matches_complementaryHeader) { + DECL_DEFAULT_VARS + DECL_SORT(srt) + DECL_CONST(a, srt) + DECL_PRED(p, {srt}) + DECL_PRED(q, {srt}) + + Literal* lit1 = p(a); + Literal* lit2 = q(a); + + FlatTerm* ft1 = FlatTerm::create(TermList(lit1)); + FlatTerm* ft2 = FlatTerm::create(TermList(lit2)); + + ASS((*ft1)[0].isOppositeFun(lit1->complementaryHeader())) + ASS(!(*ft1)[0].isOppositeFun(lit1->header())) + ASS((*ft1)[0].isFun(lit1->header())) + ASS(!(*ft1)[0].isFun(lit1->complementaryHeader())) + ASS(!(*ft1)[0].isOppositeFun(lit2->header())) + ASS(!(*ft1)[0].isOppositeFun(lit2->complementaryHeader())) + + ASS((*ft2)[0].isOppositeFun(lit2->complementaryHeader())) + ASS(!(*ft2)[0].isOppositeFun(lit2->header())) + ASS((*ft2)[0].isFun(lit2->header())) + ASS(!(*ft2)[0].isFun(lit2->complementaryHeader())) + ASS(!(*ft2)[0].isOppositeFun(lit1->header())) + ASS(!(*ft2)[0].isOppositeFun(lit1->complementaryHeader())) + + ft1->destroy(); + ft2->destroy(); +} diff --git a/cmake/sources.cmake b/cmake/sources.cmake index ef6438d31..06a0ddf2f 100644 --- a/cmake/sources.cmake +++ b/cmake/sources.cmake @@ -50,6 +50,7 @@ set(UNIT_TESTS UnitTests/tDeque.cpp UnitTests/tDisagreement.cpp UnitTests/tDynamicHeap.cpp + UnitTests/tFlatTerm.cpp UnitTests/tFunctionDefinitionHandler.cpp UnitTests/tHash.cpp UnitTests/tIndexManager.cpp From d5c713023d6b6bcb70ff9d925d5aecca1071a0cb Mon Sep 17 00:00:00 2001 From: Synrom Date: Wed, 9 Sep 2026 11:59:29 +0200 Subject: [PATCH 13/15] Integrate PR feedback --- Indexing/CodeTree.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/Indexing/CodeTree.cpp b/Indexing/CodeTree.cpp index 0379679f4..07e9fa753 100644 --- a/Indexing/CodeTree.cpp +++ b/Indexing/CodeTree.cpp @@ -676,10 +676,7 @@ void CodeTree::Matcher::init(const CodeTree& tree=&tree_; canEnterOpposites=canEnterOpposites_; #if GROUND_TERM_CHECK - if (canEnterOpposites) { - // TODO: GROUND_TERM_CHECK is currently incompatible with opposite matching - ASSERTION_VIOLATION; - } + ASS(!canEnterOpposites); #endif entry=entry_; opposite=false; From e145ceb8e2d049c05d66e49cadebb1b1f99885cf Mon Sep 17 00:00:00 2001 From: Synrom Date: Wed, 9 Sep 2026 14:31:14 +0200 Subject: [PATCH 14/15] Make sres a template variable --- Indexing/ClauseCodeTree.cpp | 148 +++++++++++------- Indexing/ClauseCodeTree.hpp | 19 ++- Indexing/CodeTree.cpp | 131 +++++++++------- Indexing/CodeTree.hpp | 53 +++++-- Indexing/TermCodeTree.hpp | 8 +- ...odeTreeForwardSubsumptionAndResolution.cpp | 15 +- ...odeTreeForwardSubsumptionAndResolution.hpp | 5 + Shell/PartialRedundancyHandler.cpp | 4 +- Shell/PredicateElimination.cpp | 4 +- 9 files changed, 242 insertions(+), 145 deletions(-) diff --git a/Indexing/ClauseCodeTree.cpp b/Indexing/ClauseCodeTree.cpp index ee986a939..3ebe14111 100644 --- a/Indexing/ClauseCodeTree.cpp +++ b/Indexing/ClauseCodeTree.cpp @@ -336,7 +336,8 @@ bool ClauseCodeTree::removeOneOfAlternatives(CodeOp* op, Clause* cl * and fail if there isn't any at the beginning (possibly also among alternatives). */ template -void ClauseCodeTree::LiteralMatcher::init(const CodeTree& tree_, CodeOp* entry_, +template +void ClauseCodeTree::LiteralMatcher::init(const CodeTree& tree_, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, bool canEnterOpposites, bool seekOnlySuccess) { @@ -372,7 +373,8 @@ void ClauseCodeTree::LiteralMatcher::init(const CodeTree& tree_, Co * Try to find a match, and if one is found, return true */ template -bool ClauseCodeTree::LiteralMatcher::next() +template +bool ClauseCodeTree::LiteralMatcher::next() { if(eagerlyMatched()) { _matched = eagerResults.isNonEmpty(); @@ -416,7 +418,8 @@ bool ClauseCodeTree::LiteralMatcher::next() * Perform eager matching and return true iff new matches were found */ template -bool ClauseCodeTree::LiteralMatcher::doEagerMatching() +template +bool ClauseCodeTree::LiteralMatcher::doEagerMatching() { ASS(!eagerlyMatched()); //eager matching can be done only once ASS(!finished()); @@ -465,7 +468,8 @@ bool ClauseCodeTree::LiteralMatcher::doEagerMatching() } template -void ClauseCodeTree::LiteralMatcher::recordMatch() +template +void ClauseCodeTree::LiteralMatcher::recordMatch() { ASS(_matched); @@ -475,12 +479,14 @@ void ClauseCodeTree::LiteralMatcher::recordMatch() //no need to record matches which we already know will not lead to anything return; } - if(!ils->matchCnt && opposite) { - ils->noNonOppositeMatches=true; - } else if (ils->noNonOppositeMatches && !opposite) { - ils->noNonOppositeMatches=false; + if constexpr (sres) { + if(!ils->matchCnt && opposite) { + ils->noNonOppositeMatches=true; + } else if (ils->noNonOppositeMatches && !opposite) { + ils->noNonOppositeMatches=false; + } } - ils->addMatch(Base::linfos[Base::curLInfo].liIndex, Base::bindings, opposite); + ils->template addMatch(Base::linfos[Base::curLInfo].liIndex, Base::bindings, opposite); } @@ -489,16 +495,16 @@ void ClauseCodeTree::LiteralMatcher::recordMatch() /** * Initialize the ClauseMatcher to retrieve generalizetions * of the @b query_ clause. - * If @b sres_ if true, we perform subsumption resolution + * If @b sres if true, we perform subsumption resolution */ template -void ClauseCodeTree::ClauseMatcher::init(ClauseCodeTree* tree_, Clause* query_, bool sres_) +template +void ClauseCodeTree::ClauseMatcher::init(ClauseCodeTree* tree_, Clause* query_) { ASS(!tree_->isEmpty()); query=query_; tree=tree_; - sres=sres_; lms.reset(); #if VDEBUG @@ -545,7 +551,7 @@ void ClauseCodeTree::ClauseMatcher::init(ClauseCodeTree* tree_, Cla liIndex++; } } - if(sres) { + if constexpr (sres) { sresLiteral=sresNoLiteral; } @@ -554,7 +560,8 @@ void ClauseCodeTree::ClauseMatcher::init(ClauseCodeTree* tree_, Cla } template -void ClauseCodeTree::ClauseMatcher::reset() +template +void ClauseCodeTree::ClauseMatcher::reset() { unsigned liCnt=lInfos.size(); for(unsigned i=0;i::ClauseMatcher::reset() * Return next clause matching query or 0 if there is not such */ template -Clause* ClauseCodeTree::ClauseMatcher::next(int& resolvedQueryLit) +template +Clause* ClauseCodeTree::ClauseMatcher::next(int& resolvedQueryLit) { if(lms.isEmpty()) { return 0; } for(;;) { - LiteralMatcher* lm = &*lms.top(); + LiteralMatcher* lm = &*lms.top(); //get next literal from the literal matcher bool found=lm->next(); @@ -607,25 +615,30 @@ Clause* ClauseCodeTree::ClauseMatcher::next(int& resolvedQueryLit) //so we can increase here CodeOp* newLitEntry=lm->op+1; - //check that we have cleared the sresLiteral value if it is no longer valid - ASS(!sres || sresLiteral==sresNoLiteral || sresLiteralgetILS()->noNonOppositeMatches) { - sresLiteral=lms.size()-1; - } + if constexpr (sres) { + //check that we have cleared the sresLiteral value if it is no longer valid + ASS(sresLiteral==sresNoLiteral || sresLiteralgetILS()->noNonOppositeMatches) { + sresLiteral=lms.size()-1; + } + } + canEnterOpposites = (sresLiteral == sresNoLiteral); } bool seekOnlySuccess=lms.size()==query->length(); - bool canEnterOpposites=sres && (sresLiteral == sresNoLiteral); enterLiteral(newLitEntry, seekOnlySuccess, canEnterOpposites); } } } template -inline bool ClauseCodeTree::ClauseMatcher::canEnterLiteral(CodeOp* op) +template +inline bool ClauseCodeTree::ClauseMatcher::canEnterLiteral(CodeOp* op) { ASS(op->isLitEnd()); ASS_EQ(lms.top()->op, op); @@ -654,7 +667,7 @@ inline bool ClauseCodeTree::ClauseMatcher::canEnterLiteral(CodeOp* matchIndex--; MatchInfo* mi=ils->getMatch(matchIndex); if(!existsCompatibleMatch(ils, mi, prevILS)) { - ils->deleteMatch(matchIndex); //decreases ils->matchCnt + ils->template deleteMatch(matchIndex); //decreases ils->matchCnt } } if(!ils->matchCnt) { @@ -675,14 +688,15 @@ inline bool ClauseCodeTree::ClauseMatcher::canEnterLiteral(CodeOp* * to see just clauses that end at this point). */ template -void ClauseCodeTree::ClauseMatcher::enterLiteral(CodeOp* entry, bool seekOnlySuccess, bool canEnterOpposites) +template +void ClauseCodeTree::ClauseMatcher::enterLiteral(CodeOp* entry, bool seekOnlySuccess, bool canEnterOpposites) { if(!seekOnlySuccess) { RSTAT_MCTR_INC("enterLiteral levels (non-sos)", lms.size()); } if(lms.isNonEmpty()) { - Recycled& prevLM = lms.top(); + Recycled, NoReset>& prevLM = lms.top(); ILStruct* ils=prevLM->op->getILS(); ASS_EQ(ils->timestamp,tree->_curTimeStamp); ASS(!ils->visited); @@ -692,27 +706,28 @@ void ClauseCodeTree::ClauseMatcher::enterLiteral(CodeOp* entry, boo size_t linfoCnt=lInfos.size(); - Recycled lm; + Recycled, NoReset> lm; lm->init(*tree, entry, lInfos.array(), linfoCnt, canEnterOpposites, seekOnlySuccess); lms.push(std::move(lm)); } template -void ClauseCodeTree::ClauseMatcher::leaveLiteral() +template +void ClauseCodeTree::ClauseMatcher::leaveLiteral() { ASS(lms.isNonEmpty()); lms.pop(); if(lms.isNonEmpty()) { - LiteralMatcher* prevLM = &*lms.top(); + LiteralMatcher* prevLM = &*lms.top(); ILStruct* ils=prevLM->op->getILS(); ASS_EQ(ils->timestamp,tree->_curTimeStamp); ASS(ils->visited); ils->finished=true; - if(sres) { + if constexpr (sres) { //clear the resolved literal flag if we have backtracked from it unsigned depth=lms.size()-1; if(sresLiteral==depth) { @@ -727,7 +742,8 @@ void ClauseCodeTree::ClauseMatcher::leaveLiteral() //////////////// Multi-literal matching template -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 @@ -738,18 +754,20 @@ bool ClauseCodeTree::ClauseMatcher::checkCandidate(Clause* cl, int& //if clause doesn't have multiple literals, there is no need //for multi-literal matching resolvedQueryLit=-1; - if(sres && clen==1) { - size_t matchCnt=lms[0]->getILS()->matchCnt; - for(size_t i=0;igetILS()->getMatch(i); - if(mi->opposite()) { - resolvedQueryLit=lInfos[mi->getLiIndex()].litIndex; - } - else { - //we prefer subsumption to subsumption resolution - resolvedQueryLit=-1; - break; - } + if constexpr (sres) { + if (clen==1) { + size_t matchCnt=lms[0]->getILS()->matchCnt; + for(size_t i=0;igetILS()->getMatch(i); + if(mi->opposite()) { + resolvedQueryLit=lInfos[mi->getLiIndex()].litIndex; + } + else { + //we prefer subsumption to subsumption resolution + resolvedQueryLit=-1; + break; + } + } } } return true; @@ -761,7 +779,7 @@ bool ClauseCodeTree::ClauseMatcher::checkCandidate(Clause* cl, int& bool newMatches=false; for(int i=clen-1;i>=0;i--) { - LiteralMatcher* lm = &*lms[i]; + LiteralMatcher* lm = &*lms[i]; if(lm->eagerlyMatched()) { break; } @@ -783,7 +801,8 @@ bool ClauseCodeTree::ClauseMatcher::checkCandidate(Clause* cl, int& } template -bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQueryLit) +template +bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQueryLit) { //TODO: perform _set_, not _multiset_ subsumption for subsumption resolution @@ -815,7 +834,13 @@ bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQu remaining.setSide(clen); for(unsigned j=0;jgetILS(); - remaining.set(j,0,allowOpposites ? ils->matchCnt : ils->nonOppositeMatchCnt); + unsigned matchesToTry = ils->matchCnt; + if constexpr (sres) { + if (!allowOpposites) { + matchesToTry = ils->nonOppositeMatchCnt; + } + } + remaining.set(j,0,matchesToTry); } unsigned failLev=0; @@ -828,10 +853,12 @@ bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQu //no more choices at this level, so try going up if(i==0) { RSTAT_MCTR_INC("zero level fails at", failLev); - if(sres && !allowOpposites) { - /* Non-opposite-only pass failed, retry allowing opposite matches */ - allowOpposites=true; - goto search_again; + if constexpr (sres) { + if(!allowOpposites) { + /* Non-opposite-only pass failed, retry allowing opposite matches */ + allowOpposites=true; + goto search_again; + } } return false; } @@ -866,7 +893,7 @@ bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQu } resolvedQueryLit=-1; - if(sres) { + if constexpr (sres) { for(unsigned i=0;igetILS(); MatchInfo* mi=ils->getMatch(matchIndex[i]); @@ -881,7 +908,8 @@ bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQu } template -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->getLiIndex()].litIndex==lInfos[nq->getLiIndex()].litIndex || (bq->opposite() && nq->opposite()) ) { @@ -927,7 +955,8 @@ bool ClauseCodeTree::ClauseMatcher::compatible(ILStruct* bi, MatchI } template -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::ClauseMatcher::existsCompatibleMatch(ILStruct* template class ClauseCodeTree; template class ClauseCodeTree; +template struct ClauseCodeTree::LiteralMatcher; +template struct ClauseCodeTree::LiteralMatcher; +template struct ClauseCodeTree::LiteralMatcher; +template struct ClauseCodeTree::LiteralMatcher; +template struct ClauseCodeTree::ClauseMatcher; +template struct ClauseCodeTree::ClauseMatcher; +template struct ClauseCodeTree::ClauseMatcher; +template struct ClauseCodeTree::ClauseMatcher; + } diff --git a/Indexing/ClauseCodeTree.hpp b/Indexing/ClauseCodeTree.hpp index 5a16bde8a..47ba3fb3e 100644 --- a/Indexing/ClauseCodeTree.hpp +++ b/Indexing/ClauseCodeTree.hpp @@ -57,9 +57,9 @@ class ClauseCodeTree : public CodeTree bool removeOneOfAlternatives(CodeOp* op, Clause* cl, Stack* firstsInBlocks); struct RemovingLiteralMatcher - : public Matcher + : public Matcher { - using Base = Matcher; + using Base = Matcher; void init(CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, const ClauseCodeTree& tree_, Stack* firstsInBlocks_); @@ -71,11 +71,14 @@ class ClauseCodeTree : public CodeTree /** Context for finding matches of literals * - * Here the actual execution of the code of the tree takes place */ + * Here the actual execution of the code of the tree takes place + * sres selects between subsumption+resolution (true) and subsumption-only (false) + * */ + template struct LiteralMatcher - : public Matcher + : public Matcher { - using Base = Matcher; + using Base = Matcher; using Base::op; using Base::_matched; using Base::finished; @@ -101,9 +104,10 @@ class ClauseCodeTree : public CodeTree }; public: + template struct ClauseMatcher { - void init(ClauseCodeTree* tree_, Clause* query_, bool sres_); + void init(ClauseCodeTree* tree_, Clause* query_); void reset(); bool keepRecycled() const { return lInfos.keepRecycled(); } @@ -127,7 +131,6 @@ class ClauseCodeTree : public CodeTree Clause* query; ClauseCodeTree* tree; - bool sres; static const unsigned sresNoLiteral=static_cast(-1); unsigned sresLiteral; @@ -144,7 +147,7 @@ class ClauseCodeTree : public CodeTree */ DArray lInfos; - Stack> lms; + Stack, NoReset>> lms; }; private: diff --git a/Indexing/CodeTree.cpp b/Indexing/CodeTree.cpp index 07e9fa753..ea0a7f8b3 100644 --- a/Indexing/CodeTree.cpp +++ b/Indexing/CodeTree.cpp @@ -268,8 +268,10 @@ void CodeTree::ILStruct::ensureFreshness(unsigned globalTimestamp) } } +template void CodeTree::ILStruct::addMatch(unsigned liIndex, DArray& bindingArray, bool opposite) { + ASS(sres || !opposite); if(matchCnt==matches.size()) { matches.expand(matchCnt ? (matchCnt*2) : 4); size_t newSize=matches.size(); @@ -282,18 +284,22 @@ void CodeTree::ILStruct::addMatch(unsigned liIndex, DArray& bindingArr matches[matchCnt]=MatchInfo::alloc(varCnt); } - /* Maintain the invariant that non-opposite matches occupy [0, nonOppositeMatchCnt): - * an opposite match is simply appended, while a non-opposite match is swapped into - * position nonOppositeMatchCnt before that boundary is advanced. */ - if(opposite) { - matches[matchCnt]->init(this, liIndex, bindingArray, /*opposite=*/true); - } - else { - if(nonOppositeMatchCnt!=matchCnt) { - swap(matches[nonOppositeMatchCnt], matches[matchCnt]); + if constexpr (sres) { + /* Maintain the invariant that non-opposite matches occupy [0, nonOppositeMatchCnt): + * an opposite match is simply appended, while a non-opposite match is swapped into + * position nonOppositeMatchCnt before that boundary is advanced. */ + if(opposite) { + matches[matchCnt]->init(this, liIndex, bindingArray, /*opposite=*/true); + } + else { + if(nonOppositeMatchCnt!=matchCnt) { + swap(matches[nonOppositeMatchCnt], matches[matchCnt]); + } + matches[nonOppositeMatchCnt]->init(this, liIndex, bindingArray, /*opposite=*/false); + nonOppositeMatchCnt++; } - matches[nonOppositeMatchCnt]->init(this, liIndex, bindingArray, /*opposite=*/false); - nonOppositeMatchCnt++; + } else { + matches[matchCnt]->init(this, liIndex, bindingArray, /*opposite=*/false); } matchCnt++; } @@ -306,24 +312,34 @@ void CodeTree::ILStruct::addMatch(unsigned liIndex, DArray& bindingArr * to filter them by this function, the traversal should go from higher * indexes down to zero. */ +template void CodeTree::ILStruct::deleteMatch(unsigned matchIndex) { ASS_L(matchIndex, matchCnt); matchCnt--; - /* Removing a non-opposite match must preserve the [0, nonOppositeMatchCnt) invariant */ - if(matchIndex(unsigned, DArray&, bool); +template void CodeTree::ILStruct::addMatch(unsigned, DArray&, bool); +template void CodeTree::ILStruct::deleteMatch(unsigned); +template void CodeTree::ILStruct::deleteMatch(unsigned); + CodeTree::MatchInfo*& CodeTree::ILStruct::getMatch(unsigned matchIndex) { ASS(!finished); @@ -574,8 +590,8 @@ CodeTree::CodeOp*& CodeTree::SearchStructImpl::targetOp(const T& val) //////////////// Matcher //////////////////// -template -bool CodeTree::Matcher::execute() +template +bool CodeTree::Matcher::execute() { if(fresh) { fresh=false; @@ -670,8 +686,8 @@ bool CodeTree::Matcher::execute() } } -template -void CodeTree::Matcher::init(const CodeTree& tree_, CodeOp* entry_, bool canEnterOpposites_, LitInfo* linfos_, size_t linfoCnt_, Stack* firstsInBlocks_) +template +void CodeTree::Matcher::init(const CodeTree& tree_, CodeOp* entry_, bool canEnterOpposites_, LitInfo* linfos_, size_t linfoCnt_, Stack* firstsInBlocks_) { tree=&tree_; canEnterOpposites=canEnterOpposites_; @@ -705,8 +721,8 @@ void CodeTree::Matcher::init(const CodeTree& * 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++; @@ -723,8 +739,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); @@ -739,8 +755,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); @@ -780,8 +796,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); @@ -812,8 +828,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); @@ -822,6 +838,9 @@ inline bool CodeTree::Matcher::doCheckFun() if(!fte.isFun(functor)) { /* the top-level predicate didn't match, so match * against negation for subsumption resolution */ + if constexpr (!sres) { + return false; + } if (canEnterOpposites && tp == 0 && fte.isOppositeFun(functor)) { opposite=true; } else { @@ -833,8 +852,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); @@ -857,14 +876,8 @@ inline bool CodeTree::Matcher::doCheckGroundT return true; } -template -inline typename CodeTree::Matcher::MarkedOp CodeTree::Matcher::markOp(CodeOp *op) -{ - return MarkedOp(op, opposite); -} - -template -inline bool CodeTree::Matcher::doSearchStruct() +template +inline bool CodeTree::Matcher::doSearchStruct() { ASS_EQ(op->_instruction(), SEARCH_STRUCT); @@ -872,15 +885,17 @@ inline bool CodeTree::Matcher::doSearchStruct CodeOp* target=op->getSearchStruct()->getTargetOp(fte, /*opposite=*/false); /* look up the branch for the negated predicate, so it * can be tried on backtracking for subsumption resolution */ - if (canEnterOpposites && tp == 0 && op->getSearchStruct()->kind == SearchStruct::FN_STRUCT) { - CodeOp* alt = op->getSearchStruct()->getTargetOp(fte, /*opposite=*/true); - if (alt && target != alt) { - /* 'opposite' will be determined by doCheckFun - * when this backtracking point is resumed */ - if constexpr (removing) { - btStack.emplace(tp, MarkedOp(alt, /*opposite=*/false), RemovingBase::firstsInBlocks->size()); - } else { - btStack.emplace(tp, MarkedOp(alt, /*opposite=*/false)); + if constexpr (sres) { + if (canEnterOpposites && tp == 0 && op->getSearchStruct()->kind == SearchStruct::FN_STRUCT) { + CodeOp* alt = op->getSearchStruct()->getTargetOp(fte, /*opposite=*/true); + if (alt && target != alt) { + /* 'opposite' will be determined by doCheckFun + * when this backtracking point is resumed */ + if constexpr (removing) { + btStack.emplace(tp, MarkedOp(alt, /*opposite=*/false), RemovingBase::firstsInBlocks->size()); + } else { + btStack.emplace(tp, MarkedOp(alt, /*opposite=*/false)); + } } } } @@ -894,11 +909,13 @@ 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; +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 9a8642c03..b8ff08187 100644 --- a/Indexing/CodeTree.hpp +++ b/Indexing/CodeTree.hpp @@ -139,10 +139,11 @@ class CodeTree unsigned* globalVarPermutation; unsigned timestamp; - //from here on, the values are valid only if the timestamp is current - void addMatch(unsigned liIndex, DArray& bindingArray, bool opposite); - void deleteMatch(unsigned matchIndex); + //from here on, the values are valid only if the timestamp is current + /** boolean template sres variable indicates whether this ILStruct supports subsumption resolution */ + template void addMatch(unsigned liIndex, DArray& bindingArray, bool opposite); + template void deleteMatch(unsigned matchIndex); MatchInfo*& getMatch(unsigned matchIndex); unsigned matchCnt; @@ -340,7 +341,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 { @@ -350,24 +351,46 @@ class CodeTree /** * A CodeOp* tagged in its lowest bit with the 'opposite' flag + * When sres is false, it becomes a plain CodeOp* */ class MarkedOp { - static_assert(alignof(CodeOp) >= 2, "CodeOp must be at least 2-byte aligned so its lowest bit is free for the mark"); + using Content = typename std::conditional::type; public: - MarkedOp(CodeOp* op, bool mark) { _setOp(op); _setMark(mark); } + MarkedOp(CodeOp* op, bool mark) + { + if constexpr (sres) { + static_assert(alignof(CodeOp) >= 2, "CodeOp must be at least 2-byte aligned so its lowest bit is free for the mark"); + static_assert(sizeof(void *) <= sizeof(uint64_t), "must be able to fit a pointer into a 64-bit integer"); + _content = 0; + BitUtils::setBits<1, CHAR_BIT * sizeof(CodeOp*)>(_content, reinterpret_cast(op)); + BitUtils::setBits<0, 1>(_content, mark); + } else { + ASS(!mark); + _content = op; + } + } - BITFIELD(64, - BITFIELD_MEMBER(bool, getMark, _setMark, 1, - END_BITFIELD - )) - static_assert(sizeof(void *) <= sizeof(uint64_t), "must be able to fit a pointer into a 64-bit integer"); - BITFIELD_PTR_GET(CodeOp, getOp, 1) - BITFIELD_PTR_SET(CodeOp, _setOp, 1) + CodeOp* getOp() const + { + if constexpr (sres) { + return reinterpret_cast(BitUtils::getBits<1, CHAR_BIT * sizeof(CodeOp*)>(_content)); + } else { + return _content; + } + } + + bool getMark() const + { + if constexpr (sres) { + return BitUtils::getBits<0, 1>(_content); + } else { + return false; + } + } private: - // bitfield - uint64_t _content = 0; + Content _content = 0; }; /** diff --git a/Indexing/TermCodeTree.hpp b/Indexing/TermCodeTree.hpp index 5590ae709..2731f0ef9 100644 --- a/Indexing/TermCodeTree.hpp +++ b/Indexing/TermCodeTree.hpp @@ -45,21 +45,21 @@ class TermCodeTree : public CodeTree private: struct RemovingTermMatcher - : public Matcher + : public Matcher { public: - using Base = Matcher; + using Base = Matcher; void init(FlatTerm* ft_, const TermCodeTree& tree_, Stack* firstsInBlocks_); }; public: struct TermMatcher - : public Matcher + : public Matcher { TermMatcher(); - using Base = Matcher; + using Base = Matcher; using Base::ft; void init(const CodeTree& tree, TypedTermList t); diff --git a/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp b/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp index 98f1973c1..28a5f1b15 100644 --- a/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp +++ b/Inferences/CodeTreeForwardSubsumptionAndResolution.cpp @@ -30,6 +30,17 @@ CodeTreeForwardSubsumptionAndResolution::CodeTreeForwardSubsumption template bool CodeTreeForwardSubsumptionAndResolution::perform(Clause *cl, Clause *&replacement, ClauseIterator &premises) +{ + if (_subsumptionResolution) { + return performWith(cl, replacement, premises); + } else { + return performWith(cl, replacement, premises); + } +} + +template +template +bool CodeTreeForwardSubsumptionAndResolution::performWith(Clause *cl, Clause *&replacement, ClauseIterator &premises) { if (_ct->isEmpty()) { return false; @@ -41,9 +52,9 @@ bool CodeTreeForwardSubsumptionAndResolution::perform(Clause *cl, C constexpr double RSI_SKIP_PROB = 0.02; bool rsi = env.options->randomizedSimplifications(); - static typename ClauseCodeTree::ClauseMatcher cm; + static typename ClauseCodeTree::template ClauseMatcher cm; - cm.init(_ct, cl, _subsumptionResolution); + cm.init(_ct, cl); Clause* premise; int resolvedQueryLit; diff --git a/Inferences/CodeTreeForwardSubsumptionAndResolution.hpp b/Inferences/CodeTreeForwardSubsumptionAndResolution.hpp index 5a3048937..0d303594f 100644 --- a/Inferences/CodeTreeForwardSubsumptionAndResolution.hpp +++ b/Inferences/CodeTreeForwardSubsumptionAndResolution.hpp @@ -35,6 +35,11 @@ class CodeTreeForwardSubsumptionAndResolution Kernel::ClauseIterator &premises) override; private: + template + bool performWith(Kernel::Clause *cl, + Kernel::Clause *&replacement, + Kernel::ClauseIterator &premises); + const bool _subsumptionResolution; std::shared_ptr> _index; Indexing::ClauseCodeTree* _ct; diff --git a/Shell/PartialRedundancyHandler.cpp b/Shell/PartialRedundancyHandler.cpp index d47dc0df5..2543ac0d0 100644 --- a/Shell/PartialRedundancyHandler.cpp +++ b/Shell/PartialRedundancyHandler.cpp @@ -246,7 +246,7 @@ class PartialRedundancyHandler::ConstraintIndex struct SubstMatcher // TODO(HOL): consider turning higherOrder flag off for HOL - : public Matcher + : public Matcher { void init(const CodeTree& tree, const TermStack& ts) { @@ -281,7 +281,7 @@ class PartialRedundancyHandler::ConstraintIndex }; struct VariantMatcher - : public Matcher + : public Matcher { public: void init(FlatTerm* ft_, const CodeTree& tree_, Stack* firstsInBlocks_) { diff --git a/Shell/PredicateElimination.cpp b/Shell/PredicateElimination.cpp index 807af245b..1ed1a1f8b 100644 --- a/Shell/PredicateElimination.cpp +++ b/Shell/PredicateElimination.cpp @@ -733,8 +733,8 @@ bool PredicateElimination::forwardSubsumedOrResolved(Clause *cl, Clause *&replac return false; } - static ClauseCodeTree::ClauseMatcher cm; - cm.init(&_ct, cl, /*sres=*/true); + static ClauseCodeTree::ClauseMatcher cm; + cm.init(&_ct, cl); bool subsumed = false; Clause *premise; From 7f7a3f54830b285e86c6381e0bddce55bb6695cf Mon Sep 17 00:00:00 2001 From: Synrom Date: Wed, 9 Sep 2026 14:40:48 +0200 Subject: [PATCH 15/15] Remove Matcher::markOp --- Indexing/CodeTree.hpp | 1 - 1 file changed, 1 deletion(-) diff --git a/Indexing/CodeTree.hpp b/Indexing/CodeTree.hpp index b8ff08187..973934bf4 100644 --- a/Indexing/CodeTree.hpp +++ b/Indexing/CodeTree.hpp @@ -453,7 +453,6 @@ class CodeTree bool doCheckFun(); bool doCheckGroundTerm(); bool doSearchStruct(); - MarkedOp markOp(CodeOp*); /** * Position in the flat term