Skip to content

KBO: don't mistake a sort and a term with the same functor number for the same symbol #1018

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

Merged
quickbeam123 merged 1 commit into from
Oct 12, 2026
Merged

KBO: don't mistake a sort and a term with the same functor number for the same symbol #1018

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
14 changes: 12 additions & 2 deletions Kernel/KBO.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,16 @@ using namespace std;
using namespace Lib;
using namespace Shell;

/**
* True if @b t1 and @b t2 have the same top symbol. Type constructors and
* function symbols are numbered independently, so a sort and a term can
* share a functor number without having anything in common.
*/
static bool sameTopSymbol(const Term* t1, const Term* t2)
{
return t1->functor() == t2->functor() && t1->isSort() == t2->isSort();
}

/**
* Return result of comparison between @b l1 and @b l2 under
* an assumption, that @b traverse method have been called
Expand All @@ -49,7 +59,7 @@ Ordering::Result KBO::State::result(KBO const& kbo, AppliedTerm t1, AppliedTerm
Result res;
if(_weightDiff) {
res=_weightDiff>0 ? GREATER : LESS;
} else if(t1.term.term()->functor()!=t2.term.term()->functor()) {
} else if(!sameTopSymbol(t1.term.term(), t2.term.term())) {
if(t1.term.term()->isLiteral()) {
ASS(t2.term.term()->isLiteral());
int prec1, prec2;
Expand Down Expand Up @@ -797,7 +807,7 @@ Ordering::Result KBO::compare(AppliedTerm tl1, AppliedTerm tl2) const

state->init();
Result res;
if(t1->functor()==t2->functor()) {
if(sameTopSymbol(t1, t2)) {
res = state->traverseLexBidir(*this, tl1, tl2);
} else {
res = state->traverseNonLex</*unidirectional=*/false>(*this, tl1, tl2);
Expand Down
26 changes: 26 additions & 0 deletions UnitTests/tKBO.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -381,6 +381,32 @@ TEST_FUN(kbo_test23) {
ASS_EQ(ord.compare(f(alpha), g(beta)), Ordering::Result::INCOMPARABLE)
}

// Type constructors and function symbols are numbered independently, so a sort
// and a term can share a functor number. KBO::compare used to take that for the
// same top symbol (seen as compare(complex, one_one(complex)) == EQUAL on SWV645_5).
TEST_FUN(kbo_test24) {
DECL_DEFAULT_SORT_VARS
DECL_SORT(pad)

// pad both symbol tables so that the next type constructor
// and the next function symbol get the same number
for (unsigned i = 0; env.signature->typeCons() < env.signature->functions(); i++) {
TypeConstSugar(("padSort" + Int::toString(i)).c_str());
}
for (unsigned i = 0; env.signature->functions() < env.signature->typeCons(); i++) {
ConstSugar(("padConst" + Int::toString(i)).c_str(), pad);
}

DECL_SORT(srt)
DECL_POLY_CONST(one, 1, alpha)
ASS_EQ(srt.sugaredExpr().term()->functor(), one.functor())

auto ord = kbo(weights(), weights());

ASS_EQ(ord.compare(srt, one(srt)), Ordering::Result::LESS)
ASS_EQ(ord.compare(one(srt), srt), Ordering::Result::GREATER)
}

// isGreater tests

bool isGreaterSymmetric(const KBO& ord, TermList t1, TermList t2) {
Expand Down