2012-05-21 05:04:41 +03:00
|
|
|
/*
|
|
|
|
* 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 <stdlib.h>
|
|
|
|
#include <stdio.h>
|
|
|
|
|
|
|
|
#include "relop.h"
|
|
|
|
|
|
|
|
|
2012-05-31 18:33:52 +03:00
|
|
|
/*
|
|
|
|
* Operator to use for
|
|
|
|
*
|
|
|
|
* forall X: (A op B) == ((X opa A) -> (X opb B))
|
|
|
|
*
|
|
|
|
* For unlimited sets of values:
|
|
|
|
*
|
|
|
|
* opa -> < <= == >= >
|
|
|
|
* opb
|
|
|
|
* < >= >= 0 0 0
|
|
|
|
* <= > >= 0 0 0
|
|
|
|
* == > >= == <= <
|
|
|
|
* >= 0 0 0 <= <
|
|
|
|
* > 0 0 0 <= <=
|
|
|
|
*
|
|
|
|
* 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 implies_op[idx_n][idx_n] = {
|
|
|
|
[idx_lt][idx_lt] = rel_ge,
|
|
|
|
[idx_lt][idx_le] = rel_ge,
|
|
|
|
|
|
|
|
[idx_le][idx_lt] = rel_gt,
|
|
|
|
[idx_le][idx_le] = rel_ge,
|
|
|
|
|
|
|
|
[idx_eq][idx_lt] = rel_gt,
|
|
|
|
[idx_eq][idx_le] = rel_ge,
|
|
|
|
[idx_eq][idx_eq] = rel_eq,
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
|
|
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();
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
static enum relop swap_op(enum relop op)
|
|
|
|
{
|
|
|
|
return idx_n-1-relop2index(op);
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
int relop_implies(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)
|
|
|
|
{
|
|
|
|
if (opa <= opb)
|
|
|
|
return cmp(a,
|
|
|
|
implies_op[relop2index(opa)][relop2index(opb)], b, user);
|
|
|
|
else
|
|
|
|
return cmp(b,
|
|
|
|
swap_op(implies_op[relop2index(opb)][relop2index(opa)]),
|
|
|
|
a, user);
|
|
|
|
}
|
|
|
|
|
|
|
|
|
2012-05-21 05:04:41 +03:00
|
|
|
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();
|
|
|
|
}
|
|
|
|
}
|