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