src/cmuBdd/bddunique.c File Reference

#include "bddint.h"

Include dependency graph for bddunique.c:

Go to the source code of this file.

Defines
#define	MIN_GC_LIMIT   10000
Functions
void	bdd_rehash_var_table (var_table table, int grow)
static void	bdd_mark (cmu_bdd_manager bddm)
void	bdd_sweep_var_table (cmu_bdd_manager bddm, long i, int maybe_rehash)
void	bdd_sweep (cmu_bdd_manager bddm)
void	cmu_bdd_gc (cmu_bdd_manager bddm)
static void	bdd_set_gc_limit (cmu_bdd_manager bddm)
void	bdd_clear_temps (cmu_bdd_manager bddm)
void	bdd_cleanup (cmu_bdd_manager bddm, int code)
bdd	bdd_find_aux (cmu_bdd_manager bddm, bdd_indexindex_type indexindex, INT_PTR d1, INT_PTR d2)
static void	bdd_check (cmu_bdd_manager bddm)
bdd	bdd_find (cmu_bdd_manager bddm, bdd_indexindex_type indexindex, bdd f, bdd g)
bdd	bdd_find_terminal (cmu_bdd_manager bddm, INT_PTR value1, INT_PTR value2)
void	cmu_bdd_clear_refs (cmu_bdd_manager bddm)
var_table	bdd_new_var_table (cmu_bdd_manager bddm)
void	cmu_bdd_init_unique (cmu_bdd_manager bddm)
void	cmu_bdd_free_unique (cmu_bdd_manager bddm)

---

Define Documentation

#define MIN_GC_LIMIT   10000

Definition at line 7 of file bddunique.c.

---

Function Documentation

static void bdd_check

(

cmu_bdd_manager

bddm

)

[static]

Definition at line 227 of file bddunique.c.

{
  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);
}

void bdd_cleanup	(	cmu_bdd_manager	bddm,
		int	code
	)

Definition at line 175 of file bddunique.c.

{
  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;
    }
}

void bdd_clear_temps

(

cmu_bdd_manager

bddm

)

Definition at line 153 of file bddunique.c.

{
  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);
}  

bdd bdd_find	(	cmu_bdd_manager	bddm,
		bdd_indexindex_type	indexindex,
		bdd	f,
		bdd	g
	)

Definition at line 271 of file bddunique.c.

{
  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 bdd_find_aux	(	cmu_bdd_manager	bddm,
		bdd_indexindex_type	indexindex,
		INT_PTR	d1,
		INT_PTR	d2
	)

Definition at line 192 of file bddunique.c.

{
  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);
}

bdd bdd_find_terminal	(	cmu_bdd_manager	bddm,
		INT_PTR	value1,
		INT_PTR	value2
	)

Definition at line 306 of file bddunique.c.

{
  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);
}

static void bdd_mark

(

cmu_bdd_manager

bddm

)

[static]

Definition at line 44 of file bddunique.c.

{
  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;
                }
              }
          }
    }
}

var_table bdd_new_var_table

(

cmu_bdd_manager

bddm

)

Definition at line 362 of file bddunique.c.

{
  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 bdd_rehash_var_table	(	var_table	table,
		int	grow
	)

Definition at line 11 of file bddunique.c.

{
  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_set_gc_limit

(

cmu_bdd_manager

bddm

)

[static]

Definition at line 141 of file bddunique.c.

{
  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_sweep

(

cmu_bdd_manager

bddm

)

Definition at line 118 of file bddunique.c.

{
  long i;

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

void bdd_sweep_var_table	(	cmu_bdd_manager	bddm,
		long	i,
		int	maybe_rehash
	)

Definition at line 81 of file bddunique.c.

{
  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 cmu_bdd_clear_refs

(

cmu_bdd_manager

bddm

)

Definition at line 331 of file bddunique.c.

{
  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);
        }
}

void cmu_bdd_free_unique

(

cmu_bdd_manager

bddm

)

Definition at line 395 of file bddunique.c.

{
  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);
}

void cmu_bdd_gc

(

cmu_bdd_manager

bddm

)

Definition at line 130 of file bddunique.c.

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

void cmu_bdd_init_unique

(

cmu_bdd_manager

bddm

)

Definition at line 379 of file bddunique.c.

{
  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;
}