diff --git a/Indexing/ClauseCodeTree.cpp b/Indexing/ClauseCodeTree.cpp index d0f8c689f..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_, linfos_, linfoCnt_, firstsInBlocks_); + Base::init(tree_, entry_, /*canEnterOpposites*/ false, linfos_, linfoCnt_, firstsInBlocks_); ALWAYS(Base::prepareLiteral()); } @@ -338,11 +338,11 @@ 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(); @@ -375,8 +375,8 @@ template bool ClauseCodeTree::LiteralMatcher::next() { if(eagerlyMatched()) { - _matched=!eagerResults.isEmpty(); - if(!_matched) { + _matched = eagerResults.isNonEmpty(); + if (!_matched) { return false; } op=eagerResults.pop(); @@ -388,16 +388,28 @@ bool ClauseCodeTree::LiteralMatcher::next() return false; } - _matched=execute(); - if(!_matched) { - return false; + while ((_matched = execute())) { + ASS(op->isLitEnd() || op->isSuccess()); + if(op->isLitEnd()) { + recordMatch(); + } + + /* Defer opposite matches so that non-opposite matches are always returned first */ + if (opposite) { + eagerResults.push(op); + continue; + } + + return true; } - ASS(op->isLitEnd() || op->isSuccess()); - if(op->isLitEnd()) { - recordMatch(); + /* No non-opposite matches remain, so fall back to the deferred opposite ones */ + if (eagerResults.isNonEmpty()) { + op = eagerResults.pop(); + _matched = true; + return true; } - return true; + return false; } /** @@ -407,7 +419,6 @@ template bool ClauseCodeTree::LiteralMatcher::doEagerMatching() { ASS(!eagerlyMatched()); //eager matching can be done only once - ASS(eagerResults.isEmpty()); ASS(!finished()); //backup the current op @@ -421,7 +432,12 @@ bool ClauseCodeTree::LiteralMatcher::doEagerMatching() while(execute()) { if(op->isLitEnd()) { recordMatch(); - eagerResultsRevOrder.push(op); + if (opposite) { + /* push straight to eagerResults so opposite matches end up after all non-opposite ones */ + eagerResults.push(op); + } else { + eagerResultsRevOrder.push(op); + } } else { ASS(op->isSuccess()); @@ -459,11 +475,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 +515,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 +547,11 @@ 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 @@ -606,7 +619,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 +676,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,18 +692,9 @@ 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 - //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, seekOnlySuccess); + lm->init(tree, entry, lInfos.array(), linfoCnt, canEnterOpposites, seekOnlySuccess); lms.push(std::move(lm)); } @@ -738,8 +743,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 @@ -796,29 +801,24 @@ 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); + + /* 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); 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 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); - 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; @@ -866,8 +871,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 +884,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..a6a42179a 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(); @@ -114,7 +115,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..d2f9a6c78 100644 --- a/Indexing/CodeTree.cpp +++ b/Indexing/CodeTree.cpp @@ -132,9 +132,10 @@ 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_; + /* 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; @@ -261,10 +262,11 @@ void CodeTree::ILStruct::ensureFreshness(unsigned globalTimestamp) finished=false; noNonOppositeMatches=false; matchCnt=0; + nonOppositeMatchCnt=0; } } -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 +279,20 @@ void CodeTree::ILStruct::addMatch(unsigned liIndex, DArray& bindingArr if(!matches[matchCnt]) { matches[matchCnt]=MatchInfo::alloc(varCnt); } - matches[matchCnt]->init(this, liIndex, bindingArray); + + /* 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); + } + else { + if(nonOppositeMatchCnt!=matchCnt) { + swap(matches[nonOppositeMatchCnt], matches[matchCnt]); + } + matches[nonOppositeMatchCnt]->init(this, liIndex, bindingArray, false); + nonOppositeMatchCnt++; + } matchCnt++; } @@ -294,7 +309,17 @@ void CodeTree::ILStruct::deleteMatch(unsigned matchIndex) ASS_L(matchIndex, matchCnt); matchCnt--; - swap(matches[matchIndex], matches[matchCnt]); + /* Removing a non-opposite match must preserve the [0, nonOppositeMatchCnt) invariant */ + if(matchIndex(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 is true, look up the negated predicate symbol instead */ + 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: @@ -559,9 +589,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 +668,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 +708,8 @@ bool CodeTree::Matcher::backtrack() } auto bp=btStack.pop(); tp=bp.tp; - op=bp.op; + op=bp.markedOp.getOp(); + opposite=bp.markedOp.getMark(); if constexpr (removing) { RemovingBase::firstsInBlocks->truncate(bp.fibDepth); RemovingBase::firstsInBlocks->push(op); @@ -696,6 +729,7 @@ bool CodeTree::Matcher::prepareLiteral() ft=linfos[curLInfo].ft; tp=0; op=entry; + opposite=false; return true; } @@ -780,7 +814,13 @@ inline bool CodeTree::Matcher::doCheckFun() unsigned functor=op->_arg(); FlatTerm::Entry& fte=(*ft)[tp]; if(!fte.isFun(functor)) { - return false; + /* the top-level predicate didn't match, so match + * against negation for subsumption resolution */ + if (canEnterOpposites && tp == 0 && fte.isOppositeFun(functor)) { + opposite=true; + } else { + return false; + } } fte.expand(); tp+=FlatTerm::FUNCTION_ENTRY_COUNT; @@ -811,13 +851,33 @@ 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() { 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); + /* 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, MarkedOp(alt, false), RemovingBase::firstsInBlocks->size())); + } else { + btStack.push(BTPoint(tp, MarkedOp(alt, false))); + } + } + } if(!target) { return false; } diff --git a/Indexing/CodeTree.hpp b/Indexing/CodeTree.hpp index 7184abfff..3cf9fed57 100644 --- a/Indexing/CodeTree.hpp +++ b/Indexing/CodeTree.hpp @@ -74,13 +74,21 @@ class CodeTree struct MatchInfo { - /** Index of the matched LitInfo in the EContext */ - unsigned liIndex; + 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, 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]; - 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,11 +138,16 @@ 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); 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 */ bool visited; @@ -255,7 +268,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 @@ -332,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; }; @@ -382,7 +417,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(); @@ -392,6 +427,7 @@ class CodeTree bool doCheckFun(); bool doCheckGroundTerm(); bool doSearchStruct(); + MarkedOp markOp(CodeOp*); /** * Position in the flat term @@ -418,6 +454,15 @@ 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; + /** * Array of alternative LitInfo objects * diff --git a/Indexing/TermCodeTree.cpp b/Indexing/TermCodeTree.cpp index 4d82cd42c..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(), /*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 8afa86b12..eaeb8e9eb 100644 --- a/Kernel/FlatTerm.hpp +++ b/Kernel/FlatTerm.hpp @@ -61,6 +61,9 @@ 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. * If @b tag()==FUN_UNEXPANDED, it fills out entries for the functions diff --git a/Shell/PartialRedundancyHandler.cpp b/Shell/PartialRedundancyHandler.cpp index 772539e36..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()); + 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(), 0, 0, firstsInBlocks_); + Matcher::init(tree_, tree_->getEntryPoint(), /*canEnterOpposites_=*/false, 0, 0, firstsInBlocks_); ft=ft_; tp=0; op=entry; 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) }) }) +) + }