/* BDD unique table routines */


#include "bddint.h"


#define MIN_GC_LIMIT 10000


void
bdd_rehash_var_table(var_table table, int grow)
{
  long i;
  long hash;
  long oldsize;
  bdd *newtable;
  bdd p, q;

  oldsize=table->size;
  if (grow)
    table->size_index++;
  else
    table->size_index--;
  table->size=TABLE_SIZE(table->size_index);
  newtable=(bdd *)mem_get_block((SIZE_T)(table->size*sizeof(bdd)));
  for (i=0; i < table->size; ++i)
    newtable[i]=0;
  for (i=0; i < oldsize; ++i)
    for (p=table->table[i]; p; p=q)
      {
	q=p->next;
	hash=HASH_NODE(p->data[0], p->data[1]);
	BDD_REDUCE(hash, table->size);
	p->next=newtable[hash];
	newtable[hash]=p;
      }
  mem_free_block((pointer)table->table);
  table->table=newtable;
}


static
void
bdd_mark(cmu_bdd_manager bddm)
{
  long i, j;
  var_table table;
  bdd f, g;

  for (i=0; i <= bddm->vars; ++i)
    {
      if (i == bddm->vars)
	table=bddm->unique_table.tables[BDD_CONST_INDEXINDEX];
      else
	table=bddm->unique_table.tables[bddm->indexindexes[i]];
      for (j=0; j < table->size; ++j)
	for (f=table->table[j]; f; f=f->next)
	  {
	    BDD_SETUP(f);
	    if (BDD_REFS(f) || BDD_TEMP_REFS(f))
	      BDD_MARK(f)|=BDD_GC_MARK;
	    if (BDD_IS_USED(f) && !BDD_IS_CONST(f))
	      {
		g=(bdd)BDD_DATA0(f);
		{
		  BDD_SETUP(g);
		  BDD_MARK(g)|=BDD_GC_MARK;
		}
		g=(bdd)BDD_DATA1(f);
		{
		  BDD_SETUP(g);
		  BDD_MARK(g)|=BDD_GC_MARK;
		}
	      }
	  }
    }
}


void
bdd_sweep_var_table(cmu_bdd_manager bddm, long i, int maybe_rehash)
{
  long j;
  var_table table;
  bdd f, *p;

  table=bddm->unique_table.tables[i];
  for (j=0; j < table->size; ++j)
    for (p= &table->table[j], f= *p; f; f= *p)
      {
	BDD_SETUP(f);
	if (BDD_IS_USED(f))
	  {
	    BDD_SETUP(f);
	    BDD_MARK(f)&=~BDD_GC_MARK;
	    p= &f->next;
	  }
	else
	  {
	    *p=f->next;
	    if (i == BDD_CONST_INDEXINDEX && bddm->unique_table.free_terminal_fn)
	      (*bddm->unique_table.free_terminal_fn)(bddm,
						     BDD_DATA0(f),
						     BDD_DATA1(f),
						     bddm->unique_table.free_terminal_env);
	    BDD_FREE_REC(bddm, (pointer)f, sizeof(struct bdd_));
	    table->entries--;
	    bddm->unique_table.entries--;
	    bddm->unique_table.freed++;
	  }
      }
  if (maybe_rehash && table->size > table->entries && table->size_index > 3)
    bdd_rehash_var_table(table, 0);
}


void
bdd_sweep(cmu_bdd_manager bddm)
{
  long i;

  for (i=0; i <= bddm->vars; ++i)
    bdd_sweep_var_table(bddm, i, 1);
}


/* cmu_bdd_gc(bddm) performs a garbage collection. */

void
cmu_bdd_gc(cmu_bdd_manager bddm)
{
  bdd_mark(bddm);
  bdd_purge_cache(bddm);
  bdd_sweep(bddm);
  bddm->unique_table.gcs++;
}


static
void
bdd_set_gc_limit(cmu_bdd_manager bddm)
{
  bddm->unique_table.gc_limit=2*bddm->unique_table.entries;
  if (bddm->unique_table.gc_limit < MIN_GC_LIMIT)
    bddm->unique_table.gc_limit=MIN_GC_LIMIT;
  if (bddm->unique_table.node_limit &&
      bddm->unique_table.gc_limit > bddm->unique_table.node_limit)
    bddm->unique_table.gc_limit=bddm->unique_table.node_limit;
}


void
bdd_clear_temps(cmu_bdd_manager bddm)
{
  long i, j;
  var_table table;
  bdd f;

  for (i=0; i <= bddm->vars; ++i)
    {
      table=bddm->unique_table.tables[i];
      for (j=0; j < table->size; ++j)
	for (f=table->table[j]; f; f=f->next)
	  {
	    BDD_SETUP(f);
	    BDD_TEMP_REFS(f)=0;
	  }
    }
  cmu_bdd_gc(bddm);
  bdd_set_gc_limit(bddm);
}  


void
bdd_cleanup(cmu_bdd_manager bddm, int code)
{
  bdd_clear_temps(bddm);
  switch (code)
    {
    case BDD_ABORTED:
      (*bddm->bag_it_fn)(bddm, bddm->bag_it_env);
      break;
    case BDD_OVERFLOWED:
      if (bddm->overflow_fn)
	(*bddm->overflow_fn)(bddm, bddm->overflow_env);
      break;
    }
}


bdd
bdd_find_aux(cmu_bdd_manager bddm, bdd_indexindex_type indexindex, INT_PTR d1, INT_PTR d2)
{
  var_table table;
  long hash;
  bdd temp;

  table=bddm->unique_table.tables[indexindex];
  hash=HASH_NODE(d1, d2);
  BDD_REDUCE(hash, table->size);
  for (temp=table->table[hash]; temp; temp=temp->next)
    if (temp->data[0] == d1 && temp->data[1] == d2)
      break;
  if (!temp)
    {
      /* Not found; make a new node. */
      temp=(bdd)BDD_NEW_REC(bddm, sizeof(struct bdd_));
      temp->indexindex=indexindex;
      temp->refs=0;
      temp->mark=0;
      temp->data[0]=d1;
      temp->data[1]=d2;
      temp->next=table->table[hash];
      table->table[hash]=temp;
      table->entries++;
      bddm->unique_table.entries++;
      if (4*table->size < table->entries)
	bdd_rehash_var_table(table, 1);
    }
  bddm->unique_table.finds++;
  return (temp);
}


static
void
bdd_check(cmu_bdd_manager bddm)
{
  long nodes;

  bddm->check=100;
  /* When bag_it_fn set, clean up and abort immediately. */
  if (bddm->bag_it_fn)
    longjmp(bddm->abort.context, BDD_ABORTED);
  if (bddm->unique_table.entries > bddm->unique_table.gc_limit)
    {
      cmu_bdd_gc(bddm);
      /* Table full. */
      nodes=bddm->unique_table.entries;
      if (3*nodes > 2*bddm->unique_table.gc_limit && bddm->allow_reordering && bddm->reorder_fn)
	{
	  cmu_bdd_reorder_aux(bddm);
	  if (4*bddm->unique_table.entries > 3*nodes && 3*nodes > 4*bddm->nodes_at_start)
	    /* If we didn't save much, but we have created a reasonable number */
	    /* of nodes, then don't bother reordering next time. */
	    bddm->allow_reordering=0;
	  /* Go try again. */
	  bdd_set_gc_limit(bddm);
	  longjmp(bddm->abort.context, BDD_REORDERED);
	}
      bdd_set_gc_limit(bddm);
      if (bddm->unique_table.node_limit &&
	  bddm->unique_table.entries >= bddm->unique_table.node_limit-1000)
	{
	  /* Out of memory; go clean up. */
	  bddm->overflow=1;
	  longjmp(bddm->abort.context, BDD_OVERFLOWED);
	}
    }
  /* Maybe increase cache size if it's getting full. */
  if (3*bddm->op_cache.size < 2*bddm->op_cache.entries &&
      32*bddm->op_cache.size < bddm->op_cache.cache_ratio*bddm->unique_table.entries)
    bdd_rehash_cache(bddm, 1);
}


/* bdd_find(bddm, indexindex, f, g) creates or finds a node with the */
/* given indexindex, "then" pointer, and "else" pointer. */

bdd
bdd_find(cmu_bdd_manager bddm, bdd_indexindex_type indexindex, bdd f, bdd g)
{
  bdd temp;

  BDD_SETUP(f);
  BDD_SETUP(g);
  if (f == g)
    {
      BDD_TEMP_DECREFS(f);
      temp=f;
    }
  else
    {
      if (BDD_IS_OUTPOS(f))
	temp=bdd_find_aux(bddm, indexindex, (INT_PTR)f, (INT_PTR)g);
      else
	temp=BDD_NOT(bdd_find_aux(bddm, indexindex, (INT_PTR)BDD_NOT(f), (INT_PTR)BDD_NOT(g)));
      {
	BDD_SETUP(temp);
	BDD_TEMP_INCREFS(temp);
      }
      BDD_TEMP_DECREFS(f);
      BDD_TEMP_DECREFS(g);
    }
  bddm->check--;
  if (!bddm->check)
    bdd_check(bddm);
  return (temp);
}


/* bdd_find_terminal(bddm, value1, value2) creates or finds a terminal */
/* node with the given data value. */

bdd
bdd_find_terminal(cmu_bdd_manager bddm, INT_PTR value1, INT_PTR value2)
{
  bdd temp;

  if ((*bddm->canonical_fn)(bddm, value1, value2, bddm->transform_env))
    {
      (*bddm->transform_fn)(bddm, value1, value2, &value1, &value2, bddm->transform_env);
      temp=BDD_NOT(bdd_find_aux(bddm, BDD_CONST_INDEXINDEX, value1, value2));
    }
  else
    temp=bdd_find_aux(bddm, BDD_CONST_INDEXINDEX, value1, value2);
  {
    BDD_SETUP(temp);
    BDD_TEMP_INCREFS(temp);
  }
  bddm->check--;
  if (!bddm->check)
    bdd_check(bddm);
  return (temp);
}


/* cmu_bdd_clear_refs(bddm) sets the reference count of all nodes to 0. */

void
cmu_bdd_clear_refs(cmu_bdd_manager bddm)
{
  long i, j;
  var_table table;
  bdd f;
  assoc_list q;

  for (i=0; i <= bddm->vars; ++i)
    {
      table=bddm->unique_table.tables[i];
      for (j=0; j < table->size; ++j)
	for (f=table->table[j]; f; f=f->next)
	  {
	    BDD_SETUP(f);
	    BDD_REFS(f)=0;
	  }
    }
  for (i=0; i < bddm->vars; ++i)
    bddm->variables[i+1]->refs=BDD_MAX_REFS;
  bddm->one->refs=BDD_MAX_REFS;
  for (q=bddm->assocs; q; q=q->next)
    for (i=0; i < bddm->vars; ++i)
      if ((f=q->va.assoc[i+1]))
	{
	  BDD_SETUP(f);
	  BDD_INCREFS(f);
	}
}


var_table
bdd_new_var_table(cmu_bdd_manager bddm)
{
  long i;
  var_table table;

  table=(var_table)BDD_NEW_REC(bddm, sizeof(struct var_table_));
  table->size_index=3;
  table->size=TABLE_SIZE(table->size_index);
  table->entries=0;
  table->table=(bdd *)mem_get_block((SIZE_T)(table->size*sizeof(bdd)));
  for (i=0; i < table->size; ++i)
    table->table[i]=0;
  return (table);
}


void
cmu_bdd_init_unique(cmu_bdd_manager bddm)
{
  bddm->unique_table.tables=(var_table *)mem_get_block((SIZE_T)((bddm->maxvars+1)*sizeof(var_table)));
  bddm->unique_table.tables[BDD_CONST_INDEXINDEX]=bdd_new_var_table(bddm);
  bddm->unique_table.gc_limit=MIN_GC_LIMIT;
  bddm->unique_table.node_limit=0;
  bddm->unique_table.entries=0;
  bddm->unique_table.freed=0;
  bddm->unique_table.gcs=0;
  bddm->unique_table.finds=0;
  bddm->unique_table.free_terminal_fn=0;
  bddm->unique_table.free_terminal_env=0;
}


void
cmu_bdd_free_unique(cmu_bdd_manager bddm)
{
  long i, j;
  var_table table;
  bdd p, q;

  for (i=0; i <= bddm->vars; ++i)
    {
      table=bddm->unique_table.tables[i];
      for (j=0; j < table->size; ++j)
	for (p=table->table[j]; p; p=q)
	  {
	    q=p->next;
	    BDD_FREE_REC(bddm, (pointer)p, sizeof(struct bdd_));
	  }
      mem_free_block((pointer)table->table);
      BDD_FREE_REC(bddm, (pointer)table, sizeof(struct var_table_));
    }
  mem_free_block((pointer)bddm->unique_table.tables);
}