/* * relop.c - Relational operators * * Copyright 2012 by Werner Almesberger * * This program is free software; you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by * the Free Software Foundation; either version 2 of the License, or * (at your option) any later version. */ #include #include #include "relop.h" /* * Operator to use for * * (A op B) -> forall X: !(X opa A) -> !(X opb B)) * * This is for unlimited sets of values. For limited sets of values, we could * decide also in some edge cases, but let's save such sophistication for * later. */ static const enum relop unreachable_op[idx_n][idx_n] = { #include "unreachable.inc" }; static int relop2index(enum relop op) { switch (op) { case rel_lt: return idx_lt; case rel_le: return idx_le; case rel_eq: return idx_eq; case rel_ge: return idx_ge; case rel_gt: return idx_gt; default: abort(); } } int relop_unreachable(enum relop opa, enum relop opb, const void *a, const void *b, int (*cmp)(const void *a, enum relop op, const void *b, const void *user), const void *user) { return cmp(a, unreachable_op[relop2index(opa)][relop2index(opb)], b, user); } void dump_relop(FILE *file, enum relop op) { switch (op) { case rel_lt: fprintf(file, "<"); break; case rel_le: fprintf(file, "<="); break; case rel_eq: fprintf(file, "="); break; case rel_ge: fprintf(file, ">="); break; case rel_gt: fprintf(file, ">"); break; default: abort(); } }