/* $Id */

/*
 * Source code for an implementation of the Omega test, a integer programming algorithm for dependence analysis, by
 * William Pugh, appeared in Supercomputing '91 and CACM Aug 92
 *
 * C Source written by: William Pugh Dept. of Computer Science Univ. of Maryland, College Park pugh@cs.umd.edu
 *
 * Options SPEED - don't bother checking debugging flags eliminateRedundantConstraints - use expensive methods to
 * eliminate all redundant constraints singleResult - only produce a single simplified result verifySimplication -
 * simplifyProblem checks for problem with no soloutions reduceWithSubstitutions - if not defined, convert
 * substitutions back to EQs APROX - approximate inexact reductions
 */


#define maxWildCards 18
#ifndef APROX
#define APROX 0
#endif

#ifdef _WIN32
extern "C" void addToCollection(const int line, const char *file, void *pointer, int type);
extern "C" void removeFromCollection(void *pointer);
#endif

#include "include/portable.h"
#include "include/flags.h"
#include <assert.h>
#include <stdio.h>
#include <stdlib.h>
#include "include/ip.h"


#define EQ_type 1
#define GEQ_type 2
#define keyMult 31
#define indexMult 17
#define abs(x) ((x) >= 0 ? (x) : -(x))
#define max(x,y) ((x) > (y) ? (x) : (y))
#define min(x,y) ((x) < (y) ? (x) : (y))
#define setMax(m,x) { if ((m) < (x)) m = (x); }
#define setMin(m,x) { if ((m) > (x)) m = (x); }
#ifndef TRUE
#  define TRUE 1
#endif
#ifndef FALSE
#  define FALSE 0
#endif
#define nVars (problemPtr->getVarsN())
#define nEQ (problemPtr->getNumEqs())
#define nGEQ (problemPtr->getNumGEqs())
#define nSUB (problemPtr->getNumSUBs())
#define SUBs (problemPtr->_SUBs)
#define GEQs (problemPtr->_GEQs)
#define EQs (problemPtr->_EQs)
#define safeVars (problemPtr->_safeVars)
#define printEQ(e) printEqn(problemPtr,e,0,0)
#define printGEQ(e) printEqn(problemPtr,e,1,0)
#define printGEQextra(e) printEqn(problemPtr,e,1,1)
#define variable(i) orgVariable(problemPtr->_var[i])
#define orgVariable(i) (i == 0 ? "1" : (i < 0?wildName[-i]: (*problemPtr->_getVarName)(i,problemPtr->_getVarNameArgs)))
#define doTrace (trace && TRACE)
#define doDelete(e,nV) {if (DEBUG) {fprintf(outputFile,"Deleting %d (last:%d): ",e,nGEQ-1); printGEQ(&GEQs[e]);fprintf(outputFile,"\n");}; \
                        if (e < nGEQ-1) eqnncpy (&GEQs[e], &GEQs[nGEQ - 1],(nV)); \
                        (problemPtr->addNumGEqs(-1));}

#define doDeleteExtra(e,nV) {if (DEBUG) {fprintf(outputFile,"Deleting %d: ",e); printGEQextra(&GEQs[e]);fprintf(outputFile,"\n");}; \
                             if (e < nGEQ-1) eqnncpy (&GEQs[e], &GEQs[nGEQ - 1],(nV)); \
                             (problemPtr->addNumGEqs(-1));}
#define isRed(e) (desiredResult == SIMPLIFY && (e)->color)


static int mayBeRed = 0;
#define hashTableSize 550
#define maxKeys 500

#ifdef SPEED
#define TRACE 0
#define DBUG 0
#define DEBUG 0
#else
#define TRACE (debugLevel)
#define DBUG  (debugLevel > 1)
#define DEBUG (debugLevel > 2)
#endif
extern void addingEqualityConstraint(Problem * problemPtr, int e);

#define mallocProblem ((Problem *) malloc(sizeof(Problem)))

static struct _eqn hashMaster[hashTableSize];

int nonConvex = 0;

int firstCheckForRedundantEquations = 0;

static int doItAgain;

static int conservative = 0;

static FILE *outputFile;	/* printProblem writes its output to this file */

static int nextKey;
static char wildName[200][20];
static int nextWildCard = 0;
static int trace = 1;
static int depth = 0;
static int foundReduction;
static int packing[maxVars];

static int inApproximateMode = 0;

#if reduceWithSubstitutions
int reduceWithSubs = 1;
#else
int reduceWithSubs = 0;
#endif

static int pleaseNoEqualitiesInSimplifiedProblems = 0;

int hashVersion = 0;

#define noProblem ((Problem *) 0)

Problem *originalProblem = noProblem;

void noProcedure(Problem *problemPtr) { }
void(*whenReduced) (Problem *problemPtr) = noProcedure;

static int gcd(int b, int a)
{
    if (b == 1)
        return (1);
    while (b != 0) {
        int t = b;
        b = a % b;
        a = t;
    };
    return (a);
}


int checkIfSingleVar(Eqn e, int i)
{
    for (; i > 0; i--)
        if (e->coef[i]) {
            i--;
            break;
        };
    for (; i > 0; i--)
        if (e->coef[i])
            break;
    return (i == 0);
}


void initializeVariables(Problem *p)
{
    int i;
    for (i = p->getVarsN(); i > 0; i--)
        p->forwardingAddress[i] = p->_var[i] = i;
    p->variablesInitialized = 1;
}

void initializeProblem(Problem *p)
{    
    p->hashVersion = hashVersion;
    p->variablesInitialized = 0;
    p->variablesFreed = 0;
    p->_safeVars = 0;
    p->_init(0, 0, 0, 0);
}

void problemcpy(Problem *p1, Problem *p2)
{
    int e, i;    
    p1->hashVersion = p2->hashVersion;
    p1->variablesInitialized = p2->variablesInitialized;
    p1->variablesFreed = p2->variablesFreed;
    p1->_safeVars = p2->_safeVars;
    p1->_init(p2->getNumEqs(), p2->getNumGEqs(), p2->getNumSUBs(), p2->getVarsN());

    for (e = p2->getNumEqs() - 1; e >= 0; e--)
        eqnncpy(&(p1->_EQs[e]), &(p2->_EQs[e]), p2->getVarsN());

    for (e = p2->getNumGEqs() - 1; e >= 0; e--)
        eqnncpy(&(p1->_GEQs[e]), &(p2->_GEQs[e]), p2->getVarsN());

    for (e = p2->getNumSUBs() - 1; e >= 0; e--)
        eqnncpy(&(p1->_SUBs[e]), &(p2->_SUBs[e]), p2->getVarsN());

    p1->_var.resize(p2->getVarsN() + 1);
        
    for (i = 0; i <= p2->getVarsN(); i++)
        p1->_var[i] = p2->_var[i];

    p1->forwardingAddress.resize(maxVars + 2);
    for (i = 0; i <= maxVars; i++)
        p1->forwardingAddress[i] = p2->forwardingAddress[i];
    p1->_getVarName = p2->_getVarName;
    p1->_getVarNameArgs = p2->_getVarNameArgs;
}



static void printTerm(Problem *problemPtr, Eqn e, int c)
{
    int i;
    int first;
    int n = nVars;
    int wentFirst = -1;
    first = 1;
    for (i = 1; i <= n; i++)
        if (c * e->coef[i] > 0) {

            first = 0;
            wentFirst = i;

            if (c * e->coef[i] == 1)
                fprintf(outputFile, "%s", variable(i));
            else
                fprintf(outputFile, "%d%s", c * e->coef[i], variable(i));
            break;
        };
    for (i = 1; i <= n; i++)
        if (i != wentFirst && c * e->coef[i] != 0) {
            if (!first && c * e->coef[i] > 0)
                fprintf(outputFile, "+");

            first = 0;

            if (c * e->coef[i] == 1)
                fprintf(outputFile, "%s", variable(i));
            else if (c * e->coef[i] == -1)
                fprintf(outputFile, "-%s", variable(i));
            else
                fprintf(outputFile, "%d%s", c * e->coef[i], variable(i));
        };
    if (!first && c * e->coef[0] > 0)
        fprintf(outputFile, "+");
    if (first || c * e->coef[0] != 0)
        fprintf(outputFile, "%d", c * e->coef[0]);
}


void printEqn(Problem *problemPtr, Eqn e, int test, int extra)
{
    char buf[maxVars * 12 + 80];

    sprintEqn(buf, problemPtr, e, test, extra);
    fprintf(outputFile, "%s", buf);
}

void sprintEqn(char *str, Problem *problemPtr, Eqn e, int test, int extra)
{
    int i;
    int first;
    int n = nVars + extra;

    if (test) {
        if (DEBUG && e->touched) {
            sprintf(str, "!");
            while (*str)
                str++;
        }
        else if (DBUG && !e->touched && e->key != 0) {
            sprintf(str, "%d: ", e->key);
            while (*str)
                str++;
        }
    }
    if (e->color) {
        sprintf(str, "[");
        while (*str)
            str++;
    }
    first = 1;
    for (i = 0; i <= n; i++)
        if (e->coef[i] < 0) {
            if (!first) {
                sprintf(str, "+");
                while (*str)
                    str++;
            }
            else
                first = 0;
            if (i == 0) {
                sprintf(str, "%d", -e->coef[i]);
                while (*str)
                    str++;
            }
            else if (e->coef[i] == -1) {
                sprintf(str, "%s", variable(i));
                while (*str)
                    str++;
            }
            else {
                sprintf(str, "%d%s", -e->coef[i], variable(i));
                while (*str)
                    str++;
            }
        };
    if (first) {
        sprintf(str, "0");
        while (*str)
            str++;
    }
    if (test == 0) {
        sprintf(str, " = ");
        while (*str)
            str++;
    }
    else {
        sprintf(str, " <= ");
        while (*str)
            str++;
    }

    first = 1;
    for (i = 0; i <= n; i++)
        if (e->coef[i] > 0) {
            if (!first) {
                sprintf(str, "+");
                while (*str)
                    str++;
            }
            else
                first = 0;
            if (i == 0) {
                sprintf(str, "%d", e->coef[i]);
                while (*str)
                    str++;
            }
            else if (e->coef[i] == 1) {
                sprintf(str, "%s", variable(i));
                while (*str)
                    str++;
            }
            else {
                sprintf(str, "%d%s", e->coef[i], variable(i));
                while (*str)
                    str++;
            }
        }
    if (first) {
        sprintf(str, "0");
        while (*str)
            str++;
    }
    if (e->color) {
        sprintf(str, "]");
        while (*str)
            str++;
    }
}

void printVars(Problem *problemPtr)
{
    int i;
    fprintf(outputFile, "variables = ");
    if (problemPtr->_safeVars > 0)
        fprintf(outputFile, "(");
    for (i = 1; i <= nVars; i++) {
        fprintf(outputFile, "%s", variable(i));
        if (i == problemPtr->_safeVars)
            fprintf(outputFile, ")");
        if (i < nVars)
            fprintf(outputFile, ", ");
    };
    fprintf(outputFile, "\n");
}

void printProblem(Problem *problemPtr)
{
    int e;

    if (!problemPtr->variablesInitialized)
        initializeVariables(problemPtr);
    printVars(problemPtr);
    for (e = 0; e < nEQ; e++) {
        printEQ(&EQs[e]);
        fprintf(outputFile, "\n");
    };
    for (e = 0; e < nGEQ; e++) {
        printGEQ(&GEQs[e]);
        fprintf(outputFile, "\n");
    };
    for (e = 0; e < nSUB; e++) {
        Eqn eq = &SUBs[e];
        if (DBUG && eq->color)
            fprintf(outputFile, "[");
        if (eq->key > 0)
            fprintf(outputFile, "%s := ", orgVariable(eq->key));
        else
            fprintf(outputFile, "#%d := ", eq->key);
        printTerm(problemPtr, eq, 1);
        if (DBUG && eq->color)
            fprintf(outputFile, "]");
        fprintf(outputFile, "\n");
    };
    fflush(outputFile);
}


void printRedEquations(Problem *problemPtr)
{
    int e;

    if (!problemPtr->variablesInitialized)
        initializeVariables(problemPtr);
    printVars(problemPtr);
    for (e = 0; e < nEQ; e++) {
        if (EQs[e].color == red) {
            printEQ(&EQs[e]);
            fprintf(outputFile, "\n");
        }
    };
    for (e = 0; e < nGEQ; e++) {
        if (GEQs[e].color == red) {
            printGEQ(&GEQs[e]);
            fprintf(outputFile, "\n");
        }
    };
    for (e = 0; e < nSUB; e++) {
        if (SUBs[e].color == red) {
            Eqn eq = &SUBs[e];
            if (DBUG && eq->color)
                fprintf(outputFile, "[");
            if (eq->key > 0)
                fprintf(outputFile, "%s := ", orgVariable(eq->key));
            else
                fprintf(outputFile, "#%d := ", eq->key);
            printTerm(problemPtr, eq, 1);
            if (DBUG && eq->color)
                fprintf(outputFile, "]");
            fprintf(outputFile, "\n");
        }
    };
    fflush(outputFile);
}


void prettyPrintProblem(Problem *problemPtr)
{
    int e;
    int v;
    int live[maxGEQs];
    int v1, v2, v3;
    int t, change;
    int stuffPrinted = 0;


    typedef enum {
        none, le, lt
    } partialOrderType;

    partialOrderType po[maxVars][maxVars];
    int poE[maxVars][maxVars];
    int lastLinks[maxVars];
    int firstLinks[maxVars];
    int chainLength[maxVars];
    int chain[maxVars];
    int i, m, multiprint;


    if (!problemPtr->variablesInitialized)
        initializeVariables(problemPtr);

    if (nVars > 0) {
        eliminateRedundant(problemPtr, 0);

        for (e = 0; e < nEQ; e++) {
            if (stuffPrinted)
                fprintf(outputFile, "; ");
            stuffPrinted = 1;
            printEQ(&EQs[e]);
        };

        for (e = 0; e < nGEQ; e++)
            live[e] = TRUE;

        while (1) {
            for (v = 1; v <= nVars; v++) {
                lastLinks[v] = firstLinks[v] = 0;
                chainLength[v] = 0;
                for (v2 = 1; v2 <= nVars; v2++)
                    po[v][v2] = none;
            };

            for (e = 0; e < nGEQ; e++)
                if (live[e]) {
                    for (v = 1; v <= nVars; v++) {
                        if (GEQs[e].coef[v] == 1)
                            firstLinks[v]++;
                        else if (GEQs[e].coef[v] == -1)
                            lastLinks[v]++;
                    };

                    v1 = nVars;
                    while (v1 > 0 && GEQs[e].coef[v1] == 0)
                        v1--;
                    v2 = v1 - 1;
                    while (v2 > 0 && GEQs[e].coef[v2] == 0)
                        v2--;
                    v3 = v2 - 1;
                    while (v3 > 0 && GEQs[e].coef[v3] == 0)
                        v3--;

                    if (GEQs[e].coef[0] > 0 || GEQs[e].coef[0] < -1
                        || v2 <= 0 || v3 > 0
                        || GEQs[e].coef[v1] * GEQs[e].coef[v2] != -1) {
                        /* Not a partial order relation */

                    }
                    else {
                        if (GEQs[e].coef[v1] == 1) {
                            v3 = v2;
                            v2 = v1;
                            v1 = v3;
                        };
                        /* relation is v1 <= v2 or v1 < v2 */
                        po[v1][v2] = ((GEQs[e].coef[0] == 0) ? le : lt);
                        poE[v1][v2] = e;
                    };
                }
            for (v = 1; v <= nVars; v++)
                chainLength[v] = lastLinks[v];

            /* Just in case nVars <= 0 */
            change = FALSE;
            for (t = 0; t < nVars; t++) {
                change = FALSE;
                for (v1 = 1; v1 <= nVars; v1++)
                    for (v2 = 1; v2 <= nVars; v2++)
                        if (po[v1][v2] != none &&
                            chainLength[v1] <= chainLength[v2]) {
                            chainLength[v1] = chainLength[v2] + 1;
                            change = TRUE;
                        }
            };

            if (change) {
                /* caught in cycle */
                assert(0);
            };


            v = 1;
            for (v1 = 2; v1 <= nVars; v1++)
                if (chainLength[v1] + firstLinks[v1] > chainLength[v] + firstLinks[v])
                    v = v1;

            if (chainLength[v] == 0)
                break;

            if (stuffPrinted)
                fprintf(outputFile, "; ");
            stuffPrinted = 1;
            /* chain starts at v */
            /* print firstLinks */
            {
                int tmp, first;
                first = 1;
                for (e = 0; e < nGEQ; e++)
                    if (live[e] && GEQs[e].coef[v] == 1) {
                        if (!first)
                            fprintf(outputFile, ", ");
                        tmp = GEQs[e].coef[v];
                        GEQs[e].coef[v] = 0;
                        printTerm(problemPtr, &GEQs[e], -1);
                        GEQs[e].coef[v] = tmp;
                        live[e] = FALSE;
                        first = 0;
                    };
                if (!first)
                    fprintf(outputFile, " <= ");
            };


            /* find chain */
            chain[0] = v;
            m = 1;
            while (1) {
                /* print chain */
                for (v2 = 1; v2 <= nVars; v2++)
                    if (po[v][v2] && chainLength[v] == 1 + chainLength[v2])
                        break;
                if (v2 > nVars)
                    break;
                chain[m++] = v2;
                v = v2;
            }

            fprintf(outputFile, "%s", variable(chain[0]));

            multiprint = 0;
            for (i = 1; i < m; i++) {
                v = chain[i - 1];
                v2 = chain[i];
                if (po[v][v2] == le)
                    fprintf(outputFile, " <= ");
                else
                    fprintf(outputFile, " < ");
                fprintf(outputFile, "%s", variable(v2));
                live[poE[v][v2]] = FALSE;
                if (!multiprint && i < m - 1)
                    for (v3 = 1; v3 <= nVars; v3++) {
                        if (v == v3 || v2 == v3)
                            continue;
                        if (po[v][v2] != po[v][v3])
                            continue;
                        if (po[v2][chain[i + 1]] != po[v3][chain[i + 1]])
                            continue;
                        fprintf(outputFile, ",%s", variable(v3));
                        live[poE[v][v3]] = FALSE;
                        live[poE[v3][chain[i + 1]]] = FALSE;
                        multiprint = 1;
                    }
                else
                    multiprint = 0;
            };

            v = chain[m - 1];
            /* print lastLinks */
            {
                int tmp, first;
                first = 1;
                for (e = 0; e < nGEQ; e++)
                    if (live[e] && GEQs[e].coef[v] == -1) {
                        if (!first)
                            fprintf(outputFile, ", ");
                        else
                            fprintf(outputFile, " <= ");
                        tmp = GEQs[e].coef[v];
                        GEQs[e].coef[v] = 0;
                        printTerm(problemPtr, &GEQs[e], 1);
                        GEQs[e].coef[v] = tmp;
                        live[e] = FALSE;
                        first = 0;
                    };
            };
        };


        for (e = 0; e < nGEQ; e++)
            if (live[e]) {
                if (stuffPrinted)
                    fprintf(outputFile, "; ");
                stuffPrinted = 1;
                printGEQ(&GEQs[e]);
            };

        for (e = 0; e < nSUB; e++) {
            Eqn eq = &SUBs[e];
            if (stuffPrinted)
                fprintf(outputFile, "; ");
            stuffPrinted = 1;
            if (eq->key > 0)
                fprintf(outputFile, "%s := ", orgVariable(eq->key));
            else
                fprintf(outputFile, "#%d := ", eq->key);
            printTerm(problemPtr, eq, 1);
        };
    };
    fflush(outputFile);
}


static void nameWildcard(Problem *problemPtr, int i)
{
    --nextWildCard;
    if (nextWildCard < -maxWildCards)
        nextWildCard = -1;
    problemPtr->_var[i] = nextWildCard;
}

static int addNewWildcard(Problem *problemPtr)
{
    int e;
    int i = ++safeVars;
    problemPtr->addToVarsN(1);
    //nVars++;
    if (nVars != i) {
        for (e = nGEQ - 1; e >= 0; e--) {
            if (GEQs[e].coef[i] != 0)
                GEQs[e].touched = TRUE;
            GEQs[e].coef[nVars] = GEQs[e].coef[i];

        };
        for (e = nEQ - 1; e >= 0; e--) {
            EQs[e].coef[nVars] = EQs[e].coef[i];
        };
        for (e = nSUB - 1; e >= 0; e--) {
            SUBs[e].coef[nVars] = SUBs[e].coef[i];
        };
        problemPtr->_var[nVars] = problemPtr->_var[i];
    };
    for (e = nGEQ - 1; e >= 0; e--)
        GEQs[e].coef[i] = 0;
    for (e = nEQ - 1; e >= 0; e--)
        EQs[e].coef[i] = 0;
    for (e = nSUB - 1; e >= 0; e--)
        SUBs[e].coef[i] = 0;
    nameWildcard(problemPtr, i);
    return (i);
}

extern void substitute(Problem * problemPtr, Eqn sub, int i, int c); 
extern void deleteVariable(Problem *problemPt, int j);

static void doMod(Problem *problemPtr, int factor, int e, int j)
/* Solve e = factor alpha for x_j and substitute */
{
    int k, i;
    struct _eqn eq;
    int nFactor;
    int killJ = FALSE;
    eqncpy(&eq, &EQs[e]);
    for (k = nVars; k >= 0; k--) {
        eq.coef[k] = intMod(eq.coef[k], factor);
        if (2 * eq.coef[k] >= factor)
            eq.coef[k] -= factor;
    };
    nFactor = eq.coef[j];
    if (j <= safeVars && problemPtr->_var[j] > 0) {
        i = addNewWildcard(problemPtr);
        eq.coef[nVars] = eq.coef[i];
        eq.coef[j] = 0;
        eq.coef[i] = -factor;
        killJ = TRUE;
    }
    else {
        eq.coef[j] = -factor;
        if (problemPtr->_var[j] > 0)
            nameWildcard(problemPtr, j);
    };
    substitute(problemPtr, &eq, j, nFactor);
    for (k = nVars; k >= 0; k--)
        EQs[e].coef[k] = EQs[e].coef[k] / factor;
    if (killJ)
        deleteVariable(problemPtr, j);
    if (DEBUG) {
        fprintf(outputFile, "Mod-ing and normalizing produces:\n");
        printProblem(problemPtr);
    };
}

void
negateGEQ(Problem * problemPtr, int e)
{

    int i;
    for (i = nVars; i >= 0; i--)
        GEQs[e].coef[i] = -GEQs[e].coef[i];
    GEQs[e].coef[0]--;
    GEQs[e].touched = TRUE;
}

static int verifyProblem(Problem *problemPtr)
{
    int result, e, anyColor;
    Problem tmpProblem;
    /*tmpProblem = mallocProblem;
    if (tmpProblem == NULL)
    {
        printf("ERROR!!\n");
    }
    tmpProblem->_init();*/

    problemcpy(&tmpProblem, problemPtr);
    tmpProblem._safeVars = 0;
    tmpProblem.setNumSUBs(0);
    anyColor = 0;
    for (e = nGEQ - 1; e >= 0; e--)
        anyColor |= GEQs[e].color;
    anyColor |= pleaseNoEqualitiesInSimplifiedProblems;
    if (anyColor) {
        originalProblem = noProblem;
    }
    else
        originalProblem = problemPtr;
    if (DBUG) {
        fprintf(outputFile, "verifying problem");
        if (anyColor)
            fprintf(outputFile, " (color mode)");
        fprintf(outputFile, " :\n");
        printProblem(problemPtr);
    };

    result = solve(&tmpProblem, UNKNOWN);
    originalProblem = noProblem;
    //free(tmpProblem);
    if (DBUG) {
        if (result)
            fprintf(outputFile, "verified problem\n");
        else
            fprintf(outputFile, "disproved problem\n");
        printProblem(problemPtr);
    };
    return result;
}


#define implies(A,B) (A==(A&B))

void resurrectSubs(Problem * problemPtr);

int eliminateRedundant(Problem *problemPtr, bool expensive)
{
    int e, e1, e2, e3, p, q, i, k, alpha, alpha1, alpha2, alpha3;
    int c;
    int isDead[maxGEQs];
    unsigned int P[maxGEQs], Z[maxGEQs], N[maxGEQs];
    unsigned int PP, PZ, PN;	/* possible Positives, possible zeros & possible negatives */

    for (e = nGEQ - 1; e >= 0; e--) {
        int tmp = 1;
        isDead[e] = 0;
        P[e] = Z[e] = N[e] = 0;
        for (i = nVars; i >= 1; i--) {
            if (GEQs[e].coef[i] > 0)
                P[e] |= tmp;
            else if (GEQs[e].coef[i] < 0)
                N[e] |= tmp;
            else
                Z[e] |= tmp;
            tmp <<= 1;
        }
    }


    for (e1 = nGEQ - 1; e1 >= 0; e1--)
        if (!isDead[e1])
            for (e2 = e1 - 1; e2 >= 0; e2--)
                if (!isDead[e2]) {
                    for (p = nVars; p > 1; p--) {
                        for (q = p - 1; q > 0; q--) {
                            alpha = (GEQs[e1].coef[p] * GEQs[e2].coef[q] - GEQs[e2].coef[p] * GEQs[e1].coef[q]);
                            if (alpha != 0)
                                goto foundPQ;
                        };
                    };
                    continue;

                foundPQ:
                    PZ = (Z[e1] & Z[e2]) | (P[e1] & N[e2]) | (N[e1] & P[e2]);
                    PP = P[e1] | P[e2];
                    PN = N[e1] | N[e2];

                    for (e3 = nGEQ - 1; e3 >= 0; e3--)
                        if (e3 != e1 && e3 != e2) {

                            if (!implies(Z[e3], PZ))
                                goto nextE3;

                            alpha1 = GEQs[e2].coef[q] * GEQs[e3].coef[p] - GEQs[e2].coef[p] * GEQs[e3].coef[q];
                            alpha2 = -(GEQs[e1].coef[q] * GEQs[e3].coef[p] - GEQs[e1].coef[p] * GEQs[e3].coef[q]);
                            alpha3 = alpha;

                            if (alpha1 * alpha2 <= 0)
                                goto nextE3;
                            if (alpha1 < 0) {
                                alpha1 = -alpha1;
                                alpha2 = -alpha2;
                                alpha3 = -alpha3;
                            }
                            if (alpha3 > 0) {
                                /* Trying to prove e3 is redundant */
                                if (!implies(P[e3], PP) | !implies(N[e3], PN))
                                    goto nextE3;
                                if (!GEQs[e3].color && (GEQs[e1].color || GEQs[e2].color))
                                    goto nextE3;

                                /* verify alpha1*v1+alpha2*v2 = alpha3*v3 */
                                for (k = nVars; k >= 1; k--)
                                    if (alpha3 * GEQs[e3].coef[k]
                                        != alpha1 * GEQs[e1].coef[k] + alpha2 * GEQs[e2].coef[k])
                                        goto nextE3;

                                c = alpha1 * GEQs[e1].coef[0] + alpha2 * GEQs[e2].coef[0];
                                if (c < alpha3 * (GEQs[e3].coef[0] + 1)) {
                                    if (DBUG) {
                                        printProblem(problemPtr);
                                        fprintf(outputFile, "found redundant inequality\n");
                                        fprintf(outputFile, "alpha1, alpha2, alpha3 = %d,%d,%d\n",
                                            alpha1, alpha2, alpha3);

                                        printGEQ(&(GEQs[e1]));
                                        fprintf(outputFile, "\n");
                                        printGEQ(&(GEQs[e2]));
                                        fprintf(outputFile, "\n=> ");
                                        printGEQ(&(GEQs[e3]));
                                        fprintf(outputFile, "\n\n");
                                    };

                                    isDead[e3] = 1;
                                }
                            }
                            else {
                                /*
                                 * trying to prove e3 <= 0 and therefore e3 = 0, or trying to prove e3 < 0, and
                                 * therefore the problem has no solutions
                                 *
                                 */
                                if (!implies(P[e3], PN) | !implies(N[e3], PP))
                                    goto nextE3;
                                if (GEQs[e1].color || GEQs[e2].color || GEQs[e3].color)
                                    goto nextE3;

                                alpha3 = alpha3;
                                /* verify alpha1*v1+alpha2*v2 = alpha3*v3 */
                                for (k = nVars; k >= 1; k--)
                                    if (alpha3 * GEQs[e3].coef[k]
                                        != alpha1 * GEQs[e1].coef[k] + alpha2 * GEQs[e2].coef[k])
                                        goto nextE3;

                                c = alpha1 * GEQs[e1].coef[0] + alpha2 * GEQs[e2].coef[0];
                                if (c < alpha3 * (GEQs[e3].coef[0])) {

                                    /* We just proved e3 < 0, so no solutions exist */
                                    if (DBUG) {
                                        printProblem(problemPtr);
                                        fprintf(outputFile, "found implied over tight inequality\n");
                                        fprintf(outputFile, "alpha1, alpha2, alpha3 = %d,%d,%d\n",
                                            alpha1, alpha2, -alpha3);
                                        printGEQ(&(GEQs[e1]));
                                        fprintf(outputFile, "\n");
                                        printGEQ(&(GEQs[e2]));
                                        fprintf(outputFile, "\n=> not ");
                                        printGEQ(&(GEQs[e3]));
                                        fprintf(outputFile, "\n\n");
                                    };
                                    return (0);

                                }
                                else if (c < alpha3 * (GEQs[e3].coef[0] + 1)) {

                                    /* We just proved that e3 <=0, so e3 = 0 */
                                    if (DBUG) {
                                        printProblem(problemPtr);
                                        fprintf(outputFile, "found implied tight inequality\n");
                                        fprintf(outputFile, "alpha1, alpha2, alpha3 = %d,%d,%d\n",
                                            alpha1, alpha2, -alpha3);
                                        printGEQ(&(GEQs[e1]));
                                        fprintf(outputFile, "\n");
                                        printGEQ(&(GEQs[e2]));
                                        fprintf(outputFile, "\n=> inverse ");
                                        printGEQ(&(GEQs[e3]));
                                        fprintf(outputFile, "\n\n");
                                    };
                                    //eqncpy(&EQs[nEQ++], &GEQs[e3]);
                                    const int numEQ = nEQ;
                                    problemPtr->addNumEqs(1);
                                    eqncpy(&EQs[numEQ], &GEQs[e3]);
                                    

                                    assert(nEQ <= maxEQs);
                                    addingEqualityConstraint(problemPtr, nEQ - 1);
                                    isDead[e3] = 1;

                                }
                            }
                        nextE3:;
                        }
                }
    for (e = nGEQ - 1; e >= 0; e--)
        if (isDead[e])
            doDelete(e, nVars);

    /* if (nEQ) return (solve(problemPtr, SIMPLIFY)); */

    if (!expensive)
        return (1);
    {
        Problem tmpProblem;
        int oldTrace = trace;
        trace = 0;
        /*tmpProblem = mallocProblem;
        if (tmpProblem == NULL)
        {
            printf("ERROR!!\n");
        }
        tmpProblem->_init();*/

        conservative++;
        for (e = nGEQ - 1; e >= 0; e--) {
            if (DEBUG) {
                fprintf(outputFile, "checking equation %d to see if it is redundant: ", e);
                printGEQ(&(GEQs[e]));
                fprintf(outputFile, "\n");
            };
            problemcpy(&tmpProblem, problemPtr);
            negateGEQ(&tmpProblem, e);
            tmpProblem._safeVars = 0;
            tmpProblem.variablesFreed = 0;
            if (!solve(&tmpProblem, FALSE))
                doDelete(e, nVars);
        };
        trace = oldTrace;
        //free(tmpProblem);
        conservative--;
    };
#if reduceWithSubstitutions
#else
    resurrectSubs(problemPtr);
    assert(nSUB == 0);
#endif
    return (1);
}


int smoothWeirdEquations(Problem *problemPtr)
{
    int e1, e2, e3, p, q, k, alpha, alpha1, alpha2, alpha3;
    int c;
    int v;
    int result = 0;

    for (e1 = nGEQ - 1; e1 >= 0; e1--)
        if (!GEQs[e1].color) {
            int g = 999999;
            for (v = nVars; v >= 1; v--)
                if (GEQs[e1].coef[v] != 0 && abs(GEQs[e1].coef[v]) < g)
                    g = abs(GEQs[e1].coef[v]);
            if (g > 20) {

                e3 = nGEQ;
                for (v = nVars; v >= 1; v--)
                    GEQs[e3].coef[v] = intDiv(6 * GEQs[e1].coef[v] + g / 2, g);
                GEQs[e3].color = 0;
                GEQs[e3].touched = 1;
                GEQs[e3].coef[0] = 9997;
                if (DBUG) {
                    fprintf(outputFile, "Checking to see if we can derive: ");
                    printGEQ(&GEQs[e3]);
                    fprintf(outputFile, "\n from: ");
                    printGEQ(&GEQs[e1]);
                    fprintf(outputFile, "\n");
                };


                for (e2 = nGEQ - 1; e2 >= 0; e2--)
                    if (e1 != e2 && !GEQs[e2].color) {
                        for (p = nVars; p > 1; p--) {
                            for (q = p - 1; q > 0; q--) {
                                alpha = (GEQs[e1].coef[p] * GEQs[e2].coef[q] - GEQs[e2].coef[p] * GEQs[e1].coef[q]);
                                if (alpha != 0)
                                    goto foundPQ;
                            };
                        };
                        continue;

                    foundPQ:

                        alpha1 = GEQs[e2].coef[q] * GEQs[e3].coef[p] - GEQs[e2].coef[p] * GEQs[e3].coef[q];
                        alpha2 = -(GEQs[e1].coef[q] * GEQs[e3].coef[p] - GEQs[e1].coef[p] * GEQs[e3].coef[q]);
                        alpha3 = alpha;

                        if (alpha1 * alpha2 <= 0)
                            continue;
                        if (alpha1 < 0) {
                            alpha1 = -alpha1;
                            alpha2 = -alpha2;
                            alpha3 = -alpha3;
                        }
                        if (alpha3 > 0) {
                            /* Trying to prove e3 is redundant */

                            /* verify alpha1*v1+alpha2*v2 = alpha3*v3 */
                            for (k = nVars; k >= 1; k--)
                                if (alpha3 * GEQs[e3].coef[k]
                                    != alpha1 * GEQs[e1].coef[k] + alpha2 * GEQs[e2].coef[k])
                                    goto nextE2;

                            c = alpha1 * GEQs[e1].coef[0] + alpha2 * GEQs[e2].coef[0];
                            if (c < alpha3 * (GEQs[e3].coef[0] + 1))
                                GEQs[e3].coef[0] = intDiv(c, alpha3);

                        }
                    nextE2:;
                    }
                if (GEQs[e3].coef[0] < 9997) {
                    result++;
                    problemPtr->addNumGEqs(1);
                    //nGEQ++;
                    if (DBUG) {
                        fprintf(outputFile, "Smoothing wierd equations; adding:\n");
                        printGEQ(&GEQs[e3]);
                        fprintf(outputFile, "\nto:\n");
                        printProblem(problemPtr);
                        fprintf(outputFile, "\n\n");
                    };
                };
            }
        }
    return (result);
}

void
coalesce(Problem * problemPtr)
{
    int e, e2, colors;
    int isDead[maxGEQs];

    colors = 0;
    for (e = 0; e < nGEQ; e++)
        if (GEQs[e].color)
            colors++;
    if (colors < 2)
        return;
    for (e = 0; e < nGEQ; e++)
        isDead[e] = 0;
    for (e = 0; e < nGEQ; e++)
        if (GEQs[e].color)
            for (e2 = e + 1; e2 < nGEQ; e2++)
                if (GEQs[e].key == -GEQs[e2].key
                    && GEQs[e].coef[0] == -GEQs[e2].coef[0]) 
                {
                    const int numEQ = nEQ;
                    problemPtr->addNumEqs(1);
                    eqncpy(&EQs[numEQ], &GEQs[e]);
                    
                    assert(nEQ <= maxEQs);
                    isDead[e] = 1;
                    isDead[e2] = 1;
                };
    for (e = nGEQ - 1; e >= 0; e--)
        if (isDead[e]) {
            doDelete(e, nVars);
        }
}

void eliminateRed(Problem *problemPtr, bool eliminateAll)
{
    int e, e2, e3, i, j, k, a, alpha1, alpha2;
    int c = 0;
    int isDead[maxGEQs];
    int deadCount = 0;

    if (DEBUG) {
        fprintf(outputFile, "in eliminate RED:\n");
        printProblem(problemPtr);
    };
    if (nEQ > 0) {
        simplifyProblem(problemPtr);
    };

    for (e = nGEQ - 1; e >= 0; e--)
        isDead[e] = 0;
    for (e = nGEQ - 1; e >= 0; e--)
        if (!GEQs[e].color && !isDead[e])
            for (e2 = e - 1; e2 >= 0; e2--)
                if (!GEQs[e2].color && !isDead[e2]) {
                    a = 0;
                    for (i = nVars; i > 1; i--) {
                        for (j = i - 1; j > 0; j--) {
                            a = (GEQs[e].coef[i] * GEQs[e2].coef[j] - GEQs[e2].coef[i] * GEQs[e].coef[j]);
                            if (a != 0)
                                goto foundPair;
                        };
                    };
                    continue;

                foundPair:
                    if (DEBUG) {
                        fprintf(outputFile, "found two equations to combine, i = %s, ", variable(i));
                        fprintf(outputFile, "j = %s, alpha = %d\n", variable(j), a);
                        printGEQ(&(GEQs[e]));
                        fprintf(outputFile, "\n");
                        printGEQ(&(GEQs[e2]));
                        fprintf(outputFile, "\n");
                    };
                    for (e3 = nGEQ - 1; e3 >= 0; e3--)
                        if (GEQs[e3].color) {
                            alpha1 = GEQs[e2].coef[j] * GEQs[e3].coef[i] - GEQs[e2].coef[i] * GEQs[e3].coef[j];
                            alpha2 = -(GEQs[e].coef[j] * GEQs[e3].coef[i] - GEQs[e].coef[i] * GEQs[e3].coef[j]);
                            if ((a > 0 && alpha1 > 0 && alpha2 > 0) || (a < 0 && alpha1 < 0 && alpha2 < 0)) {
                                if (DEBUG) {
                                    fprintf(outputFile, "alpha1 = %d, alpha2 = %d; comparing against: ", alpha1, alpha2);
                                    printGEQ(&(GEQs[e3]));
                                    fprintf(outputFile, "\n");
                                };
                                for (k = nVars; k >= 0; k--) {
                                    c = alpha1 * GEQs[e].coef[k] + alpha2 * GEQs[e2].coef[k];
                                    if (c != a * GEQs[e3].coef[k])
                                        break;
                                    if (DEBUG && k > 0)
                                        fprintf(outputFile, " %s: %d, %d\n", variable(k), c, a * GEQs[e3].coef[k]);
                                };
                                if (k < 0
                                    || (k == 0 &&
                                    ((a > 0 && c < a * GEQs[e3].coef[k]) || (a < 0 && c > a * GEQs[e3].coef[k])))) {
                                    if (DEBUG) {
                                        deadCount++;
                                        fprintf(outputFile, "red equation#%d is dead (%d dead so far, %d remain)\n",
                                            e3, deadCount, nGEQ - deadCount);
                                        printGEQ(&(GEQs[e]));
                                        fprintf(outputFile, "\n");
                                        printGEQ(&(GEQs[e2]));
                                        fprintf(outputFile, "\n");
                                        printGEQ(&(GEQs[e3]));
                                        fprintf(outputFile, "\n");
                                    };
                                    isDead[e3] = 1;
                                };
                            };
                        };
                };
    for (e = nGEQ - 1; e >= 0; e--)
        if (isDead[e])
            doDelete(e, nVars);


    if (DBUG) {
        fprintf(outputFile, "in eliminate RED, easy tests done:\n");
        printProblem(problemPtr);
    };

    {
        int redFound = 0;
        for (e = nGEQ - 1; e >= 0; e--)
            if (GEQs[e].color)
                redFound = 1;
        if (!redFound) {
            if (DBUG)
                fprintf(outputFile, "fast checks worked\n");
#if reduceWithSubstitutions
#else
            assert(pleaseNoEqualitiesInSimplifiedProblems || nSUB == 0);
#endif
            return;
        };
    }

#ifndef verifySimplication
    if (!verifyProblem(problemPtr))
        return;
#endif

    {
        Problem tmpProblem;
        int oldTrace = trace;
        trace = 0;
        conservative++;
        /*tmpProblem = mallocProblem;
        if (tmpProblem == NULL)
        {
            printf("ERROR!!\n");
        }
        tmpProblem->_init();*/

        for (e = nGEQ - 1; e >= 0; e--)
            if (GEQs[e].color) {
                if (DBUG) {
                    fprintf(outputFile, "checking equation %d to see if it is redundant: ", e);
                    printGEQ(&(GEQs[e]));
                    fprintf(outputFile, "\n");
                };
                problemcpy(&tmpProblem, problemPtr);
                negateGEQ(&tmpProblem, e);
                tmpProblem._safeVars = 0;
                tmpProblem.variablesFreed = 0;
                tmpProblem.setNumSUBs(0);
                if (!solve(&tmpProblem, FALSE)) {
                    if (DBUG)
                        fprintf(outputFile, "it is redundant\n");
                    doDelete(e, nVars);
                }
                else {
                    if (DBUG)
                        fprintf(outputFile, "it is not redundant\n");
                    if (!eliminateAll) {
                        if (DBUG)
                            fprintf(outputFile, "no need to check other red equations\n");
                        break;
                    }
                };
            };
        trace = oldTrace;
        conservative--;

        //free(tmpProblem);
    };
    /* simplifyProblem(problemPtr); */
#if reduceWithSubstitutions
#else
    assert(pleaseNoEqualitiesInSimplifiedProblems || nSUB == 0);
#endif
}



void swap(int *i, int *j)
{
    int tmp;
    tmp = *i;
    *i = *j;
    *j = tmp;
}

void chainUnprotect(Problem *problemPtr)
{
    int i, e;
    int unprotect[maxVars];
    for (i = 1; i <= problemPtr->_safeVars; i++) {
        unprotect[i] = (problemPtr->_var[i] < 0);
        for (e = nSUB - 1; e >= 0; e--)
            if (SUBs[e].coef[i])
                unprotect[i] = 0;
    };
    if (DBUG) {
        fprintf(outputFile, "Doing chain reaction unprotection\n");
        printProblem(problemPtr);
        for (i = 1; i <= problemPtr->_safeVars; i++)
            if (unprotect[i])
                fprintf(outputFile, "unprotecting %s\n", variable(i));
    };
    for (i = 1; i <= problemPtr->_safeVars; i++)
        if (unprotect[i]) {
            /* wild card */
            if (i < problemPtr->_safeVars) {
                int j = problemPtr->_safeVars;
                swap(&problemPtr->_var[i], &problemPtr->_var[j]);
                for (e = nGEQ - 1; e >= 0; e--) {
                    GEQs[e].touched = 1;
                    swap(&GEQs[e].coef[i], &GEQs[e].coef[j]);
                };
                for (e = nEQ - 1; e >= 0; e--)
                    swap(&EQs[e].coef[i], &EQs[e].coef[j]);
                for (e = nSUB - 1; e >= 0; e--)
                    swap(&SUBs[e].coef[i], &SUBs[e].coef[j]);
                swap(&unprotect[i], &unprotect[j]);
                i--;
            };
            problemPtr->_safeVars--;
        };
    if (DBUG) {
        fprintf(outputFile, "After chain reactions\n");
        printProblem(problemPtr);
    };
}

void
resurrectSubs(Problem * problemPtr)
{
    if (problemPtr->getNumSUBs() > 0 && !pleaseNoEqualitiesInSimplifiedProblems) {
        int i, e, n, m;
        if (DBUG) {
            fprintf(outputFile,
                "problem reduced, bringing variables back to life\n");
            printProblem(problemPtr);
        };
        for (i = 1; i <= problemPtr->_safeVars; i++)
            if (problemPtr->_var[i] < 0) {
                /* wild card */
                if (i < problemPtr->_safeVars) {
                    int j = problemPtr->_safeVars;
                    swap(&problemPtr->_var[i], &problemPtr->_var[j]);
                    for (e = nGEQ - 1; e >= 0; e--) {
                        GEQs[e].touched = 1;
                        swap(&GEQs[e].coef[i], &GEQs[e].coef[j]);
                    };
                    for (e = nEQ - 1; e >= 0; e--)
                        swap(&EQs[e].coef[i], &EQs[e].coef[j]);
                    for (e = nSUB - 1; e >= 0; e--)
                        swap(&SUBs[e].coef[i], &SUBs[e].coef[j]);
                    i--;
                };
                problemPtr->_safeVars--;
            };

        m = problemPtr->getNumSUBs();
        n = max(nVars, problemPtr->_safeVars + m);
        for (e = nGEQ - 1; e >= 0; e--) 
        {
            if (singleVarGEQ(GEQs[e], nVars)) 
            {
                i = abs(GEQs[e].key);
                if (i >= problemPtr->_safeVars + 1)
                    GEQs[e].key += (GEQs[e].key > 0 ? m : -m);
            }
            else 
            {
                GEQs[e].touched = TRUE;
                GEQs[e].key = 0;
            }
        }

        const int tmpNV = nVars;
        problemPtr->addToVarsN(m);

        for (i = tmpNV; i >= problemPtr->_safeVars + 1; i--)
        {
            problemPtr->_var[i + m] = problemPtr->_var[i];
            for (e = nGEQ - 1; e >= 0; e--)
                GEQs[e].coef[i + m] = GEQs[e].coef[i];
            for (e = nEQ - 1; e >= 0; e--)
                EQs[e].coef[i + m] = EQs[e].coef[i];
            for (e = nSUB - 1; e >= 0; e--)
                SUBs[e].coef[i + m] = SUBs[e].coef[i];
        }
        
        for (i = problemPtr->_safeVars + m; i >= problemPtr->_safeVars + 1; i--) 
        {
            for (e = nGEQ - 1; e >= 0; e--)
                GEQs[e].coef[i] = 0;
            for (e = nEQ - 1; e >= 0; e--)
                EQs[e].coef[i] = 0;
            for (e = nSUB - 1; e >= 0; e--)
                SUBs[e].coef[i] = 0;
        }        
        //nVars += m;

        for (e = nSUB - 1; e >= 0; e--) 
        {
            problemPtr->_var[problemPtr->_safeVars + 1 + e] = SUBs[e].key;

            const int numEQ = nEQ;
            problemPtr->addNumEqs(1);

            eqncpy(&(EQs[numEQ]), &(SUBs[e]));
            EQs[numEQ].coef[problemPtr->_safeVars + 1 + e] = -1;
            if (DBUG) 
            {
                fprintf(outputFile, "brought back: ");
                printEQ(&EQs[numEQ]);
                fprintf(outputFile, "\n");
            }            
            //nEQ++;
            assert(nEQ <= maxEQs);
        }
        problemPtr->_safeVars += m;
        //nSUB = 0;

        problemPtr->setNumSUBs(0);
        for (i = problemPtr->_safeVars + 1; i <= nVars; i++) {
            for (e = nGEQ - 1; e >= 0; e--)
                if (GEQs[e].color && GEQs[e].coef[i]) {
                    /* variable i is in red equations */
                    int e2;
                    for (e2 = nEQ - 1; e2 >= 0; e2--)
                        if (EQs[e2].coef[i])
                            EQs[e2].color = 1;
                    break;
                }
        }

        if (DBUG) {
            fprintf(outputFile, "variables brought back to life\n");
            printProblem(problemPtr);
        };
    }
}


static void problemReduced(Problem *problemPtr)
{
#ifdef verifySimplification
    int result;
    result = verifyProblem(problemPtr);
    if (result && nEQ > 0)
        doItAgain = 1;
    else if (result)
#endif
    {
#ifdef eliminateRedundantConstraints
        if (!eliminateRedundant(problemPtr, 1))
            return;
#endif
        foundReduction = TRUE;
        if (!pleaseNoEqualitiesInSimplifiedProblems)
            coalesce(problemPtr);
        if (reduceWithSubs || pleaseNoEqualitiesInSimplifiedProblems)
            chainUnprotect(problemPtr);
        else
            resurrectSubs(problemPtr);

#ifndef singleResult
        (*whenReduced) (problemPtr);
#endif
        if (omegaPrintResult == 1) {
            fprintf(outputFile, "-------------------------------------------\n");
            fprintf(outputFile, "problem reduced:\n");
            printProblem(problemPtr);
            fprintf(outputFile, "-------------------------------------------\n");
        };


    };
}


static void freeEliminations(Problem *problemPtr, int fv)
/* do free eliminations */
{
    int tryAgain = 1;
    int i, e, e2;
    int nV = nVars;
    while (tryAgain) {
        tryAgain = 0;
        for (i = nV; i > fv; i--) {
            for (e = nGEQ - 1; e >= 0; e--)
                if (GEQs[e].coef[i])
                    break;
            if (e < 0)
                e2 = e;
            else if (GEQs[e].coef[i] > 0) {
                for (e2 = e - 1; e2 >= 0; e2--)
                    if (GEQs[e2].coef[i] < 0)
                        break;
            }
            else {
                for (e2 = e - 1; e2 >= 0; e2--)
                    if (GEQs[e2].coef[i] > 0)
                        break;
            };
            if (e2 < 0) {
                int e3;
                for (e3 = nSUB - 1; e3 >= 0; e3--)
                    if (SUBs[e3].coef[i])
                        break;
                if (e3 >= 0)
                    continue;
                for (e3 = nEQ - 1; e3 >= 0; e3--)
                    if (EQs[e3].coef[i])
                        break;
                if (e3 >= 0)
                    continue;
                if (DBUG)
                    fprintf(outputFile, "a free elimination of %s\n", variable(i));
                if (e >= 0) {
                    doDelete(e, nV);
                    for (e--; e >= 0; e--)
                        if (GEQs[e].coef[i])
                            doDelete(e, nV);
                    tryAgain = (i < nV);
                };
                deleteVariable(problemPtr, i);
                nV = nVars;
            };
        };
    };

    if (DEBUG) {
        fprintf(outputFile, "\nafter free eliminations:\n");
        printProblem(problemPtr);
        fprintf(outputFile, "\n");
    };
}

static void freeRedEliminations(Problem * problemPtr)
/* do free red eliminations */
{
    int tryAgain = 1;
    int i, e, e2;
    int nV = nVars;
    int isRedVar[maxVars];
    int isDeadVar[maxVars];
    int isDeadGEQ[maxGEQs];
    for (i = nV; i > 0; i--) {
        isRedVar[i] = 0;
        isDeadVar[i] = 0;
    };
    for (e = nGEQ - 1; e >= 0; e--) {
        isDeadGEQ[e] = 0;
        if (GEQs[e].color)
            for (i = nV; i > 0; i--)
                if (GEQs[e].coef[i] != 0)
                    isRedVar[i] = 1;
    };

    while (tryAgain) {
        tryAgain = 0;
        for (i = nV; i > 0; i--)
            if (!isRedVar[i] && !isDeadVar[i]) {
                for (e = nGEQ - 1; e >= 0; e--)
                    if (!isDeadGEQ[e] && GEQs[e].coef[i])
                        break;
                if (e < 0)
                    e2 = e;
                else if (GEQs[e].coef[i] > 0) {
                    for (e2 = e - 1; e2 >= 0; e2--)
                        if (!isDeadGEQ[e2] && GEQs[e2].coef[i] < 0)
                            break;
                }
                else {
                    for (e2 = e - 1; e2 >= 0; e2--)
                        if (!isDeadGEQ[e2] && GEQs[e2].coef[i] > 0)
                            break;
                };
                if (e2 < 0) {
                    int e3;
                    for (e3 = nSUB - 1; e3 >= 0; e3--)
                        if (SUBs[e3].coef[i])
                            break;
                    if (e3 >= 0)
                        continue;
                    for (e3 = nEQ - 1; e3 >= 0; e3--)
                        if (EQs[e3].coef[i])
                            break;
                    if (e3 >= 0)
                        continue;
                    if (DBUG)
                        fprintf(outputFile, "a free red elimination of %s\n", variable(i));
                    for (; e >= 0; e--)
                        if (GEQs[e].coef[i])
                            isDeadGEQ[e] = 1;
                    tryAgain = 1;
                    isDeadVar[i] = 1;
                };
            };
    };

    for (e = nGEQ - 1; e >= 0; e--)
        if (isDeadGEQ[e])
            doDelete(e, nV);

    for (i = nV; i > 0; i--)
        if (isDeadVar[i])
            deleteVariable(problemPtr, i);


    if (DEBUG) {
        fprintf(outputFile, "\nafter free red eliminations:\n");
        printProblem(problemPtr);
        fprintf(outputFile, "\n");
    };
}

void addingEqualityConstraint(Problem *problemPtr, int e)
{
    int e2, i, j;

    if (originalProblem != noProblem && originalProblem != problemPtr && !conservative) 
    {
        //e2 = originalProblem->_numEQs++;
        e2 = originalProblem->getNumEqs();
        originalProblem->addNumEqs(1);

        if (DBUG)
            fprintf(outputFile,
                "adding equality constraint %d to outer problem\n",
                e2);
        eqnnzero(&originalProblem->_EQs[e2], originalProblem->getVarsN());
        for (i = nVars; i >= 1; i--) {
            for (j = originalProblem->getVarsN(); j >= 1; j--)
                if (originalProblem->_var[j] == problemPtr->_var[i])
                    break;
            if (j <= 0) {
                if (DBUG)
                    fprintf(outputFile, "retracting\n");
                //originalProblem->_numEQs--;
                originalProblem->addNumEqs(-1);
                return;
            };
            originalProblem->_EQs[e2].coef[j] = EQs[e].coef[i];
        };
        originalProblem->_EQs[e2].coef[0] = EQs[e].coef[0];
        if (DBUG)
            printProblem(originalProblem);
    };
}




void substitute(Problem * problemPtr, Eqn sub, int i, int c)
{
    int e, j, j0, k;
    int topVar;

    {
        int *p = &packing[0];
        for (k = nVars; k >= 0; k--)
            if (sub->coef[k])
                *(p++) = k;
        topVar = (p - &packing[0]) - 1;
    };


    if (DBUG || doTrace) {
        fprintf(outputFile, "substituting using %s := ", variable(i));
        printTerm(problemPtr, sub, -c);
        fprintf(outputFile, "\n");
        printVars(problemPtr);
    };

    if (topVar < 0) {
        for (e = nEQ - 1; e >= 0; e--)
            EQs[e].coef[i] = 0;
        for (e = nGEQ - 1; e >= 0; e--)
            if (GEQs[e].coef[i] != 0) {
                GEQs[e].touched = TRUE;
                GEQs[e].coef[i] = 0;
            };
        for (e = nSUB - 1; e >= 0; e--)
            SUBs[e].coef[i] = 0;

        if (i <= problemPtr->_safeVars && problemPtr->_var[i] >= 0) {
            //Eqn eqn = &(SUBs[nSUB++]);
            problemPtr->addNumSUBs(1);
            Eqn eqn = &(SUBs[nSUB - 1]);            

            for (k = nVars; k >= 0; k--)
                eqn->coef[k] = 0;
            eqn->key = problemPtr->_var[i];
            eqn->color = 0;
        };
    }
    else if (topVar == 0 && packing[0] == 0) {
        c = -sub->coef[0] * c;
        for (e = nEQ - 1; e >= 0; e--) {
            EQs[e].coef[0] += EQs[e].coef[i] * c;
            EQs[e].coef[i] = 0;
        };
        for (e = nGEQ - 1; e >= 0; e--)
            if (GEQs[e].coef[i] != 0) {
                GEQs[e].coef[0] += GEQs[e].coef[i] * c;
                GEQs[e].coef[i] = 0;
                GEQs[e].touched = TRUE;
            };
        for (e = nSUB - 1; e >= 0; e--) {
            SUBs[e].coef[0] += SUBs[e].coef[i] * c;
            SUBs[e].coef[i] = 0;
        };
        if (i <= problemPtr->_safeVars && problemPtr->_var[i] >= 0) {
            //Eqn eqn = &(SUBs[nSUB++]);
            problemPtr->addNumSUBs(1);
            Eqn eqn = &(SUBs[nSUB - 1]);            

            for (k = nVars; k >= 1; k--)
                eqn->coef[k] = 0;
            eqn->coef[0] = c;
            eqn->key = problemPtr->_var[i];
            eqn->color = 0;
        };
    }
    else {
        for (e = nEQ - 1; e >= 0; e--) {
            Eqn eqn = &(EQs[e]);
            k = eqn->coef[i];
            if (k != 0) {
                k = c * k;
                eqn->coef[i] = 0;
                for (j = topVar; j >= 0; j--) {
                    j0 = packing[j];
                    eqn->coef[j0] -= sub->coef[j0] * k;
                };
            };
            if (DEBUG) {
                printEQ(eqn);
                fprintf(outputFile, "\n");
            };
        };
        for (e = nGEQ - 1; e >= 0; e--) {
            Eqn eqn = &(GEQs[e]);
            k = eqn->coef[i];
            if (k != 0) {
                k = c * k;
                eqn->touched = TRUE;
                eqn->coef[i] = 0;
                for (j = topVar; j >= 0; j--) {
                    j0 = packing[j];
                    eqn->coef[j0] -= sub->coef[j0] * k;
                };
            };
            if (DEBUG) {
                printGEQ(eqn);
                fprintf(outputFile, "\n");
            };
        };
        for (e = nSUB - 1; e >= 0; e--) {
            Eqn eqn = &(SUBs[e]);
            k = eqn->coef[i];
            if (k != 0) {
                k = c * k;
                eqn->coef[i] = 0;
                for (j = topVar; j >= 0; j--) {
                    j0 = packing[j];
                    eqn->coef[j0] -= sub->coef[j0] * k;
                };
            };
            if (DEBUG) {
                fprintf(outputFile, "%s := ", orgVariable(eqn->key));
                printTerm(problemPtr, eqn, 1);
                fprintf(outputFile, "\n");
            };
        };

        if (DEBUG)
            fprintf(outputFile, "---\n\n");
        if (i <= problemPtr->_safeVars && problemPtr->_var[i] >= 0) {
            Eqn eqn;
            //eqn = &(SUBs[nSUB++]);
            problemPtr->addNumSUBs(1);
            eqn = &(SUBs[nSUB - 1]);            

            c = -c;
            for (k = nVars; k >= 0; k--)
                eqn->coef[k] = c * (sub->coef[k]);
            eqn->key = problemPtr->_var[i];
            eqn->color = sub->color;
        };
    };

}

void substituteRed(Problem *problemPtr, Eqn sub, int i, int c, bool * foundBlack)
{
    int e, j, j0, k;
    int topVar;

    {
        int *p = &packing[0];
        for (k = nVars; k >= 0; k--)
            if (sub->coef[k])
                *(p++) = k;
        topVar = (p - &packing[0]) - 1;
    };

    *foundBlack = 0;

    if (DBUG || doTrace) {
        if (sub->color)
            fprintf(outputFile, "[");
        fprintf(outputFile, "substituting using %s := ", variable(i));
        printTerm(problemPtr, sub, -c);
        if (sub->color)
            fprintf(outputFile, "]");
        fprintf(outputFile, "\n");
        printVars(problemPtr);
    };

    for (e = nEQ - 1; e >= 0; e--) {
        Eqn eqn = &(EQs[e]);
        k = eqn->coef[i];
        if (k != 0) {
            if (!eqn->color)
                *foundBlack = 1;
            else {
                k = c * k;
                eqn->coef[i] = 0;
                for (j = topVar; j >= 0; j--) {
                    j0 = packing[j];
                    eqn->coef[j0] -= sub->coef[j0] * k;
                };
            };
        };
        if (DEBUG) {
            printEQ(eqn);
            fprintf(outputFile, "\n");
        };
    };
    for (e = nGEQ - 1; e >= 0; e--) {
        Eqn eqn = &(GEQs[e]);
        k = eqn->coef[i];
        if (k != 0) {
            if (!eqn->color)
                *foundBlack = 1;
            else {
                k = c * k;
                eqn->touched = TRUE;
                eqn->coef[i] = 0;
                for (j = topVar; j >= 0; j--) {
                    j0 = packing[j];
                    eqn->coef[j0] -= sub->coef[j0] * k;
                };
            };
        };
        if (DEBUG) {
            printGEQ(eqn);
            fprintf(outputFile, "\n");
        };
    };
    for (e = nSUB - 1; e >= 0; e--) {
        Eqn eqn = &(SUBs[e]);
        k = eqn->coef[i];
        if (k != 0) {
            if (!eqn->color)
                *foundBlack = 1;
            else {
                k = c * k;
                eqn->coef[i] = 0;
                for (j = topVar; j >= 0; j--) {
                    j0 = packing[j];
                    eqn->coef[j0] -= sub->coef[j0] * k;
                };
            };
        };
        if (DEBUG) {
            fprintf(outputFile, "%s := ", orgVariable(eqn->key));
            printTerm(problemPtr, eqn, 1);
            fprintf(outputFile, "\n");
        };
    };

    if (DEBUG)
        fprintf(outputFile, "---\n\n");
    if (i <= problemPtr->_safeVars && problemPtr->_var[i] >= 0) {
        *foundBlack = 1;
    };

}



void deleteVariable(Problem *problemPtr, int i)
{
    int nV = nVars;
    int e;
    if (i < safeVars) {
        int j = safeVars;
        for (e = nGEQ - 1; e >= 0; e--) {
            GEQs[e].touched = TRUE;
            GEQs[e].coef[i] = GEQs[e].coef[j];
            GEQs[e].coef[j] = GEQs[e].coef[nV];
        };
        for (e = nEQ - 1; e >= 0; e--) {
            EQs[e].coef[i] = EQs[e].coef[j];
            EQs[e].coef[j] = EQs[e].coef[nV];
        };
        for (e = nSUB - 1; e >= 0; e--) {
            SUBs[e].coef[i] = SUBs[e].coef[j];
            SUBs[e].coef[j] = SUBs[e].coef[nV];
        };
        problemPtr->_var[i] = problemPtr->_var[j];
        problemPtr->_var[j] = problemPtr->_var[nV];
    }
    else if (i < nV) {
        for (e = nGEQ - 1; e >= 0; e--)
            if (GEQs[e].coef[nV]) {
                GEQs[e].coef[i] = GEQs[e].coef[nV];
                GEQs[e].touched = TRUE;
            };
        for (e = nEQ - 1; e >= 0; e--)
            EQs[e].coef[i] = EQs[e].coef[nV];
        for (e = nSUB - 1; e >= 0; e--)
            SUBs[e].coef[i] = SUBs[e].coef[nV];
        problemPtr->_var[i] = problemPtr->_var[nV];
    };
    if (i <= safeVars)
        safeVars--;
    problemPtr->addToVarsN(-1);
    //nVars--;
}

static void convertEQtoGEQs(Problem * problemPtr, int eq)
{
    int i;
    if (DBUG)
        fprintf(outputFile, "Converting Eq to GEQs\n");

    int numGE = nGEQ;
    problemPtr->addNumGEqs(1);

    eqncpy(&GEQs[numGE], &EQs[eq]);
    GEQs[numGE].touched = 1;
    //nGEQ++;
    
    numGE = nGEQ;
    problemPtr->addNumGEqs(1);

    eqncpy(&GEQs[numGE], &EQs[eq]);
    GEQs[numGE].touched = 1;
    for (i = 0; i <= nVars; i++)
        GEQs[numGE].coef[i] = -GEQs[numGE].coef[i];
    //nGEQ++;
    
    if (DBUG)
        printProblem(problemPtr);
}


static void  doElimination(Problem *problemPtr, int e, int i)
{
    struct _eqn sub;
    int c;
    int nV = nVars;
    if (DBUG || doTrace)
        fprintf(outputFile, "eliminating variable %s\n", variable(i));
    eqncpy(&sub, &EQs[e]);
    c = sub.coef[i];
    sub.coef[i] = 0;
    if (c == 1 || c == -1) {
        if (EQs[e].color) {
            bool fB;
            substituteRed(problemPtr, &sub, i, c, &fB);
            if (fB)
                convertEQtoGEQs(problemPtr, e);
            else
                deleteVariable(problemPtr, i);
        }
        else {
            substitute(problemPtr, &sub, i, c);
            deleteVariable(problemPtr, i);
        }
    }
    else {
        int a = abs(c);
        if (TRACE)
            fprintf(outputFile, "performing non-exact elimination, c = %d\n", c);
        assert(inApproximateMode);
        for (e = nEQ - 1; e >= 0; e--)
            if (EQs[e].coef[i]) {
                Eqn eqn = &(EQs[e]);
                int j, k;
                for (j = nV; j >= 0; j--)
                    eqn->coef[j] *= a;
                k = eqn->coef[i];
                eqn->coef[i] = 0;
                for (j = nV; j >= 0; j--)
                    eqn->coef[j] -= sub.coef[j] * k / c;
            };
        for (e = nGEQ - 1; e >= 0; e--)
            if (GEQs[e].coef[i]) {
                Eqn eqn = &(GEQs[e]);
                int j, k;
                for (j = nV; j >= 0; j--)
                    eqn->coef[j] *= a;
                k = eqn->coef[i];
                eqn->coef[i] = 0;
                for (j = nV; j >= 0; j--)
                    eqn->coef[j] -= sub.coef[j] * k / c;
                eqn->touched = 1;
            };
        for (e = nSUB - 1; e >= 0; e--)
            if (SUBs[e].coef[i]) {
                Eqn eqn = &(SUBs[e]);
                int j, k;
                assert(0);
                for (j = nV; j >= 0; j--)
                    eqn->coef[j] *= a;
                k = eqn->coef[i];
                eqn->coef[i] = 0;
                for (j = nV; j >= 0; j--)
                    eqn->coef[j] -= sub.coef[j] * k / c;
            };
        deleteVariable(problemPtr, i);
    };
}
 
static int solveEQ(Problem *problemPtr, int desiredResult)
{
    int i, j, e;
    int g, g2;
    g = 0;


    if (DBUG && nEQ > 0) {
        fprintf(outputFile, "\nSolveEQ\n");
        printProblem(problemPtr);
        fprintf(outputFile, "\n");
    };

    if (mayBeRed) {
        i = 0;
        j = nEQ - 1;
        while (1) {
            struct _eqn eq;
            while (i <= j && EQs[i].color)
                i++;
            while (i <= j && !EQs[j].color)
                j--;
            if (i >= j)
                break;
            eqncpy(&eq, &EQs[i]);
            eqncpy(&EQs[i], &EQs[j]);
            eqncpy(&EQs[j], &eq);
            i++;
            j--;
        };
    };



    /* Eliminate all EQ equations */
    for (e = nEQ - 1; e >= 0; e--) {
        Eqn eqn = &(EQs[e]);
        int sv;

        if (inApproximateMode && !nGEQ && safeVars == nVars)
            return (TRUE);

        if (DEBUG)
            fprintf(outputFile, "----\n");
        for (i = nVars; i > 0; i--)
            if ((g = eqn->coef[i]) != 0)
                break;
        /*
         * if (isRed(eqn)) { if (DBUG) fprintf(outputFile, "Can't handle Red equality\n");
         * convertEQtoGEQs(problemPtr,eqn); if (DBUG) printProblem(problemPtr); continue; };
         */
        for (j = i - 1; j > 0; j--)
            if (eqn->coef[j])
                break;
        if (j == 0) {
            if (eqn->coef[0] % g != 0) {
                if (DBUG)
                    printEQ(eqn);
                if (DBUG)
                    fprintf(outputFile, "\nequations have no solution \n");
                return (FALSE);
            };
            eqn->coef[0] = eqn->coef[0] / g;
            eqn->coef[i] = 1;
            //nEQ--;
            problemPtr->addNumEqs(-1);
            doElimination(problemPtr, e, i);
            continue;
        }
        else if (j == -1) {
            if (eqn->coef[0] != 0) {
                if (DBUG)
                    printEQ(eqn);
                if (DBUG)
                    fprintf(outputFile, "\nequations have no solution \n");
                return (FALSE);
            };
            //nEQ--;
            problemPtr->addNumEqs(-1);
            continue;
        };
        /* i == position of last non-zero coef */
        /* g == coef of i */
        /* j == position of next non-zero coef */

        if (g < 0)
            g = -g;
        if (g == 1) {
            //nEQ--;
            problemPtr->addNumEqs(-1);
            doElimination(problemPtr, e, i);
        }
        else {
            int k = j;
            bool promotionPossible =
                (j <= safeVars && safeVars + 1 == i
                    && !isRed(eqn)
                    && !inApproximateMode);
            if (DEBUG && promotionPossible)
                fprintf(outputFile, " Promotion possible\n");
        normalizeEQ:
            if (j > safeVars) {
                for (; g != 1 && j > safeVars; j--)
                    g = gcd(abs(eqn->coef[j]), g);
                g2 = g;
            }
            else if (i > safeVars)
                g2 = g;
            else
                g2 = 0;
            for (; g != 1 && j > 0; j--)
                g = gcd(abs(eqn->coef[j]), g);
            if (g > 1) {
                if (eqn->coef[0] % g != 0) {
                    if (DBUG)
                        printEQ(eqn);
                    if (DBUG)
                        fprintf(outputFile, "\nequations have no solution \n");
                    return (FALSE);
                };

                for (j = 0; j <= nVars; j++)
                    eqn->coef[j] /= g;
                g2 = g2 / g;
            };
            if (g2 > 1) {
                int e2;
                for (e2 = e - 1; e2 >= 0; e2--)
                    if (EQs[e2].coef[i])
                        break;
                if (e2 == -1)
                    for (e2 = nGEQ - 1; e2 >= 0; e2--)
                        if (GEQs[e2].coef[i])
                            break;
                if (e2 == -1)
                    for (e2 = nSUB - 1; e2 >= 0; e2--)
                        if (SUBs[e2].coef[i])
                            break;
                if (e2 == -1) {
                    bool change = 0;
                    if (DBUG)
                        fprintf(outputFile, "Ha! We own it! \n");
                    if (DEBUG)
                        printEQ(eqn);
                    if (DEBUG)
                        fprintf(outputFile, " \n");
                    g = eqn->coef[i];
                    g = abs(g);
                    for (j = i - 1; j >= 0; j--) {
                        int t = eqn->coef[j];
                        t = intMod(t, g);
                        if (2 * t >= g)
                            t -= g;
                        if (t != eqn->coef[j]) {
                            eqn->coef[j] = t;
                            change = 1;
                        };
                    };
                    if (!change) {
                        if (DBUG)
                            fprintf(outputFile, "So what?\n");
                    }
                    else {
                        nameWildcard(problemPtr, i);
                        if (DEBUG)
                            printEQ(eqn);
                        if (DEBUG)
                            fprintf(outputFile, " \n");
                        e++;
                        continue;
                    };
                };
            }
            if (promotionPossible) {
                if (DEBUG) {
                    fprintf(outputFile, "promoting %s to safety\n", variable(i));
                    printVars(problemPtr);
                };
                safeVars++;
                if (problemPtr->_var[i] > 0)
                    nameWildcard(problemPtr, i);
                promotionPossible = 0;
                j = k;
                goto normalizeEQ;
            };

            if (g2 > 1 && !inApproximateMode) 
            {
                if (DEBUG)
                    fprintf(outputFile, "adding equation to handle safe variable \n");
                if (DEBUG)
                    printEQ(eqn);
                if (DEBUG)
                    fprintf(outputFile, "\n----\n");
                i = addNewWildcard(problemPtr);
                //nEQ++;
                problemPtr->addNumEqs(1);

                assert(nEQ <= maxEQs);
                eqnzero(&EQs[e + 1]);
                eqnncpy(&EQs[e + 1], eqn, safeVars);
                for (j = nVars; j >= 0; j--) {
                    EQs[e + 1].coef[j] = intMod(EQs[e + 1].coef[j], g2);
                    if (2 * EQs[e + 1].coef[j] >= g2)
                        EQs[e + 1].coef[j] -= g2;
                };
                EQs[e + 1].coef[i] = g2;
                e += 2;
                if (DEBUG)
                    printProblem(problemPtr);
                continue;
            };

            sv = safeVars;
            if (g2 == 0)
                sv = 0;

            /* find variable to eliminate */
            if (g2 > 1) {
                assert(inApproximateMode);
                if (TRACE) {
                    fprintf(outputFile, "non-exact elimination: ");
                    printEQ(eqn);
                    fprintf(outputFile, "\n");
                    printProblem(problemPtr);
                    fflush(outputFile);
                };
                for (i = nVars; i > sv; i--)
                    if (EQs[e].coef[i] != 0)
                        break;
            }
            else
                for (i = nVars; i > sv; i--)
                    if (EQs[e].coef[i] == 1 || EQs[e].coef[i] == -1)
                        break;

            if (i > sv) {
                //nEQ--;
                problemPtr->addNumEqs(-1);
                doElimination(problemPtr, e, i);
                if (g2 > 1 && TRACE) {
                    fprintf(outputFile, "result of non-exact elimination:\n");
                    printProblem(problemPtr);
                    fflush(outputFile);
                };
            }
            else {
                int factor = 100000;
                j = 0;
                if (DEBUG)
                    fprintf(outputFile, "doing moding\n");
                for (i = nVars; i != sv; i--)
                    if ((EQs[e].coef[i] & 1) != 0) {
                        j = i;
                        i--;
                        for (; i != sv; i--)
                            if ((EQs[e].coef[i] & 1) != 0)
                                break;
                        break;
                    };
                if (j != 0 && i == sv) {
                    doMod(problemPtr, 2, e, j);
                    e++;
                    continue;
                };

                j = 0;
                for (i = nVars; i != sv; i--)
                    if (EQs[e].coef[i] != 0 && factor > abs(EQs[e].coef[i]) + 1) {
                        factor = abs(EQs[e].coef[i]) + 1;
                        j = i;
                    };
                if (j == sv) {
                    fprintf(outputFile, "should not have happened\n");
                    Exit(2);
                };
                doMod(problemPtr, factor, e, j);
                /* go back and try this equation again */
                e++;
            };
        };


    };
    //nEQ = 0;
    problemPtr->setNumEqs(0);
    return (UNKNOWN);
}


static int solveGEQ(Problem *problemPtr, int desiredResult);
static int solveDepth = 0;

int solve(Problem *problemPtr, int desiredResult)
{
    int result;

    assert(nVars >= safeVars);
    if (desiredResult != SIMPLIFY)
        safeVars = 0;

    solveDepth++;
    if (solveDepth > 50) {
        fprintf(outputFile, "Solve depth = %d, inApprox = %d, aborting\n",
            solveDepth, inApproximateMode);
        printProblem(problemPtr);
        fflush(outputFile);
#ifndef SPEED
        debugLevel = 3;
#else
        Exit(2);
#endif
        if (solveDepth > 60)
            Exit(2);
    };

    do {
        doItAgain = 0;
        if (solveEQ(problemPtr, desiredResult) == FALSE) {
            solveDepth--;
            return (FALSE);
        };
        if (inApproximateMode && !nGEQ) {
            result = TRUE;
            foundReduction = 1;
            break;
        }
        else
            result = solveGEQ(problemPtr, desiredResult);
    } while (doItAgain && desiredResult == SIMPLIFY);
    solveDepth--;

#if reduceWithSubstitutions
#else
    resurrectSubs(problemPtr);
    assert(pleaseNoEqualitiesInSimplifiedProblems || !result || nSUB == 0);
#endif

    return (result);
}

static int fastLookup[maxKeys * 2];

static int solveGEQ(Problem *problemPtr, int desiredResult)
{
    int i, j, k, e;
    int nV, fv;
    int result;
    int coupledSubscripts;
    int eliminateAgain;
    int smoothed = 0;
    j = 0;
solveGEQstart:
    while (1) {
        if (nGEQ > maxGEQs) {
            fprintf(outputFile, "TOO MANY EQUATIONS GENERATED\n");
            Exit(2);
        };
        if (DBUG)
            fprintf(outputFile, "\nSolveGEQ(%d):\n", desiredResult);
        if (DEBUG)
            printProblem(problemPtr);
        if (DBUG)
            fprintf(outputFile, "\n");

        nV = nVars;

        if (nV == 1) {
            int uColor = black;
            int lColor = black;
            int upperBound = posInfinity;
            int lowerBound = negInfinity;
            for (e = nGEQ - 1; e >= 0; e--) {
                int a = GEQs[e].coef[1];
                int c = GEQs[e].coef[0];
                /* our equation is ax + c >= 0, or ax >= -c, or c >= -ax */
                if (a == 0) {
                    if (c < 0) {
                        if (DBUG)
                            fprintf(outputFile, "equations have no solution \n");
                        return (FALSE);
                    };
                }
                else if (a > 0) {
                    if (a != 1)
                        c = intDiv(c, a);
                    if (lowerBound < -c ||
                        (lowerBound == -c && !isRed(&GEQs[e]))) {
                        lowerBound = -c;
                        lColor = GEQs[e].color;
                    }
                }
                else {
                    if (a != -1)
                        c = intDiv(c, -a);
                    if (upperBound > c ||
                        (upperBound == c && !isRed(&GEQs[e]))) {
                        upperBound = c;
                        uColor = GEQs[e].color;
                    }
                };
            };
            if (DEBUG)
                fprintf(outputFile, "upper bound = %d\n", upperBound);
            if (DEBUG)
                fprintf(outputFile, "lower bound = %d\n", lowerBound);
            if (lowerBound > upperBound) {
                if (DBUG)
                    fprintf(outputFile, "equations have no solution \n");
                return (FALSE);
            };
            if (desiredResult == SIMPLIFY) {
                //nGEQ = 0;
                problemPtr->setNumGEqs(0);
                if (safeVars == 1) {

                    if (lowerBound == upperBound && !uColor && !lColor) {
                        EQs[0].coef[0] = -lowerBound;
                        EQs[0].coef[1] = 1;
                        EQs[0].color = 0;
                        //nEQ = 1;
                        problemPtr->setNumEqs(1);
                        return (solve(problemPtr, desiredResult));
                    }
                    else {
                        if (lowerBound > negInfinity) {
                            GEQs[0].coef[0] = -lowerBound;
                            GEQs[0].coef[1] = 1;
                            GEQs[0].key = 1;
                            GEQs[0].color = lColor;
                            GEQs[0].touched = 0;
                            //nGEQ = 1;
                            problemPtr->setNumGEqs(1);
                        }

                        if (upperBound < posInfinity) 
                        {
                            const int numGE = nGEQ;
                            problemPtr->addNumGEqs(1);

                            GEQs[numGE].coef[0] = upperBound;
                            GEQs[numGE].coef[1] = -1;
                            GEQs[numGE].key = -1;
                            GEQs[numGE].color = uColor;
                            GEQs[numGE].touched = 0;
                            //nGEQ++;                            
                        }
                    }
                }
                else
                    problemPtr->setVarsN(0);
                problemReduced(problemPtr);
                return (FALSE);
            };
            if (originalProblem != noProblem && !lColor && !uColor && !conservative && lowerBound == upperBound) {
                EQs[0].coef[0] = -lowerBound;
                EQs[0].coef[1] = 1;
                //nEQ = 1;
                problemPtr->setNumEqs(1);
                addingEqualityConstraint(problemPtr, 0);
            };
            return (TRUE);
        };

        if (!problemPtr->variablesFreed) {
            problemPtr->variablesFreed = 1;
            if (desiredResult != SIMPLIFY)
                freeEliminations(problemPtr, 0);
            else
                freeEliminations(problemPtr, safeVars);
            nV = nVars;
            if (nV == 1)
                continue;
        };


        coupledSubscripts = 0;
        for (e = 0; e < nGEQ; e++) {
            if (!GEQs[e].touched) {
                if (!singleVarGEQ(GEQs[e], nV))
                    coupledSubscripts = 1;
            }
            else {
                int g;
                int topVar;
                int i0;
                int hashCode;


                {
                    int *p = &packing[0];
                    for (k = 1; k <= nV; k++)
                        if (GEQs[e].coef[k]) {
                            *(p++) = k;
                        };
                    topVar = (p - &packing[0]) - 1;
                };

                if (topVar == -1) {
                    if (GEQs[e].coef[0] < 0) {
                        if (DBUG)
                            printGEQ(&GEQs[e]);
                        if (DBUG)
                            fprintf(outputFile, "\nequations have no solution \n");
                        return (FALSE);
                    };
                    doDelete(e, nV);
                    e--;
                    continue;
                }
                else if (topVar == 0) {
                    int singleVar = packing[0];
                    g = GEQs[e].coef[singleVar];
                    if (g > 0) {
                        GEQs[e].coef[singleVar] = 1;
                        GEQs[e].key = singleVar;
                    }
                    else {
                        g = -g;
                        GEQs[e].coef[singleVar] = -1;
                        GEQs[e].key = -singleVar;
                    };
                    if (g > 1)
                        GEQs[e].coef[0] = intDiv(GEQs[e].coef[0], g);
                }
                else {

                    coupledSubscripts = 1;
                    i0 = topVar;
                    i = packing[i0--];
                    g = GEQs[e].coef[i];
                    hashCode = g * (i + 3);
                    if (g < 0)
                        g = -g;
                    for (; i0 >= 0; i0--) {
                        int x;
                        i = packing[i0];
                        x = GEQs[e].coef[i];
                        hashCode = hashCode * keyMult * (i + 3) + x;
                        if (x < 0)
                            x = -x;
                        if (x == 1) {
                            g = 1;
                            i0--;
                            break;
                        }
                        else
                            g = gcd(x, g);
                    };
                    for (; i0 >= 0; i0--) {
                        int x;
                        i = packing[i0];
                        x = GEQs[e].coef[i];
                        hashCode = hashCode * keyMult * (i + 3) + x;
                    };
                    if (g > 1) {
                        GEQs[e].coef[0] = intDiv(GEQs[e].coef[0], g);
                        i0 = topVar;
                        i = packing[i0--];
                        GEQs[e].coef[i] = GEQs[e].coef[i] / g;
                        hashCode = GEQs[e].coef[i] * (i + 3);
                        for (; i0 >= 0; i0--) {
                            i = packing[i0];
                            GEQs[e].coef[i] = GEQs[e].coef[i] / g;
                            hashCode = hashCode * keyMult * (i + 3) + GEQs[e].coef[i];
                        };
                    };

                    {
                        int g2 = abs(hashCode);
                        if (DEBUG) {
                            fprintf(outputFile, "Hash code = %d, eqn = ", hashCode);
                            printGEQ(&GEQs[e]);
                            fprintf(outputFile, "\n");
                        };
                        j = g2 % hashTableSize;
                        while (1) {
                            Eqn proto = &(hashMaster[j]);
                            if (proto->touched == g2) {
                                if (proto->coef[0] == topVar) {
                                    if (hashCode >= 0)
                                        for (i0 = topVar; i0 >= 0; i0--) {
                                            i = packing[i0];
                                            if (GEQs[e].coef[i] != proto->coef[i])
                                                break;
                                        }
                                    else
                                        for (i0 = topVar; i0 >= 0; i0--) {
                                            i = packing[i0];
                                            if (GEQs[e].coef[i] != -proto->coef[i])
                                                break;
                                        };
                                    if (i0 < 0) {
                                        if (hashCode >= 0)
                                            GEQs[e].key = proto->key;
                                        else
                                            GEQs[e].key = -proto->key;
                                        break;
                                    };
                                };
                            }
                            else if (proto->touched < 0) {
                                eqnzero(proto);
                                if (hashCode >= 0)
                                    for (i0 = topVar; i0 >= 0; i0--) {
                                        i = packing[i0];
                                        proto->coef[i] = GEQs[e].coef[i];
                                    }
                                else
                                    for (i0 = topVar; i0 >= 0; i0--) {
                                        i = packing[i0];
                                        proto->coef[i] = -GEQs[e].coef[i];
                                    }
                                proto->coef[0] = topVar;
                                proto->touched = g2;
                                if (DEBUG)
                                    fprintf(outputFile, " constraint key = %d\n", nextKey);
                                proto->key = nextKey++;
                                if (proto->key > maxKeys) {
                                    fprintf(outputFile, "too many hash keys generated \n");
                                    fflush(outputFile);
                                    Exit(2);
                                };
                                if (hashCode >= 0)
                                    GEQs[e].key = proto->key;
                                else
                                    GEQs[e].key = -proto->key;
                                break;
                            };
                            j = (j + 1) % hashTableSize;
                        };
                    };
                };

                GEQs[e].touched = FALSE;
            };

            {
                int eKey = GEQs[e].key;
                int e2;
                if (e > 0) {
                    int cTerm = GEQs[e].coef[0];
                    e2 = fastLookup[maxKeys - eKey];
                    if (e2 < e && GEQs[e2].key == -eKey) {
                        if (GEQs[e2].coef[0] < -cTerm) {
                            if (DBUG) {
                                printGEQ(&GEQs[e]);
                                fprintf(outputFile, "\n");
                                printGEQ(&GEQs[e2]);
                                fprintf(outputFile, "\nequations have no solution \n");
                            };
                            return (FALSE);
                        };
                        if (GEQs[e2].coef[0] == -cTerm && !GEQs[e2].color && !GEQs[e].color) 
                        {
                            /*
                             * if (!addIt && 0) { int i; for (i = safeVars + 1; i <= nVars; i++) if (GEQs[e].coef[i] ==
                             * 1 || GEQs[e].coef[i] == -1) addIt = 1; };
                             */
                            const int numEQ = nEQ;
                            problemPtr->addNumEqs(1);

                            eqncpy(&EQs[numEQ], &GEQs[e]);
                            if (!GEQs[e2].color)
                                addingEqualityConstraint(problemPtr, numEQ);
                            assert(!GEQs[e2].color);
                            assert(!GEQs[e].color);
                            //nEQ++;
                            
                            assert(nEQ <= maxEQs);
                        }
                    }

                    e2 = fastLookup[maxKeys + eKey];
                    if (e2 < e && GEQs[e2].key == eKey) {
                        if (GEQs[e2].coef[0] > cTerm) {
                            GEQs[e2].coef[0] = cTerm;
                            GEQs[e2].color = GEQs[e].color;
                        }
                        else if (GEQs[e2].coef[0] == cTerm)
                            GEQs[e2].color &= GEQs[e].color;
                        doDelete(e, nV);
                        e--;
                        continue;
                    };
                };
                fastLookup[maxKeys + eKey] = e;
            };
        };

        nV = nVars;

        if ((doTrace && desiredResult == SIMPLIFY) || DBUG) {
            fprintf(outputFile, "\nafter normalization:\n");
            printProblem(problemPtr);
            fprintf(outputFile, "\n");
            fprintf(outputFile, "eliminating variable using fourier-motzkin elimination\n");
        };

        do {
            eliminateAgain = 0;

            if (nEQ > 0)
                return (solve(problemPtr, desiredResult));

            if (!coupledSubscripts) {
                if (safeVars == 0)
                {
                    //nGEQ = 0;
                    problemPtr->setNumGEqs(0);
                }
                else
                    for (e = nGEQ - 1; e >= 0; e--)
                        if (GEQs[e].key > safeVars || -safeVars > GEQs[e].key)
                            doDelete(e, nV);
                problemPtr->setVarsN(safeVars);
                //nVars = safeVars;
                if (desiredResult == SIMPLIFY) {
                    problemReduced(problemPtr);
                    return (FALSE);
                };
                return (TRUE);
            };

            if (desiredResult != SIMPLIFY)
                fv = 0;
            else
                fv = safeVars;

            if (nGEQ == 0) {
                if (desiredResult == SIMPLIFY) {
                    problemPtr->setVarsN(safeVars);
                    //nVars = safeVars;
                    problemReduced(problemPtr);
                    return (FALSE);
                };
                return (TRUE);
            };
            if (desiredResult == SIMPLIFY && nV == safeVars) {
                problemReduced(problemPtr);
                return (FALSE);
            };


            if (nGEQ > maxGEQs - 30 || nGEQ > 2 * nV * nV + 4 * nV + 10) {
                if (DBUG)
                    fprintf(outputFile, "TOO MANY EQUATIONS; %d equations, %d variables, ELIMINATING REDUNDANT ONES\n", nGEQ, nV);
                if (!eliminateRedundant(problemPtr, 0))
                    return 0;
                nV = nVars;
                if (nEQ > 0)
                    return (solve(problemPtr, desiredResult));
                if (DBUG)
                    fprintf(outputFile, "END ELIMINATION OF REDUNDANT EQUATIONS\n");
            };



            {
                int minC, maxC, minCj;
                int lowerBoundCount;
                int e2, Le, Ue;
                int possibleEasyIntSolution;
                int exact = 0;
                int luckyExact = 0;
                int newEqns = 0;
                minCj = 0;
                Le = 0;
                lowerBoundCount = 0;

                if (desiredResult != SIMPLIFY)
                    fv = 0;
                else
                    fv = safeVars;

                {
                    int best = 1000000;
                    int jLe, jLowerBoundCount, upperBoundCount;

                    jLe = 0;
                    jLowerBoundCount = 0;


                    for (i = nV; i != fv; i--) {
                        int score;
                        int ub = -2;
                        int lb = -2;
                        int lucky = 0;
                        minC = maxC = 0;
                        lowerBoundCount = 0;
                        upperBoundCount = 0;
                        for (e = nGEQ - 1; e >= 0; e--)
                            if (GEQs[e].coef[i] < 0) {
                                setMin(minC, GEQs[e].coef[i]);
                                upperBoundCount++;
                                if (GEQs[e].coef[i] < -1) {
                                    if (ub == -2)
                                        ub = e;
                                    else
                                        ub = -1;
                                };
                            }
                            else if (GEQs[e].coef[i] > 0) {
                                setMax(maxC, GEQs[e].coef[i]);
                                lowerBoundCount++;
                                Le = e;
                                if (GEQs[e].coef[i] > 1) {
                                    if (lb == -2)
                                        lb = e;
                                    else
                                        lb = -1;
                                };
                            };
                            if (lowerBoundCount == 0 || upperBoundCount == 0) {
                                lowerBoundCount = 0;
                                break;
                            };
                            if (ub >= 0 && lb >= 0 && GEQs[lb].key == -GEQs[ub].key) {
                                int Lc = GEQs[lb].coef[i];
                                int Uc = -GEQs[ub].coef[i];
                                int diff = Lc * GEQs[ub].coef[0] + Uc * GEQs[lb].coef[0];
                                lucky = (diff >= (Uc - 1) * (Lc - 1));
                            };
                            if (maxC == 1 || minC == -1 || lucky || APROX || inApproximateMode) {
                                newEqns = score = upperBoundCount * lowerBoundCount;
                                if (DEBUG)
                                    fprintf(outputFile,
                                        "For %s, exact, score = %d*%d, range = %d ... %d, \nlucky = %d, APROX = %d, inApproximateMode=%d \n",
                                        variable(i), upperBoundCount, lowerBoundCount,
                                        minC, maxC, lucky, APROX, inApproximateMode);
                                if (!exact || score < best) {

                                    best = score;
                                    j = i;
                                    minCj = minC;
                                    jLe = Le;
                                    jLowerBoundCount = lowerBoundCount;
                                    exact = 1;
                                    luckyExact = lucky;
                                    if (score == 1)
                                        break;
                                };
                            }
                            else if (!exact) {
                                if (DEBUG)
                                    fprintf(outputFile,
                                        "For %s, non-exact, score = %d*%d, range = %d ... %d \n",
                                        variable(i), upperBoundCount, lowerBoundCount,
                                        minC, maxC);
                                newEqns = upperBoundCount * lowerBoundCount;
                                score = maxC - minC;
                                if (best > score) {
                                    best = score;
                                    j = i;
                                    minCj = minC;
                                    jLe = Le;
                                    jLowerBoundCount = lowerBoundCount;
                                };
                            };
                    };
                    if (lowerBoundCount == 0) {
                        freeEliminations(problemPtr, safeVars);
                        nV = nVars;
                        continue;
                    };
                    i = j;
                    minC = minCj;
                    Le = jLe;
                    lowerBoundCount = jLowerBoundCount;
                };

#ifdef singleResult
                if (desiredResult == SIMPLIFY && !exact) {
                    nonConvex = 1;
                    problemReduced(problemPtr);
                    return (TRUE);
                };
#endif

                if ((doTrace && desiredResult == SIMPLIFY) || DBUG) {
                    fprintf(outputFile, "going to eliminate %s\n", variable(i));
                    if (luckyExact)
                        fprintf(outputFile, "(a lucky exact elimination)\n");
                    else if (exact)
                        fprintf(outputFile, "(an exact elimination)\n");
                };


                smoothed = 0;

                if (i != nV) {
                    int t;
                    j = nVars;
                    if (DEBUG) {
                        fprintf(outputFile, "Swapping %d and %d\n", i, j);
                        printProblem(problemPtr);
                    };
                    swap(&problemPtr->_var[i], &problemPtr->_var[j]);
                    for (e = nGEQ - 1; e >= 0; e--)
                        if (GEQs[e].coef[i] != GEQs[e].coef[j]) {
                            GEQs[e].touched = TRUE;
                            t = GEQs[e].coef[i];
                            GEQs[e].coef[i] = GEQs[e].coef[j];
                            GEQs[e].coef[j] = t;
                        };
                    for (e = nSUB - 1; e >= 0; e--)
                        if (SUBs[e].coef[i] != SUBs[e].coef[j]) {
                            t = SUBs[e].coef[i];
                            SUBs[e].coef[i] = SUBs[e].coef[j];
                            SUBs[e].coef[j] = t;
                        };
                    if (DEBUG) {
                        fprintf(outputFile, "Swapping complete \n");
                        printProblem(problemPtr);
                        fprintf(outputFile, "\n");
                    };

                    i = j;
                }
                else if (DEBUG) {
                    fprintf(outputFile, "No swap needed\n");
                    printProblem(problemPtr);
                };
                problemPtr->addToVarsN(-1);
                //nVars--;
                nV = nVars;

                if (exact) {
#define maxDead maxGEQs
                    if (nV == 1) {
                        int upperBound = posInfinity;
                        int lowerBound = negInfinity;
                        int ub_color = -1;
                        int lb_color = -1;
                        int constantTerm, coefficient;
                        int topEqn = nGEQ - 1;
                        int Lc = GEQs[Le].coef[i];
                        for (Le = topEqn; Le >= 0; Le--)
                            if ((Lc = GEQs[Le].coef[i]) == 0) {
                                if (GEQs[Le].coef[1] == 1) {
                                    constantTerm = -GEQs[Le].coef[0];
                                    if (constantTerm > lowerBound ||
                                        (constantTerm == lowerBound &&
                                            !isRed(&GEQs[Le]))) {
                                        lowerBound = constantTerm;
                                        lb_color = GEQs[Le].color;
                                    }
                                    if (DEBUG) {
                                        if (GEQs[Le].color == black)
                                            fprintf(outputFile, " :::=> %s >= %d\n",
                                                variable(1), constantTerm);
                                        else
                                            fprintf(outputFile, " :::=> [%s >= %d]\n",
                                                variable(1), constantTerm);
                                    }
                                }
                                else {
                                    constantTerm = GEQs[Le].coef[0];
                                    if (constantTerm < upperBound ||
                                        (constantTerm == upperBound
                                            && !isRed(&GEQs[Le]))) {
                                        upperBound = constantTerm;
                                        ub_color = GEQs[Le].color;
                                    }
                                    if (DEBUG) {
                                        if (GEQs[Le].color == black)
                                            fprintf(outputFile, " :::=> %s <= %d\n",
                                                variable(1), constantTerm);
                                        else
                                            fprintf(outputFile, " :::=> [%s <= %d]\n",
                                                variable(1), constantTerm);
                                    }
                                };
                            }
                            else if (Lc > 0) {
                                for (Ue = topEqn; Ue >= 0; Ue--)
                                    if (GEQs[Ue].coef[i] < 0) {
                                        if (GEQs[Le].key != -GEQs[Ue].key) {
                                            int Uc = -GEQs[Ue].coef[i];
                                            coefficient = GEQs[Ue].coef[1] * Lc + GEQs[Le].coef[1] * Uc;
                                            constantTerm = GEQs[Ue].coef[0] * Lc + GEQs[Le].coef[0] * Uc;
                                            if (DEBUG) {
                                                printGEQextra(&(GEQs[Ue]));
                                                fprintf(outputFile, "\n");
                                                printGEQextra(&(GEQs[Le]));
                                                fprintf(outputFile, "\n");
                                            };
                                            if (coefficient > 0) {
                                                constantTerm = -(intDiv(constantTerm, coefficient));
                                                /* assert(black == 0) */
                                                if (constantTerm > lowerBound ||
                                                    (constantTerm == lowerBound &&
                                                    (desiredResult != SIMPLIFY ||
                                                        (GEQs[Ue].color == black && GEQs[Le].color == black)))) {
                                                    lowerBound = constantTerm;
                                                    lb_color = GEQs[Ue].color || GEQs[Le].color;
                                                }
                                                if (DEBUG) {
                                                    if (GEQs[Ue].color || GEQs[Le].color)
                                                        fprintf(outputFile, " ::=> [%s >= %d]\n",
                                                            variable(1), constantTerm);
                                                    else
                                                        fprintf(outputFile, " ::=> %s >= %d\n",
                                                            variable(1), constantTerm);
                                                }
                                            }
                                            else {
                                                constantTerm = (intDiv(constantTerm, -coefficient));
                                                if (constantTerm < upperBound ||
                                                    (constantTerm == upperBound &&
                                                        GEQs[Ue].color == black && GEQs[Le].color == black)) {
                                                    upperBound = constantTerm;
                                                    ub_color = GEQs[Ue].color || GEQs[Le].color;
                                                }
                                                if (DEBUG) {
                                                    if (GEQs[Ue].color || GEQs[Le].color)
                                                        fprintf(outputFile, " ::=> [%s <= %d]\n",
                                                            variable(1), constantTerm);
                                                    else
                                                        fprintf(outputFile, " ::=> %s <= %d\n",
                                                            variable(1), constantTerm);
                                                }
                                            }
                                        };
                                    };
                            };
                            //nGEQ = 0;
                            problemPtr->setNumGEqs(0);
                            if (DEBUG)
                                fprintf(outputFile,
                                    " therefore, %c%d <= %c%s%c <= %d%c\n",
                                    lb_color ? '[' : ' ', lowerBound,
                                    (lb_color && !ub_color) ? ']' : ' ',
                                    variable(1),
                                    (!lb_color && ub_color) ? '[' : ' ',
                                    upperBound, ub_color ? ']' : ' ');
                            if (lowerBound > upperBound)
                                return (FALSE);
                            if (safeVars == 1) {
                                if (upperBound == lowerBound
                                    && !(ub_color | lb_color)
                                    && !pleaseNoEqualitiesInSimplifiedProblems) {
                                    //nEQ++;
                                    problemPtr->addNumEqs(1);
                                    EQs[0].coef[1] = -1;
                                    EQs[0].coef[0] = upperBound;
                                    EQs[0].color = ub_color | lb_color;
                                    if (desiredResult == SIMPLIFY &&
                                        !EQs[0].color)
                                        return (solve(problemPtr, desiredResult));
                                };
                                if (upperBound != posInfinity) {
                                    GEQs[0].coef[1] = -1;
                                    GEQs[0].coef[0] = upperBound;
                                    GEQs[0].color = ub_color;
                                    GEQs[0].key = -1;
                                    GEQs[0].touched = 0;
                                    //nGEQ++;
                                    problemPtr->addNumGEqs(1);
                                }

                                if (lowerBound != negInfinity) 
                                {
                                    const int numGE = nGEQ;
                                    problemPtr->addNumGEqs(1);

                                    GEQs[numGE].coef[1] = 1;
                                    GEQs[numGE].coef[0] = -lowerBound;
                                    GEQs[numGE].color = lb_color;
                                    GEQs[numGE].key = 1;
                                    GEQs[numGE].touched = 0;
                                    //nGEQ++;                                    
                                }
                            }

                            if (desiredResult == SIMPLIFY) {
                                problemReduced(problemPtr);
                                return (FALSE);
                            }
                            else {
                                if (!conservative &&
                                    (desiredResult != SIMPLIFY ||
                                    (!lb_color && !ub_color))
                                    && originalProblem != noProblem && lowerBound == upperBound) {
                                    for (i = originalProblem->getVarsN(); i >= 0; i--)
                                        if (originalProblem->_var[i] == problemPtr->_var[1])
                                            break;
                                    if (i == 0)
                                        break;
                                    //e = originalProblem->_numEQs++;
                                    e = originalProblem->getNumEqs();
                                    problemPtr->addNumEqs(1);

                                    eqnnzero(&originalProblem->_EQs[e], originalProblem->getVarsN());
                                    originalProblem->_EQs[e].coef[i] = -1;
                                    originalProblem->_EQs[e].coef[0] = upperBound;
                                    if (DEBUG) {
                                        fprintf(outputFile, "adding equality constraint %d to outer problem\n",
                                            e);
                                        printProblem(originalProblem);
                                    };
                                };
                                return (TRUE);
                            };
                    };
                    eliminateAgain = 1;

                    if (lowerBoundCount == 1) {
                        struct _eqn lbEqn;
                        int Lc = GEQs[Le].coef[i];
                        if (DBUG)
                            fprintf(outputFile, "an inplace elimination\n");

                        eqnncpy(&lbEqn, &GEQs[Le], (nV + 1));
                        doDeleteExtra(Le, nV + 1);
                        for (Ue = nGEQ - 1; Ue >= 0; Ue--)
                            if (GEQs[Ue].coef[i] < 0)
                                if (lbEqn.key == -GEQs[Ue].key) {
                                    doDeleteExtra(Ue, nV + 1);
                                }
                                else {
                                    int Uc = -GEQs[Ue].coef[i];
                                    GEQs[Ue].touched = TRUE;
                                    GEQs[Ue].color |= lbEqn.color;
                                    eliminateAgain = 0;
                                    for (k = 0; k <= nV; k++)
                                        GEQs[Ue].coef[k] = GEQs[Ue].coef[k] * Lc + lbEqn.coef[k] * Uc;
                                    if (DEBUG) {
                                        printGEQ(&(GEQs[Ue]));
                                        fprintf(outputFile, "\n");
                                    };
                                };
                                continue;
                    }
                    else {
                        int deadEqns[maxDead];
                        int numDead = 0;
                        int topEqn = nGEQ - 1;
                        lowerBoundCount--;
                        if (DEBUG)
                            fprintf(outputFile, "lower bound count = %d\n", lowerBoundCount);
                        for (Le = topEqn; Le >= 0; Le--)
                            if (GEQs[Le].coef[i] > 0) {
                                int Lc = GEQs[Le].coef[i];
                                for (Ue = topEqn; Ue >= 0; Ue--)
                                    if (GEQs[Ue].coef[i] < 0) {
                                        if (GEQs[Le].key != -GEQs[Ue].key) {
                                            int Uc = -GEQs[Ue].coef[i];
                                            if (numDead == 0)
                                            {
                                                //e2 = nGEQ++;
                                                e2 = nGEQ;
                                                problemPtr->addNumGEqs(1);
                                            }
                                            else
                                                e2 = deadEqns[--numDead];
                                            assert(e2 < maxGEQs);
                                            if (DEBUG)
                                                fprintf(outputFile, "Le = %d, Ue = %d, gen = %d\n", Le, Ue, e2);
                                            if (DEBUG) {
                                                printGEQextra(&(GEQs[Le]));
                                                fprintf(outputFile, "\n");
                                                printGEQextra(&(GEQs[Ue]));
                                                fprintf(outputFile, "\n");
                                            };
                                            eliminateAgain = 0;

                                            for (k = nV; k >= 0; k--)
                                                GEQs[e2].coef[k] = GEQs[Ue].coef[k] * Lc + GEQs[Le].coef[k] * Uc;
                                            GEQs[e2].coef[nV + 1] = 0;
                                            GEQs[e2].touched = TRUE;
                                            GEQs[e2].color = GEQs[Ue].color | GEQs[Le].color;

                                            if (DEBUG) {
                                                printGEQ(&(GEQs[e2]));
                                                fprintf(outputFile, "\n");
                                            };
                                        };
                                        if (lowerBoundCount == 0) {
                                            deadEqns[numDead++] = Ue;
                                            if (DEBUG)
                                                fprintf(outputFile, "Killed %d\n", Ue);
                                        };
                                    };
                                lowerBoundCount--;
                                deadEqns[numDead++] = Le;
                                if (DEBUG)
                                    fprintf(outputFile, "Killed %d\n", Le);
                            };
                        {
                            int isDead[maxGEQs];
                            for (e = nGEQ - 1; e >= 0; e--)
                                isDead[e] = FALSE;
                            while (numDead > 0) {
                                e = deadEqns[--numDead];
                                isDead[e] = TRUE;
                            };
                            for (e = nGEQ - 1; e >= 0; e--)
                                if (isDead[e])
                                    doDeleteExtra(e, nV + 1);
                        };
                        continue;
                    };
                }
                else {
                    Problem *rS, *iS;

                    rS = mallocProblem;
#ifdef _WIN32
                    addToCollection(__LINE__, __FILE__, rS, 1);
#endif
                    initializeProblem(rS);
                    iS = mallocProblem;
#ifdef _WIN32
                    addToCollection(__LINE__, __FILE__, iS, 1);
#endif
                    initializeProblem(iS);
                    rS->_getVarName = problemPtr->_getVarName;
                    rS->_getVarNameArgs = problemPtr->_getVarNameArgs;
                    iS->_getVarName = problemPtr->_getVarName;
                    iS->_getVarNameArgs = problemPtr->_getVarNameArgs;

                    e2 = 0;
                    possibleEasyIntSolution = TRUE;
                    for (e = 0; e < nGEQ; e++)
                        if (GEQs[e].coef[i] == 0) {
                            eqncpy(&(rS->_GEQs[e2]), &GEQs[e]);
                            eqncpy(&(iS->_GEQs[e2]), &GEQs[e]);
                            if (DEBUG) {
                                int t;
                                fprintf(outputFile, "Copying (%d, %d): ", i, GEQs[e].coef[i]);
                                printGEQextra(&GEQs[e]);
                                fprintf(outputFile, "\n");
                                for (t = 0; t <= nV + 1; t++)
                                    fprintf(outputFile, "%d ", GEQs[e].coef[t]);
                                fprintf(outputFile, "\n");

                            };
                            e2++;
                            assert(e2 < maxGEQs);
                        };
                    for (Le = nGEQ - 1; Le >= 0; Le--)
                        if (GEQs[Le].coef[i] > 0) {
                            int Lc = GEQs[Le].coef[i];
                            for (Ue = nGEQ - 1; Ue >= 0; Ue--)
                                if (GEQs[Ue].coef[i] < 0)
                                    if (GEQs[Le].key != -GEQs[Ue].key) {
                                        int Uc = -GEQs[Ue].coef[i];
                                        rS->_GEQs[e2].touched = iS->_GEQs[e2].touched = TRUE;
                                        if (DEBUG) {
                                            fprintf(outputFile, "---\n");
                                            fprintf(outputFile, "Le = %d, Ue = %d, gen = %d\n", Le, Ue, e2);
                                            printGEQextra(&GEQs[Le]);
                                            fprintf(outputFile, "\n");
                                            printGEQextra(&GEQs[Ue]);
                                            fprintf(outputFile, "\n");
                                        };

                                        for (k = nV; k >= 0; k--)
                                            iS->_GEQs[e2].coef[k] = rS->_GEQs[e2].coef[k] =
                                            GEQs[Ue].coef[k] * Lc + GEQs[Le].coef[k] * Uc;
                                        iS->_GEQs[e2].coef[0] -= (Uc - 1) * (Lc - 1);
                                        iS->_GEQs[e2].color = rS->_GEQs[e2].color
                                            = GEQs[Ue].color || GEQs[Le].color;

                                        if (DEBUG) {
                                            printGEQ(&(rS->_GEQs[e2]));
                                            fprintf(outputFile, "\n");
                                        };
                                        e2++;
                                        assert(e2 < maxGEQs);
                                    }
                                    else {
                                        int Uc = -GEQs[Ue].coef[i];
                                        if (GEQs[Ue].coef[0] * Lc + GEQs[Le].coef[0] * Uc - (Uc - 1) * (Lc - 1) < 0)
                                            possibleEasyIntSolution = FALSE;
                                    };

                        };
                    iS->variablesInitialized = rS->variablesInitialized = 1;
                    iS->setVarsN(nVars);
                    rS->setVarsN(nVars);
                    //iS->_numGEQs = rS->_numGEQs = e2;
                    //iS->_numEQs = rS->_numEQs = 0;
                    //iS->_numSUBs = rS->_numSUBs = nSUB;
                    iS->setNumGEqs(e2);
                    rS->setNumGEqs(e2);

                    iS->setNumEqs(0);
                    rS->setNumEqs(0);

                    iS->setNumSUBs(nSUB);
                    rS->setNumSUBs(nSUB);

                    iS->_safeVars = rS->_safeVars = safeVars;
                    {
                        int t;
                        for (t = nV; t >= 0; t--)
                            rS->_var[t] = problemPtr->_var[t];
                        for (t = nV; t >= 0; t--)
                            iS->_var[t] = problemPtr->_var[t];
                        for (e = nSUB - 1; e >= 0; e--) {
                            eqnncpy(&(rS->_SUBs[e]), &(SUBs[e]), nVars);
                            eqnncpy(&(iS->_SUBs[e]), &(SUBs[e]), nVars);
                        };
                    };
                    problemPtr->addToVarsN(1);
                    //nVars++;
                    nV = nVars;
                    if (desiredResult != TRUE) {
                        int t = trace;
                        if (DBUG)
                            fprintf(outputFile, "\nreal solution(%d):\n", depth);
                        depth++;
                        trace = 0;
                        if (originalProblem == noProblem) {
                            originalProblem = problemPtr;
                            result = solveGEQ(rS, FALSE);
                            originalProblem = noProblem;
                        }
                        else
                            result = solveGEQ(rS, FALSE);
                        trace = t;
                        depth--;
                        if (result == FALSE) {
#ifdef _WIN32
                            removeFromCollection(rS);
                            removeFromCollection(iS);
#endif
                            free(rS);
                            free(iS);
                            return (result);
                        };

                        if (nEQ > 0) {
#ifdef _WIN32
                            removeFromCollection(rS);
                            removeFromCollection(iS);
#endif
                            /* An equality constraint must have been found */
                            free(rS);
                            free(iS);
                            return (solve(problemPtr, desiredResult));
                        };
                    };
                    if (desiredResult != FALSE) {
                        if (possibleEasyIntSolution) {
                            if (DBUG)
                                fprintf(outputFile, "\ninteger solution(%d):\n", depth);
                            depth++;
                            conservative++;
                            result = solveGEQ(iS, desiredResult);
                            conservative--;
                            depth--;
                            if (result != FALSE) {
#ifdef _WIN32
                                removeFromCollection(rS);
                                removeFromCollection(iS);
#endif
                                free(rS);
                                free(iS);
                                return (result);
                            };
                        };
                        if (DBUG)
                            fprintf(outputFile, "have to do exact analysis\n");
                        {
                            int worstLowerBoundConstant = -minC;
                            int lowerBounds = 0;
                            int lowerBound[maxGEQs];
                            int smallest;
                            int t;
                            conservative++;
                            for (e = 0; e < nGEQ; e++)
                                if (GEQs[e].coef[i] > 1)
                                    lowerBound[lowerBounds++] = e;
                            /* sort array */
                            for (j = 0; j < lowerBounds; j++) {
                                smallest = j;
                                for (k = j + 1; k < lowerBounds; k++)
                                    if (GEQs[lowerBound[smallest]].coef[i] > GEQs[lowerBound[k]].coef[i])
                                        smallest = k;
                                t = lowerBound[smallest];
                                lowerBound[smallest] = lowerBound[j];
                                lowerBound[j] = t;
                            };
                            if (DEBUG) {
                                fprintf(outputFile, "lower bound coeeficients = ");
                                for (j = 0; j < lowerBounds; j++)
                                    fprintf(outputFile, " %d", GEQs[lowerBound[j]].coef[i]);
                                fprintf(outputFile, "\n");
                            };


                            for (j = 0; j < lowerBounds; j++) {
                                int maxIncr;
                                int c;
                                e = lowerBound[j];
                                maxIncr = ((GEQs[e].coef[i] - 1) * (worstLowerBoundConstant - 1) - 1)
                                    / worstLowerBoundConstant;

                                /* maxIncr += 2; */
                                if ((doTrace && desiredResult == SIMPLIFY) || DBUG) {
                                    fprintf(outputFile, "for equation ");
                                    printGEQ(&GEQs[e]);
                                    fprintf(outputFile, "\ntry decrements from 0 to %d\n", maxIncr);
                                    printProblem(problemPtr);
                                };
                                if (maxIncr > 50) {
                                    if (!smoothed && smoothWeirdEquations(problemPtr)) {
                                        conservative--;
#ifdef _WIN32
                                        removeFromCollection(rS);
                                        removeFromCollection(iS);
#endif
                                        free(rS);
                                        free(iS);
                                        smoothed = 1;
                                        goto solveGEQstart;
                                    };
                                };
                                eqncpy(&EQs[0], &GEQs[e]);
                                /*
                                 * if (GEQs[e].color) fprintf(outputFile,"warning: adding black equality constraint
                                 * based on red inequality\n");
                                 */
                                EQs[0].color = black;
                                eqnzero(&GEQs[e]);
                                GEQs[e].touched = TRUE;
                                //nEQ = 1;
                                problemPtr->setNumEqs(1);
                                for (c = maxIncr; c >= 0; c--) {
                                    if (DBUG)
                                        fprintf(outputFile, "trying next decrement of %d\n", maxIncr - c);
                                    if (DBUG)
                                        printProblem(problemPtr);
                                    problemcpy(rS, problemPtr);
                                    if (DEBUG)
                                        printProblem(rS);
                                    result = solve(rS, desiredResult);
                                    if (result == TRUE) {
#ifdef _WIN32
                                        removeFromCollection(rS);
                                        removeFromCollection(iS);
#endif
                                        free(rS);
                                        free(iS);
                                        conservative--;
                                        return (TRUE);
                                    };
                                    EQs[0].coef[0]--;
                                };
                                if (j + 1 < lowerBounds) {
                                    //nEQ = 0;
                                    problemPtr->setNumEqs(0);
                                    eqncpy(&GEQs[e], &EQs[0]);
                                    GEQs[e].touched = 1;
                                    GEQs[e].color = black;
                                    problemcpy(rS, problemPtr);
                                    if (DEBUG)
                                        fprintf(outputFile, "exhausted lower bound, checking if still feasible ");
                                    result = solve(rS, FALSE);
                                    if (result == FALSE)
                                        break;
                                };
                            };
                            if ((doTrace && desiredResult == SIMPLIFY) || DBUG)
                                fprintf(outputFile, "fall-off the end\n");
#ifdef _WIN32
                            removeFromCollection(rS);
                            removeFromCollection(iS);
#endif
                            free(rS);
                            free(iS);

                            conservative--;
                            return (FALSE);
                        };
                    };
#ifdef _WIN32
                    removeFromCollection(rS);
                    removeFromCollection(iS);
#endif
                    free(rS);
                    free(iS);
                };
                return (UNKNOWN);
            };
        } while (eliminateAgain);
    };
}


/*
 * Return 1 if red equations constrain the set of possible solutions. We assume that there are solutions to the black
 * equations by themselves, so if there is no solution to the combined problem, we return 1.
 */

int hasRedEquations(Problem * problemPtr, bool expensive)
{
    int result;
    int e;
    int i;

    if (TRACE) {
        fprintf(outputFile, "Checking for red equations:\n");
        printProblem(problemPtr);
    };

    pleaseNoEqualitiesInSimplifiedProblems++;
    mayBeRed++;
    result = !simplifyProblem(problemPtr);
    mayBeRed--;
    pleaseNoEqualitiesInSimplifiedProblems--;
    if (result) {
        return 1;
    }
    freeRedEliminations(problemPtr);


    assert(nEQ == 0);

    for (e = nGEQ - 1; e >= 0; e--)
        if (GEQs[e].color == red)
            result = 1;
    if (!result)
        return 0;

    if (!expensive)
        for (i = safeVars; i >= 1; i--) {
            int ub = 0;
            int lb = 0;
            for (e = nGEQ - 1; e >= 0; e--) {
                if (GEQs[e].coef[i])
                    if (GEQs[e].coef[i] > 0)
                        lb |= (1 + GEQs[e].color);
                    else	/* (GEQs[e].coef[i] < 0) */
                        ub |= (1 + GEQs[e].color);
            }
            if (ub == 2 || lb == 2) {
                if (DBUG)
                    fprintf(outputFile, "checks for upper/lower bounds worked!\n");
#if reduceWithSubstitutions
#else
                resurrectSubs(problemPtr);
                assert(nSUB == 0);
#endif
                return 1;
            };
        };


    if (TRACE)
        fprintf(outputFile, "*** Doing potentially expensive elimination tests for red equations\n");
    pleaseNoEqualitiesInSimplifiedProblems++;
    eliminateRed(problemPtr, expensive);
    pleaseNoEqualitiesInSimplifiedProblems--;
    result = 0;
    assert(nEQ == 0);
    for (e = nGEQ - 1; e >= 0; e--)
        if (GEQs[e].color == red)
            result = 1;
    if (TRACE)
        if (!result)
            fprintf(outputFile, "******************** Redudant Red Equations eliminated!!\n");
        else
            fprintf(outputFile, "******************** Red Equations remain\n");
    if (DEBUG)
        printProblem(problemPtr);

#if reduceWithSubstitutions
#else
    resurrectSubs(problemPtr);
    assert(nSUB == 0);
#endif
    return result;
}

int simplifyApproximate(Problem *problemPtr)
{
    int result;

    inApproximateMode = 1;
    if (TRACE)
        fprintf(outputFile, "Entering Approximate Mode\n");

    result = simplifyProblem(problemPtr);

    if (nVars != safeVars) {
        fprintf(outputFile, "assertion blown!\n");
        printProblem(problemPtr);
        fflush(outputFile);
        assert(nVars == safeVars);
    };

    if (TRACE)
        fprintf(outputFile, "Leaving Approximate Mode\n");
    inApproximateMode = 0;

#if reduceWithSubstitutions
#else
    assert(nSUB == 0);
#endif
    return (result);
}

int simplifyProblem(Problem *problemPtr)
{
    int i;
    foundReduction = FALSE;

    if (!problemPtr->variablesInitialized) {
        initializeVariables(problemPtr);
    };


#ifdef clearForwardingPointers
    for (i = 1; i <= nVars; i++)
        if (problemPtr->_var[i] > 0)
            problemPtr->forwardingAddress[problemPtr->_var[i]] = 0;
#endif

    if (nextKey * 3 > maxKeys) {
        int e;
        hashVersion++;
        nextKey = maxVars + 1;
        for (e = nGEQ - 1; e >= 0; e--)
            GEQs[e].touched = TRUE;
        for (i = 0; i < hashTableSize; i++)
            hashMaster[i].touched = -1;
        problemPtr->hashVersion = hashVersion;
    }
    else if (problemPtr->hashVersion != hashVersion) {
        int e;
        for (e = nGEQ - 1; e >= 0; e--)
            GEQs[e].touched = TRUE;
        problemPtr->hashVersion = hashVersion;
    };

    nonConvex = 0;
    if (nVars > nEQ + 3 * safeVars)
        freeEliminations(problemPtr, safeVars);

    solve(problemPtr, SIMPLIFY);
    if (foundReduction) {
        for (i = 1; i <= safeVars; i++)
            problemPtr->forwardingAddress[problemPtr->_var[i]] = i;
        for (i = 0; i < nSUB; i++)
            problemPtr->forwardingAddress[SUBs[i].key] = -i - 1;
    };
#if reduceWithSubstitutions
#else
    assert(pleaseNoEqualitiesInSimplifiedProblems
        || !foundReduction || nSUB == 0);
#endif
    return (foundReduction);
}


void unprotectVariable(Problem *problemPtr, int v)
{
    int e, t, j, i;
    i = problemPtr->forwardingAddress[v];
    if (i < 0) {
        i = -1 - i;
        //nSUB--;
        problemPtr->addNumSUBs(-1);
        if (i < nSUB) {
            eqncpy(&SUBs[i], &SUBs[nSUB]);
            problemPtr->forwardingAddress[SUBs[i].key] = -i - 1;
        };
    }
    else {
        int bringToLife[maxVars];
        int comingBack = 0;
        int e2;
        for (e = nSUB - 1; e >= 0; e--)
            if (bringToLife[e] = (SUBs[e].coef[i] != 0))
                comingBack++;

        for (e2 = nSUB - 1; e2 >= 0; e2--)
            if (bringToLife[e2]) {
                problemPtr->addToVarsN(1);
                //nVars++;
                safeVars++;
                if (safeVars < nVars) {
                    for (e = nGEQ - 1; e >= 0; e--) {
                        GEQs[e].coef[nVars] = GEQs[e].coef[safeVars];
                        GEQs[e].coef[safeVars] = 0;
                    };
                    for (e = nEQ - 1; e >= 0; e--) {
                        EQs[e].coef[nVars] = EQs[e].coef[safeVars];
                        EQs[e].coef[safeVars] = 0;
                    };
                    for (e = nSUB - 1; e >= 0; e--) {
                        SUBs[e].coef[nVars] = SUBs[e].coef[safeVars];
                        SUBs[e].coef[safeVars] = 0;
                    };
                    problemPtr->_var[nVars] = problemPtr->_var[safeVars];
                    problemPtr->forwardingAddress[problemPtr->_var[nVars]] = nVars;
                }
                else {
                    for (e = nGEQ - 1; e >= 0; e--) {
                        GEQs[e].coef[safeVars] = 0;
                    };
                    for (e = nEQ - 1; e >= 0; e--) {
                        EQs[e].coef[safeVars] = 0;
                    };
                    for (e = nSUB - 1; e >= 0; e--) {
                        SUBs[e].coef[safeVars] = 0;
                    };
                };

                problemPtr->_var[safeVars] = SUBs[e2].key;
                problemPtr->forwardingAddress[SUBs[e2].key] = safeVars;

                const int numEQ = nEQ;
                problemPtr->addNumEqs(1);

                eqncpy(&(EQs[numEQ]), &(SUBs[e2]));
                //EQs[nEQ++].coef[problemPtr->_safeVars] = -1;
                EQs[numEQ].coef[problemPtr->_safeVars] = -1;                

                assert(nEQ <= maxEQs);
                if (e2 < nSUB - 1)
                    eqncpy(&(SUBs[e2]), &(SUBs[nSUB - 1]));
                //nSUB--;
                problemPtr->addNumSUBs(-1);
            };




        if (i < safeVars) {
            j = safeVars;
            for (e = nSUB - 1; e >= 0; e--) {
                t = SUBs[e].coef[j];
                SUBs[e].coef[j] = SUBs[e].coef[i];
                SUBs[e].coef[i] = t;
            };
            for (e = nGEQ - 1; e >= 0; e--)
                if (GEQs[e].coef[j] != GEQs[e].coef[i]) {
                    GEQs[e].touched = TRUE;
                    t = GEQs[e].coef[j];
                    GEQs[e].coef[j] = GEQs[e].coef[i];
                    GEQs[e].coef[i] = t;
                };
            for (e = nEQ - 1; e >= 0; e--) {
                t = EQs[e].coef[j];
                EQs[e].coef[j] = EQs[e].coef[i];
                EQs[e].coef[i] = t;
            };
            t = problemPtr->_var[j];
            problemPtr->_var[j] = problemPtr->_var[i];
            problemPtr->_var[i] = t;
            problemPtr->forwardingAddress[problemPtr->_var[i]] = i;
            problemPtr->forwardingAddress[problemPtr->_var[j]] = j;
        };
        safeVars--;
    };
    chainUnprotect(problemPtr);

}


int constrainVariableSign(Problem *problemPtr, int color, int i, int sign)
{
    int nV = nVars;
    int e, k, j;

    k = problemPtr->forwardingAddress[i];
    if (k < 0) {
        k = -1 - k;

        if (sign != 0) {
            //e = nGEQ++;
            e = nGEQ;
            problemPtr->addNumGEqs(1);

            eqncpy(&GEQs[e], &SUBs[k]);
            for (j = 0; j <= nV; j++)
                GEQs[e].coef[j] *= sign;
            GEQs[e].coef[0]--;
            GEQs[e].touched = 1;
            GEQs[e].color = color;
        }
        else {
            //e = nEQ++;
            e = nEQ;
            problemPtr->addNumEqs(1);

            assert(nEQ <= maxEQs);
            eqncpy(&EQs[e], &SUBs[k]);
            EQs[e].color = color;
        };

    }
    else if (sign != 0) {
        //e = nGEQ++;
        e = nGEQ;
        problemPtr->addNumGEqs(1);

        eqnzero(&GEQs[e]);
        GEQs[e].coef[k] = sign;
        GEQs[e].coef[0] = -1;
        GEQs[e].touched = 1;
        GEQs[e].color = color;
    }
    else {
        //e = nEQ++;
        e = nEQ;
        problemPtr->addNumEqs(1);

        assert(nEQ <= maxEQs);
        eqnzero(&EQs[e]);
        EQs[e].coef[k] = 1;
        EQs[e].color = color;
    };
    unprotectVariable(problemPtr, i);
    return (simplifyProblem(problemPtr));
}

void constrainVariableValue(Problem *problemPtr, int color, int i, int value)
{
    int e, k;

    k = problemPtr->forwardingAddress[i];
    if (k < 0) {
        k = -1 - k;

        //e = nEQ++;
        e = nEQ;
        problemPtr->addNumEqs(1);

        assert(nEQ <= maxEQs);
        eqncpy(&EQs[e], &SUBs[k]);
        EQs[e].coef[0] -= value;

    }
    else {
        //e = nEQ++;
        e = nEQ;
        problemPtr->addNumEqs(1);

        eqnzero(&EQs[e]);
        EQs[e].coef[k] = 1;
        EQs[e].coef[0] = -value;
    };
    EQs[e].color = color;
}

int queryVariable(Problem *problemPtr, int i, int *lowerBound, int *upperBound)
{
    int nV = nVars;
    int e, j;
    int isSimple;
    int coupled = FALSE;
    i = problemPtr->forwardingAddress[i];

    (*lowerBound) = negInfinity;
    (*upperBound) = posInfinity;

    if (i < 0) {
        int easy = TRUE;
        i = -i - 1;
        for (j = 1; j <= nV; j++)
            if (SUBs[i].coef[j] != 0)
                easy = FALSE;
        if (easy) {
            *upperBound = *lowerBound = SUBs[i].coef[0];
            return (FALSE);
        };
        return (TRUE);
    };

    for (e = nSUB - 1; e >= 0; e--)
        if (SUBs[e].coef[i] != 0)
            coupled = TRUE;

    for (e = nEQ - 1; e >= 0; e--)
        if (EQs[e].coef[i] != 0) {
            isSimple = TRUE;
            for (j = 1; j <= nV; j++)
                if (i != j && EQs[e].coef[j] != 0) {
                    isSimple = FALSE;
                    coupled = TRUE;
                    break;
                };
            if (!isSimple)
                continue;
            else {
                *lowerBound = *upperBound = -EQs[e].coef[i] * EQs[e].coef[0];
                return (FALSE);
            };
        };
    for (e = nGEQ - 1; e >= 0; e--)
        if (GEQs[e].coef[i] != 0) {
            if (GEQs[e].key == i) {
                setMax(*lowerBound, -GEQs[e].coef[0]);
            }
            else if (GEQs[e].key == -i) {
                setMin(*upperBound, GEQs[e].coef[0]);
            }
            else
                coupled = TRUE;
        };
    return (coupled);
}

extern void queryCoupledVariable(Problem *problemPtr, int i, int *l, int *u, int *couldBeZero, int lowerBound, int upperBound);

int queryVariableBounds(Problem *problemPtr, int i, int *l, int *u)
{
    int coupled;
    *l = negInfinity;
    *u = posInfinity;
    coupled = queryVariable(problemPtr, i, l, u);
    if (!coupled || (nVars == 1 && problemPtr->forwardingAddress[i] == 1))
        return 0;
    if (abs(problemPtr->forwardingAddress[i]) == 1 && nVars + nSUB == 2 && nEQ + nSUB == 1) {
        int couldBeZero;
        queryCoupledVariable(problemPtr, i, l, u, &couldBeZero, negInfinity, posInfinity);
        return 0;
    };
    return 1;
}

void queryCoupledVariable(Problem *problemPtr, int i, int *l, int *u, int *couldBeZero, int lowerBound, int upperBound)
{
    int e, b1, b2;
    Eqn eqn;
    int sign;
    int v;

    if (abs(problemPtr->forwardingAddress[i]) != 1 || nVars + nSUB != 2 || nEQ + nSUB != 1) {
        fprintf(outputFile, "queryCoupledVariablecalled with bad parameters\n");
        printProblem(problemPtr);
        Exit(2);
    };

    if (problemPtr->forwardingAddress[i] == -1) {
        eqn = &SUBs[0];
        sign = 1;
        v = 1;
    }
    else {
        eqn = &EQs[0];
        sign = -eqn->coef[1];
        v = 2;
    };

    /* Variable i is defined in terms of variable v */

    for (e = nGEQ - 1; e >= 0; e--)
        if (GEQs[e].coef[v] != 0) {
            if (GEQs[e].coef[v] == 1) {
                setMax(lowerBound, -GEQs[e].coef[0])
            }
            else {
                setMin(upperBound, GEQs[e].coef[0]);
            };
        };
    /* lowerBound and upperBound are bounds on the value of v */

    if (lowerBound > upperBound) {
        *l = posInfinity;
        *u = negInfinity;
        *couldBeZero = 0;
        return;
    };
    if (lowerBound == negInfinity) {
        if (eqn->coef[v] > 0)
            b1 = sign * negInfinity;
        else
            b1 = -sign * negInfinity;
    }
    else
        b1 = sign * (eqn->coef[0] + eqn->coef[v] * lowerBound);
    if (upperBound == posInfinity) {
        if (eqn->coef[v] > 0)
            b2 = sign * posInfinity;
        else
            b2 = -sign * posInfinity;
    }
    else
        b2 = sign * (eqn->coef[0] + eqn->coef[v] * upperBound);

    /* b1 and b2 are bounds on the value of i (don't know which is upper bound) */
    if (b1 <= b2) {
        setMax(*l, b1);
        setMin(*u, b2);
    }
    else {
        setMax(*l, b2);
        setMin(*u, b1);
    };
    *couldBeZero = *l <= 0 && 0 <= *u && intMod(eqn->coef[0], abs(eqn->coef[v])) == 0;
}



int queryVariableSigns(Problem *problemPtr, int i, int dd_lt, int dd_eq, int dd_gt, int lowerBound, int upperBound, bool *distKnown, int *dist)
{
    int result;
    int l, u;
    int couldBeZero;

    l = negInfinity;
    u = posInfinity;

    queryCoupledVariable(problemPtr, i, &l, &u, &couldBeZero, lowerBound, upperBound);
    result = 0;
    if (l < 0)
        result |= dd_gt;
    if (u > 0)
        result |= dd_lt;
    if (couldBeZero)
        result |= dd_eq;
    if (l == u) {
        *distKnown = 1;
        *dist = l;
    }
    else 
        *distKnown = 0;    
    return (result);
}


static int omegaInitialized = 0;

void initializeOmega()
{
    int i;
    if (omegaInitialized)
        return;

    nextWildCard = 0;
    nextKey = maxVars + 1;
    for (i = 0; i < hashTableSize; i++)
        hashMaster[i].touched = -1;

    sprintf(wildName[1], "alpha");
    sprintf(wildName[2], "beta");
    sprintf(wildName[3], "gamma");
    sprintf(wildName[4], "delta");
    sprintf(wildName[5], "tau");
    sprintf(wildName[6], "sigma");
    sprintf(wildName[7], "chi");
    sprintf(wildName[8], "omega");
    sprintf(wildName[9], "pi");
    sprintf(wildName[10], "ni");
    sprintf(wildName[11], "Alpha");
    sprintf(wildName[12], "Beta");
    sprintf(wildName[13], "Gamma");
    sprintf(wildName[14], "Delta");
    sprintf(wildName[15], "Tau");
    sprintf(wildName[16], "Sigma");
    sprintf(wildName[17], "Chi");
    sprintf(wildName[18], "Omega");
    sprintf(wildName[19], "Pi");

    omegaInitialized = 1;
}


void setOutputFile(FILE * file)
{
    /* sets the file to which printProblem should send its output to "file" */

    outputFile = file;

}				/* end setOutputFile(FILE *file) */