(Limited) Operator overloading / Comparison predicate type

[fbrausse]

Dear all,

In some other projects of mine I have been using a type like the following and I have come to like it because it simplifies life with the different comparisons. So my question here has two parts: (a) Is there a policy for ESBMC's code regarding disallowing or discouraging the use of operator overloading? The reason I'm asking this is because I have barely seen any except for the ubiquitous std::shared_ptr things via expr2tc/type2tc.

This is the type and methods I'd like to use/introduce:

/* Symbolic representation of an order/equality predicate */

enum cmp_t { LE, LT, GE, GT, EQ, NE, };

/* Some properties of cmp_t */
static inline bool is_less(cmp_t c) { return (unsigned)c <= LT; }
static inline bool is_strict(cmp_t c) { return (unsigned)c & 0x1; }
static inline cmp_t make_strict(cmp_t c) { return (cmp_t)((unsigned)c | 0x1); }
static inline bool is_order(cmp_t c) { return !((unsigned)c >> 2); }

/* Flip a cmp_t */
static inline cmp_t operator-(cmp_t c)
{
	switch (c) {
	case LE: return GE;
	case LT: return GT;
	case GE: return LE;
	case GT: return LT;
	case EQ:
	case NE:
		return c;
	}
	unreachable();
}

/* Negate a cmp_t */
static inline cmp_t operator!(cmp_t c)
{
	switch (c) {
	case LE: return GT;
	case LT: return GE;
	case GE: return LT;
	case GT: return LE;
	case EQ: return NE;
	case NE: return EQ;
	}
	unreachable();
}

template <typename T>
static inline auto do_cmp(const T &l, cmp_t c, const T &r)
{
	switch (c) {
	case LE: return l <= r;
	case LT: return l <  r;
	case GE: return l >= r;
	case GT: return l >  r;
	case EQ: return l == r;
	case NE: return l != r;
	}
	unreachable();
}

My second question would be (b) whether there has been/still is any reason for the (less|greater)(equal)?than2t and equality2t|notequal2t expressions to be separate or, if not, whether there would be interest in unifying them with something like the above predicate type?