Skip to content

Commit

Permalink
Merge pull request #599 from vprover/refactor-ordering-comparators
Browse files Browse the repository at this point in the history 
Refactor ordering comparators
  • Loading branch information
@MichaelRawson
MichaelRawson authored Sep 13, 2024
2 parents 363fe65 + df71b21 commit 1d4a45a
Show file tree
Hide file tree
Showing 16 changed files with 325 additions and 607 deletions.
2 changes: 1 addition & 1 deletion Forwards.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -107,7 +107,7 @@ class LiteralSelector;
class Ordering;
typedef Lib::SmartPtr<Ordering> OrderingSP;
struct OrderingComparator;
typedef std::unique_ptr<const OrderingComparator> OrderingComparatorUP;
typedef std::unique_ptr<OrderingComparator> OrderingComparatorUP;

typedef unsigned SplitLevel;
typedef const SharedSet<SplitLevel> SplitSet;
Expand Down
2 changes: 1 addition & 1 deletion Indexing/Index.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -116,7 +116,7 @@ struct TermLiteralClause
struct DemodulatorData
{
DemodulatorData(TypedTermList term, TermList rhs, Clause* clause, bool preordered, const Ordering& ord)
: term(term), rhs(rhs), clause(clause), preordered(preordered)
: term(term), rhs(rhs), clause(clause), preordered(preordered), comparator(ord.createComparator(term, rhs))
{
#if VDEBUG
ASS(term.containsAllVariablesOf(rhs));
Expand Down
2 changes: 1 addition & 1 deletion Inferences/ForwardDemodulation.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -173,7 +173,7 @@ bool ForwardDemodulationImpl<combinatorySupSupport>::perform(Clause* cl, Clause*
auto appl = lhs.isVar() ? (SubstApplicator*)&applWithEqSort : (SubstApplicator*)&applWithoutEqSort;

if (_precompiledComparison) {
if (!preordered && (_preorderedOnly || !ordering.isGreater(lhs,rhs,appl,const_cast<OrderingComparatorUP&>(qr.data->comparator)))) {
if (!preordered && (_preorderedOnly || !qr.data->comparator->check(appl))) {
continue;
}
} else {
Expand Down
85 changes: 2 additions & 83 deletions Kernel/KBO.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,82 +38,6 @@ using namespace std;
using namespace Lib;
using namespace Shell;


/**
* Class to represent the current state of the KBO comparison.
* Based on Bernd Loechner's "Things to Know when Implementing KBO"
* (https://doi.org/10.1007/s10817-006-9031-4)
* @since 30/04/2008 flight Brussels-Tel Aviv
*/
class KBO::State
{
public:
/** Initialise the state */
State(KBO* kbo)
: _kbo(*kbo)
{}

void init()
{
_weightDiff=0;
_posNum=0;
_negNum=0;
_lexResult=EQUAL;
_varDiffs.reset();
}

/**
* Lexicographic traversal of two terms with same top symbol,
* i.e. traversing their symbols in lockstep, as descibed in
* the Loechner et al. paper above. It performs a bidirectional
* comparison between the two terms, i.e. we can get any value
* of @b Result.
*/
Result traverseLexBidir(AppliedTerm t1, AppliedTerm t2);
/**
* Optimised, unidirectional version of @b traverseLexBidir
* where we only care about @b GREATER and @b EQUAL, otherwise
* it returns as early as possible with @b INCOMPARABLE.
*/
Result traverseLexUnidir(AppliedTerm t1, AppliedTerm t2);
/**
* Performs a non-lexicographic (i.e. non-lockstep) traversal
* of two terms in case their top symbols are not the same.
*/
template<bool unidirectional>
Result traverseNonLex(AppliedTerm t1, AppliedTerm t2);

template<int coef, bool varsOnly> void traverse(AppliedTerm tt);

Result result(AppliedTerm t1, AppliedTerm t2);
protected:
template<int coef> void recordVariable(unsigned var);

bool checkVars() const { return _negNum <= 0; }
Result innerResult(TermList t1, TermList t2);
Result applyVariableCondition(Result res)
{
if(_posNum>0 && (res==LESS || res==EQUAL)) {
res=INCOMPARABLE;
} else if(_negNum>0 && (res==GREATER || res==EQUAL)) {
res=INCOMPARABLE;
}
return res;
}

int _weightDiff;
/** The variable counters */
DHMap<unsigned, int, IdentityHash, DefaultHash> _varDiffs;
/** Number of variables, that occur more times in the first literal */
int _posNum;
/** Number of variables, that occur more times in the second literal */
int _negNum;
/** First comparison result */
Result _lexResult;
/** The ordering used */
KBO& _kbo;
}; // class KBO::State

/**
* Return result of comparison between @b l1 and @b l2 under
* an assumption, that @b traverse method have been called
Expand Down Expand Up @@ -955,14 +879,9 @@ bool KBO::isGreater(AppliedTerm lhs, AppliedTerm rhs) const
return isGreaterOrEq(lhs,rhs)==GREATER;
}

bool KBO::isGreater(TermList lhs, TermList rhs, const SubstApplicator* applicator, OrderingComparatorUP& comparator) const
OrderingComparatorUP KBO::createComparator(TermList lhs, TermList rhs) const
{
if (!comparator) {
// cout << "preprocessing " << lhs << " " << rhs << endl;
comparator = make_unique<KBOComparator>(lhs, rhs, *this);
// cout << comparator->toString() << endl;
}
return static_cast<const KBOComparator*>(comparator.get())->check(applicator);
return make_unique<KBOComparator>(lhs, rhs, *this);
}

int KBO::symbolWeight(const Term* t) const
Expand Down
80 changes: 78 additions & 2 deletions Kernel/KBO.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -158,15 +158,14 @@ class KBO

Result compare(AppliedTerm t1, AppliedTerm t2) const override;
bool isGreater(AppliedTerm t1, AppliedTerm t2) const override;
bool isGreater(TermList lhs, TermList rhs, const SubstApplicator* applicator, OrderingComparatorUP& comparator) const override;
OrderingComparatorUP createComparator(TermList lhs, TermList rhs) const override;

protected:
Result isGreaterOrEq(AppliedTerm tt1, AppliedTerm tt2) const;
unsigned computeWeight(AppliedTerm tt) const;

Result comparePredicates(Literal* l1, Literal* l2) const override;

class State;
friend class KBOComparator;

// int functionSymbolWeight(unsigned fun) const;
Expand All @@ -186,6 +185,83 @@ class KBO
template<class SigTraits>
void showConcrete_(std::ostream&) const;

/**
* Class to represent the current state of the KBO comparison.
* Based on Bernd Loechner's "Things to Know when Implementing KBO"
* (https://doi.org/10.1007/s10817-006-9031-4)
* @since 30/04/2008 flight Brussels-Tel Aviv
*/
class State
{
public:
/** Initialise the state */
State(KBO* kbo)
: _kbo(*kbo)
{}

void init()
{
_weightDiff=0;
_posNum=0;
_negNum=0;
_lexResult=EQUAL;
_varDiffs.reset();
}

/**
* Lexicographic traversal of two terms with same top symbol,
* i.e. traversing their symbols in lockstep, as descibed in
* the Loechner et al. paper above. It performs a bidirectional
* comparison between the two terms, i.e. we can get any value
* of @b Result.
*/
Result traverseLexBidir(AppliedTerm t1, AppliedTerm t2);
/**
* Optimised, unidirectional version of @b traverseLexBidir
* where we only care about @b GREATER and @b EQUAL, otherwise
* it returns as early as possible with @b INCOMPARABLE.
*/
Result traverseLexUnidir(AppliedTerm t1, AppliedTerm t2);
/**
* Performs a non-lexicographic (i.e. non-lockstep) traversal
* of two terms in case their top symbols are not the same.
*/
template<bool unidirectional>
Result traverseNonLex(AppliedTerm t1, AppliedTerm t2);

template<int coef, bool varsOnly> void traverse(AppliedTerm tt);

Result result(AppliedTerm t1, AppliedTerm t2);
protected:
template<int coef> void recordVariable(unsigned var);

bool checkVars() const { return _negNum <= 0; }
Result innerResult(TermList t1, TermList t2);
Result applyVariableCondition(Result res)
{
if(_posNum>0 && (res==LESS || res==EQUAL)) {
res=INCOMPARABLE;
} else if(_negNum>0 && (res==GREATER || res==EQUAL)) {
res=INCOMPARABLE;
}
return res;
}

friend class KBOComparator;

int _weightDiff;
/** The variable counters */
DHMap<unsigned, int, IdentityHash, DefaultHash> _varDiffs;
/** Number of variables, that occur more times in the first literal */
int _posNum;
/** Number of variables, that occur more times in the second literal */
int _negNum;
/** First comparison result */
Result _lexResult;
/** The ordering used */
KBO& _kbo;
}; // class KBO::State

/**
* State used for comparing terms and literals
*/
Expand Down
75 changes: 37 additions & 38 deletions Kernel/KBOComparator.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,12 +20,20 @@ using namespace std;
using namespace Lib;
using namespace Shell;

KBOComparator::KBOComparator(TermList tl1, TermList tl2, const KBO& kbo)
: _kbo(kbo), _instructions()
KBOComparator::KBOComparator(TermList lhs, TermList rhs, const KBO& kbo)
: OrderingComparator(lhs, rhs, kbo)
{
}

void KBOComparator::makeReady()
{
ASS(!_ready);

const auto& kbo = static_cast<const KBO&>(_ord);

// stack of subcomparisons in lexicographic order (w.r.t. tl1 and tl2)
Stack<pair<TermList,TermList>> todo;
todo.push(make_pair(tl1,tl2));
todo.push(make_pair(_lhs,_rhs));

while (todo.isNonEmpty()) {
auto kv = todo.pop();
Expand Down Expand Up @@ -81,26 +89,34 @@ KBOComparator::KBOComparator(TermList tl1, TermList tl2, const KBO& kbo)

// if both are proper terms, we calculate
// weight and variable balances first
DHMap<unsigned,int> vars;
int w = 0;
countSymbols(kbo, vars, w, lhs, 1);
countSymbols(kbo, vars, w, rhs, -1);

// we only care about the non-zero weights and counts
bool varInbalance = false;
DHMap<unsigned,int>::Iterator vit(vars);
auto state = kbo._state;
#if VDEBUG
// we make sure kbo._state is not used while we're using it
kbo._state = nullptr;
#endif
auto w = state->_weightDiff;
decltype(state->_varDiffs)::Iterator vit(state->_varDiffs);
Stack<pair<unsigned,int>> nonzeros;
while (vit.hasNext()) {
unsigned v;
int cnt;
vit.next(v,cnt);
if (cnt!=0) {
nonzeros.push(make_pair(v,cnt));
w-=cnt; // we have to remove the variable weights from w
}
if (cnt<0) {
varInbalance = true;
}
}
#if VDEBUG
kbo._state = state;
state = nullptr;
#endif

// if the condition below does not hold, the weight/var balances are satisfied
if (w < 0 || varInbalance) {
// reinterpret weight here to unsigned because the compiler might not do it
Expand Down Expand Up @@ -154,8 +170,15 @@ KBOComparator::KBOComparator(TermList tl1, TermList tl2, const KBO& kbo)
}
}

bool KBOComparator::check(const SubstApplicator* applicator) const
bool KBOComparator::check(const SubstApplicator* applicator)
{
if (!_ready) {
makeReady();
_ready = true;
}

const auto& kbo = static_cast<const KBO&>(_ord);

for (unsigned i = 0; i < _instructions.size();) {
switch (static_cast<InstructionTag>(_instructions[i]._tag())) {
case InstructionTag::WEIGHT: {
Expand All @@ -169,7 +192,7 @@ bool KBOComparator::check(const SubstApplicator* applicator) const

auto var = _instructions[j]._firstUint();
auto coeff = _instructions[j]._coeff();
AppliedTerm tt(TermList(var,false), applicator, true);
AppliedTerm tt(TermList::var(var), applicator, true);

VariableIterator vit(tt.term);
while (vit.hasNext()) {
Expand All @@ -181,7 +204,7 @@ bool KBOComparator::check(const SubstApplicator* applicator) const
return false;
}
}
auto w = _kbo.computeWeight(tt);
auto w = kbo.computeWeight(tt);
weight += coeff*w;
// due to descending order of counts,
// this also means failure
Expand All @@ -200,7 +223,7 @@ bool KBOComparator::check(const SubstApplicator* applicator) const
break;
}
case InstructionTag::COMPARE_VV: {
auto res = _kbo.isGreaterOrEq(
auto res = kbo.isGreaterOrEq(
AppliedTerm(TermList::var(_instructions[i]._firstUint()), applicator, true),
AppliedTerm(TermList::var(_instructions[i]._secondUint()), applicator, true));
if (res==Ordering::EQUAL) {
Expand All @@ -211,7 +234,7 @@ bool KBOComparator::check(const SubstApplicator* applicator) const
}
case InstructionTag::COMPARE_VT: {
ASS(_instructions[i+1]._tag()==InstructionTag::DATA);
auto res = _kbo.isGreaterOrEq(
auto res = kbo.isGreaterOrEq(
AppliedTerm(TermList::var(_instructions[i]._firstUint()), applicator, true),
AppliedTerm(TermList(_instructions[i+1]._term()), applicator, true));
if (res==Ordering::EQUAL) {
Expand All @@ -223,7 +246,7 @@ bool KBOComparator::check(const SubstApplicator* applicator) const
case InstructionTag::COMPARE_TV: {
ASS(_instructions[i+1]._tag()==InstructionTag::DATA);
// note that in this case the term is the second argument
auto res = _kbo.isGreaterOrEq(
auto res = kbo.isGreaterOrEq(
AppliedTerm(TermList(_instructions[i+1]._term()), applicator, true),
AppliedTerm(TermList::var(_instructions[i]._firstUint()), applicator, true));
if (res==Ordering::EQUAL) {
Expand All @@ -242,30 +265,6 @@ bool KBOComparator::check(const SubstApplicator* applicator) const
return false;
}


void KBOComparator::countSymbols(const KBO& kbo, DHMap<unsigned,int>& vars, int& w, TermList t, int coeff)
{
if (t.isVar()) {
int* vcnt;
vars.getValuePtr(t.var(), vcnt, 0);
(*vcnt) += coeff;
return;
}

w += coeff*kbo.symbolWeight(t.term());
SubtermIterator sti(t.term());
while (sti.hasNext()) {
auto st = sti.next();
if (st.isVar()) {
int* vcnt;
vars.getValuePtr(st.var(), vcnt, 0);
(*vcnt) += coeff;
} else {
w += coeff*kbo.symbolWeight(st.term());
}
}
}

std::string KBOComparator::toString() const
{
std::stringstream str;
Expand Down
Loading

0 comments on commit 1d4a45a

Please sign in to comment.