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