remove include & rename

1 files changed, 908 insertions, 0 deletions

diff --git a/omegalib/omega/src/pres_print.cc b/omegalib/omega/src/pres_print.cc
new file mode 100644
index 0000000..4f2cd0d
--- /dev/null
+++ b/omegalib/omega/src/pres_print.cc
@@ -0,0 +1,908 @@
+#include <omega/pres_gen.h>
+#include <omega/pres_var.h>
+#include <omega/pres_tree.h>
+#include <omega/pres_conj.h>
+#include <omega/Relation.h>
+#include <basic/Bag.h>
+#include <omega/omega_i.h>
+#include <omega/omega_core/oc.h>
+
+namespace omega {
+
+////////////////////////////////////////
+//                                    //
+//        Print functions.            //
+//                                    //
+////////////////////////////////////////
+
+void Conjunct::reorder_for_print(bool reverseOrder, int first_pass_input, int first_pass_output, bool sort) {
+  Conjunct *C2 = copy_conj_same_relation();
+  Variable_ID_Tuple newpos(0),wcvars(0),gvars(0);
+
+// We reorder the original Variable_ID's into the newpos list; later, we 
+// copy from their original column (using find_column) to the new one.
+  int n = mappedVars.size();
+  int i;
+  // there may be more inp/outp vars than maxVars; must do dynamically
+  // skip_set_checks++;
+  Tuple<bool> input_used(myRelation->n_inp());
+  Tuple<bool> output_used(myRelation->n_out());
+  for(i=1; i<=myRelation->n_inp();i++) input_used[i] = false;
+  for(i=1; i<=myRelation->n_out();i++) output_used[i] = false;
+  for(i=1; i<=n;i++) {
+    if (mappedVars[i]->kind() == Input_Var)
+      input_used[mappedVars[i]->get_position()] = true; 
+    else if (mappedVars[i]->kind() == Output_Var)
+      output_used[mappedVars[i]->get_position()] = true; 
+    else if(mappedVars[i]->kind() == Global_Var)
+      gvars.append(mappedVars[i]);
+  }
+
+
+  if(sort)
+    for(i=1; i<=gvars.size();i++)
+      for(int j=1; j <= gvars.size(); j++)
+        if(gvars[j]->get_global_var()->base_name()
+           < gvars[j+1]->get_global_var()->base_name()) {
+          Variable_ID t = gvars[j]; gvars[j] = gvars[j+1]; gvars[j+1] = t;
+        }
+
+  newpos.join(gvars);
+
+  if(!reverseOrder) {
+    for(i=1; i<=min(myRelation->n_inp(),first_pass_input);i++)
+      if (input_used[i]) newpos.append(input_vars[i]);
+    for(i=1; i<=min(myRelation->n_out(),first_pass_output);i++)
+      if (output_used[i]) newpos.append(output_vars[i]);
+    for(i=max(1,first_pass_input+1); i<=myRelation->n_inp();i++)
+      if (input_used[i]) newpos.append(input_vars[i]);
+    for(i=max(1,first_pass_output+1); i<=myRelation->n_out();i++)
+      if (output_used[i]) newpos.append(output_vars[i]);
+  }
+  else {
+    for(i=1; i<=min(myRelation->n_out(),first_pass_output);i++)
+      if (output_used[i]) newpos.append(output_vars[i]);
+    for(i=1; i<=min(myRelation->n_inp(),first_pass_input);i++)
+      if (input_used[i]) newpos.append(input_vars[i]);
+    for(i=max(1,first_pass_output+1); i<=myRelation->n_out();i++)
+      if (output_used[i]) newpos.append(output_vars[i]);
+    for(i=max(1,first_pass_input+1); i<=myRelation->n_inp();i++)
+      if (input_used[i]) newpos.append(input_vars[i]);
+  }
+
+
+  for(i=1; i<=n;i++)
+    if (mappedVars[i]->kind() == Wildcard_Var)
+      wcvars.append(mappedVars[i]);
+
+  if(sort)
+    for(i=1; i<=gvars.size();i++)
+      for(int j=1; j <= gvars.size(); j++)
+        if(gvars[j]->name() < gvars[j+1]->name()) {
+          Variable_ID t = gvars[j]; gvars[j] = gvars[j+1]; gvars[j+1] = t;
+        }
+
+  newpos.join(wcvars);
+
+  assert(problem->nVars == newpos.size()); // i.e. no other variable types
+
+  // Copy coef columns into new order.  Constant column is unchanged.
+  for(int e=0; e<problem->nGEQs; e++) problem->GEQs[e].touched = 1;
+ 
+  for(i=1; i<=problem->nVars; i++) {
+    int col = find_column(newpos[i]); // Find column in original conj.
+    assert(col != 0);
+    copy_column(problem, i,      // Copy it from orig. column in the copy.
+                C2->problem, col, 0, 0);
+    problem->var[i] = i;
+  }
+  for(i=1; i<=problem->nVars; i++)   
+    problem->forwardingAddress[i] = i;
+
+  mappedVars = newpos;
+  delete C2;
+  // skip_set_checks--;
+}
+
+void Rel_Body::print_with_subs(FILE *output_file, bool printSym, bool newline) {
+  std::string s = this->print_with_subs_to_string(printSym, newline);
+  fprintf(output_file, "%s", s.c_str());
+}
+
+void Rel_Body::print_with_subs() {
+  this->print_with_subs(stdout, 0, 1);
+}
+
+static std::string tryToPrintVarToStringWithDiv(Conjunct *C, Variable_ID v) {
+  std::string s;
+  bool seen = false;
+// This assumes that there is one EQ involving v, that v cannot be 
+// substituted and hence has a non-unit coefficient.
+  for(EQ_Iterator e(C); e; e++) {
+    if ((*e).get_coef(v) != 0) {
+      assert(!seen);  // This asserts just one EQ with v 
+      coef_t v_coef = (*e).get_coef(v);
+      int v_sign = v_coef > 0 ? 1 : -1;
+      v_coef *= v_sign;
+      int sign_adj = -v_sign;
+
+      s += "intDiv(";
+      bool first=true;
+      for(Constr_Vars_Iter i(*e,false); i; i++) {
+        if ((*i).var != v && (*i).coef != 0) {
+          coef_t this_coef = sign_adj*(*i).coef;
+          if(!first && this_coef > 0)
+            s+= "+";
+          if (this_coef == 1)
+            s += (*i).var->name();
+          else if (this_coef == -1) {
+            s +=  "-"; s += (*i).var->name();
+          }
+          else {
+            s += to_string(this_coef) + "*" + (*i).var->name();
+          }
+          first = false;
+        }
+      }
+      coef_t the_const = (*e).get_const()* sign_adj;
+      if (the_const > 0 && !first)
+        s+= "+";
+      if (the_const != 0)
+        s += to_string(the_const);
+      s += "," + to_string(v_coef) + ")";
+      seen = true;
+    }
+  }
+  return s;
+}
+
+
+// This function prints the output tuple of a relation with each one as a 
+// function of the input variables.  
+// This will fail or look goofy  if the outputs are not affine functions of
+// the inputs.
+// BIG WARNING: Call this only from the codegen stuff, since it assumes things
+// about coefficients
+std::string Rel_Body::print_outputs_with_subs_to_string() {
+  // Rel_Body S(this),Q(this);
+  Rel_Body *S = this->clone();
+  Rel_Body *Q = this->clone();
+  S->setup_names();
+  Conjunct *C = S->single_conjunct();
+  Conjunct *D = Q->single_conjunct(); // ordered_elimination futzes with conj
+  std::string s; //  = "[";
+  C->reorder_for_print();
+  C->ordered_elimination(S->global_decls()->length());
+  // Print output names with substitutions in them
+  for(int i=1; i<=S->n_out(); i++) {
+    std::string t;
+    int col = C->find_column(output_vars[i]);
+    if (col != 0)
+      t = C->print_sub_to_string(col);
+    if (col == 0 || t == output_vars[i]->name()) // no sub found
+      // Assume you can't get a unit coefficient on v, must use div
+      t = tryToPrintVarToStringWithDiv(D, output_vars[i]);
+    s += t;
+    if (i < S->n_out())  s += ",";
+  }
+  // s += "] ";
+  delete S;
+  delete Q;
+  return s;
+}
+
+std::string Rel_Body::print_outputs_with_subs_to_string(int i) {
+  // Rel_Body S(this),Q(this);
+  Rel_Body *S = this->clone();
+  Rel_Body *Q = this->clone();
+  S->setup_names();
+  Conjunct *C = S->single_conjunct();
+  Conjunct *D = Q->single_conjunct(); // ordered_elimination futzes with conj
+  std::string s; 
+  C->reorder_for_print();
+  C->ordered_elimination(S->global_decls()->length());
+  // Print output names with substitutions in them
+  {
+    std::string t;
+    int col = C->find_column(output_vars[i]);
+    if (col != 0)
+      t = C->print_sub_to_string(col);
+    if (col == 0 || t == output_vars[i]->name()) // no sub found?
+      t = tryToPrintVarToStringWithDiv(D, output_vars[i]);
+    // should check for failure
+    s += t;
+  }
+  delete S;
+  delete Q;
+  return s;
+}
+
+std::string Rel_Body::print_with_subs_to_string(bool printSym, bool newline) {
+  std::string s="";
+
+  if (pres_debug) {
+    fprintf(DebugFile,"print_with_subs_to_string:\n");
+    prefix_print(DebugFile);
+  }
+
+  int anythingPrinted = 0;
+
+  if (this->is_null()) {
+    s = "NULL Rel_Body\n";
+    return s;
+  }
+
+  // Rel_Body R(this);
+  Rel_Body *R = this->clone();
+  bool firstRelation = true;
+
+  for(DNF_Iterator DI(R->query_DNF()); DI.live(); DI.next()) {
+    Rel_Body S(R, DI.curr());
+    Conjunct *C = S.single_conjunct();
+    if(!simplify_conj(C, true, 4, EQ_BLACK))  continue;
+
+    S.setup_names();
+
+    if(! firstRelation) {
+      s += " union";
+      if (newline) s += "\n ";
+    }
+    else
+      firstRelation = false;
+
+    anythingPrinted = 1;
+
+    C->reorder_for_print(false,C->max_ufs_arity_of_in(),
+                         C->max_ufs_arity_of_out());
+    C->ordered_elimination(S.Symbolic.length()
+                           +C->max_ufs_arity_of_in()
+                           +C->max_ufs_arity_of_out());
+// assert(C->problem->variablesInitialized);
+
+    if (pres_debug) S.prefix_print(DebugFile);
+
+    /* Do actual printing of Conjunct C as a relation */
+    s += "{";
+ 
+    if (!Symbolic.empty()) {
+      if (printSym) s += "Sym=[";
+      for (Variable_ID_Iterator Sym_I = S.Symbolic; Sym_I;) 
+      {
+        if (printSym)
+          s += (*Sym_I)->name();
+        Sym_I++;
+        if (printSym && Sym_I) s+=  ",";
+      }
+      if (printSym) s += "] ";
+    }
+
+    int i, col;
+ 
+    if (S.number_input != 0) {
+      s +=  "[";
+      // Print input names with substitutions in them
+      for(i=1; i<=S.number_input; i++) {
+        col = C->find_column(input_vars[i]);
+        if (col != 0)
+          s += C->problem->print_sub_to_string(col);
+        else
+          s += input_vars[i]->name();
+        if (i<S.number_input) s += ",";
+      }
+      s +=  "]";
+    }
+ 
+    if (! S.is_set())
+      s +=  " -> ";
+
+    if (S.number_output != 0) {
+      s += "[";
+ 
+      // Print output names with substitutions in them
+      for(i=1; i<=S.number_output; i++) {
+        col = C->find_column(output_vars[i]);
+        if (col != 0)
+          s += C->problem->print_sub_to_string(col);
+        else
+          s +=  output_vars[i]->name();
+        if (i < S.number_output)  s += ",";
+      }
+      s += "] ";
+    }
+ 
+    if (C->is_unknown()) {
+      if (S.number_input != 0 || S.number_output != 0)
+        s += ":";
+      s += " UNKNOWN";
+    }
+    else {
+      // Empty conj means TRUE, so don't print colon
+      if (C->problem->nEQs != 0 || C->problem->nGEQs != 0)  {
+        C->problem->clearSubs();
+        if (S.number_input != 0 || S.number_output != 0)
+          s += ":";
+        s += " ";
+        s += C->print_to_string(false);
+      }
+      else {
+        if (S.number_input == 0 && S.number_output == 0)
+          s += " TRUE ";
+      }
+    }
+
+    s +=  "}";
+  }
+
+  if (!anythingPrinted) {
+    R->setup_names();
+    s = "{";
+    s += R->print_variables_to_string(printSym);
+    if (R->number_input != 0 || R->number_output != 0)
+      s += " :";
+    s += " FALSE }";
+    if (newline) s += "\n";
+
+    delete R;
+    return s;
+  }
+
+  if (newline) s += "\n";
+  
+  delete R;
+  return s;
+}
+
+
+void print_var_addrs(std::string &s, Variable_ID v) {
+  if(pres_debug>=2) {
+    char ss[20];
+    sprintf(ss, "(%p,%p)", v, v->remap);
+    s += ss;
+  }
+}
+
+std::string Rel_Body::print_variables_to_string(bool printSym) {
+  std::string s="";
+
+  if (! Symbolic.empty()) {
+    if (printSym) s += " Sym=[";
+    for (Variable_ID_Iterator Sym_I(Symbolic); Sym_I; ) {
+      if (printSym) s +=  (*Sym_I)->name();
+      print_var_addrs(s, *Sym_I);
+      Sym_I++;
+      if (printSym && Sym_I)  s += ",";
+    }
+    if (printSym) s += "] ";
+  }
+  int i;
+
+  if (number_input) {
+    s += "[";
+    for (i=1;i<=number_input;i++) {
+      s += input_vars[i]->name();
+      print_var_addrs(s, input_vars[i]);
+      if(i < number_input) s += ",";
+    }
+    s += "] ";
+  }
+
+  if (number_output) {
+    s += "-> [";
+    for (i=1;i<=number_output;i++) {
+      s += output_vars[i]->name();
+      print_var_addrs(s, output_vars[i]);
+      if(i < number_output) s += ",";
+    }
+    s += "] ";
+  }
+
+  return s;  
+}
+
+
+int F_Declaration::priority() {
+  return 3;
+}
+
+int Formula::priority () {
+  return 0;
+}
+
+int F_Or::priority() {
+  return 0;
+}
+
+int F_And::priority() {
+  return 1;
+}
+
+int Conjunct::priority() {
+  return 1;
+}
+
+int F_Not::priority() {
+  return 2;
+}
+
+
+//
+// print() functions
+//
+void Formula::print(FILE *output_file) {
+  if(myChildren.empty()) {
+    if(node_type()==Op_Relation || node_type()==Op_Or)
+      fprintf(output_file, "FALSE");
+    else if(node_type()==Op_And)
+      fprintf(output_file, "TRUE");
+    else {
+      assert(0);
+    }
+  }
+    
+  for(List_Iterator<Formula*> c(myChildren); c;) {
+    if (node_type() == Op_Exists || node_type() == Op_Forall 
+        || (*c)->priority() < priority()) 
+      fprintf(output_file, "( ");
+    (*c)->print(output_file);
+    if (node_type() == Op_Exists || node_type() == Op_Forall 
+        || (*c)->priority() < priority()) 
+      fprintf(output_file, " )");
+    c++;
+    if(c.live())
+      print_separator(output_file);
+  }
+}
+
+std::string Rel_Body::print_formula_to_string() {
+  std::string s;
+  setup_names();
+  for(DNF_Iterator DI(query_DNF()); DI.live();)  {
+
+    s += (*DI)->print_to_string(1);
+    DI.next();
+    if (DI.live()) s += " && ";
+    if (pres_debug) fprintf(DebugFile,"Partial print to string: %s\n",
+                            s.c_str());
+  }
+  return s;
+}
+
+void Rel_Body::print(FILE *output_file, bool printSym) {
+  if (this->is_null()) {
+    fprintf(output_file, "NULL Rel_Body\n");
+    return;
+  }
+
+  setup_names();
+
+  fprintf(output_file, "{");
+
+  std::string s = print_variables_to_string(printSym);
+  fprintf(output_file, "%s", s.c_str());
+
+  fprintf(output_file, ": ");
+  
+  if(simplified_DNF==NULL) {
+    Formula::print(output_file);
+  }
+  else {
+    assert(children().empty());
+    simplified_DNF->print(output_file);
+  }
+
+  fprintf(output_file, " }\n");
+}
+
+void Rel_Body::print() {
+  this->print(stdout);
+}
+
+void F_Not::print(FILE *output_file) {
+  fprintf(output_file, " not ");
+  Formula::print(output_file);
+}
+
+void F_And::print_separator(FILE *output_file) {
+  fprintf(output_file, " and ");
+}
+
+void Conjunct::print(FILE *output_file) {
+  std::string s = print_to_string(true);
+  fprintf(output_file, "%s", s.c_str());
+}
+
+std::string Conjunct::print_to_string(int true_printed) {
+  std::string s=""; 
+
+  int num = myLocals.size();
+  if(num) {
+    s += "exists ( ";
+    int i;
+    for (i = 1; i <= num; i++) {
+      Variable_ID v = myLocals[i];
+      s += v->char_name();
+      if(i < num) s += ",";
+    }
+    if (true_printed || !(is_true())) s += " : ";
+  }
+
+  if(is_true()) {
+    s += true_printed ? "TRUE" : "";
+  }
+  else { 
+    if (is_unknown()) 
+      s += "UNKNOWN";
+    else {
+      s += problem->prettyPrintProblemToString();
+      if (!exact)
+        s += " && UNKNOWN";
+    } 
+  }
+
+
+  if (num) s += ")";
+  return s;
+}
+
+void F_Or::print_separator(FILE *output_file) {
+  fprintf(output_file, " or ");
+}
+
+void F_Declaration::print(FILE *output_file) {
+  std::string s="";
+  for(Variable_ID_Iterator VI(myLocals); VI; ) {
+    s += (*VI)->name();
+    VI++;
+    if(VI) s += ",";
+  }
+  fprintf(output_file, "( %s : ", s.c_str());
+  Formula::print(output_file);
+  fprintf(output_file, ")");
+}
+
+void F_Forall::print(FILE *output_file) {
+  fprintf(output_file, "forall ");
+  F_Declaration::print(output_file);
+}
+
+void F_Exists::print(FILE *output_file) {
+  fprintf(output_file, "exists ");
+  F_Declaration::print(output_file);
+}
+
+void Formula::print_separator(FILE *) {
+  assert(0);    // should never be called, it's only for derived classes
+}
+
+// 
+// Setup names in formula.  
+//
+
+typedef  Set<Global_Var_ID> g_set;
+void Rel_Body::setup_names() {
+  int i;
+
+
+  if (use_ugly_names) return;
+
+  if (pres_debug>=2)
+    fprintf(DebugFile,"Setting up names for 0x%p\n", this);
+
+  for(i=1; i<=number_input; i++) {
+    input_vars[i]->base_name = In_Names[i];
+  }
+  for(i=1; i<=number_output; i++) {
+    output_vars[i]->base_name = Out_Names[i];
+  }
+
+  g_set gbls;
+
+  wildCardInstanceNumber = 0;
+
+  for(i=1; i<= Symbolic.size(); i++) {
+    gbls.insert(Symbolic[i]->get_global_var());
+  }
+
+  foreach(g,Global_Var_ID,gbls,
+          g->instance = g->base_name()++);
+
+  for(i=1; i<=number_input; i++) {
+    if (!input_vars[i]->base_name.null())
+      input_vars[i]->instance = input_vars[i]->base_name++;
+  }
+  for(i=1; i<=number_output; i++) {
+    if (!output_vars[i]->base_name.null())
+      output_vars[i]->instance = output_vars[i]->base_name++;
+  }
+
+  if (simplified_DNF != NULL)  // It is simplified
+    simplified_DNF->setup_names();
+  else                         // not simplified
+    Formula::setup_names();
+
+  for(i=1; i<=number_output; i++) {
+    if (!output_vars[i]->base_name.null())
+      output_vars[i]->base_name--;
+  }
+  for(i=1; i<=number_input; i++) {
+    if (!input_vars[i]->base_name.null())
+      input_vars[i]->base_name--;
+  }
+  foreach(g,Global_Var_ID,gbls, g->base_name()--);
+}
+
+void Formula::setup_names() {
+  if (pres_debug>=2)
+    fprintf(DebugFile,"Setting up names for formula 0x%p\n", this);
+
+  for(List_Iterator<Formula*> c(myChildren); c; c++)
+    (*c)->setup_names();
+}
+
+void DNF::setup_names() {
+  if (pres_debug>=2)
+    fprintf(DebugFile,"Setting up names for DNF 0x%p\n", this);
+
+  for(DNF_Iterator DI(this); DI.live(); DI.next()) 
+    DI.curr()->setup_names();
+}
+
+
+void F_Declaration::setup_names() {
+  if (pres_debug>=2)
+    fprintf(DebugFile,"Setting up names for Declaration 0x%p\n", this);
+
+  // Allow re-use of wc names in other scopes
+  int savedWildCardInstanceNumber = wildCardInstanceNumber;
+
+  for(Tuple_Iterator<Variable_ID> VI(myLocals); VI; VI++) {
+    Variable_ID v = *VI;
+    if (!v->base_name.null()) v->instance = v->base_name++;
+    else  v->instance = wildCardInstanceNumber++;
+  }
+
+  for(List_Iterator<Formula*> c(children()); c; c++)
+    (*c)->setup_names();
+
+  for(Tuple_Iterator<Variable_ID> VI2(myLocals); VI2; VI2++) {
+    Variable_ID v = *VI2;
+    if (!v->base_name.null()) v->base_name--;
+  }
+  wildCardInstanceNumber = savedWildCardInstanceNumber;
+}
+
+
+//
+// Prefix_print functions.
+// Print Formula Tree, used in debugging.
+//
+static int level = 0;
+
+void Formula::prefix_print(FILE *output_file, int debug) {
+  for(List_Iterator<Formula*> c(children()); c; c++)
+    (*c)->prefix_print(output_file, debug);
+  level--;
+}
+
+
+void Rel_Body::prefix_print() {
+  this->prefix_print(stdout, 1);
+}
+
+void Rel_Body::prefix_print(FILE *output_file, int debug) {
+  int old_use_ugly_names = use_ugly_names;
+  use_ugly_names = 0;
+
+  setup_names();
+
+  level = 0;
+  if(pres_debug>=2) fprintf(output_file, "(@%p)", this);
+  fprintf(output_file, is_set() ? "SET: " : "RELATION: ");
+  std::string s = print_variables_to_string(true);
+  fprintf(output_file, "%s\n", s.c_str());
+
+  if(simplified_DNF==NULL) {
+    Formula::prefix_print(output_file, debug);
+  } else {
+    assert(children().empty());
+    simplified_DNF->prefix_print(output_file, debug, true);
+  }
+  fprintf(output_file, "\n");
+  use_ugly_names = old_use_ugly_names;
+}
+
+
+void F_Forall::prefix_print(FILE *output_file, int debug) {
+  Formula::print_head(output_file);
+  fprintf(output_file, "forall [");
+  F_Declaration::prefix_print(output_file, debug);
+  for (Variable_ID_Iterator VI(myLocals); VI; VI++)
+    assert((*VI)->kind() == Forall_Var);
+
+}
+
+void F_Exists::prefix_print(FILE *output_file, int debug) {
+  Formula::print_head(output_file);
+  if(pres_debug>=2) fprintf(output_file, "(@%p)", this);
+  fprintf(output_file, "exists [");
+  F_Declaration::prefix_print(output_file, debug);
+  for (Variable_ID_Iterator VI(myLocals); VI; VI++)
+    assert((*VI)->kind() == Exists_Var);
+}
+
+void F_Declaration::prefix_print(FILE *output_file, int debug) {
+  std::string s = "";
+  for (Variable_ID_Iterator VI(myLocals); VI; ) {
+    s += (*VI)->name();
+    print_var_addrs(s, *VI);
+    VI++;
+    if(VI) s += ",";
+  }
+  s += "]\n";
+  fprintf(output_file, "%s", s.c_str());
+  Formula::prefix_print(output_file, debug);
+}
+
+void F_Or::prefix_print(FILE *output_file, int debug) {
+  Formula::print_head(output_file);
+  fprintf(output_file, "or\n");
+  Formula::prefix_print(output_file, debug);
+}
+
+void F_And::prefix_print(FILE *output_file, int debug) {
+  Formula::print_head(output_file);
+  fprintf(output_file, "and\n");
+  Formula::prefix_print(output_file, debug);
+}
+
+void F_Not::prefix_print(FILE *output_file, int debug) {
+  Formula::print_head(output_file);
+  fprintf(output_file, "not\n");
+  Formula::prefix_print(output_file, debug);
+}
+
+void Conjunct::prefix_print(FILE *output_file, int debug) {
+  static char dir_glyphs[] = { '-', '?', '+' };
+
+  if (debug) {
+    Formula::print_head(output_file);
+    if(pres_debug>=2) fprintf(output_file, "(@%p)", this);
+    fprintf(output_file, "%s CONJUNCT, ", exact ? "EXACT" : "INEXACT");
+    if (simplified) fprintf(output_file, "simplified, ");
+    if (verified) fprintf(output_file, "verified, ");
+    if (possible_leading_0s != -1 && guaranteed_leading_0s != -1)
+      assert (guaranteed_leading_0s <= possible_leading_0s);
+    if (guaranteed_leading_0s != -1 && guaranteed_leading_0s == possible_leading_0s)
+      fprintf(output_file,"# leading 0's = %d,",  possible_leading_0s);
+    else if (possible_leading_0s != -1 || guaranteed_leading_0s != -1) {
+      if (guaranteed_leading_0s != -1)
+        fprintf(output_file,"%d <= ",guaranteed_leading_0s);
+      fprintf(output_file,"#O's");
+      if (possible_leading_0s != -1)
+        fprintf(output_file," <= %d",possible_leading_0s);
+      fprintf(output_file,", ");
+    }
+    if (dir_glyphs[leading_dir+1] != '?')
+      fprintf(output_file," first = %c, ", dir_glyphs[leading_dir+1]);
+    fprintf(output_file,"myLocals=[");
+    std::string s="";
+    for (Variable_ID_Iterator VI(myLocals); VI; ) {
+      assert( (*VI)->kind() == Wildcard_Var);
+      s += (*VI)->name();
+      print_var_addrs(s, *VI);
+      VI++;
+      if(VI) s +=  ",";
+    }
+    s += "] mappedVars=[";
+    for(Variable_ID_Iterator MVI(mappedVars); MVI; ) {
+      s += (*MVI)->name();
+      print_var_addrs(s, *MVI);
+      MVI++;
+      if(MVI) s += ",";
+    }
+    fprintf(output_file, "%s]\n", s.c_str());
+  }
+  else
+    level++;
+
+  setOutputFile(output_file);
+  setPrintLevel(level+1);
+  problem->printProblem(debug);
+  setPrintLevel(0);
+  Formula::prefix_print(output_file, debug);
+}
+
+void Formula::print_head(FILE *output_file) {
+  level++;
+  int i;
+  for(i=0; i<level; i++) {
+    fprintf(output_file, ". ");
+  }
+}
+
+//
+// Print DNF.
+//
+void DNF::print(FILE *out_file) {
+  DNF_Iterator p(this);
+  if (!p.live())
+    fprintf(out_file, "FALSE");
+  else
+    for(; p.live(); ) {
+      p.curr()->print(out_file);
+      p.next();
+      if(p.live())
+        fprintf(out_file, " or ");
+    }
+}
+
+void DNF::prefix_print(FILE *out_file, int debug, bool parent_names_setup) {
+  wildCardInstanceNumber = 0;
+  Variable_ID_Tuple all_vars;
+  if(!use_ugly_names && !parent_names_setup) {
+    // We need to manually set up all of the input,output, and symbolic 
+    // variables, since during simplification, a dnf's conjuncts may not 
+    // be listed as part of a relation, or perhaps as part of different
+    // relations (?) (grr).
+    for(DNF_Iterator p0(this); p0.live(); p0.next()) {
+      for(Variable_Iterator vi((*p0)->mappedVars); vi; vi++)
+        if((*vi)->kind() != Wildcard_Var && all_vars.index(*vi) == 0)
+          all_vars.append(*vi);
+      (*p0)->setup_names();
+    }
+    foreach(v,Variable_ID,all_vars,
+            if (!v->base_name.null()) v->instance = v->base_name++;
+            else  v->instance = wildCardInstanceNumber++;
+      );
+  }
+
+  int i = 1;
+  level = 0;
+  for(DNF_Iterator p(this); p.live(); p.next(), i++) {
+    fprintf(out_file, "#%d ", i);
+    if(*p == NULL)
+      fprintf(out_file, "(NULL)\n");
+    else 
+      (*p)->prefix_print(out_file, debug);
+  }
+    
+  foreach(v,Variable_ID,all_vars,if (!v->base_name.null()) v->base_name--);
+
+  fprintf(out_file, "\n");
+}
+
+std::string Constraint_Handle::print_to_string() const {
+  assert(0);
+  return "FOO";
+}
+
+std::string EQ_Handle::print_to_string() const {
+  relation()->setup_names();
+  std::string s =  c->print_EQ_to_string(e);
+  return s;
+}
+
+std::string GEQ_Handle::print_to_string() const {
+  relation()->setup_names();
+  std::string s =  c->print_GEQ_to_string(e);
+  return s;
+}
+
+std::string Constraint_Handle::print_term_to_string() const {
+  assert(0);
+  return "FOO";
+}
+
+std::string EQ_Handle::print_term_to_string() const {
+  relation()->setup_names();
+  std::string s =  c->print_EQ_term_to_string(e);
+  return s;
+}
+
+std::string GEQ_Handle::print_term_to_string() const {
+  relation()->setup_names();
+  std::string s =  c->print_GEQ_term_to_string(e);
+  return s;
+}
+
+}