/* BDD variable block routines */


#include "bddint.h"


static
void
add_block(block b1, block b2)
{
  long i, j, k;
  block start, end;

  if (b1->num_children)
    {
      i=bdd_find_block(b1, b2->first_index);
      start=b1->children[i];
      j=bdd_find_block(b1, b2->last_index);
      end=b1->children[j];
      if (i == j)
	add_block(start, b2);
      else
	{
	  if (start->first_index != b2->first_index || end->last_index != b2->last_index)
	    cmu_bdd_fatal("add_block: illegal block overlap");
	  b2->num_children=j-i+1;
	  b2->children=(block *)mem_get_block((SIZE_T)(sizeof(block)*b2->num_children));
	  for (k=0; k < b2->num_children; ++k)
	    b2->children[k]=b1->children[i+k];
	  b1->children[i]=b2;
	  ++i;
	  for (k=j+1; k < b1->num_children; ++k, ++i)
	    b1->children[i]=b1->children[k];
	  b1->num_children-=(b2->num_children-1);
	  b1->children=(block *)mem_resize_block((pointer)b1->children, (SIZE_T)(sizeof(block)*b1->num_children));
	}
    }
  else
    {
      /* b1 and b2 are blocks representing just single variables. */
      b1->num_children=1;
      b1->children=(block *)mem_get_block((SIZE_T)(sizeof(block)*b1->num_children));
      b1->children[0]=b2;
      b2->num_children=0;
      b2->children=0;
    }
}


block
cmu_bdd_new_var_block(cmu_bdd_manager bddm, bdd v, long n)
{
  block b;

  if (bdd_check_arguments(1, v))
    {
      BDD_SETUP(v);
      if (cmu_bdd_type_aux(bddm, v) != BDD_TYPE_POSVAR)
	{
	  cmu_bdd_warning("cmu_bdd_new_var_block: second argument is not a positive variable");
	  if (BDD_IS_CONST(v))
	    return ((block)0);
	}
      b=(block)BDD_NEW_REC(bddm, sizeof(struct block_));
      b->reorderable=0;
      b->first_index=BDD_INDEX(bddm, v);
      if (n <= 0)
	{
	  cmu_bdd_warning("cmu_bdd_new_var_block: invalid final argument");
	  n=1;
	}
      b->last_index=b->first_index+n-1;
      if (b->last_index >= bddm->vars)
	{
	  cmu_bdd_warning("cmu_bdd_new_var_block: range covers non-existent variables");
	  b->last_index=bddm->vars-1;
	}
      add_block(bddm->super_block, b);
      return (b);
    }
  return ((block)0);
}