combine .cvsignore files into .gitignore file

[sppoc.git] / Omega / omega / omega_lib / src / pres_print.c

/* $Id: pres_print.c,v 1.2 2006/05/04 08:59:31 boulet Exp $ */

#include <basic/bool.h>
#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 <basic/Exit.h>
#include <omega/omega_core/oc.h>



////////////////////////////////////////
//                                    //
//        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) 
    {
        String s = this->print_with_subs_to_string(printSym, newline);
        fprintf(output_file, (const char *) s);
    }

void Rel_Body::print_with_subs() 
    {
    this->print_with_subs(stdout, 0, 1);
    }

static
String tryToPrintVarToStringWithDiv(Conjunct *C, Variable_ID v) {
    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 += itoS(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 += itoS(the_const);
            s += "," + itoS(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
String Rel_Body::print_outputs_with_subs_to_string() 
{
    Rel_Body S(this),Q(this);
    S.setup_names();
    Conjunct *C = S.single_conjunct();
    Conjunct *D = Q.single_conjunct(); // ordered_elimination futzes with conj
    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++) {
        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 += "] ";
    return s;
}

String Rel_Body::print_outputs_with_subs_to_string(int i) 
{
    Rel_Body S(this),Q(this);
    S.setup_names();
    Conjunct *C = S.single_conjunct();
    Conjunct *D = Q.single_conjunct(); // ordered_elimination futzes with conj
    String s; 
    C->reorder_for_print();
    C->ordered_elimination(S.global_decls()->length());
    // Print output names with substitutions in them
    {
        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;
    }
    return s;
}

String Rel_Body::print_with_subs_to_string(bool printSym, bool newline) 
{
    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);
    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, 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";
        return s;
        }

    if (newline) s += "\n";
    return s;
}


void print_var_addrs(String &s, Variable_ID v) {
  if(pres_debug>=2) {
    char ss[20];
    sprintf(ss, "(%p,%p)", v, v->remap);
    s += ss;
  }
}

String Rel_Body::print_variables_to_string(bool printSym)
{
  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);
        }
    }

String Rel_Body::print_formula_to_string() {
    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",
                (const char *) s);
        };
    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, "{");

  String s = print_variables_to_string(printSym);
  fprintf(output_file, (const char *) s);

  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) {
  String s = print_to_string(true);
  fprintf(output_file, (const char *) s);
}

String Conjunct::print_to_string(int true_printed) {
  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) {
  String s="";
  for(Variable_ID_Iterator VI(myLocals); VI; ) {
    s += (*VI)->name();
    VI++;
    if(VI) s += ",";
  }
  fprintf(output_file, "( %s : ", (const char *) s);
  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: ");
  String s = print_variables_to_string(true);
  fprintf(output_file, "%s\n", (const char *) s);

  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) {
  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, (const char *) s);
  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=[");
      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", (const char *) s);
      }
  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");
}

String Constraint_Handle::print_to_string() const {
    assert(0);
    Exit(1);
    return "FOO";
}

String EQ_Handle::print_to_string() const {
    relation()->setup_names();
    String s =  c->print_EQ_to_string(e);
    return s;
}

String GEQ_Handle::print_to_string() const {
    relation()->setup_names();
    String s =  c->print_GEQ_to_string(e);
    return s;
}

String Constraint_Handle::print_term_to_string() const {
    assert(0);
    Exit(1);
    return "FOO";
}

String EQ_Handle::print_term_to_string() const {
    relation()->setup_names();
    String s =  c->print_EQ_term_to_string(e);
    return s;
}

String GEQ_Handle::print_term_to_string() const {
    relation()->setup_names();
    String s =  c->print_GEQ_term_to_string(e);
    return s;
}