import contract;

public class BBag extends BSet {

  contract con = new contract();

  public BBag(int size) {
    super(size);

    if (!con.require(size>0, "(new) set size must be positive")) return;
    count = new int[size];
    con.ensure( empty(), "(new) empty set");
    con.ensure(!full(), "(new) non-full set");
  }
  
  public void add(int el) {
    if (!con.require(!full(), "(add) got full set")) return;
    int i;
    for (i=0; (i<nelt)&&(elts[i]!=el); ++i);
    if(nelt < nmax) {
      if(i==nelt) {
	elts[i]=el;
	count[i]=1;
	nelt++;
      }
      else 
	count[i]++;
    }
    con.ensure(has(el), "(add) set should have elt");
    con.ensure(!empty(), "(add) set should not be empty");
  }

  public void add_many(int el, int num) {
    int i;
    for (i=0; i<num; ++i) 
      add(el);
  }

  public void remove(int el) {
    int i;
    for (i=0; (i<nelt)&&(elts[i]!=el);++i);
    if (i<nelt) {
      if (count[i]>1)
	count[i]--;
      else {
	for(i++; i<nelt; i++) {
	  elts[i-1]=elts[i];
	  count[i-1]=count[i];
	}
	nelt--;
      }
    }
  }
  
  public void remove_many(int el, int num) {
    int i;
    for (i=0; i<num; ++i)
      remove(el);
    }
  
  public int size() {
    int sz = 0;
    int i;
    for (i = 0; i<nelt; ++i)
      sz = sz + count[i];
    return sz;
  }

  public int number(int el) {
    if (!super.has(el)) return 0;
    else {
      int i;
      for (i=0; elts[i]!=el; ++i);
      return count[i];
    }
  }
  
  public boolean equal(BBag b) {
    if (nelt!=b.nelt) return false;
    if (size()!=b.size()) return false;
    if (nelt==0) return true;
    int i;
    int j;
    for (i=0,j=0; (i<nelt)&&(j<nelt); i++) {
      for (j=0; (j<nelt)&&(elts[i] != b.elts[j]); j++);
      if ((j==nelt)||(count[j]!=b.count[j])) return false;
    }
    return true;
  }
  
  public void print() {
    int i;
    System.out.print("{");
    for (i=0; i<nelt; ++i) {
      int j;
      for (j=0; j<count[i]; ++j)
	System.out.print((i!=0 ? ", " : "")+elts[i]);
    }
    System.out.println("}");
  }
    
  private int count[];
}