diff options
Diffstat (limited to 'omegalib/omega/src/pres_print.cc')
| -rw-r--r-- | omegalib/omega/src/pres_print.cc | 908 |
1 files changed, 0 insertions, 908 deletions
diff --git a/omegalib/omega/src/pres_print.cc b/omegalib/omega/src/pres_print.cc deleted file mode 100644 index 4f2cd0d..0000000 --- a/omegalib/omega/src/pres_print.cc +++ /dev/null @@ -1,908 +0,0 @@ -#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; -} - -} |