cmake build

1 files changed, 1460 insertions, 0 deletions

diff --git a/omegalib/omega_lib/src/pres_conj.cc b/omegalib/omega_lib/src/pres_conj.cc
new file mode 100644
index 0000000..f3f458d
--- /dev/null
+++ b/omegalib/omega_lib/src/pres_conj.cc
@@ -0,0 +1,1460 @@
+/*****************************************************************************
+ Copyright (C) 1994-2000 the Omega Project Team
+ Copyright (C) 2005-2011 Chun Chen
+ All Rights Reserved.
+
+ Purpose:
+   class Conjunct.
+
+ Notes:
+
+ History:
+*****************************************************************************/
+
+#include <omega/omega_core/oc.h>
+#include <omega/pres_conj.h>
+#include <omega/pres_cmpr.h>
+#include <omega/Relation.h>
+#include <omega/omega_i.h>
+#include <set>
+
+namespace omega {
+
+int NR_CONJUNCTS, MAX_CONJUNCTS;
+
+/*
+ * Make a new wildcard variable, return WC number.
+ * Should be static to this file, but must be a friend of conjunct.
+ */
+int new_WC(Conjunct *nc, Problem *) {
+  Variable_ID wc = nc->declare();
+  int wc_no = nc->map_to_column(wc);
+  return(wc_no);
+}
+
+
+const char* get_var_name(unsigned int col, void * void_conj) {
+#if defined PRINT_COLUMN_NUMBERS
+  static char scum[512];
+#endif
+  Conjunct *c = (Conjunct *) void_conj;
+  if (col == 0)
+    return 0;
+  Variable_ID v = c->mappedVars[col];
+  assert(v!=0);
+#if defined PRINT_COLUMN_NUMBERS
+  strcpy(scum, v->char_name());
+  sprintf(scum + strlen(scum), "(%d)", col);
+  return scum;
+#endif
+  return v->char_name();
+}
+
+void Conjunct::promise_that_ub_solutions_exist(Relation &R) {
+#ifndef NDEBUG
+  Relation verify=Relation(R, this);
+  assert(verify.is_upper_bound_satisfiable());
+#endif 
+  verified = true;
+}
+
+
+int Conjunct::max_ufs_arity_of_set() {
+  int ma = 0, a;
+  for (Variable_ID_Iterator v(mappedVars); v; v++)
+    if ((*v)->kind() == Global_Var && (*v)->function_of() == Set_Tuple 
+        && query_variable_used(*v)) {
+      a = (*v)->get_global_var()->arity();
+      if (a > ma)
+        ma = a;
+    }
+  return ma;
+}
+
+
+int Conjunct::max_ufs_arity_of_in() {
+  int ma = 0, a;
+  for (Variable_ID_Iterator v(mappedVars); v; v++)
+    if ((*v)->kind() == Global_Var && (*v)->function_of() == Input_Tuple
+        && query_variable_used(*v)) {
+      a = (*v)->get_global_var()->arity();
+      if (a > ma)
+        ma = a;
+    }
+  return ma;
+}
+
+
+int Conjunct::max_ufs_arity_of_out() {
+  int ma = 0, a;
+  for (Variable_ID_Iterator v(mappedVars); v; v++)
+    if ((*v)->kind() == Global_Var &&  (*v)->function_of() == Output_Tuple
+        && query_variable_used(*v)) {
+      a = (*v)->get_global_var()->arity();
+      if (a > ma)
+        ma = a;
+    }
+  return ma;
+}
+
+
+bool Conjunct::is_unknown() const { 
+  assert(problem || comp_problem);
+  return !exact && ((problem && problem->nEQs==0 && problem->nGEQs==0) ||
+                    (comp_problem && comp_problem->no_constraints()));
+}
+
+
+/*
+ * Remove black constraints from the problem.
+ * Make all the remaining red constraints black.
+ */
+void Conjunct::rm_color_constrs() {
+  int geqs = 0, eqs = 0;
+
+  possible_leading_0s = -1;
+  guaranteed_leading_0s = -1;
+  leading_dir = 0;
+
+  for(int i=0; i<problem->nGEQs; i++) {
+    if(problem->GEQs[i].color) {
+      if(geqs!=i)
+        eqnncpy(&problem->GEQs[geqs], &problem->GEQs[i], problem->nVars);
+      problem->GEQs[geqs].color = EQ_BLACK;
+      geqs++;
+    }
+  }
+  problem->nGEQs = geqs;
+  
+  for(int i=0; i<problem->nEQs; i++) {
+    if(problem->EQs[i].color) {
+      if(eqs!=i)
+        eqnncpy(&problem->EQs[eqs], &problem->EQs[i], problem->nVars);
+      problem->EQs[eqs].color = EQ_BLACK;
+      eqs++;
+    }
+  }
+  problem->nEQs = eqs;
+}
+
+
+
+//
+// Conjunct constructors.
+//
+Conjunct::Conjunct() : 
+  F_Declaration(NULL, NULL),
+  mappedVars(0),
+  n_open_constraints(0),
+  cols_ordered(false),
+  simplified(false),
+  verified(false),
+  guaranteed_leading_0s(-1),
+  possible_leading_0s(-1),
+  leading_dir(0),
+  exact(true),
+  r_constrs(0) {
+  NR_CONJUNCTS++;
+  if (NR_CONJUNCTS>MAX_CONJUNCTS) MAX_CONJUNCTS = NR_CONJUNCTS;
+  problem = new Problem;
+  comp_problem = NULL;
+  problem->get_var_name = get_var_name;
+  problem->getVarNameArgs = (void *) this;
+}
+
+
+Conjunct::Conjunct(Formula *f, Rel_Body *r) : 
+  F_Declaration(f,r),
+  mappedVars(0),
+  n_open_constraints(0),
+  cols_ordered(false),
+  simplified(false),
+  verified(false),
+  guaranteed_leading_0s(-1),
+  possible_leading_0s(-1),
+  leading_dir(0),
+  exact(true),
+  r_constrs(0) { 
+  NR_CONJUNCTS++;
+  if (NR_CONJUNCTS>MAX_CONJUNCTS) MAX_CONJUNCTS = NR_CONJUNCTS;
+  problem = new Problem;
+  comp_problem = NULL;
+  problem->get_var_name = get_var_name;
+  problem->getVarNameArgs = (void *) this ;
+}
+
+void internal_copy_conjunct(Conjunct* to, Conjunct* fr);
+
+//
+// Copy Conjunct.
+//
+Conjunct* Conjunct::copy_conj_diff_relation(Formula *parent, Rel_Body *rel_body) {
+  Conjunct *new_conj;
+  if(problem && comp_problem==NULL) {
+    new_conj = new Conjunct(parent, rel_body);
+    internal_copy_conjunct(new_conj, this);
+  }
+  else if (problem==NULL && comp_problem) {
+    /* copy compressed conjunct */
+    assert(0 && "copy compressed conjunct");
+    new_conj = 0;
+  }
+  else {
+    assert(0 && "problem == NULL");
+    new_conj = 0;
+  }
+  return new_conj;
+}
+
+
+void internal_copy_conjunct(Conjunct* to, Conjunct* fr) {
+  copy_conj_header(to, fr);
+
+  // 
+  // We repeat part of what is done by copy_conj_header(to, fr) by
+  // calling Problem::operator=(const Problem &).  
+  // copy_conj_header should go away, but there is some code that still needs 
+  // it in negate_conj.  
+  //
+  to->r_constrs = fr->r_constrs;
+  to->simplified = fr->simplified;
+  to->verified = fr->verified;
+  to->guaranteed_leading_0s = fr->guaranteed_leading_0s;
+  to->possible_leading_0s = fr->possible_leading_0s;
+  to->leading_dir = fr->leading_dir;
+  // the following duplicates some work of the "copy_conj_header" brain damage
+  *to->problem = *fr->problem; 
+  to->problem->getVarNameArgs = (void *)to;   // important
+}
+
+
+//
+// Copy Conjunct variable declarations
+// and problem parameters but not problem itself.
+//
+void copy_conj_header(Conjunct* to, Conjunct* fr) {
+  free_var_decls(to->myLocals);  to->myLocals.clear();
+
+  copy_var_decls(to->myLocals, fr->myLocals);
+  to->mappedVars = fr->mappedVars;
+  to->remap();
+  reset_remap_field(fr->myLocals);
+
+  to->cols_ordered = fr->cols_ordered;
+  to->r_constrs = fr->r_constrs;
+  to->simplified = fr->simplified;
+  to->verified = fr->verified;
+  to->guaranteed_leading_0s = fr->guaranteed_leading_0s;
+  to->possible_leading_0s = fr->possible_leading_0s;
+  to->leading_dir = fr->leading_dir;
+  to->n_open_constraints = fr->n_open_constraints;
+  to->exact=fr->exact;
+
+  Problem *fp = fr->problem;
+  Problem *tp = to->problem;
+  tp->nVars = fp->nVars;
+  tp->safeVars = fp->safeVars;
+  tp->variablesInitialized = fp->variablesInitialized;
+  tp->variablesFreed = fp->variablesFreed;
+  for(int i=1; i<=maxVars; i++) {  // only need nVars of var
+    tp->forwardingAddress[i] = fp->forwardingAddress[i];
+    tp->var[i] = fp->var[i];
+  }
+  to->problem->get_var_name = get_var_name;
+  to->problem->getVarNameArgs = (void *)to ;
+}
+
+
+void Conjunct::reverse_leading_dir_info() {
+  leading_dir *= -1;
+}
+
+
+void Conjunct::enforce_leading_info(int guaranteed, int possible, int dir) {
+  skip_finalization_check++;
+  guaranteed_leading_0s = guaranteed;
+
+  int d = min(relation()->n_inp(),relation()->n_out());
+
+  assert(0 <= guaranteed);
+  assert(guaranteed <= possible);
+  assert(possible <= d);
+
+  for(int i = 1; i <= guaranteed; i++) {
+    EQ_Handle e = add_EQ();
+    e.update_coef_during_simplify(input_var(i), -1);
+    e.update_coef_during_simplify(output_var(i), 1);
+    e.finalize();
+  }
+
+
+  if (guaranteed == possible && guaranteed >= 0  && possible+1 <= d && dir) {
+    GEQ_Handle g = add_GEQ();
+    if (dir > 0) {
+      g.update_coef_during_simplify(input_var(possible+1), -1);
+      g.update_coef_during_simplify(output_var(possible+1), 1);
+    }
+    else {
+      g.update_coef_during_simplify(input_var(possible+1), 1);
+      g.update_coef_during_simplify(output_var(possible+1), -1);
+    }
+    g.update_const_during_simplify(-1);
+    g.finalize();
+    possible_leading_0s = possible;
+    leading_dir = dir;
+  }
+	else {
+    possible_leading_0s = d;
+    leading_dir = 0;
+  }
+
+  skip_finalization_check--;
+#if ! defined NDEBUG
+  assert_leading_info();
+#endif
+}
+	
+
+void Conjunct::invalidate_leading_info(int changed) {
+  if (changed == -1) {
+    guaranteed_leading_0s = possible_leading_0s = -1;
+    leading_dir = 0;
+	}
+  else {
+    int d = min(relation()->n_inp(), relation()->n_out());
+    assert(1 <= changed && changed <= d);
+    if (possible_leading_0s == changed -1) {
+      possible_leading_0s  = d;
+		}
+    guaranteed_leading_0s = min(guaranteed_leading_0s,changed-1);
+	}
+#if ! defined NDEBUG
+  assert_leading_info();
+#endif
+}
+
+
+int Conjunct::leading_dir_valid_and_known() {
+  if (relation()->is_set()) {
+    return 0;
+	}
+  // if we know leading dir, we can rule out extra possible 0's
+  assert(leading_dir == 0 ||
+         possible_leading_0s == guaranteed_leading_0s);
+
+  return (possible_leading_0s == guaranteed_leading_0s &&
+          possible_leading_0s >= 0 &&
+          possible_leading_0s < min(relation()->n_inp(),relation()->n_out())
+          && leading_dir);
+}
+
+
+#if ! defined NDEBUG
+void Conjunct::assert_leading_info() {
+  if (relation()->is_set()) {
+    return;
+	}
+
+  int d = min(relation()->n_inp(), relation()->n_out());
+
+  if ( guaranteed_leading_0s == -1
+       && guaranteed_leading_0s == possible_leading_0s)
+    assert(leading_dir == 0);
+ 
+  if(leading_dir != 0 && 
+	   possible_leading_0s != guaranteed_leading_0s) {
+    use_ugly_names++;
+    prefix_print(DebugFile);
+    use_ugly_names--;
+	}
+	
+  assert(leading_dir == 0 || possible_leading_0s == guaranteed_leading_0s);
+
+  assert(possible_leading_0s <= d && guaranteed_leading_0s <= d);
+
+  assert(possible_leading_0s == -1 || guaranteed_leading_0s <= possible_leading_0s);
+
+  // check that there must be "guaranteed_leading_0s" 0s
+  int carried_level;
+  for (carried_level = 1; carried_level <= guaranteed_leading_0s; carried_level++) {
+    Variable_ID in = input_var(carried_level),
+	    out = output_var(carried_level);
+    coef_t lb, ub;
+    bool guar;
+    query_difference(out, in, lb, ub, guar);
+    if (lb != 0 && ub != 0) {
+	    // probably "query_difference" is just approximate
+	    // add the negation of leading_dir and assert that
+	    // the result is unsatisfiable;
+	    // add in > out (in-out-1>=0) and assert unsatisfiable.
+
+	    Conjunct *test = copy_conj_same_relation();
+	    test->problem->turnRedBlack();
+	    skip_finalization_check++;
+	    
+	    GEQ_Handle g = test->add_GEQ();
+	    g.update_coef_during_simplify(in, -1);
+	    g.update_coef_during_simplify(out, 1);
+	    g.update_const_during_simplify(-1);
+	    g.finalize();
+	    assert(!simplify_conj(test, true, 0, 0));
+	    // test was deleted by simplify_conj, as it was FALSE
+
+	    test = copy_conj_same_relation();
+	    test->problem->turnRedBlack();
+	    g = test->add_GEQ();
+	    g.update_coef_during_simplify(in, 1);
+	    g.update_coef_during_simplify(out, -1);
+	    g.update_const_during_simplify(-1);
+	    g.finalize();
+	    assert(!simplify_conj(test, true, 0, 0));
+	    // test was deleted by simplify_conj, as it was FALSE
+
+	    skip_finalization_check--;
+    }
+	}
+
+  carried_level = possible_leading_0s+1;
+
+  // check that there can't be another
+  if (guaranteed_leading_0s == possible_leading_0s
+      && possible_leading_0s >= 0 &&
+      carried_level <= min(relation()->n_inp(), relation()->n_out()))	{
+    Variable_ID in = input_var(carried_level),
+	    out = output_var(carried_level);
+    coef_t lb, ub;
+    bool guar;
+    query_difference(out, in, lb, ub, guar);
+    if (lb <= 0 && ub >= 0) {
+	    // probably "query_difference" is just approximate
+	    // add a 0 and see if its satisfiable
+
+	    Conjunct *test = copy_conj_same_relation();
+	    test->problem->turnRedBlack();
+	    skip_finalization_check++;
+
+	    EQ_Handle e = test->add_EQ();
+	    e.update_coef_during_simplify(in, -1);
+	    e.update_coef_during_simplify(out, 1);
+	    e.finalize();
+	    assert(!simplify_conj(test, true, 0, 0));
+	    // test was deleted by simplify_conj, as it was FALSE
+
+	    skip_finalization_check--;
+    }
+	}
+
+  // check leading direction info
+  if (leading_dir_valid_and_known()) {
+    Variable_ID in = input_var(guaranteed_leading_0s+1),
+	    out = output_var(guaranteed_leading_0s+1);
+    coef_t lb, ub;
+    bool guar;
+    query_difference(out, in, lb, ub, guar);
+    if ((leading_dir < 0 && ub >= 0) ||
+        (leading_dir > 0 && lb <= 0)) {
+	    // probably "query_difference" is just approximate
+	    // add the negation of leading_dir and assert that
+	    // the result is unsatisfiable;
+	    // eg for leading_dir = +1 (in must be < out),
+	    // add in >= out (in-out>=0) and assert unsatisfiable.
+
+	    Conjunct *test = copy_conj_same_relation();
+	    test->problem->turnRedBlack();
+	    skip_finalization_check++;
+	    
+	    GEQ_Handle g = test->add_GEQ();
+	    g.update_coef_during_simplify(in, leading_dir);
+	    g.update_coef_during_simplify(out, -leading_dir);
+	    g.finalize();
+
+	    assert(!simplify_conj(test, true, 0, 0));
+	    // test was deleted by simplify_conj, as it was FALSE
+
+	    skip_finalization_check--;
+    }
+	}
+}
+#endif
+
+
+Variable_ID Conjunct::declare(Const_String s) {
+  return do_declare(s, Wildcard_Var);
+}
+
+Variable_ID Conjunct::declare() {
+  return do_declare(Const_String(), Wildcard_Var);
+}
+
+Variable_ID Conjunct::declare(Variable_ID v) {
+  return do_declare(v->base_name, Wildcard_Var);
+}
+
+Conjunct* Conjunct::really_conjunct() {
+  return this;
+}
+
+
+Variable_ID_Tuple* Conjunct::variables() {
+  return &mappedVars;
+}
+
+Stride_Handle Conjunct::add_stride(int step, int preserves_level) {
+  assert_not_finalized();
+  Variable_ID wild = declare();
+  int c;
+  c = problem->newEQ();
+  simplified = false;
+  verified = false;
+  if (! preserves_level) {
+    if (leading_dir == 0)
+	    possible_leading_0s = -1;
+    // otherwise we must still have leading_dir, and thus no more 0's
+	}
+  problem->EQs[c].color = EQ_BLACK;
+  eqnnzero(&problem->EQs[c],problem->nVars);
+  n_open_constraints++;
+  EQ_Handle h = EQ_Handle(this, c);
+  h.update_coef(wild,step);
+  return h;
+}
+
+// This should only be used to copy constraints from simplified relations, 
+// i.e. there are no quantified variables in c except wildcards.
+EQ_Handle Conjunct::add_EQ(const Constraint_Handle &c, int /*preserves_level, currently unused*/) {
+  EQ_Handle e = add_EQ();
+  copy_constraint(e,c);
+  return e;
+}
+
+
+EQ_Handle Conjunct::add_EQ(int preserves_level) {
+  assert_not_finalized();
+  int c;
+  c = problem->newEQ();
+  simplified = false;
+  verified = false;
+  if (!preserves_level)	{
+    if (leading_dir == 0)
+	    possible_leading_0s = -1;
+    // otherwise we must still have leading_dir, and thus no more 0's
+	}
+  problem->EQs[c].color = EQ_BLACK;
+  eqnnzero(&problem->EQs[c],problem->nVars);
+  n_open_constraints++;
+  return EQ_Handle(this, c);
+}
+
+
+// This should only be used to copy constraints from simplified relations, 
+// i.e. there are no quantified variables in c except wildcards.
+GEQ_Handle Conjunct::add_GEQ(const Constraint_Handle &c, int /*preserves_level, currently unused */) {
+  GEQ_Handle g = add_GEQ();
+  copy_constraint(g,c);
+  return g;
+}
+
+
+GEQ_Handle Conjunct::add_GEQ(int preserves_level) {
+  assert_not_finalized();
+  int c;
+  c = problem->newGEQ();
+  simplified = false;
+  verified = false;
+  if (!preserves_level)	{
+    if (leading_dir == 0)
+	    possible_leading_0s = -1;
+    // otherwise we must still have leading_dir, and thus no more 0's
+	}
+  problem->GEQs[c].color = EQ_BLACK;
+  eqnnzero(&problem->GEQs[c],problem->nVars);
+  n_open_constraints++;
+  return GEQ_Handle(this, c);
+}
+
+
+Conjunct *Conjunct::find_available_conjunct() {
+	return this;
+}
+
+
+bool Conjunct::can_add_child() {
+  return false;
+}
+
+
+void Conjunct::combine_columns() {
+  int nvars = mappedVars.size(),i,j,k;
+
+  for(i=1; i<=nvars; i++)
+    for(j=i+1; j<=nvars; j++) {
+      // If they are the same, copy into the higher numbered column.
+      // That way we won't have problems with already-merged columns later
+      assert(i != j);
+      if(mappedVars[i] == mappedVars[j]) {
+        if (pres_debug)
+          fprintf(DebugFile, "combine_col:Actually combined %d,%d\n",
+                  j,i);
+        for(k=0; k<problem->nEQs; k++)
+          problem->EQs[k].coef[j] += problem->EQs[k].coef[i];
+        for(k=0; k<problem->nGEQs; k++)
+          problem->GEQs[k].coef[j] += problem->GEQs[k].coef[i];
+        zero_column(problem, i, 0, 0, problem->nEQs, problem->nGEQs);
+        // Create a wildcard w/no constraints.  temporary measure, 
+        // so we don't have to shuffle columns
+        Variable_ID zero_var = declare();
+        mappedVars[i] = zero_var;
+        break;
+      }
+    }
+}
+
+
+void Conjunct::finalize() {
+// Debugging version of finalize; copy the conjunct and free the old one,
+// so that purify will catch accesses to finalized constraints
+//    assert(n_open_constraints == 0);
+//    Conjunct *C = this->copy();
+//    parent().replace_child(this, C);
+//    delete this;
+}
+
+Conjunct::~Conjunct() {
+  NR_CONJUNCTS--;
+  delete problem;
+  delete comp_problem;
+}
+
+
+//
+// Cost = # of terms in DNF when negated
+//  or CantBeNegated if too bad (i.e. bad wildcards)
+//  or AvoidNegating if it would be inexact
+//
+// Also check pres_legal_negations --
+//   If set to any_negation, just return the number
+//   If set to one_geq_or_stride, return CantBeNegated if c > 1
+//   If set to one_geq_or_eq, return CantBeNegated if not a single geq or eq
+//
+
+int Conjunct::cost() {
+  int c;
+  int i;
+  int wc_no;
+  int wc_j = 0;  // initialize to shut up the compiler
+
+  // cost 1 per GEQ, and if 1 GEQ has wildcards, +2 for each of them
+
+  c = problem->nGEQs;
+  for(i=0; i<problem->nGEQs; i++) {
+    wc_no = 0;
+    for(int j=1; j<=problem->nVars; j++) if(problem->GEQs[i].coef[j]!=0) {
+        Variable_ID v = mappedVars[j];
+        if(v->kind()==Wildcard_Var) {
+          wc_no++;
+          c+=2;
+          wc_j = j;
+        }
+      }
+    if (wc_no > 1) return CantBeNegated;
+  }
+
+  for(i=0; i<problem->nEQs; i++) {
+    wc_no = 0;
+    for(int j=1; j<=problem->nVars; j++) if(problem->EQs[i].coef[j]!=0) {
+        Variable_ID v = mappedVars[j];
+        if(v->kind()==Wildcard_Var) {
+          wc_no++;
+          wc_j = j;
+        }
+      }
+
+    if (wc_no == 0)	  // no wildcards
+      c+=2;
+    else if (wc_no == 1) { // one wildcard - maybe we can negate it
+      int i2;
+      for(i2=0; i2<problem->nEQs; i2++)
+        if(i != i2 && problem->EQs[i2].coef[wc_j]!=0)  break;
+      if (i2 >= problem->nEQs)  // Stride constraint
+        c++;
+      else   // We are not ready to handle this
+        return CantBeNegated;
+    }
+    else		  // Multiple wildcards
+      return CantBeNegated;
+  }
+  if (!exact) return AvoidNegating;
+
+  if (pres_legal_negations == any_negation) {
+    return c;
+  }
+  else {
+    // single GEQ ok either way as long as no wildcards
+    // (we might be able to handle wildcards, but I haven't thought about it)
+    if (problem->nEQs==0 && problem->nGEQs<=1) {
+      if (c>1) { // the GEQ had a wildcard -- I'm not ready to go here.
+	      if (pres_debug > 0) {
+          fprintf(DebugFile,
+                  "Refusing to negate a GEQ with wildcard(s)"
+                  " under restricted_negation;  "
+                  "It may be possible to fix this.\n");
+        }
+	      return CantBeNegated;
+	    }
+      return c;
+    }
+    else if (problem->nEQs==1 && problem->nGEQs==0) {
+      assert(c == 1 || c == 2);
+
+      if (pres_legal_negations == one_geq_or_stride) {
+	      if (c == 1)
+          return c;     // stride constraint is ok
+	      else {
+          if (pres_debug > 0) {
+            fprintf(DebugFile, "Refusing to negate a non-stride EQ under current pres_legal_negations.\n");
+          }
+          return CantBeNegated;
+        }
+	    }
+      else {
+	      assert(pres_legal_negations == one_geq_or_eq);
+	      return c;
+	    }
+    }
+    else {
+      if (pres_debug > 0) {
+	      fprintf(DebugFile, "Refusing to negate multiple constraints under current pres_legal_negations.\n");
+	    }
+      return CantBeNegated;
+    }
+  }
+}
+
+
+//
+// Merge CONJ1 & CONJ2 -> CONJ.
+// Action: MERGE_REGULAR or MERGE_COMPOSE: regular merge.
+//         MERGE_GIST    make constraints from conj2 red, i.e.
+//                        Gist Conj2 given Conj1 (T.S. comment). 
+// Reorder columns as we go.
+// Merge the columns for identical variables.  
+// We assume we know nothing about the ordering of conj1, conj2.
+//
+// Does not consume its arguments
+//
+// Optional 4th argument gives the relation for the result - if
+//  null, conj1 and conj2 must have the same relation, which will
+//  be used for the result
+//
+// The only members of conj1 and conj2 that are used are: problem,
+//  mappedVars and declare(), and the leading_0s/leading_dir members
+//  and exact.
+//
+// NOTE: variables that are shared between conjuncts are necessarily 
+// declared above, not here; so we can simply create columns for the 
+// locals of each conj after doing the protected vars.  
+//
+Conjunct* merge_conjs(Conjunct* conj1, Conjunct* conj2,
+                      Merge_Action action, Rel_Body *body) {
+  // body must be set unless both conjuncts are from the same relation
+  assert(body || conj1->relation() == conj2->relation());
+
+  if (body == conj1->relation() && body == conj2->relation())
+    body = 0;  // we test this later to see if there is a new body
+
+  Conjunct *conj3 = new Conjunct(NULL, body ? body : conj2->relation());
+  Problem *p1 = conj1->problem;
+  Problem *p2 = conj2->problem;
+  Problem *p3 = conj3->problem;
+  int i;
+
+  if (action != MERGE_COMPOSE) {
+    conj1->assert_leading_info();
+    conj2->assert_leading_info();
+	}
+
+  if(pres_debug>=2) {
+    use_ugly_names++;
+    fprintf(DebugFile, ">>> Merge conjuncts: Merging%s:\n",
+            (action == MERGE_GIST ? " for gist" :
+             (action == MERGE_COMPOSE ? " for composition" : "")));
+    conj1->prefix_print(DebugFile);
+    conj2->prefix_print(DebugFile);
+    fprintf(DebugFile, "\n");
+    use_ugly_names--;
+	}
+
+
+
+  switch(action) {
+  case MERGE_REGULAR:
+  case MERGE_COMPOSE:
+    conj3->exact=conj1->exact && conj2->exact;
+    break;
+  case MERGE_GIST:
+    conj3->exact=conj2->exact;
+    break;
+	}
+
+  if (action == MERGE_COMPOSE) {
+    conj3->guaranteed_leading_0s=min(conj1->guaranteed_leading_0s,
+                                     conj2->guaranteed_leading_0s);
+    conj3->possible_leading_0s=min((unsigned int) conj1->possible_leading_0s,
+                                   (unsigned int) conj2->possible_leading_0s);
+
+    assert( conj3->guaranteed_leading_0s <= conj3->possible_leading_0s);
+
+    // investigate leading_dir - not well tested code
+    if (conj1->guaranteed_leading_0s<0 || conj2->guaranteed_leading_0s<0) {
+	    conj3->leading_dir = 0;
+    }
+    else if (conj1->guaranteed_leading_0s == conj2->guaranteed_leading_0s)
+	    if (conj1->leading_dir == conj2->leading_dir)
+        conj3->leading_dir = conj1->leading_dir;
+	    else
+        conj3->leading_dir = 0;
+    else if (conj1->guaranteed_leading_0s < conj2->guaranteed_leading_0s) {
+	    conj3->leading_dir = conj1->leading_dir;
+    }
+    else { // (conj1->guaranteed_leading_0s > conj2->guaranteed_leading_0s)
+	    conj3->leading_dir = conj2->leading_dir;
+    }
+
+    if (conj3->leading_dir == 0)
+	    conj3->possible_leading_0s = min(conj3->relation()->n_inp(),
+                                       conj3->relation()->n_out());
+
+    assert(conj3->guaranteed_leading_0s <= conj3->possible_leading_0s);
+    assert(conj3->guaranteed_leading_0s == conj3->possible_leading_0s
+           || !conj3->leading_dir);
+	}
+  else if (!body) { // if body is set, who knows what leading 0's mean?
+    assert(action == MERGE_REGULAR || action == MERGE_GIST);
+
+    int feasable = 1;
+
+    int redAndBlackGuarLeadingZeros = max(conj1->guaranteed_leading_0s,
+                                          conj2->guaranteed_leading_0s);
+    if (action == MERGE_REGULAR) 
+	    conj3->guaranteed_leading_0s= redAndBlackGuarLeadingZeros;
+    else conj3->guaranteed_leading_0s=conj1->guaranteed_leading_0s;
+
+    conj3->possible_leading_0s=min((unsigned)conj1->possible_leading_0s,
+                                   (unsigned)conj2->possible_leading_0s);
+    if (conj3->possible_leading_0s < redAndBlackGuarLeadingZeros)
+	    feasable = 0;
+    else if (conj3->guaranteed_leading_0s == -1 
+             || conj3->possible_leading_0s > redAndBlackGuarLeadingZeros)
+	    conj3->leading_dir = 0;
+    else {
+	    if (conj1->guaranteed_leading_0s == conj2->guaranteed_leading_0s)
+        if (!conj1->leading_dir_valid_and_known())
+          conj3->leading_dir = conj2->leading_dir;
+        else if (!conj2->leading_dir_valid_and_known())
+          conj3->leading_dir = conj1->leading_dir;
+        else if (conj1->leading_dir * conj2->leading_dir > 0)
+          conj3->leading_dir = conj1->leading_dir; // 1,2 same dir
+        else
+          feasable = 0;  // 1 and 2 go in opposite directions
+	    else if (conj3->possible_leading_0s != conj3->guaranteed_leading_0s)
+        conj3->leading_dir = 0;
+	    else if (conj1->guaranteed_leading_0s<conj2->guaranteed_leading_0s) {
+        assert(!conj1->leading_dir_valid_and_known());
+        conj3->leading_dir = conj2->leading_dir;
+      }
+	    else {
+        assert(!conj2->leading_dir_valid_and_known());
+        conj3->leading_dir = conj1->leading_dir;
+      }
+    }
+
+    if (!feasable) {
+	    if(pres_debug>=2)
+        fprintf(DebugFile, ">>> Merge conjuncts: quick check proves FALSE.\n");
+
+	    // return 0 = 1
+
+	    int e = p3->newEQ(); 
+	    p3->EQs[e].color   = EQ_BLACK;
+	    p3->EQs[e].touched = 1;
+	    p3->EQs[e].key     = 0;
+	    p3->EQs[e].coef[0] = 1;
+
+	    // Make sure these don't blow later assertions
+	    conj3->possible_leading_0s = conj3->guaranteed_leading_0s = -1;
+	    conj3->leading_dir = 0;
+
+	    return conj3;
+    }
+	}
+  else { // provided "body" argument but not composing, leading 0s meaningless
+    conj3->guaranteed_leading_0s = conj3->possible_leading_0s = -1;
+    conj3->leading_dir = 0;
+	}
+
+  // initialize omega stuff
+
+  for(i=0; i<p1->nGEQs+p2->nGEQs; i++) {
+    int e = p3->newGEQ();
+    assert(e == i);
+    p3->GEQs[e].color   = EQ_BLACK;
+    p3->GEQs[e].touched = 1;
+    p3->GEQs[e].key     = 0;
+	}
+  for(i=0; i<p1->nEQs+p2->nEQs; i++) {
+    int e = p3->newEQ();
+    assert(e == i);
+    p3->EQs[e].color   = EQ_BLACK;
+    p3->EQs[e].touched = 1;
+    p3->EQs[e].key     = 0;
+	}
+
+  assert(p3->nGEQs == p1->nGEQs + p2->nGEQs);
+  assert(p3->nEQs == p1->nEQs + p2->nEQs);
+
+  // flag constraints from second constraint as red, if necessary  
+  if (action == MERGE_GIST) {
+    for(i=0; i<p2->nEQs; i++) {
+	    p3->EQs[i+p1->nEQs].color = EQ_RED;
+    }
+    for(i=0; i<p2->nGEQs; i++) {
+	    p3->GEQs[i+p1->nGEQs].color = EQ_RED;
+    }
+	}
+
+  // copy constant column
+  copy_column(p3, 0, p1, 0, 0, 0);
+  copy_column(p3, 0, p2, 0, p1->nEQs, p1->nGEQs);
+  
+  // copy protected variables column from conj1
+  int new_col = 1;
+  Variable_Iterator VI(conj1->mappedVars);
+  for(i=1; VI; VI++, i++) {
+    Variable_ID v = *VI;
+    if(v->kind() != Wildcard_Var) {
+	    conj3->mappedVars.append(v);
+	    int fr_ix = i;
+	    copy_column(p3, new_col, p1, fr_ix, 0, 0);
+	    zero_column(p3, new_col, p1->nEQs, p1->nGEQs,
+                  p2->nEQs, p2->nGEQs);
+	    new_col++;
+    }
+	}
+  
+  // copy protected variables column from conj2,
+  // checking if conj3 already has this variable from conj1
+  for(i=1; i <= conj2->mappedVars.size(); i++) {
+    Variable_ID v = conj2->mappedVars[i];
+    if(v->kind() != Wildcard_Var) {
+	    int to_ix = conj3->mappedVars.index(v);
+	    int fr_ix = i;
+	    if(to_ix > 0) {
+        // use old column
+        copy_column(p3, to_ix, p2, fr_ix, p1->nEQs, p1->nGEQs);
+      }
+	    else {
+        // create new column
+        conj3->mappedVars.append(v);
+        zero_column(p3, new_col, 0, 0, p1->nEQs, p1->nGEQs);
+        copy_column(p3, new_col, p2, fr_ix, p1->nEQs, p1->nGEQs);
+        new_col++;
+      }
+    }
+	}
+
+  p3->safeVars = new_col-1;
+  
+  // copy wildcards from conj1
+  for(i=1; i <= conj1->mappedVars.size(); i++) {
+    Variable_ID v = conj1->mappedVars[i];
+    if(v->kind() == Wildcard_Var) {
+	    Variable_ID nv = conj3->declare(v);
+	    conj3->mappedVars.append(nv);
+	    int fr_ix = i;
+	    copy_column(p3, new_col, p1, fr_ix, 0, 0);
+	    zero_column(p3, new_col, p1->nEQs, p1->nGEQs,
+                  p2->nEQs, p2->nGEQs);
+	    new_col++;
+    }
+	}
+  
+  // copy wildcards from conj2
+  for(i=1; i <= conj2->mappedVars.size(); i++) {
+    Variable_ID v = conj2->mappedVars[i];
+    if(v->kind() == Wildcard_Var) {
+	    Variable_ID nv = conj3->declare(v);
+	    conj3->mappedVars.append(nv);
+	    int fr_ix = i;
+	    zero_column(p3, new_col, 0, 0, p1->nEQs, p1->nGEQs);
+	    copy_column(p3, new_col, p2, fr_ix, p1->nEQs, p1->nGEQs);
+	    new_col++;
+    }
+	}
+ 
+  p3->nVars = new_col-1;
+  checkVars(p3->nVars);
+  p3->variablesInitialized = 1;
+  for(i=1; i<=p3->nVars; i++)
+    p3->var[i] = p3->forwardingAddress[i] = i;
+    
+  conj3->cols_ordered = true;
+  conj3->simplified = false;
+  conj3->verified = false;
+    
+  if(pres_debug>=2) {
+    use_ugly_names++;
+    fprintf(DebugFile, ">>> Merge conjuncts: result is:\n");
+    conj3->prefix_print(DebugFile);
+    fprintf(DebugFile, "\n");
+    use_ugly_names--;
+	}
+
+  conj3->assert_leading_info();
+
+  return conj3;
+}
+
+
+
+
+//
+// Reorder variables by swapping.
+// cols_ordered is just a hint that thorough check needs to be done.
+// Sets _safeVars.
+// 
+void Conjunct::reorder() {
+  if(!cols_ordered) {
+    int var_no = mappedVars.size();
+    int first_wild = 1;
+    int last_prot = var_no;
+    while(first_wild < last_prot) {
+      for(; first_wild<=var_no && mappedVars[first_wild]->kind()!=Wildcard_Var;
+          first_wild++) ;
+      for(; last_prot>=1 && mappedVars[last_prot]->kind()==Wildcard_Var;
+          last_prot--) ;
+      if(first_wild < last_prot) {
+        problem->swapVars(first_wild, last_prot);
+        problem->variablesInitialized = false;
+        Var_Decl *t = mappedVars[first_wild];
+        mappedVars[first_wild] = mappedVars[last_prot];
+        mappedVars[last_prot] = t;
+        if(pres_debug) {
+          fprintf(DebugFile, "<<<OrderConjCols>>>: swapped var-s %d and %d\n", first_wild, last_prot);
+        }
+      }
+    }
+
+    int safe_vars;
+    for(safe_vars=0;
+        safe_vars<var_no && mappedVars[safe_vars+1]->kind()!=Wildcard_Var;
+        safe_vars++) ;
+
+#if ! defined NDEBUG
+    for(int s = safe_vars ; s<var_no ; s++ ) {
+      assert(mappedVars[s+1]->kind() == Wildcard_Var);
+    }
+#endif
+
+    problem->safeVars = safe_vars;
+    cols_ordered = true;
+  }
+}
+
+
+
+// Wherever possible, move function symbols to input tuple.
+// This ensures that if in == out, red F(in) = x is redundant
+// with black F(out) = x
+
+void Conjunct::move_UFS_to_input() {  
+  if (guaranteed_leading_0s > 0) {
+    std::set<Global_Var_ID> already_done;
+    int remapped = 0;
+    skip_finalization_check++;
+    Rel_Body *body = relation();
+
+    assert(body);
+	
+    for (Variable_ID_Iterator func(*body->global_decls()); func; func++) {
+	    Global_Var_ID f = (*func)->get_global_var();
+	    if (f->arity() <= guaranteed_leading_0s)
+        if (already_done.find(f) == already_done.end() &&
+            body->has_local(f, Input_Tuple) &&
+            body->has_local(f, Output_Tuple)) {
+          already_done.insert(f);
+
+          // equatE f(in) = f(out)
+          Variable_ID f_in  = body->get_local(f, Input_Tuple);
+          Variable_ID f_out = body->get_local(f, Output_Tuple);
+          if (f_in != f_out) {
+            EQ_Handle e = add_EQ(1);
+		
+            e.update_coef_during_simplify(f_in, -1);
+            e.update_coef_during_simplify(f_out, 1);
+		
+            f_out->remap = f_in;
+            remapped = 1;
+          }
+        }	    
+    }
+
+    if (remapped) {
+	    remap();
+	    combine_columns();
+	    reset_remap_field(*body->global_decls());
+	    remapped = 0;
+    }
+	
+    skip_finalization_check--;
+	}
+}
+
+
+
+
+
+//
+// Simplify CONJ.
+// Return TRUE if there are solutions, FALSE -- no solutions.
+//
+int simplify_conj(Conjunct* conj, int ver_sim, int simplificationEffort, int color) {
+  if (conj->verified 
+      && simplificationEffort <= conj->r_constrs 
+      && (conj->simplified  || simplificationEffort < 0)
+      && !color) {
+	  if(pres_debug) {
+	    fprintf(DebugFile, "$$$ Redundant simplify_conj ignored (%d,%d,%d)\n",ver_sim,simplificationEffort,color);
+	    conj->prefix_print(DebugFile);
+    }
+	  return 1;
+  }
+
+  if (simplificationEffort < 0) simplificationEffort = 0;
+  conj->move_UFS_to_input();
+  conj->reorder();
+
+  Problem *p = conj->problem;
+
+  use_ugly_names++;
+
+  int i;
+  for(i=0; i<p->nGEQs; i++) {
+    p->GEQs[i].touched = 1;
+  }
+  for(i=0; i<p->nEQs; i++) {
+    p->EQs[i].touched = 1;
+  }
+
+  if(pres_debug) {
+    fprintf(DebugFile, "$$$ simplify_conj (%d,%d,%d)[\n",ver_sim,simplificationEffort,color);
+    conj->prefix_print(DebugFile);
+  }
+
+  assert(conj->cols_ordered);
+
+  int ret_code;
+  assert(p == conj->problem);
+  if(!color) {
+    ret_code = conj->simplifyProblem(ver_sim && ! conj->verified,0,simplificationEffort);
+  }
+  else {
+    ret_code = conj->redSimplifyProblem(simplificationEffort,1);
+    ret_code = (ret_code==redFalse ? 0 : 1);
+  }
+  assert(p->nSUBs==0);
+
+  if(ret_code == 0) {
+    if(pres_debug)
+      fprintf(DebugFile, "] $$$ simplify_conj : false\n\n");
+    delete conj;
+    use_ugly_names--;
+    return(false);
+  }
+
+
+  //
+  // mappedVars is mapping from columns to Variable_IDs.
+  // Recompute mappedVars for problem returned from ip.c
+  //
+  Variable_ID_Tuple new_mapped(0);  // This is expanded by "append"
+  for (i=1; i<=p->safeVars; i++) {
+    // what is now in column i used to be in column p->var[i]
+    Variable_ID v = conj->mappedVars[p->var[i]];
+    assert(v->kind() != Wildcard_Var);
+    new_mapped.append(v);
+  }
+
+  /* Redeclare all wildcards that weren't eliminated. */
+  free_var_decls(conj->myLocals);  conj->myLocals.clear();
+
+  conj->mappedVars = new_mapped;  
+  for (i = p->safeVars+1; i<=p->nVars; i++) {
+    Variable_ID v = conj->declare();
+    conj->mappedVars.append(v);
+  }
+
+  // reset var and forwarding address if desired.
+  p->variablesInitialized = 1;
+  for(i=1; i<=conj->problem->nVars; i++)
+    conj->problem->var[i] = conj->problem->forwardingAddress[i] = i;
+      
+  if(pres_debug) {
+    fprintf(DebugFile, "] $$$ simplify_conj\n");
+    conj->prefix_print(DebugFile);
+    fprintf(DebugFile, "\n");
+  }
+
+
+  use_ugly_names--;
+  conj->simplified = true;
+  conj->setup_anonymous_wildcard_names();
+
+  return(true);
+}
+
+
+int Conjunct::rank() {
+  Conjunct *C = this->copy_conj_same_relation();
+  C->reorder();
+  C->ordered_elimination(C->relation()->global_decls()->size());
+  int C_rank = 0;
+  for(Variable_Iterator vi = C->mappedVars; vi; vi++)
+    if(C->find_column(*vi) > 0) C_rank++;
+  delete C;
+  return C_rank;
+
+}
+
+
+void Conjunct::query_difference(Variable_ID v1, Variable_ID v2, coef_t &lowerBound, coef_t &upperBound, bool &guaranteed) {
+  int c1 = get_column(v1);
+  int c2 = get_column(v2);
+  assert(c1 && c2);
+  problem->query_difference(c1, c2, lowerBound, upperBound, guaranteed);
+}
+
+
+void Conjunct::query_variable_bounds(Variable_ID v, coef_t &lowerBound, coef_t &upperBound) {
+  int c = get_column(v);
+  assert (c);
+  problem->query_variable_bounds(c, &lowerBound, &upperBound);
+}
+
+coef_t Conjunct::query_variable_mod(Variable_ID v, coef_t factor) {
+  int c = get_column(v);
+  assert(c);
+  return problem->query_variable_mod(c, factor);
+}
+
+bool Conjunct::query_variable_used(Variable_ID v) {
+  for (GEQ_Iterator g = GEQs(); g.live(); g.next()) {
+    if ((*g).get_coef(v)) return true;
+	}
+  for (EQ_Iterator e = EQs(); e.live(); e.next()) {
+    if ((*e).get_coef(v)) return true;
+	}
+  return false;
+}
+
+
+int Conjunct::simplifyProblem(int verify, int subs, int redundantElimination) {
+  if (verified) verify = 0;
+  int result = problem->simplifyProblem(verify, subs, redundantElimination);
+  if (result == false && !exact)
+    exact=true;
+  assert(!(verified && verify && result == false));
+  if (verify && result) verified = true;
+  else if (!result) verified = false;
+  return result;
+}
+
+
+// not as confident about this one as the previous:
+int Conjunct::redSimplifyProblem(int effort, int computeGist) {
+  redCheck result = problem->redSimplifyProblem(effort, computeGist);
+  if (result == redFalse && !exact)
+    exact=true;
+  return result;
+}
+
+
+//
+// Add given list of wildcards S to this Conjunct.
+// Clears argument. (That's very important, otherwise those var_id's get freed)
+// Push_exists takes responsibility for reusing or deleting Var_ID's;
+//  here we reuse them.  Must also empty out the Tuple when finished (joins).
+void Conjunct::push_exists(Variable_ID_Tuple &S) {
+  for(Tuple_Iterator<Variable_ID> VI(S); VI; VI++) {
+    (*VI)->var_kind = Wildcard_Var;
+  }
+  myLocals.join(S);       // Sets S to be empty.
+  cols_ordered = false;
+  simplified = false;
+}
+
+
+Conjunct *Formula::add_conjunct() {
+  assert_not_finalized();
+  assert(can_add_child());
+  Conjunct *f = new Conjunct(this, myRelation);
+  myChildren.append(f);
+  return f;
+}
+
+// Compress/uncompress functions
+
+bool Conjunct::is_compressed() {
+  if(problem!=NULL && comp_problem==NULL) {
+    return false;
+  }
+  else if(problem==NULL && comp_problem!=NULL) {
+    return true;
+  }
+  else {
+    assert(0 && "Conjunct::is_compressed: bad conjunct");
+    return false;
+  }
+}
+
+
+void Conjunct::compress() {
+  if(!is_compressed()) {    // compress
+    comp_problem = new Comp_Problem(problem);
+    delete problem;
+    problem = NULL;
+  }
+}
+
+
+void Conjunct::uncompress() {
+  if(is_compressed()) {
+    problem = comp_problem->UncompressProblem();
+    delete comp_problem;
+    comp_problem = NULL;
+  }
+}
+
+
+Comp_Problem::Comp_Problem(Problem *problem) :
+  _nVars(problem->nVars), 
+  _safeVars(problem->safeVars),
+  _get_var_name(problem->get_var_name), 
+  _getVarNameArgs(problem->getVarNameArgs),
+  eqs(&problem->EQs[0],problem->nEQs,problem->nVars), 
+  geqs(&problem->GEQs[0],problem->nGEQs,problem->nVars) {
+}
+
+Comp_Constraints::Comp_Constraints(eqn *constrs, int no_constrs, int no_vars) :
+  n_constrs(no_constrs), 
+  n_vars(no_vars) {
+  coefs = new coef_t[(n_vars+1)*n_constrs];
+  int e, v;
+  for(e=0; e<n_constrs; e++) {
+    for(v=0; v<=n_vars; v++) {
+      coefs[coef_index(e,v)] = constrs[e].coef[v];
+    }
+  }
+}
+
+
+Comp_Constraints::~Comp_Constraints() {
+  delete coefs;
+}
+
+
+Problem *Comp_Problem::UncompressProblem() {
+  Problem *p = new Problem(eqs.n_constraints(), geqs.n_constraints());
+  p->get_var_name     = get_var_name;
+  p->getVarNameArgs = _getVarNameArgs;
+  p->nVars          = _nVars;
+  p->safeVars       = _safeVars;
+  for(int i=1; i<=p->nVars; i++) {
+		p->forwardingAddress[i] = i;
+		p->var[i] = i;
+  }
+  eqs.UncompressConstr(&p->EQs[0], p->nEQs);
+  geqs.UncompressConstr(&p->GEQs[0], p->nGEQs);
+  return p;
+}
+
+void Comp_Constraints::UncompressConstr(eqn *constrs, short &pn_constrs) {
+  int e, v;
+  for(e=0; e<n_constrs; e++) {
+    eqnnzero(&constrs[e], 0);
+    for(v=0; v<=n_vars; v++) {
+      constrs[e].coef[v] = coefs[coef_index(e,v)];
+    }
+    constrs[e].touched = 1;
+  }
+  pn_constrs = n_constrs;
+}
+
+
+void Conjunct::convertEQstoGEQs(bool excludeStrides) { 
+  simplify_conj(this,true,1,EQ_BLACK);  // don't remember why I want to comment this statement out with reason "will cause inconsistency between Conjunct::mappedVars and Problem::nVars",  06/09/2009 by chun
+  problem->convertEQstoGEQs(excludeStrides);
+}
+
+
+void Conjunct::calculate_dimensions(Relation &R, int &ndim_all, int &ndim_domain) {
+
+  Conjunct * c = this;
+  Relation rc=Relation(R, c);
+
+  if(relation_debug) {
+    fprintf(DebugFile,"{{{\nIn Conjunct::calculate_dimensions:\n");
+    rc.prefix_print(DebugFile);
+  }
+
+  rc=Approximate(rc);
+  Relation rd=rc;
+
+  if(relation_debug) {
+    fprintf(DebugFile,"Conjunct::calculate_dimensions: Approximated as:\n");
+    rc.prefix_print(DebugFile);
+  }
+
+  // skip_set_checks++;
+
+  Conjunct * rc_conj=rc.single_conjunct();
+  ndim_all=rc.n_inp()+rc.n_out();
+  ndim_all-=rc_conj->n_EQs();
+
+  rc = Project_On_Sym(rc);
+  rc.simplify();
+
+  if(relation_debug) {
+    fprintf(DebugFile, "Conjunct::calculate_dimensions: after project_on_sym\n");
+    rc.prefix_print(DebugFile);
+  }
+
+  int n_eq_sym = 1000;
+  for (DNF_Iterator s(rc.query_DNF()); s.live(); s.next()) 
+    n_eq_sym = min(n_eq_sym, s.curr()->n_EQs());
+  ndim_all+=n_eq_sym;
+  // skip_set_checks--;
+
+  if (R.is_set()) 
+    ndim_domain = ndim_all;
+  else {
+    /* get dimensions for the domain (broadcasting) */
+
+    rd=Domain(rd);
+    rd.simplify();
+
+    if(relation_debug) {
+      fprintf(DebugFile,"Domain is:\n");
+      rd.prefix_print(DebugFile);
+    }
+
+    rc_conj=rd.single_conjunct();
+    ndim_domain=rd.n_set()-rc_conj->n_EQs()+n_eq_sym;
+  }
+
+  if(relation_debug) {
+    fprintf(DebugFile,"n_eq_sym=%d \n",n_eq_sym);
+    fprintf(DebugFile,"Dimensions: all=%d domain=%d\n}}}\n", ndim_all,ndim_domain);
+  }
+}
+
+} // namespace