@@ -122,20 +122,32 @@ bool Term::containsUnresolvedSymbols() const {
122122 return false ;
123123}
124124
125- // / Shortlex order on terms.
125+ namespace {
126+
127+ // / Shortlex order on symbol ranges.
126128// /
127129// / First we compare length, then perform a lexicographic comparison
128- // / on symbols if the two terms have the same length.
129- int MutableTerm::compare (const MutableTerm &other,
130- const ProtocolGraph &graph) const {
131- if (size () != other.size ())
132- return size () < other.size () ? -1 : 1 ;
133-
134- for (unsigned i = 0 , e = size (); i < e; ++i) {
135- auto lhs = (*this )[i];
136- auto rhs = other[i];
137-
138- int result = lhs.compare (rhs, graph);
130+ // / on symbols if the two ranges have the same length.
131+ // /
132+ // / This is used to implement Term::compare() and MutableTerm::compare()
133+ // / below.
134+ template <typename Iter>
135+ int shortlexCompare (Iter lhsBegin, Iter lhsEnd,
136+ Iter rhsBegin, Iter rhsEnd,
137+ const ProtocolGraph &protos) {
138+ unsigned lhsSize = (lhsEnd - lhsBegin);
139+ unsigned rhsSize = (rhsEnd - rhsBegin);
140+ if (lhsSize != rhsSize)
141+ return lhsSize < rhsSize ? -1 : 1 ;
142+
143+ while (lhsBegin != lhsEnd) {
144+ auto lhs = *lhsBegin;
145+ auto rhs = *rhsBegin;
146+
147+ ++lhsBegin;
148+ ++rhsBegin;
149+
150+ int result = lhs.compare (rhs, protos);
139151 if (result != 0 ) {
140152 assert (lhs != rhs);
141153 return result;
@@ -147,6 +159,20 @@ int MutableTerm::compare(const MutableTerm &other,
147159 return 0 ;
148160}
149161
162+ }
163+
164+ // / Shortlex order on terms.
165+ int Term::compare (Term other,
166+ const ProtocolGraph &protos) const {
167+ return shortlexCompare (begin (), end (), other.begin (), other.end (), protos);
168+ }
169+
170+ // / Shortlex order on mutable terms.
171+ int MutableTerm::compare (const MutableTerm &other,
172+ const ProtocolGraph &protos) const {
173+ return shortlexCompare (begin (), end (), other.begin (), other.end (), protos);
174+ }
175+
150176// / Replace the subterm in the range [from,to) with \p rhs.
151177// /
152178// / Note that \p rhs must precede [from,to) in the linear
0 commit comments