Skip to content

Fixed issue 823#835

Open
joe-hauns wants to merge 1 commit intomasterfrom
fix-823
Open

Fixed issue 823#835
joe-hauns wants to merge 1 commit intomasterfrom
fix-823

Conversation

@joe-hauns
Copy link
Copy Markdown
Contributor

@joe-hauns joe-hauns commented Mar 30, 2026

This PR fixes #823, and creates unit tests capturing the bug.

@joe-hauns joe-hauns requested a review from mezpusz March 30, 2026 09:59
SortId sort() const { return _srt; }

TermSugar sort(SortId s) { _srt = s; return *this; }
TermSugar sort(SortId s) { return TermSugar(TermList(*this), s);}
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Based on the name I would expect that this function returns the sort, but in fact it makes the term sorted right? What do you think about naming it a bit more explicitly, like makeSorted or something similar?

std::ostream& Pretty<Literal>::prettyPrint(std::ostream& out) const
{
const Literal& lit = _self;
return out << lit;
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this should be removed, I added it for debug purposes.


bool unify(TermList t1, int bank1, TermList t2, int bank2, bool fixedPointIteration)
{
if (!this->unifyOnce(t1, bank1, t2, bank2)) return false;
Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This could be just return this->unifyOnce(t1, bank1, t2, bank2) && (!fixedPointIteration || this->fixedPointIteration()), no?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Sort unification is not done for two variable equalities

2 participants