named_lin_ineq.cc

c到DHL的转换工具

    assert(l.n() == names().n());
    ineqs().init(l);
    return *this;
}

void named_lin_ineq::align_named_lin_ineqs(named_lin_ineq & A,
					   named_lin_ineq & B)
{
    A.align_with(B);
}

boolean named_lin_ineq::operator==(const named_lin_ineq & c2) const
{
    if((this->const_ineqs().m() == 0)&&(c2.const_ineqs().m() == 0))
        return TRUE;
    if((this->const_ineqs().m() == 0)||(c2.const_ineqs().m() == 0))
        return FALSE;
    
    named_lin_ineq * l1;
    named_lin_ineq * l2;
    boolean delend = FALSE;

    if(is_aligned(*this, c2)) {
        l1 = (named_lin_ineq *)this;
        l2 = (named_lin_ineq *)&c2;
    } else {
        l1 = new named_lin_ineq(this);
        l2 = new named_lin_ineq(c2);
        delend = TRUE;
        l1->align_with(*l2);
    }

    boolean ret = (((*l1) >> (*l2))&&
		   ((*l2) >> (*l1)));
    if(delend) {
        delete l1;
        delete l2;
    }
    return ret;
}



named_lin_ineq named_lin_ineq::operator&(const named_lin_ineq & c) const
{
    if (m() == 0)
	if (c.m() == 0)
	    return named_lin_ineq();
	else
	    return c;
    else if (c.m() == 0)
	return *this;
    else if (is_aligned(*this, c)) {
	named_lin_ineq a1(this);
	a1 &= c.const_ineqs();
	return a1;
    } else {
	named_lin_ineq a1(this);
	named_lin_ineq a2(c);
	a1.align_with(a2);
	
	a1 &= a2.const_ineqs();
	return a1;
    }
}

// Deletes are there to save memory
named_lin_ineq * named_lin_ineq::and_(named_lin_ineq * c1,
                                     named_lin_ineq * c2,
                                     boolean del1,
                                     boolean del2)
{
    if (c1)
	if (c2) {
	    named_lin_ineq * ret = new named_lin_ineq(c1);
	    *ret &= *c2;
	    if(del1) delete c1;
	    if(del2) delete c2;
	    return ret;
	} else {
	    if (del1) return c1;
	    else
		return new named_lin_ineq(c1);
	}
    else 
	if (c2) {
	    if(del2) return c2;
	    else
		return new named_lin_ineq(c2);
	} else {
	    return 0;
	}
}

named_lin_ineq & named_lin_ineq::operator&=(const named_lin_ineq & c)
{
    named_lin_ineq cc(c);
    this->align_with(cc);
    (*this) &= cc.ineqs();
    simplify();
    return *this;
}

named_lin_ineq & named_lin_ineq::operator&=(const lin_ineq & l)
{
    assert(l.n() == names().n());

    int oldm = m();

    ineqs() &= l;

    // get rid of linearly dependent new rows;
    ineqs().del_repetition(oldm, m()-1);
    ineqs().del_loose(oldm, m()-1);

    return *this;
}

// Given lower and upper bounds for two seperate aux vars 
// see if they can be combined toghter to form a single aux var
// returns TRUE if it works, and swaps i1 and i2 in bounds2;
boolean nli_merged_aux(lin_ineq & bounds1, lin_ineq & bounds2,
		       int i1, int i2)
{
    if (bounds1.m() != bounds2.m()) return FALSE;
    
    bounds2.do_swap_col(i1, i2);

    // faster approximation to bounds1[1:n-1] == bounds2[1:n-1];
    integer_row used(bounds2.m());
    int i, j, k;
    int m = bounds1.m();
    int n = bounds1.n();
    for (i=0; i<m; i++) {
	for (j=0; j<m; j++) {
	    if (used[j]==0) {
		const constraint &b1 = bounds1.r(i);
		const constraint &b2 = bounds2.r(j);

		// ignore constant term;
		for (k=1; k<n; k++) {
		    if (b1.c(k) != b2.c(k))
			break;
		}
		if (k<n)
		    continue;
		used[j] = 1;
		break;
	    };
	};
	if (j >= m) {
	    // failed;
	    bounds2.do_swap_col(i1,i2);
	    return FALSE;
	}
    }

    return TRUE;

    /*
      int i, j;
      for (i=0; i<
      if ((bounds1 <= bounds2) &&
          (bounds2 <= bounds1)) {
	  return TRUE;
      }

      bounds2.do_swap_col(i1, i2);
      return FALSE;
      */
}

int named_lin_ineq::merge_auxes(named_lin_ineq &c)
{
    named_lin_ineq *r1 = this;
    named_lin_ineq *r2 = &c;
    
    // do we need these?
    r1->del_zero_cols();
    r2->del_zero_cols();
    
    r1->align_with(*r2);

    int naux = 0;
    constraint indx(r1->n());
    int i, j, ix, jx;

    // count the number of aux variables and record their positions
    for(i=1; i<r1->n(); i++)
	if(r1->names()[i].kind() == nte_aux) {
	    indx[naux] = i;
	    naux++;
	}
    
    if (naux > 0) {
	// For each aux variable, find the lower bounds and the upper bounds
	// BUGBUG: ignore relations between different aux vars for now;
	// this is conservative, at least;
	lin_ineq * baux1 = new lin_ineq[naux];
	lin_ineq * baux2 = new lin_ineq[naux];
	constraint kernel(r1->n());
	constraint kernel2(r1->n());
	kernel = 0;
	kernel2 = 0;
	for(i=0; i<naux; i++) {
	    ix = indx[i];
	    kernel2[ix] = 1;
	}
	for(i=0; i<naux; i++) {
	    ix = indx[i];
	    kernel[ix] = 1;
	    kernel2[ix] = 0;
	    baux1[i].init(r1->ineqs().filter_thru(kernel, 0));
	    baux1[i].init(baux1[i].filter_away(kernel2, 0));
	    baux2[i].init(r2->ineqs().filter_thru(kernel, 0));
	    baux2[i].init(baux2[i].filter_away(kernel2, 0));
	    kernel[ix] = 0;
	    kernel2[ix] = 1;
	}

	// See if two aux variables can be merged toghter.
	// one var has to be of r1 and other has to be of r2
	// ignore aux interactions for now;
	int mergedaux = 0;
	integer_row rmauxlist(r1->n());
	for (i=0; i<naux; i++) 
	    if (baux1[i].m()>0) {
		for (j=0; j<naux; j++)
		    if (baux2[j].m()>0) {
			assert(i != j);
			ix = indx[i];
			jx = indx[j];
			// try to equate ix(in 1) and jx(in 2);
			if (nli_merged_aux(baux1[i], baux2[j], ix, jx)) {
			    // merge found, record it and
			    // mark the aux to be removed.
			    rmauxlist[jx] = 1;
			    mergedaux += 1;
			    r2->ineqs().do_swap_col(ix,jx);
			    baux1[i].clear();
			    baux2[j].clear();
			    break;
			}
		    };
	    }
	delete[] baux1;
	delete[] baux2;
	
	if (mergedaux > 0) {
	    r1->del_col(rmauxlist);
	    r2->del_col(rmauxlist);
	}
	return mergedaux;
    } else
	return 0;
}

// err towards FALSE;
boolean named_lin_ineq::operator>=(const named_lin_ineq & c) const
{
    named_lin_ineq l1(*this);
    named_lin_ineq l2(c);

    int i;
    int naux1 = 0;
    int naux2 = 0;
    
    // do we need these?
    l1.del_zero_cols();
    l2.del_zero_cols();

    const name_table &nt1 = l1.const_names();
    const name_table &nt2 = l2.const_names();

    // count the number of aux variables;
    for(i=1; i<nt1.n(); i++) {
	const name_table_entry &ntei = nt1.e(i);
	if(ntei.kind() == nte_aux) {
	    naux1++;
	} else if (nt2.find(ntei) < 0)
	    // this constrains a variable not constrained by c;
	    // so there is no way this contains c;
	    return FALSE; // 
    }

    for(i=1; i<nt2.n(); i++) {
	const name_table_entry &ntei = nt2.e(i);
	if(ntei.kind() == nte_aux)
	    naux2++;
    }
  
    if (naux1 > naux2) return FALSE; // same problem with this;

    if (naux1 > 0) {
	int mergedauxes = l1.merge_auxes(l2);
	
	if (naux1 > mergedauxes) return FALSE;
	
	// BUGBUG; still doesnt handle auxes right in general;
	// consider { x = 2*aux } and { x = 4*aux };
    } else
	l1.align_with(l2);

    if(~(l1.ineqs() && l2.ineqs())) {
	return FALSE;
    }
    boolean ret = (l1.ineqs() >= l2.ineqs());
    return ret;
}

/**************************************************************************
 * a simple substitution method                                           *
 * This is a cheap alternative to expensive Fourier-Motzkin               *
 * substitution expression given in expr is of the form                   *
 * var >= sub_expr and var <= sub_expr or                                 *
 * sub_expr >= 0                                                          *
 **************************************************************************/
named_lin_ineq * named_lin_ineq::substitute(const immed & var,
                                            const named_lin_ineq & expr) const
{
    named_lin_ineq *ret = new named_lin_ineq(this);
    ret->do_substitute(var, expr);
    return ret;
}

void named_lin_ineq::do_substitute(const immed & var,
				   const named_lin_ineq & expr)
{
    int pos = find(var);
    if(pos <= 0)
        return;

    int col = expr.find(var);

    boolean tested = 1;

    tested &= (expr.m() == 2);
    tested &= ABS(expr.const_ineqs().r(0).c(col) == 1);
    for(int i=0; tested && i<expr.n(); i++)
	tested &= 
	    (expr.const_ineqs().r(0).c(i) + expr.const_ineqs().r(1).c(i) == 0);
    assert_msg(tested,("do_substitute, expr not of right form"));

    // leave in row with -var;
    int row = (expr.const_ineqs().r(0).c(col) > 0) ? 0 : 1;
    named_lin_ineq myex(expr);
    myex.del_col(col);
    myex.ineqs().do_del_row(row);

    align_with(myex);
    pos = find(var);
    for(int im=0; im<m(); im++) {
        int coeff = ineqs()[im][pos];
        if(coeff) {
            ineqs()[im].do_addmul(myex.ineqs()[0], coeff);
            ineqs()[im][pos] = 0;
        }
    }

    del_col(pos);
}

void named_lin_ineq::find_bounds()
{
    poly_iterator Poly(ineqs());
    constraint del_list(ineqs().n());
    del_list = 0;
    for(int a=1; a< ineqs().n(); a++)
        if(names()[a].kind() == nte_symconst)
            del_list[a] = -1;
    // sort by symconsts, then by rank;
    Poly.set_sort_order(del_list.data_array());

    assert(!~ineqs());
    // fm-pairwise project ineqs, sort them;
    lin_ineq *M = Poly.get_iterator(0);
    assert(!~*M);
    // try to get rid of some of the extra constraints;
    M = Poly.reduce_extra_constraints2_ptr();
    assert(!~*M);
    ineqs().init(M);
    // sort them again;
    ineqs().sort();
}


void named_lin_ineq::add_col(const name_table_entry & nte, int i)
{
    names().insert(nte, i);
    ineqs().do_insert_col(i);
    assert(ineqs().n() == names().n());
}


void named_lin_ineq::project()
{
    constraint del_list(n());
    del_list = 0;

    // sort order is approximately;
    // symbolic constants eqns last, then others vaguely by rank;
    // (really something close to (rank+sum(i+1 | col i is non-0)));
    for(int a=1; a<n(); a++)
        if(names()[a].kind() == nte_symconst)
            del_list[a] = -1;
        else
            del_list[a] = 1;

    // project
    poly_iterator Poly(ineqs());
    Poly.set_sort_order(del_list.data_array());
    Poly.get_iterator(1);
    ineqs().init(Poly.reduce_extra_constraints2_ptr());
    ineqs().sort();

    cleanup();
}

void named_lin_ineq::project_away(const immed & var, int *changedp)
{
    name_table N;
    N.insert(name_table_entry(var), 1);
    project_away(N, changedp);
}

extern lin_ineq * fast_fourier_motzkin(lin_ineq & in, integer_row *elim = 0,
				       boolean iterate=TRUE);

static void del_unit_stride_rows(lin_ineq &lq,
				 const integer_row &elim)
{
    int i, j;
    integer_row delrows(lq.m());
    for (j=0; j<lq.n(); j++) {
	if (elim.c(j))
	    for (i=0; i<lq.m(); i++) {
		int entry = lq[i][j];
		if (entry)
		    if (ABS(entry) <= 1)
			delrows[i]=1; // do del it;
	    }
    }
    lq.do_del_rows(delrows);
}

int use_alt_project = 0;
int debug_suifmath_project = 0;

void named_lin_ineq::project_away(const name_table & N, int *changed)
{
    constraint elim(n());
    int i;
    int j=1;

    for(i=1; i<N.n(); i++) {           // for each name to be deleted
	int pos = names().find(N.e(i).name());  // position of that name
	if ((pos > 0) && !elim[pos]) {
	    elim[pos] = 1;               // filter anything in that pos;
	    swap_col(pos, n()-j);         // switch it to the end;
	    elim.do_swap_col(pos, n()-j);
	    j++;
	}
    }
    if (j==1) return;  // nothing to project;
    if (changed) *changed = 1;

    // look for existing aux vars; eliminate them, too;
    for(i=1; i<n(); i++) {
	if (names()[n()-i].kind() == nte_aux) {
	    if (i>j) {
		swap_col(n()-i, n()-j);
	    }
	    elim[n()-j] = 1;
	    j++;
	};
    }
    
    // project;