Skip to content
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

Jump to bottom

Code tree search structs refactor + lazily expanded flat terms #543

Merged
merged 4 commits into from
Apr 12, 2024
Merged

Code tree search structs refactor + lazily expanded flat terms #543

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
a336557
Refactor code tree search structs; change flat term to lazily expandi…
mezpusz Apr 10, 2024
eeab3ca
Review
mezpusz Apr 11, 2024
e0a6b0c
Refactor CodeOp bitfields
mezpusz Apr 11, 2024
e4f00b2
Review
mezpusz Apr 12, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
74 changes: 43 additions & 31 deletions Indexing/CodeTree.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,8 +73,8 @@ CodeTree::LitInfo CodeTree::LitInfo::getOpposite(const LitInfo& li)
FlatTerm* ft=FlatTerm::copy(li.ft);
ft->changeLiteralPolarity();
#if GROUND_TERM_CHECK
ASS_EQ((*ft)[1].tag(), FlatTerm::FUN_TERM_PTR);
(*ft)[1]._ptr=Literal::complementaryLiteral(static_cast<Literal*>((*ft)[1].ptr()));
ASS_EQ((*ft)[1]._tag(), FlatTerm::FUN_TERM_PTR);
(*ft)[1]._ptr=Literal::complementaryLiteral(static_cast<Literal*>((*ft)[1]._term()));
#endif

LitInfo res=li;
Expand Down Expand Up @@ -441,6 +441,18 @@ CodeTree::SearchStruct::SearchStruct(Kind kind, size_t length)
targets.reserve(length);
}

void CodeTree::SearchStruct::destroy()
{
switch(kind) {
case FN_STRUCT:
delete static_cast<FnSearchStruct*>(this);
break;
case GROUND_TERM_STRUCT:
delete static_cast<GroundTermSearchStruct*>(this);
break;
}
}

template<bool doInsert>
bool CodeTree::SearchStruct::getTargetOpPtr(const CodeOp& insertedOp, CodeOp**& tgt)
{
Expand All @@ -466,11 +478,11 @@ CodeTree::CodeOp* CodeTree::SearchStruct::getTargetOp(const FlatTerm::Entry* ftP
if(!ftPos->isFun()) { return 0; }
switch(kind) {
case FN_STRUCT:
return static_cast<FnSearchStruct*>(this)->targetOp<false>(ftPos->number());
return static_cast<FnSearchStruct*>(this)->targetOp<false>(ftPos->_number());
case GROUND_TERM_STRUCT:
ftPos++;
ASS_EQ(ftPos->tag(), FlatTerm::FUN_TERM_PTR);
return static_cast<GroundTermSearchStruct*>(this)->targetOp<false>(ftPos->ptr());
ASS_EQ(ftPos->_tag(), FlatTerm::FUN_TERM_PTR);
return static_cast<GroundTermSearchStruct*>(this)->targetOp<false>(ftPos->_term());
default:
ASSERTION_VIOLATION;
}
Expand Down Expand Up @@ -531,14 +543,14 @@ inline bool CodeTree::BaseMatcher::doCheckGroundTerm()
Term* trm=op->getTargetTerm();

fte++;
ASS_EQ(fte->tag(), FlatTerm::FUN_TERM_PTR);
ASS(fte->ptr());
if(trm!=fte->ptr()) {
ASS_EQ(fte->_tag(), FlatTerm::FUN_TERM_PTR);
ASS(fte->_term());
if(trm!=fte->_term()) {
return false;
}
fte++;
ASS_EQ(fte->tag(), FlatTerm::FUN_RIGHT_OFS);
tp+=fte->number();
ASS_EQ(fte->_tag(), FlatTerm::FUN_RIGHT_OFS);
tp+=fte->_number();
return true;
}

Expand Down Expand Up @@ -572,7 +584,7 @@ CodeTree::~CodeTree()
top_ops.push(ss->targets[i]);
}
}
delete ss;
ss->destroy();
} else {
CodeBlock* cb=firstOpToCodeBlock(top_op);

Expand Down Expand Up @@ -945,7 +957,7 @@ void CodeTree::compressCheckOps(CodeOp* chainStart)
toDo.push(ss->targets[i]);
}
}
delete ss;
ss->destroy();
} else {
otherOps.push(op);
}
Expand Down Expand Up @@ -1082,7 +1094,7 @@ void CodeTree::optimizeMemoryAfterRemoval(Stack<CodeOp*>* firstsInBlocks, CodeOp
//if we're at this point, the SEARCH_STRUCT will be deleted
firstOp=&ss->landingOp;
alt=ss->landingOp.alternative();
delete ss;
ss->destroy();

//now let's continue as if there wasn't any SEARCH_STRUCT operation:)

Expand Down Expand Up @@ -1276,7 +1288,7 @@ inline bool CodeTree::RemovingMatcher::doCheckFun()
return false;
}
fte.expand();
tp+=FlatTerm::functionEntryCount;
tp+=FlatTerm::FUNCTION_ENTRY_COUNT;
return true;
}

Expand All @@ -1287,10 +1299,10 @@ inline bool CodeTree::RemovingMatcher::doAssignVar()
//we are looking for variants and they match only other variables into variables
unsigned var=op->arg();
const FlatTerm::Entry* fte=&(*ft)[tp];
if(fte->tag()!=FlatTerm::VAR) {
if(fte->_tag()!=FlatTerm::VAR) {
return false;
}
bindings[var]=fte->number();
bindings[var]=fte->_number();
tp++;
return true;
}
Expand All @@ -1302,7 +1314,7 @@ inline bool CodeTree::RemovingMatcher::doCheckVar()
//we are looking for variants and they match only other variables into variables
unsigned var=op->arg();
const FlatTerm::Entry* fte=&(*ft)[tp];
if(fte->tag()!=FlatTerm::VAR || bindings[var]!=fte->number()) {
if(fte->_tag()!=FlatTerm::VAR || bindings[var]!=fte->_number()) {
return false;
}
tp++;
Expand Down Expand Up @@ -1461,7 +1473,7 @@ inline bool CodeTree::Matcher::doCheckFun()
return false;
}
fte.expand();
tp+=FlatTerm::functionEntryCount;
tp+=FlatTerm::FUNCTION_ENTRY_COUNT;
return true;
}

Expand All @@ -1471,19 +1483,19 @@ inline void CodeTree::Matcher::doAssignVar()

unsigned var=op->arg();
const FlatTerm::Entry* fte=&(*ft)[tp];
if(fte->tag()==FlatTerm::VAR) {
bindings[var]=TermList(fte->number(),false);
if(fte->_tag()==FlatTerm::VAR) {
bindings[var]=TermList(fte->_number(),false);
tp++;
}
else {
ASS(fte->isFun());
fte++;
ASS_EQ(fte->tag(), FlatTerm::FUN_TERM_PTR);
ASS(fte->ptr());
bindings[var]=TermList(fte->ptr());
ASS_EQ(fte->_tag(), FlatTerm::FUN_TERM_PTR);
ASS(fte->_term());
bindings[var]=TermList(fte->_term());
fte++;
ASS_EQ(fte->tag(), FlatTerm::FUN_RIGHT_OFS);
tp+=fte->number();
ASS_EQ(fte->_tag(), FlatTerm::FUN_RIGHT_OFS);
tp+=fte->_number();
}
}

Expand All @@ -1493,22 +1505,22 @@ inline bool CodeTree::Matcher::doCheckVar()

unsigned var=op->arg();
const FlatTerm::Entry* fte=&(*ft)[tp];
if(fte->tag()==FlatTerm::VAR) {
if(bindings[var]!=TermList(fte->number(),false)) {
if(fte->_tag()==FlatTerm::VAR) {
if(bindings[var]!=TermList(fte->_number(),false)) {
return false;
}
tp++;
}
else {
ASS(fte->isFun());
fte++;
ASS_EQ(fte->tag(), FlatTerm::FUN_TERM_PTR);
if(bindings[var]!=TermList(fte->ptr())) {
ASS_EQ(fte->_tag(), FlatTerm::FUN_TERM_PTR);
if(bindings[var]!=TermList(fte->_term())) {
return false;
}
fte++;
ASS_EQ(fte->tag(), FlatTerm::FUN_RIGHT_OFS);
tp+=fte->number();
ASS_EQ(fte->_tag(), FlatTerm::FUN_RIGHT_OFS);
tp+=fte->_number();
}
return true;
}
Expand Down
3 changes: 1 addition & 2 deletions Indexing/CodeTree.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -263,6 +263,7 @@ class CodeTree
*/
quickbeam123 marked this conversation as resolved.
Show resolved Hide resolved
struct SearchStruct
{
void destroy();
/**
* Fills out pointer @b tgt where @b insertedOp should be
* (or is) inserted in the structure. If @b doInsert is true
Expand Down Expand Up @@ -301,8 +302,6 @@ class CodeTree
struct SearchStructImpl
: public SearchStruct
{
USE_ALLOCATOR(SearchStructImpl);

SearchStructImpl(size_t length);

using T = typename std::conditional<k==SearchStruct::FN_STRUCT,unsigned,Term*>::type;
Expand Down
42 changes: 21 additions & 21 deletions Kernel/FlatTerm.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,8 +62,8 @@ FlatTerm::FlatTerm(size_t length)

size_t FlatTerm::getEntryCount(Term* t)
{
//functionEntryCount entries per function and one per variable
return t->weight()*functionEntryCount-(functionEntryCount-1)*t->numVarOccs();
//FUNCTION_ENTRY_COUNT entries per function and one per variable
return t->weight()*FUNCTION_ENTRY_COUNT-(FUNCTION_ENTRY_COUNT-1)*t->numVarOccs();
}

FlatTerm* FlatTerm::create(Term* t)
Expand Down Expand Up @@ -148,29 +148,29 @@ FlatTerm* FlatTerm::copy(const FlatTerm* ft)

void FlatTerm::swapCommutativePredicateArguments()
{
ASS_EQ((*this)[0].tag(), FUN);
ASS_EQ((*this)[0].number()|1, 1); //as for now, the only commutative predicate is equality
ASS_EQ((*this)[0]._tag(), FUN);
ASS_EQ((*this)[0]._number()|1, 1); //as for now, the only commutative predicate is equality

size_t firstStart=3;
size_t firstLen;
if((*this)[firstStart].tag()==FUN) {
ASS_EQ((*this)[firstStart+2].tag(), FUN_RIGHT_OFS);
firstLen=(*this)[firstStart+2].number();
if((*this)[firstStart]._tag()==FUN) {
ASS_EQ((*this)[firstStart+2]._tag(), FUN_RIGHT_OFS);
firstLen=(*this)[firstStart+2]._number();
}
else {
ASS_EQ((*this)[firstStart].tag(), VAR);
ASS_EQ((*this)[firstStart]._tag(), VAR);
firstLen=1;
}

size_t secStart=firstStart+firstLen;
size_t secLen;

if((*this)[secStart].tag()==FUN) {
ASS_EQ((*this)[secStart+2].tag(), FUN_RIGHT_OFS);
secLen=(*this)[secStart+2].number();
if((*this)[secStart]._tag()==FUN) {
ASS_EQ((*this)[secStart+2]._tag(), FUN_RIGHT_OFS);
secLen=(*this)[secStart+2]._number();
}
else {
ASS_EQ((*this)[secStart].tag(), VAR);
ASS_EQ((*this)[secStart]._tag(), VAR);
secLen=1;
}
ASS_EQ(secStart+secLen,_length);
Expand All @@ -192,14 +192,14 @@ void FlatTerm::swapCommutativePredicateArguments()

void FlatTerm::Entry::expand()
{
if (tag()==FUN) {
if (_tag()==FUN) {
return;
}
ASS(tag()==FUN_UNEXPANDED);
ASS(this[1].tag()==FUN_TERM_PTR);
ASS(this[2].tag()==FUN_RIGHT_OFS);
Term* t = this[1].ptr();
size_t p = FlatTerm::functionEntryCount;
ASS(_tag()==FUN_UNEXPANDED);
ASS(this[1]._tag()==FUN_TERM_PTR);
ASS(this[2]._tag()==FUN_RIGHT_OFS);
Term* t = this[1]._term();
size_t p = FlatTerm::FUNCTION_ENTRY_COUNT;
for (unsigned i = 0; i < t->arity(); i++) {
auto arg = t->nthArgument(i);
if (arg->isVar()) {
Expand All @@ -211,11 +211,11 @@ void FlatTerm::Entry::expand()
this[p] = Entry(FUN_UNEXPANDED, arg->term()->functor());
this[p+1] = Entry(arg->term());
this[p+2] = Entry(FUN_RIGHT_OFS, getEntryCount(arg->term()));
p += this[p+2].number();
p += this[p+2]._number();
}
}
ASS_EQ(p,this[2].number());
_info.tag = FUN;
ASS_EQ(p,this[2]._number());
_setTag(FUN);
}

};
Expand Down
56 changes: 37 additions & 19 deletions Kernel/FlatTerm.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ class FlatTerm

static FlatTerm* copy(const FlatTerm* ft);

static const size_t functionEntryCount=3;
static constexpr size_t FUNCTION_ENTRY_COUNT=3;

enum EntryTag {
FUN_TERM_PTR = 0,
Expand All @@ -55,38 +55,56 @@ class FlatTerm
struct Entry
{
Entry() = default;
Entry(EntryTag tag, unsigned num) { _info.tag=tag; _info.number=num; }
Entry(Term* ptr) : _ptr(ptr) { ASS_EQ(tag(), FUN_TERM_PTR); }

inline EntryTag tag() const { return static_cast<EntryTag>(_info.tag); }
inline unsigned number() const { return _info.number; }
inline Term* ptr() const { return _ptr; }
inline bool isVar() const { return tag()==VAR; }
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; }
Entry(EntryTag tag, unsigned num) { _setTag(tag); _setNumber(num); }
Entry(Term* term) { _setTerm(term); ASS_EQ(_tag(), FUN_TERM_PTR); }

inline bool isVar() const { return _tag()==VAR; }
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; }
/**
* Should be called when @b isFun() is true.
* If @b tag()==FUN_UNEXPANDED, it fills out entries for the functions
* arguments with FUN_UNEXPANDED values. Otherwise does nothing.
*/
void expand();

union {
Term* _ptr;
struct {
unsigned tag : 4;
unsigned number : 28;
} _info;
};
uint64_t _content;

static constexpr unsigned
TAG_BITS_START = 0,
TAG_BITS_END = TAG_BITS_START + 3,
NUMBER_BITS_START = TAG_BITS_END,
NUMBER_BITS_END = NUMBER_BITS_START + 27,
MichaelRawson marked this conversation as resolved.
Show resolved Hide resolved
TERM_BITS_START = 0,
TERM_BITS_END = CHAR_BIT * sizeof(Term *);

// various properties we want to check
static_assert(TAG_BITS_START == 0, "tag must be the least significant bits");
static_assert(TERM_BITS_START == 0, "term must be the least significant bits");
static_assert(sizeof(void *) <= sizeof(uint64_t), "must be able to fit a pointer into a 64-bit integer");
static_assert(FUN_UNEXPANDED < 8, "must be able to squash orderings into 3 bits");

// getters and setters
#define GET_AND_SET(type, name, Name, NAME) \
MichaelRawson marked this conversation as resolved.
Show resolved Hide resolved
type _##name() const { return BitUtils::getBits<NAME##_BITS_START, NAME##_BITS_END>(*this); }\
void _set##Name(type val) { BitUtils::setBits<NAME##_BITS_START, NAME##_BITS_END>(*this, val); }
GET_AND_SET(unsigned, tag, Tag, TAG)
GET_AND_SET(unsigned, number, Number, NUMBER)
#undef GET_AND_SET
Term *_term() const
{ return reinterpret_cast<Term *>(BitUtils::getBits<TERM_BITS_START, TERM_BITS_END>(*this)); }
void _setTerm(Term *term)
{ BitUtils::setBits<TERM_BITS_START, TERM_BITS_END>(*this, reinterpret_cast<uint64_t>(term)); }
// end bitfield
};

inline Entry& operator[](size_t i) { ASS_L(i,_length); return _data[i]; }
inline const Entry& operator[](size_t i) const { ASS_L(i,_length); return _data[i]; }

void swapCommutativePredicateArguments();
void changeLiteralPolarity()
{ _data[0]._info.number^=1; }
{ _data[0]._setNumber(_data[0]._number()^1); }

private:
static size_t getEntryCount(Term* t);
Expand Down