summaryrefslogtreecommitdiff
path: root/omegalib/omega/src/omega_core/oc.cc
diff options
context:
space:
mode:
Diffstat (limited to 'omegalib/omega/src/omega_core/oc.cc')
-rw-r--r--omegalib/omega/src/omega_core/oc.cc754
1 files changed, 0 insertions, 754 deletions
diff --git a/omegalib/omega/src/omega_core/oc.cc b/omegalib/omega/src/omega_core/oc.cc
deleted file mode 100644
index 0dc9b49..0000000
--- a/omegalib/omega/src/omega_core/oc.cc
+++ /dev/null
@@ -1,754 +0,0 @@
-/*****************************************************************************
- Copyright (C) 1994-2000 the Omega Project Team
- Copyright (C) 2005-2011 Chun Chen
- All Rights Reserved.
-
- Purpose:
- Simplify a problem.
-
- Notes:
-
- History:
- 12/10/06 Improved gist function, by Chun Chen.
-*****************************************************************************/
-
-#include <omega/omega_core/oc_i.h>
-
-namespace omega {
-
-eqn SUBs[maxVars+1];
-Memory redMemory[maxVars+1];
-
-int Problem::reduceProblem() {
- int result;
- checkVars(nVars+1);
- assert(omegaInitialized);
- if (nVars > nEQs + 3 * safeVars)
- freeEliminations(safeVars);
-
- check();
- if (!mayBeRed && nSUBs == 0 && safeVars == 0) {
- result = solve(OC_SOLVE_UNKNOWN);
- nGEQs = 0;
- nEQs = 0;
- nSUBs = 0;
- nMemories = 0;
- if (!result) {
- int e = newEQ();
- assert(e == 0);
- eqnnzero(&EQs[0], nVars);
- EQs[0].color = EQ_BLACK;
- EQs[0].coef[0] = 1;
- }
- check();
- return result;
- }
- return solve(OC_SOLVE_SIMPLIFY);
-}
-
-
-int Problem::simplifyProblem(int verify, int subs, int redundantElimination) {
- checkVars(nVars+1);
- assert(omegaInitialized);
- setInternals();
- check();
- if (!reduceProblem()) goto returnFalse;
- if (verify) {
- addingOuterEqualities++;
- int r = verifyProblem();
- addingOuterEqualities--;
- if (!r) goto returnFalse;
- if (nEQs) { // found some equality constraints during verification
- int numRed = 0;
- if (mayBeRed)
- for (int e = nGEQs - 1; e >= 0; e--) if (GEQs[e].color == EQ_RED) numRed++;
- if (mayBeRed && nVars == safeVars && numRed == 1)
- nEQs = 0; // discard them
- else if (!reduceProblem()) {
- assert(0 && "Added equality constraint to verified problem generates false");
- }
- }
- }
- if (redundantElimination) {
- if (redundantElimination > 1) {
- if (!expensiveEqualityCheck()) goto returnFalse;
- }
- if (!quickKill(0)) goto returnFalse;
- if (redundantElimination > 1) {
- if (!expensiveKill()) goto returnFalse;
- }
- }
- resurrectSubs();
- if (redundantElimination)
- simplifyStrideConstraints();
- if (redundantElimination > 2 && safeVars < nVars) {
- if (!quickKill(0)) goto returnFalse;
- return simplifyProblem(verify, subs, redundantElimination-2);
- }
- setExternals();
- assert(nMemories == 0);
- return (1);
-
-returnFalse:
- nGEQs = 0;
- nEQs = 0;
- resurrectSubs();
- nGEQs = 0;
- nEQs = 0;
- int neweq = newEQ();
- assert(neweq == 0);
- eqnnzero(&EQs[neweq], nVars);
- EQs[neweq].color = EQ_BLACK;
- EQs[neweq].coef[0] = 1;
- nMemories = 0;
- return 0;
-}
-
-int Problem::simplifyApproximate(bool strides_allowed) {
- int result;
- checkVars(nVars+1);
- assert(inApproximateMode == 0);
-
- inApproximateMode = 1;
- inStridesAllowedMode = strides_allowed;
- if (TRACE)
- fprintf(outputFile, "Entering Approximate Mode [\n");
-
- assert(omegaInitialized);
- result = simplifyProblem(0,0,0);
-
- while (result && !strides_allowed && nVars > safeVars) {
- int e;
- for (e = nGEQs - 1; e >= 0; e--)
- if (GEQs[e].coef[nVars]) deleteGEQ(e);
- for (e = nEQs - 1; e >= 0; e--)
- if (EQs[e].coef[nVars]) deleteEQ(e);
- nVars--;
- result = simplifyProblem(0,0,0);
- }
-
- if (TRACE)
- fprintf(outputFile, "] Leaving Approximate Mode\n");
-
- assert(inApproximateMode == 1);
- inApproximateMode=0;
- inStridesAllowedMode = 0;
-
- assert(nMemories == 0);
- return (result);
-}
-
-
-
-
-/*
- * 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.
- */
-
-#ifdef GIST_CHECK
-Problem full_answer, context;
-Problem redProblem;
-#endif
-
-redCheck Problem::redSimplifyProblem(int effort, int computeGist) {
- int result;
- int e;
-
- checkVars(nVars+1);
- assert(mayBeRed >= 0);
- mayBeRed++;
-
- assert(omegaInitialized);
- if (TRACE) {
- fprintf(outputFile, "Checking for red equations:\n");
- printProblem();
- }
- setInternals();
-
-#ifdef GIST_CHECK
- int r1,r2;
- if (TRACE)
- fprintf(outputFile,"Set-up for gist invariant checking[\n");
- redProblem = *this;
- redProblem.check();
- full_answer = *this;
- full_answer.check();
- full_answer.turnRedBlack();
- full_answer.check();
- r1 = full_answer.simplifyProblem(1,0,1);
- full_answer.check();
- if (DBUG) fprintf(outputFile,"Simplifying context [\n");
- context = *this;
- context.check();
- context.deleteRed();
- context.check();
- r2 = context.simplifyProblem(1,0,1);
- context.check();
- if (DBUG) fprintf(outputFile,"] Simplifying context\n");
-
- if (!r2 && TRACE) fprintf(outputFile, "WARNING: Gist context is false!\n");
- if (TRACE)
- fprintf(outputFile,"] Set-up for gist invariant checking done\n");
-#endif
-
- // Save known integer modular equations, -- by chun 12/10/2006
- eqn ModularEQs[nEQs];
- int nModularEQs = 0;
- int old_nVars = nVars;
- for (int e = 0; e < nEQs; e++)
- if (EQs[e].color != EQ_RED)
- for (int i = safeVars+1; i <= nVars; i++)
- if (EQs[e].coef[i] != 0) {
- eqnncpy(&(ModularEQs[nModularEQs++]), &(EQs[e]), nVars);
- break;
- }
-
-
- if (solveEQ() == false) {
- if (TRACE)
- fprintf(outputFile, "Gist is FALSE\n");
- if (computeGist) {
- nMemories = 0;
- nGEQs = 0;
- nEQs = 0;
- resurrectSubs();
- nGEQs = 0;
- nEQs = 0;
- int neweq = newEQ();
- assert(neweq == 0);
- eqnnzero(&EQs[neweq], nVars);
- EQs[neweq].color = EQ_RED;
- EQs[neweq].coef[0] = 1;
- }
- mayBeRed--;
- return redFalse;
- }
-
- if (!computeGist && nMemories)
- return redConstraints;
- if (normalize() == normalize_false) {
- if (TRACE)
- fprintf(outputFile, "Gist is FALSE\n");
- if (computeGist) {
- nGEQs = 0;
- nEQs = 0;
- resurrectSubs();
- nMemories = 0;
- nGEQs = 0;
- nEQs = 0;
- int neweq = newEQ();
- assert(neweq == 0);
- eqnnzero(&EQs[neweq], nVars);
- EQs[neweq].color = EQ_RED;
- EQs[neweq].coef[0] = 1;
- }
- mayBeRed--;
- return redFalse;
- }
-
- result = 0;
- for (e = nGEQs - 1; e >= 0; e--) if (GEQs[e].color == EQ_RED) result = 1;
- for (e = nEQs - 1; e >= 0; e--) if (EQs[e].color == EQ_RED) result = 1;
- if (nMemories) result = 1;
- if (!result) {
- if (computeGist) {
- nGEQs = 0;
- nEQs = 0;
- resurrectSubs();
- nGEQs = 0;
- nMemories = 0;
- nEQs = 0;
- }
- mayBeRed--;
- return noRed;
- }
-
- result = simplifyProblem(effort?1:0,1,0);
-#ifdef GIST_CHECK
- if (!r1 && TRACE && result)
- fprintf(outputFile, "Gist is False but not detected\n");
-#endif
- if (!result) {
- if (TRACE)
- fprintf(outputFile, "Gist is FALSE\n");
- if (computeGist) {
- nGEQs = 0;
- nEQs = 0;
- resurrectSubs();
- nGEQs = 0;
- nEQs = 0;
- int neweq = newEQ();
- assert(neweq == 0);
- nMemories = 0;
- eqnnzero(&EQs[neweq], nVars);
- EQs[neweq].color = EQ_RED;
- EQs[neweq].coef[0] = 1;
- }
- mayBeRed--;
- return redFalse;
- }
-
- freeRedEliminations();
-
- result = 0;
- for (e = nGEQs - 1; e >= 0; e--) if (GEQs[e].color == EQ_RED) result = 1;
- for (e = nEQs - 1; e >= 0; e--) if (EQs[e].color == EQ_RED) result = 1;
- if (nMemories) result = 1;
- if (!result) {
- if (computeGist) {
- nGEQs = 0;
- nEQs = 0;
- resurrectSubs();
- nGEQs = 0;
- nMemories = 0;
- nEQs = 0;
- }
- mayBeRed--;
- return noRed;
- }
-
- if (effort && (computeGist || !nMemories)) {
- if (TRACE)
- fprintf(outputFile, "*** Doing potentially expensive elimination tests for red equations [\n");
- quickRedKill(computeGist);
- checkGistInvariant();
- result = nMemories;
- for (e = nGEQs - 1; e >= 0; e--) if (GEQs[e].color == EQ_RED) result++;
- for (e = nEQs - 1; e >= 0; e--) if (EQs[e].color == EQ_RED) result++;
- if (result && effort > 1 && (computeGist || !nMemories)) {
- expensiveRedKill();
- result = nMemories;
- for (e = nGEQs-1; e >= 0; e--) if (GEQs[e].color == EQ_RED) result++;
- for (e = nEQs-1; e >= 0; e--) if (EQs[e].color == EQ_RED) result++;
- }
-
- if (!result) {
- if (TRACE)
- fprintf(outputFile, "]******************** Redudant Red Equations eliminated!!\n");
- if (computeGist) {
- nGEQs = 0;
- nEQs = 0;
- resurrectSubs();
- nGEQs = 0;
- nMemories = 0;
- nEQs = 0;
- }
- mayBeRed--;
- return noRed;
- }
-
- if (TRACE) fprintf(outputFile, "]******************** Red Equations remain\n");
- if (DEBUG) printProblem();
- }
-
- if (computeGist) {
- resurrectSubs();
- cleanoutWildcards();
-
-
- // Restore saved modular equations into EQs without affecting the problem
- if (nEQs+nModularEQs > allocEQs) {
- allocEQs = padEQs(allocEQs, nEQs+nModularEQs);
- eqn *new_eqs = new eqn[allocEQs];
- for (int e = 0; e < nEQs; e++)
- eqnncpy(&(new_eqs[e]), &(EQs[e]), nVars);
- delete[] EQs;
- EQs= new_eqs;
- }
-
- for (int e = 0; e < nModularEQs; e++) {
- eqnncpy(&(EQs[nEQs+e]), &(ModularEQs[e]), old_nVars);
- EQs[nEQs+e].color = EQ_RED;
- Tuple<coef_t> t(safeVars);
- for (int i = 1; i <= safeVars; i++)
- t[i] = ModularEQs[e].coef[var[i]];
- for (int i = 1; i <= safeVars; i++)
- EQs[nEQs+e].coef[i] = t[i];
- }
-
-
- // Now simplify modular equations using Chinese remainder theorem -- by chun 12/10/2006
- for (int e = 0; e < nEQs; e++)
- if (EQs[e].color == EQ_RED) {
- int wild_pos = -1;
- for (int i = safeVars+1; i <= nVars; i++)
- if (EQs[e].coef[i] != 0) {
- wild_pos = i;
- break;
- }
-
- if (wild_pos == -1)
- continue;
-
- for (int e2 = e+1; e2 < nEQs+nModularEQs; e2++)
- if (EQs[e2].color == EQ_RED) {
- int wild_pos2 = -1;
- for (int i = safeVars+1; i <= ((e2<nEQs)?nVars:old_nVars); i++)
- if (EQs[e2].coef[i] != 0) {
- wild_pos2 = i;
- break;
- }
-
- if (wild_pos2 == -1)
- continue;
-
- coef_t g = gcd(abs(EQs[e].coef[wild_pos]), abs(EQs[e2].coef[wild_pos2]));
- coef_t g2 = 1;
- coef_t g3;
- EQs[e].color = EQs[e2].color = EQ_BLACK;
- while ((g3 = factor(g)) != 1) {
- coef_t gg = g2 * g3;
- g = g/g3;
-
- bool match = true;
- coef_t c = EQs[e].coef[0];
- coef_t c2 = EQs[e2].coef[0];
- bool change_sign = false;
- for (int i = 1; i <= safeVars; i++) {
- coef_t coef = int_mod_hat(EQs[e].coef[i], gg);
- coef_t coef2 = int_mod_hat(EQs[e2].coef[i], gg);
-
- if (coef == 0 && coef2 == 0)
- continue;
-
- if (change_sign && coef == -coef2)
- continue;
-
- if (!change_sign) {
- if (coef == coef2)
- continue;
- else if (coef == -coef2) {
- change_sign = true;
- continue;
- }
- }
-
- if (coef != 0) {
- coef_t t = query_variable_mod(i, gg/gcd(abs(coef), gg), EQ_RED, nModularEQs, old_nVars);
- if (t == posInfinity) {
- match = false;
- break;
- }
-
- c += coef * t;
- }
- if (coef2 != 0) {
- coef_t t = query_variable_mod(i, gg/gcd(abs(coef2), gg), EQ_RED, nModularEQs, old_nVars);
- if (t == posInfinity) {
- match = false;
- break;
- }
-
- c2 += coef2 * t;
- }
- }
- if ((change_sign && int_mod_hat(c, gg) != -int_mod_hat(c2, gg)) ||
- (!change_sign && int_mod_hat(c, gg) != int_mod_hat(c2, gg)))
- match = false;
-
- if (match)
- g2 = gg;
- }
- EQs[e].color = EQs[e2].color = EQ_RED;
-
- if (g2 == 1)
- continue;
-
- if (g2 == abs(EQs[e].coef[wild_pos])) {
- EQs[e].color = EQ_BLACK;
- break;
- }
- else if (e2 < nEQs && g2 == abs(EQs[e2].coef[wild_pos2]))
- EQs[e2].color = EQ_BLACK;
- else {
- coef_t g4 = abs(EQs[e].coef[wild_pos])/g2;
- while (lcm(g2, g4) != abs(EQs[e].coef[wild_pos])) {
- assert(lcm(g2, g4) < abs(EQs[e].coef[wild_pos]));
- g4 *= abs(EQs[e].coef[wild_pos])/lcm(g2, g4);
- }
-
- for (int i = 0; i <= safeVars; i++)
- EQs[e].coef[i] = int_mod_hat(EQs[e].coef[i], g4);
- EQs[e].coef[wild_pos] = (EQs[e].coef[wild_pos]>0?1:-1)*g4;
- }
- }
- }
-
- deleteBlack();
- }
-
- setExternals();
- mayBeRed--;
- assert(nMemories == 0);
- return redConstraints;
-}
-
-
-void Problem::convertEQstoGEQs(bool excludeStrides) {
- int i;
- int e;
- if (DBUG)
- fprintf(outputFile, "Converting all EQs to GEQs\n");
- simplifyProblem(0,0,0);
- for(e=0;e<nEQs;e++) {
- bool isStride = 0;
- int e2 = newGEQ();
- if (excludeStrides)
- for(i = safeVars+1; i <= nVars; i++)
- isStride = isStride || (EQs[e].coef[i] != 0);
- if (isStride) continue;
- eqnncpy(&GEQs[e2], &EQs[e], nVars);
- GEQs[e2].touched = 1;
- e2 = newGEQ();
- eqnncpy(&GEQs[e2], &EQs[e], nVars);
- GEQs[e2].touched = 1;
- for (i = 0; i <= nVars; i++)
- GEQs[e2].coef[i] = -GEQs[e2].coef[i];
- }
- // If we have eliminated all EQs, can set nEQs to 0
- // If some strides are left, we don't know the position of them in the EQs
- // array, so decreasing nEQs might remove wrong EQs -- we just leave them
- // all in. (could sort the EQs to move strides to the front, but too hard.)
- if (!excludeStrides) nEQs=0;
- if (DBUG)
- printProblem();
-}
-
-
-void Problem::convertEQtoGEQs(int eq) {
- int i;
- if (DBUG)
- fprintf(outputFile, "Converting EQ %d to GEQs\n",eq);
- int e2 = newGEQ();
- eqnncpy(&GEQs[e2], &EQs[eq], nVars);
- GEQs[e2].touched = 1;
- e2 = newGEQ();
- eqnncpy(&GEQs[e2], &EQs[eq], nVars);
- GEQs[e2].touched = 1;
- for (i = 0; i <= nVars; i++)
- GEQs[e2].coef[i] = -GEQs[e2].coef[i];
- if (DBUG)
- printProblem();
-}
-
-
-/*
- * Calculate value of variable modulo integer from problem's equation
- * set plus additional saved modular equations embedded in the same
- * EQs array (hinted by nModularEQs) if available. If there is no
- * solution, return posInfinity.
- */
-coef_t Problem::query_variable_mod(int v, coef_t factor, int color, int nModularEQs, int nModularVars) const {
- if (safeVars < v)
- return posInfinity;
-
- Tuple<bool> working_on(safeVars);
- for (int i = 1; i <= safeVars; i++)
- working_on[i] = false;
-
- return query_variable_mod(v, factor, color, nModularEQs, nModularVars, working_on);
-}
-
-coef_t Problem::query_variable_mod(int v, coef_t factor, int color, int nModularEQs, int nModularVars, Tuple<bool> &working_on) const {
- working_on[v] = true;
-
- for (int e = 0; e < nEQs+nModularEQs; e++)
- if (EQs[e].color == color) {
- coef_t coef = int_mod_hat(EQs[e].coef[v], factor);
- if (abs(coef) != 1)
- continue;
-
- bool wild_factored = true;
- for (int i = safeVars+1; i <= ((e<nEQs)?nVars:nModularVars); i++)
- if (int_mod_hat(EQs[e].coef[i], factor) != 0) {
- wild_factored = false;
- break;
- }
- if (!wild_factored)
- continue;
-
- coef_t result = 0;
- for (int i = 1; i <= safeVars; i++)
- if (i != v) {
- coef_t p = int_mod_hat(EQs[e].coef[i], factor);
-
- if (p == 0)
- continue;
-
- if (working_on[i] == true) {
- result = posInfinity;
- break;
- }
-
- coef_t q = query_variable_mod(i, factor, color, nModularEQs, nModularVars, working_on);
- if (q == posInfinity) {
- result = posInfinity;
- break;
- }
- result += p*q;
- }
-
- if (result != posInfinity) {
- result += EQs[e].coef[0];
- if (coef == 1)
- result = -result;
- working_on[v] = false;
-
- return int_mod_hat(result, factor);
- }
- }
-
- working_on[v] = false;
- return posInfinity;
-}
-
-
-
-#ifdef GIST_CHECK
-enum compareAnswer {apparentlyEqual, mightNotBeEqual, NotEqual};
-
-static compareAnswer checkEquiv(Problem *p1, Problem *p2) {
- int r1,r2;
-
- p1->check();
- p2->check();
- p1->resurrectSubs();
- p2->resurrectSubs();
- p1->check();
- p2->check();
- p1->putVariablesInStandardOrder();
- p2->putVariablesInStandardOrder();
- p1->check();
- p2->check();
- p1->ordered_elimination(0);
- p2->ordered_elimination(0);
- p1->check();
- p2->check();
- r1 = p1->simplifyProblem(1,1,0);
- r2 = p2->simplifyProblem(1,1,0);
- p1->check();
- p2->check();
-
- if (!r1 || !r2) {
- if (r1 == r2) return apparentlyEqual;
- return NotEqual;
- }
- if (p1->nVars != p2->nVars
- || p1->nGEQs != p2->nGEQs
- || p1->nSUBs != p2->nSUBs
- || p1->checkSum() != p2->checkSum()) {
- r1 = p1->simplifyProblem(0,1,1);
- r2 = p2->simplifyProblem(0,1,1);
- assert(r1 && r2);
- p1->check();
- p2->check();
- if (p1->nVars != p2->nVars
- || p1->nGEQs != p2->nGEQs
- || p1->nSUBs != p2->nSUBs
- || p1->checkSum() != p2->checkSum()) {
- r1 = p1->simplifyProblem(0,1,2);
- r2 = p2->simplifyProblem(0,1,2);
- p1->check();
- p2->check();
- assert(r1 && r2);
- if (p1->nVars != p2->nVars
- || p1->nGEQs != p2->nGEQs
- || p1->nSUBs != p2->nSUBs
- || p1->checkSum() != p2->checkSum()) {
- p1->check();
- p2->check();
- p1->resurrectSubs();
- p2->resurrectSubs();
- p1->check();
- p2->check();
- p1->putVariablesInStandardOrder();
- p2->putVariablesInStandardOrder();
- p1->check();
- p2->check();
- p1->ordered_elimination(0);
- p2->ordered_elimination(0);
- p1->check();
- p2->check();
- r1 = p1->simplifyProblem(1,1,0);
- r2 = p2->simplifyProblem(1,1,0);
- p1->check();
- p2->check();
- }
- }
- }
-
- if (p1->nVars != p2->nVars
- || p1->nSUBs != p2->nSUBs
- || p1->nGEQs != p2->nGEQs
- || p1->nSUBs != p2->nSUBs) return NotEqual;
- if (p1->checkSum() != p2->checkSum()) return mightNotBeEqual;
- return apparentlyEqual;
-}
-#endif
-
-void Problem::checkGistInvariant() const {
-#ifdef GIST_CHECK
- Problem new_answer;
- int r;
-
- check();
- fullAnswer.check();
- context.check();
-
- if (safeVars < nVars) {
- if (DBUG) {
- fprintf(outputFile,"Can't check gist invariant due to wildcards\n");
- printProblem();
- }
- return;
- }
- if (DBUG) {
- fprintf(outputFile,"Checking gist invariant on: [\n");
- printProblem();
- }
-
- new_answer = *this;
- new_answer->resurrectSubs();
- new_answer->cleanoutWildcards();
- if (DEBUG) {
- fprintf(outputFile,"which is: \n");
- printProblem();
- }
- deleteBlack(&new_answer);
- turnRedBlack(&new_answer);
- if (DEBUG) {
- fprintf(outputFile,"Black version of answer: \n");
- printProblem(&new_answer);
- }
- problem_merge(&new_answer,&context);
-
- r = checkEquiv(&full_answer,&new_answer);
- if (r != apparentlyEqual) {
- fprintf(outputFile,"GIST INVARIANT REQUIRES MANUAL CHECK:[\n");
- fprintf(outputFile,"Original problem:\n");
- printProblem(&redProblem);
-
- fprintf(outputFile,"Context:\n");
- printProblem(&context);
-
- fprintf(outputFile,"Computed gist:\n");
- printProblem();
-
- fprintf(outputFile,"Combined answer:\n");
- printProblem(&full_answer);
-
- fprintf(outputFile,"Context && red constraints:\n");
- printProblem(&new_answer);
- fprintf(outputFile,"]\n");
- }
-
- if (DBUG) {
- fprintf(outputFile,"] Done checking gist invariant on\n");
- }
-#endif
-}
-
-} // namespace
generated by cgit v1.2.3-70-g09d2 (git 2.48.1) at 2025-02-02 06:00:06 +0000