Skip to content

Commit

Permalink
Review
Browse files Browse the repository at this point in the history
  • Loading branch information
@mezpusz
mezpusz committed Apr 11, 2024
1 parent a336557 commit eeab3ca
Show file tree
Hide file tree
Showing 6 changed files with 148 additions and 115 deletions.
74 changes: 43 additions & 31 deletions Indexing/CodeTree.cpp
View file
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
Original file line number Diff line number Diff line change
Expand Up @@ -263,6 +263,7 @@ class CodeTree
*/
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
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
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,
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) \
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

0 comments on commit eeab3ca

Please sign in to comment.