Skip to content

Higher order code trees #833

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
mezpusz wants to merge 8 commits into
base: master
Choose a base branch
from
Open

Higher order code trees #833

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
c315ca8
Refactor fresh variable handling in primitive instantiation; add unit…
mezpusz Mar 25, 2026
196da67
Basic adaption of code trees for higher-order matching by not binding…
mezpusz Mar 25, 2026
e16d95e
Fix some errors
mezpusz Mar 25, 2026
fb3c402
Add HOL sampler
mezpusz Mar 26, 2026
f4f70df
Add assertion about synced higher-order options to saturation initial…
mezpusz Mar 26, 2026
4c8d594
Adapt subsumption demodulation
mezpusz Mar 26, 2026
948dc74
Merge branch 'master' into higher-order-code-tree
mezpusz Mar 26, 2026
bbedbb5
Add todo to potentially lift HO restriction in Twee goal transformation
mezpusz Mar 27, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
99 changes: 63 additions & 36 deletions Indexing/ClauseCodeTree.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,14 +36,16 @@ using namespace std;
using namespace Lib;
using namespace Kernel;

void ClauseCodeTree::onCodeOpDestroying(CodeOp* op)
template<bool higherOrder>
void ClauseCodeTree<higherOrder>::onCodeOpDestroying(CodeOp* op)
{
if (op->isLitEnd()) {
delete op->getILS();
}
}

ClauseCodeTree::ClauseCodeTree()
template<bool higherOrder>
ClauseCodeTree<higherOrder>::ClauseCodeTree()
{
_clauseCodeTree=true;
_onCodeOpDestroying = onCodeOpDestroying;
Expand All @@ -54,7 +56,8 @@ ClauseCodeTree::ClauseCodeTree()

//////////////// insertion ////////////////////

void ClauseCodeTree::insert(Clause* cl)
template<bool higherOrder>
void ClauseCodeTree<higherOrder>::insert(Clause* cl)
{
unsigned clen=cl->length();
static DArray<Literal*> lits;
Expand All @@ -77,7 +80,8 @@ void ClauseCodeTree::insert(Clause* cl)
ASS(code.isEmpty());
}

struct ClauseCodeTree::InitialLiteralOrderingComparator
template<bool higherOrder>
struct ClauseCodeTree<higherOrder>::InitialLiteralOrderingComparator
{
Comparison compare(Literal* l1, Literal* l2)
{
Expand All @@ -88,7 +92,8 @@ struct ClauseCodeTree::InitialLiteralOrderingComparator
}
};

void ClauseCodeTree::optimizeLiteralOrder(DArray<Literal*>& lits)
template<bool higherOrder>
void ClauseCodeTree<higherOrder>::optimizeLiteralOrder(DArray<Literal*>& lits)
{
unsigned clen=lits.size();
if(isEmpty() || clen<=1) {
Expand Down Expand Up @@ -139,7 +144,8 @@ void ClauseCodeTree::optimizeLiteralOrder(DArray<Literal*>& lits)
}
}

void ClauseCodeTree::evalSharing(Literal* lit, CodeOp* startOp, size_t& sharedLen, size_t& unsharedLen, CodeOp*& nextOp)
template<bool higherOrder>
void ClauseCodeTree<higherOrder>::evalSharing(Literal* lit, CodeOp* startOp, size_t& sharedLen, size_t& unsharedLen, CodeOp*& nextOp)
{
CodeStack code;
LitCompiler compiler(code);
Expand All @@ -163,7 +169,8 @@ void ClauseCodeTree::evalSharing(Literal* lit, CodeOp* startOp, size_t& sharedLe
* it is the first operation on which mismatch occurred and there was no alternative to
* proceed to (in this case it therefore holds that @b lastAttemptedOp->alternative==0 ).
*/
void ClauseCodeTree::matchCode(CodeStack& code, CodeOp* startOp, size_t& matchedCnt, CodeOp*& nextOp)
template<bool higherOrder>
void ClauseCodeTree<higherOrder>::matchCode(CodeStack& code, CodeOp* startOp, size_t& matchedCnt, CodeOp*& nextOp)
{
size_t clen=code.length();
CodeOp* treeOp=startOp;
Expand Down Expand Up @@ -207,7 +214,8 @@ void ClauseCodeTree::matchCode(CodeStack& code, CodeOp* startOp, size_t& matched

//////////////// removal ////////////////////

void ClauseCodeTree::remove(Clause* cl)
template<bool higherOrder>
void ClauseCodeTree<higherOrder>::remove(Clause* cl)
{
static DArray<LitInfo> lInfos;
Recycled<Stack<CodeOp*>> firstsInBlocks;
Expand Down Expand Up @@ -283,19 +291,21 @@ void ClauseCodeTree::remove(Clause* cl)
}
}

void ClauseCodeTree::RemovingLiteralMatcher::init(CodeOp* entry_, LitInfo* linfos_,
template<bool higherOrder>
void ClauseCodeTree<higherOrder>::RemovingLiteralMatcher::init(CodeOp* entry_, LitInfo* linfos_,
size_t linfoCnt_, ClauseCodeTree* tree_, Stack<CodeOp*>* firstsInBlocks_)
{
Matcher::init(tree_, entry_, linfos_, linfoCnt_, firstsInBlocks_);
Base::init(tree_, entry_, linfos_, linfoCnt_, firstsInBlocks_);

ALWAYS(prepareLiteral());
ALWAYS(Base::prepareLiteral());
}

/**
* The first operation of the CodeBlock containing @b op
* must already be on the @b firstsInBlocks stack.
*/
bool ClauseCodeTree::removeOneOfAlternatives(CodeOp* op, Clause* cl, Stack<CodeOp*>* firstsInBlocks)
template<bool higherOrder>
bool ClauseCodeTree<higherOrder>::removeOneOfAlternatives(CodeOp* op, Clause* cl, Stack<CodeOp*>* firstsInBlocks)
{
unsigned initDepth=firstsInBlocks->size();

Expand All @@ -320,13 +330,14 @@ bool ClauseCodeTree::removeOneOfAlternatives(CodeOp* op, Clause* cl, Stack<CodeO
* If @b seekOnlySuccess if true, we will look only for immediate SUCCESS operations
* and fail if there isn't any at the beginning (possibly also among alternatives).
*/
void ClauseCodeTree::LiteralMatcher::init(CodeTree* tree_, CodeOp* entry_,
template<bool higherOrder>
void ClauseCodeTree<higherOrder>::LiteralMatcher::init(CodeTree* tree_, CodeOp* entry_,
LitInfo* linfos_, size_t linfoCnt_,
bool seekOnlySuccess)
{
ASS_G(linfoCnt_,0);

Matcher::init(tree_,entry_,linfos_,linfoCnt_);
Base::init(tree_,entry_,linfos_,linfoCnt_);

_eagerlyMatched=false;
eagerResults.reset();
Expand All @@ -338,24 +349,25 @@ void ClauseCodeTree::LiteralMatcher::init(CodeTree* tree_, CodeOp* entry_,
//(and those must be at the entry point or its alternatives)

_eagerlyMatched=true;
fresh=false;
CodeOp* sop=entry;
Base::fresh=false;
CodeOp* sop=Base::entry;
while(sop) {
if(sop->isSuccess()) {
eagerResults.push(sop);
eagerResults.push(sop);
}
sop=sop->alternative();
}
return;
}

ALWAYS(prepareLiteral());
ALWAYS(Base::prepareLiteral());
}

/**
* Try to find a match, and if one is found, return true
*/
bool ClauseCodeTree::LiteralMatcher::next()
template<bool higherOrder>
bool ClauseCodeTree<higherOrder>::LiteralMatcher::next()
{
if(eagerlyMatched()) {
_matched=!eagerResults.isEmpty();
Expand Down Expand Up @@ -386,7 +398,8 @@ bool ClauseCodeTree::LiteralMatcher::next()
/**
* Perform eager matching and return true iff new matches were found
*/
bool ClauseCodeTree::LiteralMatcher::doEagerMatching()
template<bool higherOrder>
bool ClauseCodeTree<higherOrder>::LiteralMatcher::doEagerMatching()
{
ASS(!eagerlyMatched()); //eager matching can be done only once
ASS(eagerResults.isEmpty());
Expand Down Expand Up @@ -430,21 +443,22 @@ bool ClauseCodeTree::LiteralMatcher::doEagerMatching()
return eagerResults.isNonEmpty();
}

void ClauseCodeTree::LiteralMatcher::recordMatch()
template<bool higherOrder>
void ClauseCodeTree<higherOrder>::LiteralMatcher::recordMatch()
{
ASS(matched());
ASS(_matched);

ILStruct* ils=op->getILS();
ils->ensureFreshness(tree->_curTimeStamp);
ils->ensureFreshness(Base::tree->_curTimeStamp);
if(ils->finished) {
//no need to record matches which we already know will not lead to anything
return;
}
if(!ils->matchCnt && linfos[curLInfo].opposite) {
if(!ils->matchCnt && Base::linfos[Base::curLInfo].opposite) {
//if we're matching opposite matches, we have already tried all non-opposite ones
ils->noNonOppositeMatches=true;
}
ils->addMatch(linfos[curLInfo].liIndex, bindings);
ils->addMatch(Base::linfos[Base::curLInfo].liIndex, Base::bindings);
}


Expand All @@ -455,7 +469,8 @@ void ClauseCodeTree::LiteralMatcher::recordMatch()
* of the @b query_ clause.
* If @b sres_ if true, we perform subsumption resolution
*/
void ClauseCodeTree::ClauseMatcher::init(ClauseCodeTree* tree_, Clause* query_, bool sres_)
template<bool higherOrder>
void ClauseCodeTree<higherOrder>::ClauseMatcher::init(ClauseCodeTree* tree_, Clause* query_, bool sres_)
{
ASS(!tree_->isEmpty());

Expand Down Expand Up @@ -521,7 +536,8 @@ void ClauseCodeTree::ClauseMatcher::init(ClauseCodeTree* tree_, Clause* query_,
enterLiteral(tree->getEntryPoint(), clen==0);
}

void ClauseCodeTree::ClauseMatcher::reset()
template<bool higherOrder>
void ClauseCodeTree<higherOrder>::ClauseMatcher::reset()
{
unsigned liCnt=lInfos.size();
for(unsigned i=0;i<liCnt;i++) {
Expand All @@ -538,7 +554,8 @@ void ClauseCodeTree::ClauseMatcher::reset()
/**
* Return next clause matching query or 0 if there is not such
*/
Clause* ClauseCodeTree::ClauseMatcher::next(int& resolvedQueryLit)
template<bool higherOrder>
Clause* ClauseCodeTree<higherOrder>::ClauseMatcher::next(int& resolvedQueryLit)
{
if(lms.isEmpty()) {
return 0;
Expand All @@ -558,7 +575,7 @@ Clause* ClauseCodeTree::ClauseMatcher::next(int& resolvedQueryLit)
}
}
else if(lm->op->isSuccess()) {
Clause* candidate=lm->op->getSuccessResult<Clause>();
Clause* candidate=lm->op->template getSuccessResult<Clause>();
RSTAT_MCTR_INC("candidates", lms.size()-1);
if(checkCandidate(candidate, resolvedQueryLit)) {
RSTAT_MCTR_INC("candidates (success)", lms.size()-1);
Expand Down Expand Up @@ -589,7 +606,8 @@ Clause* ClauseCodeTree::ClauseMatcher::next(int& resolvedQueryLit)
}
}

inline bool ClauseCodeTree::ClauseMatcher::canEnterLiteral(CodeOp* op)
template<bool higherOrder>
inline bool ClauseCodeTree<higherOrder>::ClauseMatcher::canEnterLiteral(CodeOp* op)
{
ASS(op->isLitEnd());
ASS_EQ(lms.top()->op, op);
Expand Down Expand Up @@ -638,7 +656,8 @@ inline bool ClauseCodeTree::ClauseMatcher::canEnterLiteral(CodeOp* op)
* (this is to be used when all literals are matched so we want
* to see just clauses that end at this point).
*/
void ClauseCodeTree::ClauseMatcher::enterLiteral(CodeOp* entry, bool seekOnlySuccess)
template<bool higherOrder>
void ClauseCodeTree<higherOrder>::ClauseMatcher::enterLiteral(CodeOp* entry, bool seekOnlySuccess)
{
if(!seekOnlySuccess) {
RSTAT_MCTR_INC("enterLiteral levels (non-sos)", lms.size());
Expand Down Expand Up @@ -669,7 +688,8 @@ void ClauseCodeTree::ClauseMatcher::enterLiteral(CodeOp* entry, bool seekOnlySuc
lms.push(std::move(lm));
}

void ClauseCodeTree::ClauseMatcher::leaveLiteral()
template<bool higherOrder>
void ClauseCodeTree<higherOrder>::ClauseMatcher::leaveLiteral()
{
ASS(lms.isNonEmpty());

Expand Down Expand Up @@ -697,7 +717,8 @@ void ClauseCodeTree::ClauseMatcher::leaveLiteral()

//////////////// Multi-literal matching

bool ClauseCodeTree::ClauseMatcher::checkCandidate(Clause* cl, int& resolvedQueryLit)
template<bool higherOrder>
bool ClauseCodeTree<higherOrder>::ClauseMatcher::checkCandidate(Clause* cl, int& resolvedQueryLit)
{
unsigned clen=cl->length();
//the last matcher in mls is the one that yielded the SUCCESS operation
Expand Down Expand Up @@ -752,7 +773,8 @@ bool ClauseCodeTree::ClauseMatcher::checkCandidate(Clause* cl, int& resolvedQuer
// return newMatches && matchGlobalVars(resolvedQueryLit);
}

bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQueryLit)
template<bool higherOrder>
bool ClauseCodeTree<higherOrder>::ClauseMatcher::matchGlobalVars(int& resolvedQueryLit)
{
//TODO: perform _set_, not _multiset_ subsumption for subsumption resolution

Expand Down Expand Up @@ -849,7 +871,8 @@ bool ClauseCodeTree::ClauseMatcher::matchGlobalVars(int& resolvedQueryLit)
return true;
}

bool ClauseCodeTree::ClauseMatcher::compatible(ILStruct* bi, MatchInfo* bq, ILStruct* ni, MatchInfo* nq)
template<bool higherOrder>
bool ClauseCodeTree<higherOrder>::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) ) {
Expand Down Expand Up @@ -894,7 +917,8 @@ bool ClauseCodeTree::ClauseMatcher::compatible(ILStruct* bi, MatchInfo* bq, ILSt
return true;
}

bool ClauseCodeTree::ClauseMatcher::existsCompatibleMatch(ILStruct* si, MatchInfo* sq, ILStruct* targets)
template<bool higherOrder>
bool ClauseCodeTree<higherOrder>::ClauseMatcher::existsCompatibleMatch(ILStruct* si, MatchInfo* sq, ILStruct* targets)
{
size_t tcnt=targets->matchCnt;
for(size_t i=0;i<tcnt;i++) {
Expand All @@ -905,4 +929,7 @@ bool ClauseCodeTree::ClauseMatcher::existsCompatibleMatch(ILStruct* si, MatchInf
return false;
}

template class ClauseCodeTree<false>;
template class ClauseCodeTree<true>;

}
15 changes: 12 additions & 3 deletions Indexing/ClauseCodeTree.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ namespace Indexing {
using namespace Lib;
using namespace Kernel;

template<bool higherOrder>
class ClauseCodeTree : public CodeTree
{
protected:
Expand All @@ -55,8 +56,10 @@ class ClauseCodeTree : public CodeTree
bool removeOneOfAlternatives(CodeOp* op, Clause* cl, Stack<CodeOp*>* firstsInBlocks);

struct RemovingLiteralMatcher
: public Matcher</*removing*/true,false>
: public Matcher</*removing*/true,false,higherOrder>
{
using Base = Matcher</*removing*/true,false,higherOrder>;

void init(CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_,
ClauseCodeTree* tree_, Stack<CodeOp*>* firstsInBlocks_);

Expand All @@ -69,15 +72,21 @@ class ClauseCodeTree : public CodeTree
*
* Here the actual execution of the code of the tree takes place */
struct LiteralMatcher
: public Matcher</*removing*/false,false>
: public Matcher</*removing*/false,false,higherOrder>
{
using Base = Matcher</*removing*/false,false,higherOrder>;
using Base::op;
using Base::_matched;
using Base::finished;
using Base::execute;

void init(CodeTree* tree, CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_, bool seekOnlySuccess=false);
bool next();
bool doEagerMatching();

inline bool eagerlyMatched() const { return _eagerlyMatched; }

inline ILStruct* getILS() { ASS(matched()); return op->getILS(); }
inline ILStruct* getILS() { ASS(Base::matched()); return op->getILS(); }

USE_ALLOCATOR(LiteralMatcher);

Expand Down
Loading
Loading