named_lin_ineq.cc

c到DHL的转换工具

/***************************************************************************
 *                                                                         *
 ***************************************************************************/
boolean name_table::is_aligned(const name_table & na,
                               const name_table & nb)
{
    if(na.n() != nb.n()) return FALSE;

    for(int i=1; i<na.n(); i++) {
        if(na.e(i).name() != nb.e(i).name())
          if (na.e(i).kind() != nte_summary)
            return FALSE;
        if(na.e(i).name() == immed(0))
            return FALSE;
        else if(na.e(i).kind() != nb.e(i).kind())
            return FALSE;
    }
    // make sure table is ordered;
    name_table_entry_kind oldkind=nte_none;
    for (int j=1; j<na.n(); j++) {
	name_table_entry_kind newkind=na.e(j).kind();
	switch(newkind) {
	  case nte_symconst:
	    if (oldkind == nte_cond) return FALSE;
	  case nte_cond:
	    if (oldkind == nte_loop) return FALSE;
	  case nte_loop:
	    if (oldkind == nte_dim) return FALSE;
	  case nte_dim:
	    if (oldkind == nte_summary) return FALSE;
	  case nte_summary:
	    if (oldkind == nte_aux) return FALSE;
	  case nte_aux:
	  case nte_none:
	    break;
	}
	oldkind = newkind;
    }

    return TRUE;
}


/***************************************************************************
 *                                                                         *
 ***************************************************************************/
name_table name_table::operator&(const name_table & b) const
{
    name_table ret(this);
    ret &= b;
    return ret;
}

/***************************************************************************
 *                                                                         *
 ***************************************************************************/
name_table &name_table::operator&=(const name_table & b)
{
    if(is_aligned(*this, b)) {
        return *this;
    }
    integer_row ca(n());
    integer_row cb(b.n());
    this->align_with(b,ca,cb);
    return *this;
}

/***************************************************************************
 *                                                                         *
 ***************************************************************************/
name_table * name_table::align_tables(const name_table &na,
                                      const name_table &nb,
                                      integer_row & ca,
                                      integer_row & cb)
{
    name_table *newnt = new name_table(na);

    newnt->align_with(nb, ca, cb);

    return newnt;
}

/***************************************************************************
 *                                                                         *
 ***************************************************************************/
void name_table::align_with(const name_table &nb,
			    integer_row & ca,
			    integer_row & cb)
{
    int ii;
    name_table nbcopy(nb);
    assert(n() == ca.n());
    assert(nb.n() == cb.n());
    change_name_types(*this, nbcopy);

    for(ii=1; ii<n(); ii++)
        assert(e(ii).kind() != nte_none);
    for(ii=1; ii<nbcopy.n(); ii++)
        assert(nbcopy.e(ii).kind() != nte_none);

    ca[0] = cb[0] = 0;                  // consant position does not change

    for (ii=1; ii <ca.n(); ii++)
	ca[ii] = ii;
    int curr = ca.n();

    for (ii=1; ii < nbcopy.n(); ii++) {
	if ((cb[ii] = find(nbcopy.e(ii))) == -1)
	    curr++;
    }
    resize(curr);

    curr = ca.n();
    for (ii=1; ii < nbcopy.n(); ii++) {
	if ((cb[ii]) == -1) {
	    (*this)[curr] = nbcopy.e(ii);
	    cb[ii] = curr++;
	}
    };
    integer_row extrac(n());
    if (do_reorder_table(extrac)) {
	integer_row newca(ca.n()), newcb(cb.n());
	for (ii=1; ii < ca.n(); ii++) {
	    // was:     this[ca[ii]] = old[ii];
	    // becomes: this[extrac[ii]] = 
	    // ii moves to elt extrac[ca[ii]]
	    newca[ii] = extrac[ca[ii]];
	}
	ca.init(newca);
	for (ii=1; ii < cb.n(); ii++) {
	    newcb[ii] = extrac[cb[ii]];
	}
	cb.init(newcb);
    }
}

static void find_elements(name_table_entry_kind k,
			  const name_table &na, integer_row &ca,
			  int &curr)
{
    int currloc = curr;
    for (int ai=1; ai<na.n(); ai++) {
	if (na.e(ai).kind()==k) {
	    ca[ai] = currloc++;
	};
    }
    curr = currloc;
}


boolean name_table::do_reorder_table(integer_row &ca)
{
    int curr=1;
    assert(ca.n() == n());
    find_elements(nte_symconst, *this, ca, curr);
    find_elements(nte_cond, *this, ca, curr);
    find_elements(nte_loop, *this, ca, curr);
    find_elements(nte_dim, *this, ca, curr);
    find_elements(nte_summary, *this, ca, curr);
    find_elements(nte_aux, *this, ca, curr);
    assert(curr == ca.n());

    name_table thiscopy(*this);
    int i;
    for (i=1; i<n(); i++)
	(*this)[ca[i]] = thiscopy[i];
    for (i=1; i<n(); i++)
	if (ca[i] != i)
	    return TRUE;
    return FALSE;
}

/***************************************************************************
 *                                                                         *
 ***************************************************************************/
name_table * name_table::mk_align(const name_table & na,
                                  const name_table & nb)
{
    name_table * newnt;
    if(is_aligned(na, nb))
        newnt = new name_table(na);
    else {
        // indexes to the new list
        integer_row ca(na.n());
        integer_row cb(nb.n());

        newnt = name_table::align_tables(na, nb, ca, cb);
    }

    return newnt;
}

base_symtab * name_table::get_symtab(base_symtab * in) const
{
    base_symtab * curr = in;
    for(int i=1; i<n(); i++)
        curr = e(i).get_symtab(curr);

    return curr;
}




/* ##################################################
   #####   named_lin_ineq                       #####
   ################################################## */

/***************************************************************************
 *                                                                         *
 ***************************************************************************/
named_lin_ineq::~named_lin_ineq()
{

}

void named_lin_ineq::init()
{
    unum=unum_cnt++;
}

void named_lin_ineq::init(int m, int n)
{
    unum=unum_cnt++;
    names().init(n);
    ineqs().init(m,n);
}

/***************************************************************************
 *                                                                         *
 ***************************************************************************/
void named_lin_ineq::init(const named_lin_ineq & c)
{
    nt.init(c.nt);
    lq = c.lq;
}


int named_lin_ineq::init(const immed_list & il, int c)
{
    unum = il[c++].integer();
    unum_cnt = MAX(unum_cnt, unum+1);

    int num = il[c++].integer();

    names().init(num);
    for(int i=1; i<num; i++)
       names()[i].init((name_table_entry_kind)il[c++].integer(),il[c++]);
    c = ineqs().integer_matrix::init(il, c);
    return c;
}

immed_list * named_lin_ineq::cvt_immed_list() const
{
    immed_list * L = new immed_list;

    L->append(immed(uid()));
    L->append(immed(n()));
    for(int i=1; i<n(); i++) {
        L->append(immed((int)const_names().e(i).kind()));
        L->append(const_names().e(i).name());
    }
    immed_list * iq = const_ineqs().cvt_immed_list();
    L->append(iq);
    return L;
}

void named_lin_ineq::swap_col(int i, int j)
{
    name_table_entry tmp(names()[i]);
    names()[i].init(names()[j]);
    names()[j].init(tmp);

    if(ineqs().m() > 0) {
        assert(names().n() == ineqs().n());
        lq.do_swap_col(i, j);
    }
}

void named_lin_ineq::del_col(int i, int j)
{
    assert(j>=i);
    assert((i>0)&&(j>0));
    assert((i<n())&&(j<n()));

    names().remove(i,j);
    lq.do_del_col(i,j);
}


void named_lin_ineq::del_col(const integer_row & rem)
{
    assert(rem.n() == n());
    names().remove(rem);
    ineqs().do_del_columns(rem);
    assert(names().n() == ineqs().n());
}

boolean named_lin_ineq::is_clean_false() const
{
    if ((m()==1) && (n()==1) && (const_ineqs().r(0).c(0) < 0))
	return TRUE;
    else
	return FALSE;
}

static void normalize_aux_offset(lin_ineq &leq, int auxcol)
{
    int bestrow = -1;
    int bestcoeff = 0;
    for (int i1=0; i1<leq.m(); i1++) {
	const integer_row &rowi = leq.r(i1);
	int coeff = rowi.c(auxcol);
	if (coeff > 0) {
	    if ((bestcoeff <= 0) || (coeff < bestcoeff)) {
		bestrow = i1;
		bestcoeff = coeff;
	    }
	} else if (coeff < 0) {
	    if ((bestcoeff == 0) || (coeff > bestcoeff)) {
		bestrow = i1;
		bestcoeff = coeff;
	    }
	}
    }

    int bestconst = leq[bestrow][0];
    int abscoeff = ABS(bestcoeff);
    int newconst = bestconst % abscoeff;
    newconst = (newconst > 0) ? newconst : newconst + abscoeff;
    int constdiff = (newconst - bestconst)/bestcoeff;
    
    for (int i2=0; i2<leq.m(); i2++) {
	int coeffi = leq[i2][auxcol];
	if (coeffi != 0) {
	    leq[i2][0] += constdiff * coeffi;
	}
    }
}

void named_lin_ineq::cleanup()
{
    del_zero_cols();
    ineqs().del_zeros();
    if(ineqs().m() == 0)
        return;

    if (is_clean_false()) return;

    if(~ineqs() == TRUE) {
	name_table nt0(1);
	lin_ineq leq0(1,1);
	leq0[0][0] = -1;
	init(named_lin_ineq(nt0, leq0));
        return;
    }

    integer_row rem(n());
    rem = 0;
    boolean remmed = FALSE;

    // remove aux vars that are empty.
    // also remove aux vars that are multiple of 1
    // also remove auxes which are only a lower or upper bound
    for(int i=1; i<n(); i++)
        if(names()[i].kind() == nte_aux) {
            boolean zero_or_one = TRUE;
	    int upper_bds = 0;
	    int upper_row = 0;
	    int lower_bds = 0;
	    int lower_row = 0;
            for(int j=0; (j<ineqs().m()); j++)
                if(ineqs()[j][i] != 0) {
		    if (ineqs()[j][i] > 0) {
			lower_bds++;
			lower_row = j;
		    } else {
			upper_bds++;
			upper_row = j;
		    }
		    if (ABS(ineqs()[j][i]) > 1)
			zero_or_one = FALSE;
		    else {
			fprintf(stderr,
				"\n### Warning: bad aux var ineq in cleanup\n");
			print(stderr);
		    }
		}
            if (zero_or_one || (upper_bds == 0) || (lower_bds == 0)) 
		rem[i] = remmed = TRUE;
	    else if ((upper_bds == 1) && (lower_bds == 1)) {
		constraint upper_bd(ineqs()[upper_row]);
		constraint lower_bd(ineqs()[lower_row]);
		upper_bd += ineqs()[lower_row];
		if (upper_bd.rank() == 0) {
		    int diffi = ineqs()[upper_row][0] + ineqs()[lower_row][0];
		    int mult = ineqs()[lower_row][i];
		    if (ABS(diffi) >= mult-1) {
			// S has aux X with only constraints 
			// c1 <= Y + mX <= c2 where c2-c1 >= m,
			// so remove X and its constraints
			rem[i] = remmed = TRUE;
		    }
		};
	    }
        }

    // check if two auxilary vars are doing the same job
    for(int i1=1; i1<n(); i1++)
        if((names()[i1].kind() == nte_aux)&&(!rem[i1]))
            for(int i2=i1+1; i2<n(); i2++)
                if((names()[i2].kind() == nte_aux)&&(!rem[i2])) {
                    constraint filter(n());
                    filter = 0;
                    filter[i1] = 1;
                    filter[i2] = 1;             // c1*i1=a(); c2*i2=b()
		    // get rows with occurrences of i1 or i2;
                    lin_ineq L = ineqs().filter_thru(filter, 0);
                    // assert(!(~L));              // has to have an answer
                    L.do_add_rows(1);
                    L[L.m()-1] = 0;
                    L[L.m()-1][0]  = 1;
                    L[L.m()-1][i1] = 1;         // if both are the same
                    L[L.m()-1][i2] = -1;        // c1 > c2 is empty
                    if(~L) {
                        L[L.m()-1][i1] = -1;    // and c2 > c1 is empty
                        L[L.m()-1][i2] =  1;
                        if(~L) rem[i2] = remmed = TRUE;
                    }
                }

    if (remmed) {
	ineqs().do_filter_away(rem,0);
	del_zero_cols();
    }

    // canonicalize aux offsets;
    for(int i3=1; i3<n(); i3++)
        if (names()[i3].kind() == nte_aux)
	    normalize_aux_offset(ineqs(),i3);
}

void named_lin_ineq::simplify()
{
    ineqs().normalize(TRUE);
    ineqs().sort();
    ineqs().del_repetition();
    ineqs().del_loose();
    cleanup();
    return;
}

void named_lin_ineq::del_zero_cols()
{
    integer_row zeros(n());

    for(int i=n()-1; i>=1; i--) {
        int zero = zeros[i] = 1;
        for(int j=0; zero && (j<ineqs().m()); j++) 
            if(ineqs()[j][i] != 0) {
		zeros[i] = zero = 0;
	    }
    }
    del_col(zeros);
}


named_lin_ineq & named_lin_ineq::operator=(const named_lin_ineq & c)
{
    if(&c == this) return *this;

    this->init(c);
    return *this;
}


named_lin_ineq & named_lin_ineq::operator=(const lin_ineq & l)
{