src/cmuBdd/bdd.c File Reference

#include "bddint.h"

Include dependency graph for bdd.c:

Go to the source code of this file.

Functions
bdd	cmu_bdd_one (cmu_bdd_manager bddm)
bdd	cmu_bdd_zero (cmu_bdd_manager bddm)
bdd	bdd_make_external (bdd f)
long	bdd_find_block (block b, long index)
void	bdd_block_delta (block b, long delta)
static block	shift_block (cmu_bdd_manager bddm, block b, long index)
static bdd	bdd_new_var (cmu_bdd_manager bddm, bdd_index_type index)
bdd	cmu_bdd_new_var_first (cmu_bdd_manager bddm)
bdd	cmu_bdd_new_var_last (cmu_bdd_manager bddm)
bdd	cmu_bdd_new_var_before (cmu_bdd_manager bddm, bdd var)
bdd	cmu_bdd_new_var_after (cmu_bdd_manager bddm, bdd var)
bdd	cmu_bdd_var_with_index (cmu_bdd_manager bddm, long index)
bdd	cmu_bdd_var_with_id (cmu_bdd_manager bddm, long indexindex)
static bdd	cmu_bdd_and_step (cmu_bdd_manager bddm, bdd f, bdd g)
static bdd	cmu_bdd_xnor_step (cmu_bdd_manager bddm, bdd f, bdd g)
bdd	cmu_bdd_ite_step (cmu_bdd_manager bddm, bdd f, bdd g, bdd h)
bdd	cmu_bdd_ite (cmu_bdd_manager bddm, bdd f, bdd g, bdd h)
bdd	cmu_bdd_and (cmu_bdd_manager bddm, bdd f, bdd g)
bdd	cmu_bdd_nand (cmu_bdd_manager bddm, bdd f, bdd g)
bdd	cmu_bdd_or (cmu_bdd_manager bddm, bdd f, bdd g)
bdd	cmu_bdd_nor (cmu_bdd_manager bddm, bdd f, bdd g)
bdd	cmu_bdd_xor (cmu_bdd_manager bddm, bdd f, bdd g)
bdd	cmu_bdd_xnor (cmu_bdd_manager bddm, bdd f, bdd g)
bdd	cmu_bdd_identity (cmu_bdd_manager bddm, bdd f)
bdd	cmu_bdd_not (cmu_bdd_manager bddm, bdd f)
bdd	cmu_bdd_if (cmu_bdd_manager bddm, bdd f)
long	cmu_bdd_if_index (cmu_bdd_manager bddm, bdd f)
long	cmu_bdd_if_id (cmu_bdd_manager bddm, bdd f)
bdd	cmu_bdd_then (cmu_bdd_manager bddm, bdd f)
bdd	cmu_bdd_else (cmu_bdd_manager bddm, bdd f)
static bdd	cmu_bdd_intersects_step (cmu_bdd_manager bddm, bdd f, bdd g)
bdd	cmu_bdd_intersects (cmu_bdd_manager bddm, bdd f, bdd g)
bdd	cmu_bdd_implies (cmu_bdd_manager bddm, bdd f, bdd g)
int	cmu_bdd_type_aux (cmu_bdd_manager bddm, bdd f)
int	cmu_bdd_type (cmu_bdd_manager bddm, bdd f)
void	cmu_bdd_unfree (cmu_bdd_manager bddm, bdd f)
void	cmu_bdd_free (cmu_bdd_manager bddm, bdd f)
long	cmu_bdd_vars (cmu_bdd_manager bddm)
long	cmu_bdd_total_size (cmu_bdd_manager bddm)
int	cmu_bdd_cache_ratio (cmu_bdd_manager bddm, int new_ratio)
long	cmu_bdd_node_limit (cmu_bdd_manager bddm, long new_limit)
int	cmu_bdd_overflow (cmu_bdd_manager bddm)
void	cmu_bdd_overflow_closure (cmu_bdd_manager bddm, void(*overflow_fn)(cmu_bdd_manager, pointer), pointer overflow_env)
void	cmu_bdd_abort_closure (cmu_bdd_manager bddm, void(*abort_fn)(cmu_bdd_manager, pointer), pointer abort_env)
void	cmu_bdd_stats (cmu_bdd_manager bddm, FILE *fp)
static int	bdd_default_canonical_fn (cmu_bdd_manager bddm, INT_PTR value1, INT_PTR value2, pointer junk)
static void	bdd_default_transform_fn (cmu_bdd_manager bddm, INT_PTR value1, INT_PTR value2, INT_PTR *result1, INT_PTR *result2, pointer junk)
cmu_bdd_manager	cmu_bdd_init (void)
void	cmu_bdd_quit (cmu_bdd_manager bddm)

---

Function Documentation

void bdd_block_delta	(	block	b,
		long	delta
	)

Definition at line 57 of file bdd.c.

{
  long i;

  b->first_index+=delta;
  b->last_index+=delta;
  for (i=0; i < b->num_children; ++i)
    bdd_block_delta(b->children[i], delta);
}

static int bdd_default_canonical_fn	(	cmu_bdd_manager	bddm,
		INT_PTR	value1,
		INT_PTR	value2,
		pointer	junk
	)			[static]

Definition at line 992 of file bdd.c.

{
  /* Default transformation is treat the value as a 64-bit integer and to */
  /* negate it if it is positive. */
  return ((long)value1 > 0 || (!value1 && (long)value2 > 0));
}

static void bdd_default_transform_fn	(	cmu_bdd_manager	bddm,
		INT_PTR	value1,
		INT_PTR	value2,
		INT_PTR *	result1,
		INT_PTR *	result2,
		pointer	junk
	)			[static]

Definition at line 1002 of file bdd.c.

{
  if (!value2)
    /* Will be a carry when taking 2's complement of value2.  Thus, */
    /* take 2's complement of high part. */
    value1= -(long)value1;
  else
    {
      value2= -(long)value2;
      value1= ~value1;
    }
  *result1=value1;
  *result2=value2;
}

long bdd_find_block	(	block	b,
		long	index
	)

Definition at line 36 of file bdd.c.

{
  long i, j, k;

  i=0;
  j=b->num_children-1;
  while (i <= j)
    {
      k=(i+j)/2;
      if (b->children[k]->first_index <= index && b->children[k]->last_index >= index)
        return (k);
      if (b->children[k]->first_index > index)
        j=k-1;
      else
        i=k+1;
    }
  return (i);
}

bdd bdd_make_external

(

bdd

f

)

Definition at line 26 of file bdd.c.

{
  BDD_SETUP(f);
  BDD_INCREFS(f);
  BDD_TEMP_DECREFS(f);
  return (f);
}

static bdd bdd_new_var	(	cmu_bdd_manager	bddm,
		bdd_index_type	index
	)			[static]

Definition at line 114 of file bdd.c.

{
  long i;
  long temp;
  long oldmax;
  assoc_list p;
  bdd var;

  if (bddm->vars == BDD_MAX_INDEXINDEX)
    cmu_bdd_fatal("bdd_new_var: no more indexes");
  if (index > bddm->vars)
    cmu_bdd_fatal("bdd_new_var: index out of range");
  if (bddm->vars == bddm->maxvars)
    {
      /* Expand indexing tables and variable associations. */
      oldmax=bddm->maxvars;
      temp=bddm->maxvars*2;
      if (temp > BDD_MAX_INDEXINDEX-1)
        temp=BDD_MAX_INDEXINDEX-1;
      bddm->maxvars=temp;
      bddm->variables=(bdd *)mem_resize_block((pointer)bddm->variables,
                                              (SIZE_T)((bddm->maxvars+1)*sizeof(bdd)));
      bddm->indexes=(bdd_index_type *)mem_resize_block((pointer)bddm->indexes,
                                                       (SIZE_T)((bddm->maxvars+1)*sizeof(bdd_index_type)));
      bddm->indexindexes=
        (bdd_indexindex_type *)mem_resize_block((pointer)bddm->indexindexes,
                                                (SIZE_T)(bddm->maxvars*sizeof(bdd_indexindex_type)));
      bddm->unique_table.tables=
        (var_table *)mem_resize_block((pointer)bddm->unique_table.tables,
                                      (SIZE_T)((bddm->maxvars+1)*sizeof(var_table)));
      /* Variable associations are padded with nulls in case new variables */
      /* are created. */
      for (p=bddm->assocs; p; p=p->next)
        {
          p->va.assoc=(bdd *)mem_resize_block((pointer)p->va.assoc, (SIZE_T)((bddm->maxvars+1)*sizeof(bdd)));
          for (i=oldmax; i < bddm->maxvars; ++i)
            p->va.assoc[i+1]=0;
        }
      bddm->temp_assoc.assoc=(bdd *)mem_resize_block((pointer)bddm->temp_assoc.assoc, (SIZE_T)((bddm->maxvars+1)*sizeof(bdd)));
      for (i=oldmax; i < bddm->maxvars; ++i)
        bddm->temp_assoc.assoc[i+1]=0;
    }
  /* Shift index of following variables. */
  if (index != bddm->vars)
    for (i=0; i < bddm->vars; ++i)
      if (bddm->indexes[i+1] >= index)
        bddm->indexes[i+1]++;
  for (p=bddm->assocs; p; p=p->next)
    if (p->va.last >= index)
      p->va.last++;
  if (bddm->temp_assoc.last >= index)
    bddm->temp_assoc.last++;
  /* Shift indexindex values. */
  for (i=bddm->vars; i > index; --i)
    bddm->indexindexes[i]=bddm->indexindexes[i-1];
  /* Make a new variable table. */
  bddm->vars++;
  bddm->unique_table.tables[bddm->vars]=bdd_new_var_table(bddm);
  /* Create the variable. */
  var=bdd_find_aux(bddm, (bdd_indexindex_type)bddm->vars, (INT_PTR)BDD_ONE(bddm), (INT_PTR)BDD_ZERO(bddm));
  var->refs=BDD_MAX_REFS;
  /* Record everything. */
  bddm->variables[bddm->vars]=var;
  bddm->indexes[bddm->vars]=index;
  bddm->indexindexes[index]=bddm->vars;
  /* Make a new variable block containing the variable. */
  shift_block(bddm, bddm->super_block, (long)index);
  return (var);
}

void cmu_bdd_abort_closure	(	cmu_bdd_manager	bddm,
		void(*)(cmu_bdd_manager, pointer)	abort_fn,
		pointer	abort_env
	)

Definition at line 928 of file bdd.c.

{
  bddm->bag_it_fn=abort_fn;
  bddm->bag_it_env=abort_env;
}

bdd cmu_bdd_and	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	g
	)

Definition at line 501 of file bdd.c.

{
  return (cmu_bdd_ite(bddm, f, g, BDD_ZERO(bddm)));
}

static bdd cmu_bdd_and_step	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	g
	)			[static]

Definition at line 273 of file bdd.c.

{
  bdd_indexindex_type top_indexindex;
  bdd f1, f2;
  bdd g1, g2;
  bdd temp1, temp2;
  bdd result;

  BDD_SETUP(f);
  BDD_SETUP(g);
  if (BDD_IS_CONST(f))
    {
      if (f == BDD_ZERO(bddm))
        return (f);
      BDD_TEMP_INCREFS(g);
      return (g);
    }
  /* f is not constant. */
  if (BDD_IS_CONST(g))
    {
      if (g == BDD_ZERO(bddm))
        return (g);
      BDD_TEMP_INCREFS(f);
      return (f);
    }
  /* f and g are not constant. */
  if (BDD_SAME_OR_NEGATIONS(f, g))
    {
      if (f == g)
        {
          BDD_TEMP_INCREFS(f);
          return (f);
        }
      return (BDD_ZERO(bddm));
    }
  /* f and g are not constant and are not equal or negations. */
  if (BDD_OUT_OF_ORDER(f, g))
    BDD_SWAP(f, g);
  if (bdd_lookup_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)BDD_ZERO(bddm), (INT_PTR *)&result))
    return (result);
  BDD_TOP_VAR2(top_indexindex, bddm, f, g);
  BDD_COFACTOR(top_indexindex, f, f1, f2);
  BDD_COFACTOR(top_indexindex, g, g1, g2);
  temp1=cmu_bdd_and_step(bddm, f1, g1);
  temp2=cmu_bdd_and_step(bddm, f2, g2);
  result=bdd_find(bddm, top_indexindex, temp1, temp2);
  bdd_insert_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)BDD_ZERO(bddm), (INT_PTR)result);
  return (result);
}

int cmu_bdd_cache_ratio	(	cmu_bdd_manager	bddm,
		int	new_ratio
	)

Definition at line 863 of file bdd.c.

{
  int old_ratio;

  old_ratio=bddm->op_cache.cache_ratio;
  if (new_ratio < 1)
    new_ratio=1;
  else if (new_ratio > 32)
    new_ratio=32;
  bddm->op_cache.cache_ratio=new_ratio;
  return (old_ratio);
}

bdd cmu_bdd_else	(	cmu_bdd_manager	bddm,
		bdd	f
	)

Definition at line 672 of file bdd.c.

{
  if (bdd_check_arguments(1, f))
    {
      BDD_SETUP(f);
      if (BDD_IS_CONST(f))
        {
          cmu_bdd_warning("cmu_bdd_else: argument is a constant");
          return (f);
        }
      f=BDD_ELSE(f);
      BDD_RESET(f);
      BDD_INCREFS(f);
    }
  return (f);
}

void cmu_bdd_free	(	cmu_bdd_manager	bddm,
		bdd	f
	)

Definition at line 828 of file bdd.c.

{
  if (f)
    {
      BDD_SETUP(f);
      if (BDD_REFS(f) == 0)
        cmu_bdd_fatal("cmu_bdd_free: attempt to free node with zero references");
      else
        BDD_DECREFS(f);
    }
}

bdd cmu_bdd_identity	(	cmu_bdd_manager	bddm,
		bdd	f
	)

Definition at line 568 of file bdd.c.

{
  if (bdd_check_arguments(1, f))
    {
      BDD_SETUP(f);
      BDD_INCREFS(f);
    }
  return (f);
}

bdd cmu_bdd_if	(	cmu_bdd_manager	bddm,
		bdd	f
	)

Definition at line 597 of file bdd.c.

{
  if (bdd_check_arguments(1, f))
    {
      BDD_SETUP(f);
      if (BDD_IS_CONST(f))
        {
          cmu_bdd_warning("cmu_bdd_if: argument is a constant");
          return (f);
        }
      FIREWALL(bddm);
      RETURN_BDD(BDD_IF(bddm, f));
    }
  return (f);
}

long cmu_bdd_if_id	(	cmu_bdd_manager	bddm,
		bdd	f
	)

Definition at line 635 of file bdd.c.

{
  if (bdd_check_arguments(1, f))
    {
      BDD_SETUP(f);
      if (BDD_IS_CONST(f))
        return (-1l);
      return ((long)BDD_INDEXINDEX(f));
    }
  return (-1l);
}

long cmu_bdd_if_index	(	cmu_bdd_manager	bddm,
		bdd	f
	)

Definition at line 618 of file bdd.c.

{
  if (bdd_check_arguments(1, f))
    {
      BDD_SETUP(f);
      if (BDD_IS_CONST(f))
        return (-1l);
      return ((long)BDD_INDEX(bddm, f));
    }
  return (-1l);
}

bdd cmu_bdd_implies	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	g
	)

Definition at line 766 of file bdd.c.

{
  if (bdd_check_arguments(2, f, g))
    {
      FIREWALL(bddm);
      RETURN_BDD(cmu_bdd_intersects_step(bddm, f, BDD_NOT(g)));
    }
  return ((bdd)0);
}

cmu_bdd_manager cmu_bdd_init

(

void

)

Definition at line 1021 of file bdd.c.

{
  cmu_bdd_manager bddm;
  long i;

  bddm=(cmu_bdd_manager)mem_get_block((SIZE_T)sizeof(struct bdd_manager_));
  bddm->overflow=0;
  bddm->overflow_fn=0;
  bddm->overflow_env=0;
  bddm->bag_it_fn=0;
  bddm->bag_it_env=0;
  bddm->canonical_fn=bdd_default_canonical_fn;
  bddm->transform_fn=bdd_default_transform_fn;
  bddm->transform_env=0;
  bddm->reorder_fn=0;
  bddm->reorder_data=0;
  bddm->vars=0;
  bddm->maxvars=30; 
  bddm->check=1;
  bddm->variables=(bdd *)mem_get_block((SIZE_T)((bddm->maxvars+1)*sizeof(bdd)));
  bddm->indexes=(bdd_index_type *)mem_get_block((SIZE_T)((bddm->maxvars+1)*sizeof(bdd_index_type)));
  bddm->indexindexes=(bdd_indexindex_type *)mem_get_block((SIZE_T)(bddm->maxvars*sizeof(bdd_indexindex_type)));
  bddm->indexes[BDD_CONST_INDEXINDEX]=BDD_MAX_INDEX;
  for (i=0; i < REC_MGRS; ++i)
    bddm->rms[i]=mem_new_rec_mgr(MIN_REC_SIZE+ALLOC_ALIGNMENT*i);
  bddm->temp_assoc.assoc=(bdd *)mem_get_block((SIZE_T)((bddm->maxvars+1)*sizeof(bdd)));
  bddm->temp_assoc.last= -1;
  for (i=0; i < bddm->maxvars; ++i)
    bddm->temp_assoc.assoc[i+1]=0;
  bddm->curr_assoc_id= -1;
  bddm->curr_assoc= &bddm->temp_assoc;
  bddm->assocs=0;
  bddm->temp_op= -1;
  bddm->super_block=(block)BDD_NEW_REC(bddm, sizeof(struct block_));
  bddm->super_block->num_children=0;
  bddm->super_block->children=0;
  bddm->super_block->reorderable=1;
  bddm->super_block->first_index= -1;
  bddm->super_block->last_index=0;
  cmu_bdd_init_unique(bddm);
  cmu_bdd_init_cache(bddm);
  bddm->one=bdd_find_terminal(bddm, ~(INT_PTR)0, ~(INT_PTR)0);
  bddm->one->refs=BDD_MAX_REFS;
  bddm->one->mark=0;
  bddm->zero=BDD_NOT(bddm->one);
  if (sizeof(double) > 2*sizeof(long))
    cmu_bdd_warning("cmu_bdd_init: portability problem for cmu_bdd_satisfying_fraction");
  return (bddm);
}

bdd cmu_bdd_intersects	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	g
	)

Definition at line 751 of file bdd.c.

{
  if (bdd_check_arguments(2, f, g))
    {
      FIREWALL(bddm);
      RETURN_BDD(cmu_bdd_intersects_step(bddm, f, g));
    }
  return ((bdd)0);
}

static bdd cmu_bdd_intersects_step	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	g
	)			[static]

Definition at line 692 of file bdd.c.

{
  bdd_indexindex_type top_indexindex;
  bdd f1, f2;
  bdd g1, g2;
  bdd temp;

  BDD_SETUP(f);
  BDD_SETUP(g);
  if (BDD_IS_CONST(f))
    {
      if (f == BDD_ZERO(bddm))
        return (f);
      BDD_TEMP_INCREFS(g);
      return (g);
    }
  /* f is not constant. */
  if (BDD_IS_CONST(g))
    {
      if (g == BDD_ZERO(bddm))
        return (g);
      BDD_TEMP_INCREFS(f);
      return (f);
    }
  /* f and g are not constant. */
  if (BDD_SAME_OR_NEGATIONS(f, g))
    {
      if (f == g)
        {
          BDD_TEMP_INCREFS(f);
          return (f);
        }
      return (BDD_ZERO(bddm));
    }
  /* f and g are not constant and are not equal or negations. */
  if (BDD_OUT_OF_ORDER(f, g))
    BDD_SWAP(f, g);
  if (bdd_lookup_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)BDD_ZERO(bddm), (INT_PTR *)&temp))
    return (temp);
  BDD_TOP_VAR2(top_indexindex, bddm, f, g);
  BDD_COFACTOR(top_indexindex, f, f1, f2);
  BDD_COFACTOR(top_indexindex, g, g1, g2);
  temp=cmu_bdd_intersects_step(bddm, f1, g1);
  if (temp != BDD_ZERO(bddm))
    return (bdd_find(bddm, top_indexindex, temp, BDD_ZERO(bddm)));
  temp=bdd_find(bddm, top_indexindex, BDD_ZERO(bddm), cmu_bdd_intersects_step(bddm, f2, g2));
  if (temp == BDD_ZERO(bddm))
    bdd_insert_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)BDD_ZERO(bddm), (INT_PTR)temp);
  return (temp);
}

bdd cmu_bdd_ite	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	g,
		bdd	h
	)

Definition at line 487 of file bdd.c.

{
  if (bdd_check_arguments(3, f, g, h))
    {
      FIREWALL(bddm);
      RETURN_BDD(cmu_bdd_ite_step(bddm, f, g, h));
    }
  return ((bdd)0);
}

bdd cmu_bdd_ite_step	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	g,
		bdd	h
	)

Definition at line 383 of file bdd.c.

{
  int outneg;
  bdd_indexindex_type top_indexindex;
  bdd f1, f2;
  bdd g1, g2;
  bdd h1, h2;
  bdd temp1, temp2;
  bdd result;

  BDD_SETUP(f);
  BDD_SETUP(g);
  BDD_SETUP(h);
  if (BDD_IS_CONST(f))
    {
      if (f == BDD_ONE(bddm))
        {
          BDD_TEMP_INCREFS(g);
          return (g);
        }
      BDD_TEMP_INCREFS(h);
      return (h);
    }
  /* f is not constant. */
  if (BDD_SAME_OR_NEGATIONS(f, g))
    {
      if (f == g)
        g=BDD_ONE(bddm);
      else
        g=BDD_ZERO(bddm);
      BDD_RESET(g);
    }
  if (BDD_SAME_OR_NEGATIONS(f, h))
    {
      if (f == h)
        h=BDD_ZERO(bddm);
      else
        h=BDD_ONE(bddm);
      BDD_RESET(h);
    }
  if (BDD_IS_CONST(g))
    {
      if (BDD_IS_CONST(h))
        {
          if (g == h)
            return (g);
          BDD_TEMP_INCREFS(f);
          if (g == BDD_ONE(bddm))
            return (f);
          return (BDD_NOT(f));
        }
      if (g == BDD_ZERO(bddm))
        return (cmu_bdd_and_step(bddm, BDD_NOT(f), h));
      return (BDD_NOT(cmu_bdd_and_step(bddm, BDD_NOT(f), BDD_NOT(h))));
    }
  else if (BDD_SAME_OR_NEGATIONS(g, h))
    {
      if (g == h)
        {
          BDD_TEMP_INCREFS(g);
          return (g);
        }
      return (cmu_bdd_xnor_step(bddm, f, g));
    }
  else if (BDD_IS_CONST(h))
    {
    if (h == BDD_ZERO(bddm))
      return (cmu_bdd_and_step(bddm, f, g));
    else
      return (BDD_NOT(cmu_bdd_and_step(bddm, f, BDD_NOT(g))));
    }
  /* No special cases; it's a real if-then-else. */
  if (!BDD_IS_OUTPOS(f))
    {
      f=BDD_NOT(f);
      BDD_SWAP(g, h);
    }
  /* f is now an uncomplemented output pointer. */
  if (BDD_IS_OUTPOS(g))
    outneg=0;
  else
    {
      outneg=1;
      g=BDD_NOT(g);
      h=BDD_NOT(h);
    }
  /* g is now an uncomplemented output pointer. */
  if (bdd_lookup_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)h, (INT_PTR *)&result))
    return (outneg ? BDD_NOT(result) : result);
  BDD_TOP_VAR3(top_indexindex, bddm, f, g, h);
  BDD_COFACTOR(top_indexindex, f, f1, f2);
  BDD_COFACTOR(top_indexindex, g, g1, g2);
  BDD_COFACTOR(top_indexindex, h, h1, h2);
  temp1=cmu_bdd_ite_step(bddm, f1, g1, h1);
  temp2=cmu_bdd_ite_step(bddm, f2, g2, h2);
  result=bdd_find(bddm, top_indexindex, temp1, temp2);
  bdd_insert_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)h, (INT_PTR)result);
  return (outneg ? BDD_NOT(result) : result);
}

bdd cmu_bdd_nand	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	g
	)

Definition at line 510 of file bdd.c.

{
  bdd temp;

  if ((temp=cmu_bdd_and(bddm, f, g)))
    return (BDD_NOT(temp));
  return ((bdd)0);
}

bdd cmu_bdd_new_var_after	(	cmu_bdd_manager	bddm,
		bdd	var
	)

Definition at line 230 of file bdd.c.

{
  if (bdd_check_arguments(1, var))
    {
      BDD_SETUP(var);
      if (cmu_bdd_type_aux(bddm, var) != BDD_TYPE_POSVAR)
        {
          cmu_bdd_warning("cmu_bdd_new_var_after: argument is not a positive variable");
          if (BDD_IS_CONST(var))
            return (cmu_bdd_new_var_last(bddm));
        }
      return (bdd_new_var(bddm, BDD_INDEX(bddm, var)+1));
    }
  return ((bdd)0);
}

bdd cmu_bdd_new_var_before	(	cmu_bdd_manager	bddm,
		bdd	var
	)

Definition at line 209 of file bdd.c.

{
  if (bdd_check_arguments(1, var))
    {
      BDD_SETUP(var);
      if (cmu_bdd_type_aux(bddm, var) != BDD_TYPE_POSVAR)
        {
          cmu_bdd_warning("cmu_bdd_new_var_before: argument is not a positive variable");
          if (BDD_IS_CONST(var))
            return (cmu_bdd_new_var_last(bddm));
        }
      return (bdd_new_var(bddm, BDD_INDEX(bddm, var)));
    }
  return ((bdd)0);
}

bdd cmu_bdd_new_var_first

(

cmu_bdd_manager

bddm

)

Definition at line 189 of file bdd.c.

{
  return (bdd_new_var(bddm, (bdd_index_type)0));
}

bdd cmu_bdd_new_var_last

(

cmu_bdd_manager

bddm

)

Definition at line 199 of file bdd.c.

{
  return (bdd_new_var(bddm, (bdd_index_type)bddm->vars));
}

long cmu_bdd_node_limit	(	cmu_bdd_manager	bddm,
		long	new_limit
	)

Definition at line 881 of file bdd.c.

{
  long old_limit;

  old_limit=bddm->unique_table.node_limit;
  if (new_limit < 0)
    new_limit=0;
  bddm->unique_table.node_limit=new_limit;
  if (new_limit && bddm->unique_table.gc_limit > new_limit)
    bddm->unique_table.gc_limit=new_limit;
  return (old_limit);
}

bdd cmu_bdd_nor	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	g
	)

Definition at line 532 of file bdd.c.

{
  bdd temp;

  if ((temp=cmu_bdd_or(bddm, f, g)))
    return (BDD_NOT(temp));
  return ((bdd)0);
}

bdd cmu_bdd_not	(	cmu_bdd_manager	bddm,
		bdd	f
	)

Definition at line 582 of file bdd.c.

{
  if (bdd_check_arguments(1, f))
    {
      BDD_SETUP(f);
      BDD_INCREFS(f);
      return (BDD_NOT(f));
    }
  return ((bdd)0);
}

bdd cmu_bdd_one

(

cmu_bdd_manager

bddm

)

Definition at line 10 of file bdd.c.

{
  return (BDD_ONE(bddm));
}

bdd cmu_bdd_or	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	g
	)

Definition at line 523 of file bdd.c.

{
  return (cmu_bdd_ite(bddm, f, BDD_ONE(bddm), g));
}

int cmu_bdd_overflow

(

cmu_bdd_manager

bddm

)

Definition at line 899 of file bdd.c.

{
  int result;

  result=bddm->overflow;
  bddm->overflow=0;
  return (result);
}

void cmu_bdd_overflow_closure	(	cmu_bdd_manager	bddm,
		void(*)(cmu_bdd_manager, pointer)	overflow_fn,
		pointer	overflow_env
	)

Definition at line 914 of file bdd.c.

{
  bddm->overflow_fn=overflow_fn;
  bddm->overflow_env=overflow_env;
}

void cmu_bdd_quit

(

cmu_bdd_manager

bddm

)

Definition at line 1076 of file bdd.c.

{
  int i;
  assoc_list p, q;

  cmu_bdd_free_unique(bddm);
  cmu_bdd_free_cache(bddm);
  mem_free_block((pointer)bddm->variables);
  mem_free_block((pointer)bddm->indexes);
  mem_free_block((pointer)bddm->indexindexes);
  mem_free_block((pointer)bddm->temp_assoc.assoc);
  for (p=bddm->assocs; p; p=q)
    {
      q=p->next;
      mem_free_block((pointer)p->va.assoc);
      BDD_FREE_REC(bddm, (pointer)p, sizeof(struct assoc_list_));
    }
  BDD_FREE_REC(bddm, (pointer)bddm->super_block, sizeof(struct block_));
  for (i=0; i < REC_MGRS; ++i)
    mem_free_rec_mgr(bddm->rms[i]);
  mem_free_block((pointer)bddm);
}

void cmu_bdd_stats	(	cmu_bdd_manager	bddm,
		FILE *	fp
	)

Definition at line 939 of file bdd.c.

{
  long i;
  long ue, ce, cs, mem;
  SIZE_T alloc;
  assoc_list q;

  ue=bddm->unique_table.entries;
  ce=bddm->op_cache.entries;
  cs=bddm->op_cache.size;
  mem=0;
  for (i=0; i < bddm->vars; ++i)
    {
      mem+=sizeof(struct var_table_);
      mem+=bddm->unique_table.tables[i]->size*sizeof(bdd);
    }
  mem=ue*sizeof(struct bdd_);
  mem+=cs*sizeof(struct cache_bin_)+ce*sizeof(struct cache_entry_);
  mem+=bddm->maxvars*(sizeof(bdd_index_type)+sizeof(bdd_indexindex_type)+sizeof(bdd)+sizeof(var_table));
  for (q=bddm->assocs, i=1; q; q=q->next, ++i);
  mem+=i*bddm->maxvars*sizeof(bdd);
  if ((alloc=mem_allocation()))
    /* mem_allocation may be meaningless depending on mem library. */
    fprintf(fp, "Memory manager bytes allocated: %ld\n", (long)alloc);
  fprintf(fp, "Approximate bytes used: %ld\n", mem);
  fprintf(fp, "Number of nodes: %ld\n", ue);
  if (bddm->unique_table.node_limit)
    fprintf(fp, "Node limit: %ld\n", bddm->unique_table.node_limit);
  else
    fprintf(fp, "Node limit: ---\n");
  fprintf(fp, "Overflow: %s\n", bddm->overflow ? "yes" : "no");
  fprintf(fp, "Approximate bytes per node: %-.2f\n", ((double)mem)/ue);
  fprintf(fp, "Cache entries: %ld\n", ce);
  fprintf(fp, "Cache size: %ld\n", 2*cs);
  fprintf(fp, "Cache load factor: %-.2f\n", ((double)ce)/(2*cs));
  fprintf(fp, "Cache look ups: %ld\n", bddm->op_cache.lookups);
  fprintf(fp, "Cache hits: %ld\n", bddm->op_cache.hits);
  if (bddm->op_cache.lookups)
    fprintf(fp, "Cache hit rate: %-.2f\n", ((double)(bddm->op_cache.hits))/bddm->op_cache.lookups);
  else
    fprintf(fp, "Cache hit rate: ---\n");
  fprintf(fp, "Cache insertions: %ld\n", bddm->op_cache.inserts);
  fprintf(fp, "Cache collisions: %ld\n", bddm->op_cache.collisions);
  fprintf(fp, "Number of variables: %ld\n", bddm->vars);
  fprintf(fp, "Number of variable associations: %ld\n", i);
  fprintf(fp, "Number of garbage collections: %ld\n", bddm->unique_table.gcs);
  fprintf(fp, "Number of nodes garbage collected: %ld\n", bddm->unique_table.freed);
  fprintf(fp, "Number of find operations: %ld\n", bddm->unique_table.finds);
}

bdd cmu_bdd_then	(	cmu_bdd_manager	bddm,
		bdd	f
	)

Definition at line 651 of file bdd.c.

{
  if (bdd_check_arguments(1, f))
    {
      BDD_SETUP(f);
      if (BDD_IS_CONST(f))
        {
          cmu_bdd_warning("cmu_bdd_then: argument is a constant");
          return (f);
        }
      f=BDD_THEN(f);
      BDD_RESET(f);
      BDD_INCREFS(f);
    }
  return (f);
}

long cmu_bdd_total_size

(

cmu_bdd_manager

bddm

)

Definition at line 853 of file bdd.c.

{
  return (bddm->unique_table.entries);
}

int cmu_bdd_type	(	cmu_bdd_manager	bddm,
		bdd	f
	)

Definition at line 804 of file bdd.c.

{
  if (bdd_check_arguments(1, f))
    return (cmu_bdd_type_aux(bddm, f));
  return (BDD_TYPE_OVERFLOW);
}

int cmu_bdd_type_aux	(	cmu_bdd_manager	bddm,
		bdd	f
	)

Definition at line 778 of file bdd.c.

{
  BDD_SETUP(f);
  if (BDD_IS_CONST(f))
    {
      if (f == BDD_ZERO(bddm))
        return (BDD_TYPE_ZERO);
      if (f == BDD_ONE(bddm))
        return (BDD_TYPE_ONE);
      return (BDD_TYPE_CONSTANT);
    }
  if (BDD_THEN(f) == BDD_ONE(bddm) && BDD_ELSE(f) == BDD_ZERO(bddm))
    return (BDD_TYPE_POSVAR);
  if (BDD_THEN(f) == BDD_ZERO(bddm) && BDD_ELSE(f) == BDD_ONE(bddm))
    return (BDD_TYPE_NEGVAR);
  return (BDD_TYPE_NONTERMINAL);
}

void cmu_bdd_unfree	(	cmu_bdd_manager	bddm,
		bdd	f
	)

Definition at line 815 of file bdd.c.

{
  if (f)
    {
      BDD_SETUP(f);
      BDD_INCREFS(f);
    }
}

bdd cmu_bdd_var_with_id	(	cmu_bdd_manager	bddm,
		long	indexindex
	)

Definition at line 263 of file bdd.c.

{
  if (indexindex <= 0 || indexindex > bddm->vars)
    return ((bdd)0);
  return (bddm->variables[indexindex]);
}

bdd cmu_bdd_var_with_index	(	cmu_bdd_manager	bddm,
		long	index
	)

Definition at line 251 of file bdd.c.

{
  if (index < 0 || index >= bddm->vars)
    return ((bdd)0);
  return (bddm->variables[bddm->indexindexes[index]]);
}

long cmu_bdd_vars

(

cmu_bdd_manager

bddm

)

Definition at line 844 of file bdd.c.

{
  return (bddm->vars);
}

bdd cmu_bdd_xnor	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	g
	)

Definition at line 554 of file bdd.c.

{
  bdd temp;

  if ((temp=cmu_bdd_xor(bddm, f, g)))
    return (BDD_NOT(temp));
  return ((bdd)0);
}

static bdd cmu_bdd_xnor_step	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	g
	)			[static]

Definition at line 326 of file bdd.c.

{
  int outneg;
  bdd_indexindex_type top_indexindex;
  bdd f1, f2;
  bdd g1, g2;
  bdd temp1, temp2;
  bdd result;

  BDD_SETUP(f);
  BDD_SETUP(g);
  if (BDD_IS_CONST(f))
    {
      BDD_TEMP_INCREFS(g);
      if (f == BDD_ONE(bddm))
        return (g);
      return (BDD_NOT(g));
    }
  if (BDD_IS_CONST(g))
    {
      BDD_TEMP_INCREFS(f);
      if (g == BDD_ONE(bddm))
        return (f);
      return (BDD_NOT(f));
    }
  /* f and g are not constant. */
  if (BDD_SAME_OR_NEGATIONS(f, g))
    {
      if (f == g)
        return (BDD_ONE(bddm));
      return (BDD_ZERO(bddm));
    }
  /* f and g are not constant, not same, not negations. */
  if (BDD_OUT_OF_ORDER(f, g))
    BDD_SWAP(f, g);
  if (BDD_IS_OUTPOS(g))
    outneg=0;
  else
    {
      outneg=1;
      g=BDD_NOT(g);
    }
  /* g is an uncomplemented output pointer. */
  if (bdd_lookup_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)BDD_NOT(g), (INT_PTR *)&result))
    return (outneg ? BDD_NOT(result) : result);
  BDD_TOP_VAR2(top_indexindex, bddm, f, g);
  BDD_COFACTOR(top_indexindex, f, f1, f2);
  BDD_COFACTOR(top_indexindex, g, g1, g2);
  temp1=cmu_bdd_xnor_step(bddm, f1, g1);
  temp2=cmu_bdd_xnor_step(bddm, f2, g2);
  result=bdd_find(bddm, top_indexindex, temp1, temp2);
  bdd_insert_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)BDD_NOT(g), (INT_PTR)result);
  return (outneg ? BDD_NOT(result) : result);
}

bdd cmu_bdd_xor	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	g
	)

Definition at line 545 of file bdd.c.

{
  return (cmu_bdd_ite(bddm, f, BDD_NOT(g), g));
}

bdd cmu_bdd_zero

(

cmu_bdd_manager

bddm

)

Definition at line 19 of file bdd.c.

{
  return (BDD_ZERO(bddm));
}

static block shift_block	(	cmu_bdd_manager	bddm,
		block	b,
		long	index
	)			[static]

Definition at line 70 of file bdd.c.

{
  long i, j;
  block p;

  if (b->first_index >= index)
    {
      bdd_block_delta(b, 1l);
      return (b);
    }
  if (b->last_index < index)
    return (b);
  b->last_index++;
  i=bdd_find_block(b, index);
  if (i == b->num_children || b->children[i]->first_index == index)
    {
      b->children=(block *)mem_resize_block((pointer)b->children, (SIZE_T)(sizeof(block)*(b->num_children+1)));
      for (j=b->num_children-1; j >= i; --j)
        b->children[j+1]=shift_block(bddm, b->children[j], index);
      b->num_children++;
      p=(block)BDD_NEW_REC(bddm, sizeof(struct block_));
      p->reorderable=0;
      p->first_index=index;
      p->last_index=index;
      p->num_children=0;
      p->children=0;
      b->children[i]=p;
    }
  else
    while (i < b->num_children)
      {
        shift_block(bddm, b->children[i], index);
        ++i;
      }
  return (b);
}