src/cmuBdd/bddint.h File Reference

#include <setjmp.h>
#include "bdduser.h"

Include dependency graph for bddint.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Data Structures
struct	bdd_
struct	cache_entry_
struct	var_assoc_
struct	assoc_list_
struct	block_
struct	cache_bin_
struct	cache_
struct	var_table_
struct	unique_
struct	jump_buf_
struct	bdd_manager_
struct	hash_rec_
struct	hash_table_
Defines
#define	_BDDINTH
#define	BROKEN_CPP
#define	ARGS(args)   args
#define	POINTER(p)   ((pointer)(((INT_PTR)(p)) & ~(INT_PTR)0x7))
#define	BDD_POINTER(p)   ((bdd)POINTER(p))
#define	CACHE_POINTER(p)   ((cache_entry)POINTER(p))
#define	TAG(p)   ((int)(((INT_PTR)(p)) & 0x7))
#define	SET_TAG(p, t)   ((pointer)((INT_PTR)POINTER(p) | (t)))
#define	TAG0(p)   ((int)((INT_PTR)(p) & 0x1))
#define	FLIP_TAG0(p)   ((pointer)((INT_PTR)(p) ^ 0x1))
#define	TAG0_HI(p)   ((pointer)((INT_PTR)(p) | 0x1))
#define	TAG0_LO(p)   ((pointer)((INT_PTR)(p) & ~(INT_PTR)0x1))
#define	TAG1(p)   ((int)((INT_PTR)(p) & 0x2))
#define	FLIP_TAG1(p)   ((pointer)((INT_PTR)(p) ^ 0x2))
#define	TAG1_HI(p)   ((pointer)((INT_PTR)(p) | 0x2))
#define	TAG1_LO(p)   ((pointer)((INT_PTR)(p) & ~(INT_PTR)0x2))
#define	TAG2(p)   ((int)((INT_PTR)(p) & 0x4))
#define	FLIP_TAG2(p)   ((pointer)((INT_PTR)(p) ^ 0x4))
#define	TAG2_HI(p)   ((pointer)((INT_PTR)(p) | 0x4))
#define	TAG2_LO(p)   ((pointer)((INT_PTR)(p) & ~(INT_PTR)0x4))
#define	BDD_MAX_REFS   ((bdd_refcount_type)((1l << (8*sizeof(bdd_refcount_type))) - 1))
#define	BDD_MAX_TEMP_REFS   ((bdd_mark_type)((1l << (8*sizeof(bdd_mark_type)-1)) - 1))
#define	BDD_GC_MARK   ((bdd_mark_type)(1l << (8*sizeof(bdd_mark_type)-1)))
#define	BDD_CONST_INDEXINDEX   0
#define	BDD_MAX_INDEXINDEX   ((bdd_indexindex_type)((1l << (8*sizeof(bdd_indexindex_type))) - 1))
#define	BDD_MAX_INDEX   ((bdd_index_type)((1l << (8*sizeof(bdd_index_type))) - 1))
#define	CONCAT_PTR(f)   f##_ptr
#define	BDD_SETUP(f)   bdd CONCAT_PTR(f)=BDD_POINTER(f)
#define	BDD_RESET(f)   CONCAT_PTR(f)=BDD_POINTER(f)
#define	BDD_INDEXINDEX(f)   (CONCAT_PTR(f)->indexindex)
#define	BDD_DATA(f)   (CONCAT_PTR(f)->data)
#define	BDD_DATA0(f)   (CONCAT_PTR(f)->data[0])
#define	BDD_DATA1(f)   (CONCAT_PTR(f)->data[1])
#define	BDD_REFS(f)   (CONCAT_PTR(f)->refs)
#define	BDD_MARK(f)   (CONCAT_PTR(f)->mark)
#define	BDD_TEMP_REFS(f)   (CONCAT_PTR(f)->mark)
#define	BDD_INDEX(bddm, f)   ((bddm)->indexes[BDD_INDEXINDEX(f)])
#define	BDD_THEN(f)   ((bdd)(BDD_DATA0(f) ^ TAG0(f)))
#define	BDD_ELSE(f)   ((bdd)(BDD_DATA1(f) ^ TAG0(f)))
#define	BDD_SAME_OR_NEGATIONS(f, g)   (CONCAT_PTR(f) == CONCAT_PTR(g))
#define	BDD_IS_CONST(f)   (BDD_INDEXINDEX(f) == BDD_CONST_INDEXINDEX)
#define	BDD_IS_OUTPOS(f)   (!TAG0(f))
#define	BDD_OUTPOS(f)   ((bdd)TAG0_LO(f))
#define	BDD_NOT(f)   ((bdd)FLIP_TAG0(f))
#define	BDD_TOP_VAR2(top_indexindex, bddm, f, g)
#define	BDD_TOP_VAR3(top_indexindex, bddm, f, g, h)
#define	BDD_COFACTOR(top_indexindex, f, f_then, f_else)
#define	BDD_OUT_OF_ORDER(f, g)   ((INT_PTR)f > (INT_PTR)g)
#define	BDD_SWAP(f, g)
#define	BDD_IF(bddm, f)   ((bddm)->variables[BDD_INDEXINDEX(f)])
#define	BDD_INCREFS(f)
#define	BDD_DECREFS(f)
#define	BDD_TEMP_INCREFS(f)
#define	BDD_TEMP_DECREFS(f)
#define	BDD_IS_USED(f)   ((BDD_MARK(f) & BDD_GC_MARK) != 0)
#define	RETURN_BDD(thing)   return (bdd_make_external(thing))
#define	BDD_ONE(bddm)   ((bddm)->one)
#define	BDD_ZERO(bddm)   ((bddm)->zero)
#define	CACHE_TYPE_ITE   0x0
#define	CACHE_TYPE_TWO   0x1
#define	CACHE_TYPE_ONEDATA   0x2
#define	CACHE_TYPE_TWODATA   0x3
#define	CACHE_TYPE_USER1   0x4
#define	USER_ENTRY_TYPES   4
#define	OP_COFACTOR   100l
#define	OP_SATFRAC   200l
#define	OP_FWD   300l
#define	OP_REV   400l
#define	OP_RED   500l
#define	OP_EQUAL   600l
#define	OP_QNT   10000l
#define	OP_RELPROD   20000l
#define	OP_SUBST   30000l
#define	OP_COMP   100000l
#define	OP_CMPTO   200000l
#define	OP_SWAP   300000l
#define	OP_SWAPAUX   400000l
#define	MIN_REC_SIZE   ALLOC_ALIGNMENT
#define	MAX_REC_SIZE   64
#define	REC_MGRS   (((MAX_REC_SIZE-MIN_REC_SIZE)/ALLOC_ALIGNMENT)+1)
#define	BDD_ABORTED   1
#define	BDD_OVERFLOWED   2
#define	BDD_REORDERED   3
#define	FIREWALL(bddm)
#define	FIREWALL1(bddm, cleanupcode)
#define	HASH_NODE(f, g)   (((f) << 1)+(g))
#define	TABLE_SIZE(size_index)   (bdd_primes[size_index])
#define	BDD_REDUCE(i, size)
#define	BDD_NEW_REC(bddm, size)   mem_new_rec((bddm)->rms[(ROUNDUP(size)-MIN_REC_SIZE)/ALLOC_ALIGNMENT])
#define	BDD_FREE_REC(bddm, rec, size)   mem_free_rec((bddm)->rms[(ROUNDUP(size)-MIN_REC_SIZE)/ALLOC_ALIGNMENT], (rec))
#define	bdd_insert_in_cache2(bddm, op, f, g, result)   bdd_insert_in_cache31((bddm), CACHE_TYPE_TWO, (INT_PTR)(op), (INT_PTR)(f), (INT_PTR)(g), (INT_PTR)(result))
#define	bdd_lookup_in_cache2(bddm, op, f, g, result)   bdd_lookup_in_cache31((bddm), CACHE_TYPE_TWO, (INT_PTR)(op), (INT_PTR)(f), (INT_PTR)(g), (INT_PTR *)(result))
#define	bdd_insert_in_cache1(bddm, op, f, result)   bdd_insert_in_cache2((bddm), (op), (f), BDD_ONE(bddm), (result))
#define	bdd_lookup_in_cache1(bddm, op, f, result)   bdd_lookup_in_cache2((bddm), (op), (f), BDD_ONE(bddm), (result))
#define	bdd_insert_in_cache2d(bddm, op, f, g, result)   bdd_insert_in_cache31((bddm), CACHE_TYPE_TWODATA, (INT_PTR)(op), (INT_PTR)(f), (INT_PTR)(g), (INT_PTR)(result))
#define	bdd_lookup_in_cache2d(bddm, op, f, g, result)   bdd_lookup_in_cache31((bddm), CACHE_TYPE_TWODATA, (INT_PTR)(op), (INT_PTR)(f), (INT_PTR)(g), (INT_PTR *)(result))
#define	bdd_insert_in_cache1d(bddm, op, f, result1, result2)   bdd_insert_in_cache22((bddm), CACHE_TYPE_ONEDATA, (INT_PTR)(op), (INT_PTR)(f), (INT_PTR)(result1), (INT_PTR)(result2))
#define	bdd_lookup_in_cache1d(bddm, op, f, result1, result2)   bdd_lookup_in_cache22((bddm), CACHE_TYPE_ONEDATA, (INT_PTR)(op), (INT_PTR)(f), (INT_PTR *)(result1), (INT_PTR *)(result2))
#define	cache_return_fn_none   ((void (*)(cmu_bdd_manager, cache_entry))0)
#define	cache_purge_fn_none   ((void (*)(cmu_bdd_manager, cache_entry))0)
#define	cache_reclaim_fn_none   ((int (*)(cmu_bdd_manager, cache_entry, pointer))0)
Typedefs
typedef struct hash_table_ *	hash_table
typedef unsigned short	bdd_index_type
typedef unsigned short	bdd_indexindex_type
typedef unsigned char	bdd_refcount_type
typedef unsigned char	bdd_mark_type
typedef struct cache_entry_ *	cache_entry
typedef struct var_assoc_ *	var_assoc
typedef struct assoc_list_ *	assoc_list
typedef struct cache_bin_	cache_bin
typedef struct cache_	cache
typedef struct var_table_ *	var_table
typedef struct unique_	unique
typedef struct jump_buf_	jump_buf
typedef struct hash_rec_ *	hash_rec
Functions
int bdd_check_arguments	ARGS ((int,...))
void bdd_check_array	ARGS ((bdd *))
bdd bdd_make_external	ARGS ((bdd))
int cmu_bdd_type_aux	ARGS ((cmu_bdd_manager, bdd))
void bdd_rehash_var_table	ARGS ((var_table, int))
bdd bdd_find_aux	ARGS ((cmu_bdd_manager, bdd_indexindex_type, INT_PTR, INT_PTR))
bdd cmu_bdd_ite_step	ARGS ((cmu_bdd_manager, bdd, bdd, bdd))
bdd cmu_bdd_exists_temp	ARGS ((cmu_bdd_manager, bdd, long))
bdd cmu_bdd_substitute_step	ARGS ((cmu_bdd_manager, bdd, long, bdd(*) ARGS((cmu_bdd_manager, bdd, bdd, bdd)), var_assoc))
void bdd_number_shared_nodes	ARGS ((cmu_bdd_manager, bdd, hash_table, long *))
char *bdd_terminal_id	ARGS ((cmu_bdd_manager, bdd, char *(*) ARGS((cmu_bdd_manager, INT_PTR, INT_PTR, pointer)), pointer))
char *bdd_var_name	ARGS ((cmu_bdd_manager, bdd, char *(*) ARGS((cmu_bdd_manager, bdd, pointer)), pointer))
long bdd_find_block	ARGS ((block, long))
void cmu_bdd_reorder_aux	ARGS ((cmu_bdd_manager))
void cmu_mtbdd_terminal_value_aux	ARGS ((cmu_bdd_manager, bdd, INT_PTR *, INT_PTR *))
void bdd_insert_in_cache31	ARGS ((cmu_bdd_manager, int, INT_PTR, INT_PTR, INT_PTR, INT_PTR))
int bdd_lookup_in_cache31	ARGS ((cmu_bdd_manager, int, INT_PTR, INT_PTR, INT_PTR, INT_PTR *))
int bdd_lookup_in_cache22	ARGS ((cmu_bdd_manager, int, INT_PTR, INT_PTR, INT_PTR *, INT_PTR *))
int bdd_lookup_in_cache13	ARGS ((cmu_bdd_manager, int, INT_PTR, INT_PTR *, INT_PTR *, INT_PTR *))
void bdd_flush_cache	ARGS ((cmu_bdd_manager, int(*) ARGS((cmu_bdd_manager, cache_entry, pointer)), pointer))
int bdd_cache_functions	ARGS ((cmu_bdd_manager, int, int(*) ARGS((cmu_bdd_manager, cache_entry)), void(*) ARGS((cmu_bdd_manager, cache_entry)), void(*) ARGS((cmu_bdd_manager, cache_entry)), int(*) ARGS((cmu_bdd_manager, cache_entry, pointer))))
void cmu_bdd_free_cache_tag	ARGS ((cmu_bdd_manager, long))
void bdd_rehash_cache	ARGS ((cmu_bdd_manager, int))
void bdd_sweep_var_table	ARGS ((cmu_bdd_manager, long, int))
bdd bdd_find	ARGS ((cmu_bdd_manager, bdd_indexindex_type, bdd, bdd))
bdd bdd_find_terminal	ARGS ((cmu_bdd_manager, INT_PTR, INT_PTR))
void cmu_bdd_fatal	ARGS ((char *))
void bdd_insert_in_hash_table	ARGS ((hash_table, bdd, pointer))
pointer bdd_lookup_in_hash_table	ARGS ((hash_table, bdd))
void cmu_bdd_free_hash_table	ARGS ((hash_table))
Variables
long	bdd_primes []

---

Define Documentation

#define _BDDINTH

Definition at line 5 of file bddint.h.

#define ARGS

(

args

)

args

Definition at line 35 of file bddint.h.

#define BDD_ABORTED   1

Definition at line 527 of file bddint.h.

#define BDD_COFACTOR	(	top_indexindex,
		f,
		f_then,
		f_else		)

Value:

do\
  if (BDD_INDEXINDEX(f) == top_indexindex)\
    {\
      f_then=BDD_THEN(f);\
      f_else=BDD_ELSE(f);\
    }\
  else\
    {\
      f_then=f;\
      f_else=f;\
    }\
while (0)

Definition at line 198 of file bddint.h.

#define BDD_CONST_INDEXINDEX   0

Definition at line 111 of file bddint.h.

#define BDD_DATA

(

f

)

(CONCAT_PTR(f)->data)

Definition at line 126 of file bddint.h.

#define BDD_DATA0

(

f

)

(CONCAT_PTR(f)->data[0])

Definition at line 127 of file bddint.h.

#define BDD_DATA1

(

f

)

(CONCAT_PTR(f)->data[1])

Definition at line 128 of file bddint.h.

#define BDD_DECREFS

(

f

)

Value:

do\
  {\
    if (BDD_REFS(f) < BDD_MAX_REFS)\
      BDD_REFS(f)--;\
  }\
while (0)

Definition at line 263 of file bddint.h.

#define BDD_ELSE

(

f

)

((bdd)(BDD_DATA1(f) ^ TAG0(f)))

Definition at line 138 of file bddint.h.

#define BDD_FREE_REC	(	bddm,
		rec,
		size		)	mem_free_rec((bddm)->rms[(ROUNDUP(size)-MIN_REC_SIZE)/ALLOC_ALIGNMENT], (rec))

Definition at line 591 of file bddint.h.

#define BDD_GC_MARK   ((bdd_mark_type)(1l << (8*sizeof(bdd_mark_type)-1)))

Definition at line 106 of file bddint.h.

#define BDD_IF	(	bddm,
		f		)	((bddm)->variables[BDD_INDEXINDEX(f)])

Definition at line 245 of file bddint.h.

#define BDD_INCREFS

(

f

)

Value:

do\
  {\
    if (BDD_REFS(f) >= BDD_MAX_REFS-1)\
      {\
        BDD_REFS(f)=BDD_MAX_REFS;\
        BDD_TEMP_REFS(f)=0;\
      }\
   else\
     BDD_REFS(f)++;\
  }\
while (0)

Definition at line 250 of file bddint.h.

#define BDD_INDEX	(	bddm,
		f		)	((bddm)->indexes[BDD_INDEXINDEX(f)])

Definition at line 136 of file bddint.h.

#define BDD_INDEXINDEX

(

f

)

(CONCAT_PTR(f)->indexindex)

Definition at line 125 of file bddint.h.

#define bdd_insert_in_cache1	(	bddm,
		op,
		f,
		result		)	bdd_insert_in_cache2((bddm), (op), (f), BDD_ONE(bddm), (result))

Definition at line 649 of file bddint.h.

#define bdd_insert_in_cache1d	(	bddm,
		op,
		f,
		result1,
		result2		)	bdd_insert_in_cache22((bddm), CACHE_TYPE_ONEDATA, (INT_PTR)(op), (INT_PTR)(f), (INT_PTR)(result1), (INT_PTR)(result2))

Definition at line 659 of file bddint.h.

#define bdd_insert_in_cache2	(	bddm,
		op,
		f,
		g,
		result		)	bdd_insert_in_cache31((bddm), CACHE_TYPE_TWO, (INT_PTR)(op), (INT_PTR)(f), (INT_PTR)(g), (INT_PTR)(result))

Definition at line 644 of file bddint.h.

#define bdd_insert_in_cache2d	(	bddm,
		op,
		f,
		g,
		result		)	bdd_insert_in_cache31((bddm), CACHE_TYPE_TWODATA, (INT_PTR)(op), (INT_PTR)(f), (INT_PTR)(g), (INT_PTR)(result))

Definition at line 654 of file bddint.h.

#define BDD_IS_CONST

(

f

)

(BDD_INDEXINDEX(f) == BDD_CONST_INDEXINDEX)

Definition at line 140 of file bddint.h.

#define BDD_IS_OUTPOS

(

f

)

(!TAG0(f))

Definition at line 167 of file bddint.h.

#define BDD_IS_USED

(

f

)

((BDD_MARK(f) & BDD_GC_MARK) != 0)

Definition at line 294 of file bddint.h.

#define bdd_lookup_in_cache1	(	bddm,
		op,
		f,
		result		)	bdd_lookup_in_cache2((bddm), (op), (f), BDD_ONE(bddm), (result))

Definition at line 651 of file bddint.h.

#define bdd_lookup_in_cache1d	(	bddm,
		op,
		f,
		result1,
		result2		)	bdd_lookup_in_cache22((bddm), CACHE_TYPE_ONEDATA, (INT_PTR)(op), (INT_PTR)(f), (INT_PTR *)(result1), (INT_PTR *)(result2))

Definition at line 661 of file bddint.h.

#define bdd_lookup_in_cache2	(	bddm,
		op,
		f,
		g,
		result		)	bdd_lookup_in_cache31((bddm), CACHE_TYPE_TWO, (INT_PTR)(op), (INT_PTR)(f), (INT_PTR)(g), (INT_PTR *)(result))

Definition at line 646 of file bddint.h.

#define bdd_lookup_in_cache2d	(	bddm,
		op,
		f,
		g,
		result		)	bdd_lookup_in_cache31((bddm), CACHE_TYPE_TWODATA, (INT_PTR)(op), (INT_PTR)(f), (INT_PTR)(g), (INT_PTR *)(result))

Definition at line 656 of file bddint.h.

#define BDD_MARK

(

f

)

(CONCAT_PTR(f)->mark)

Definition at line 130 of file bddint.h.

#define BDD_MAX_INDEX   ((bdd_index_type)((1l << (8*sizeof(bdd_index_type))) - 1))

Definition at line 113 of file bddint.h.

#define BDD_MAX_INDEXINDEX   ((bdd_indexindex_type)((1l << (8*sizeof(bdd_indexindex_type))) - 1))

Definition at line 112 of file bddint.h.

#define BDD_MAX_REFS   ((bdd_refcount_type)((1l << (8*sizeof(bdd_refcount_type))) - 1))

Definition at line 103 of file bddint.h.

#define BDD_MAX_TEMP_REFS   ((bdd_mark_type)((1l << (8*sizeof(bdd_mark_type)-1)) - 1))

Definition at line 104 of file bddint.h.

#define BDD_NEW_REC	(	bddm,
		size		)	mem_new_rec((bddm)->rms[(ROUNDUP(size)-MIN_REC_SIZE)/ALLOC_ALIGNMENT])

Definition at line 590 of file bddint.h.

#define BDD_NOT

(

f

)

((bdd)FLIP_TAG0(f))

Definition at line 169 of file bddint.h.

#define BDD_ONE

(

bddm

)

((bddm)->one)

Definition at line 305 of file bddint.h.

#define BDD_OUT_OF_ORDER	(	f,
		g		)	((INT_PTR)f > (INT_PTR)g)

Definition at line 215 of file bddint.h.

#define BDD_OUTPOS

(

f

)

((bdd)TAG0_LO(f))

Definition at line 168 of file bddint.h.

#define BDD_OVERFLOWED   2

Definition at line 528 of file bddint.h.

#define BDD_POINTER

(

p

)

((bdd)POINTER(p))

Definition at line 53 of file bddint.h.

#define BDD_REDUCE	(	i,
		size		)

Value:

do\
  {\
    (i)%=(size);\
    if ((i) < 0)\
      (i)= -(i);\
  }\
while (0)

Definition at line 577 of file bddint.h.

#define BDD_REFS

(

f

)

(CONCAT_PTR(f)->refs)

Definition at line 129 of file bddint.h.

#define BDD_REORDERED   3

Definition at line 529 of file bddint.h.

#define BDD_RESET

(

f

)

CONCAT_PTR(f)=BDD_POINTER(f)

Definition at line 124 of file bddint.h.

#define BDD_SAME_OR_NEGATIONS	(	f,
		g		)	(CONCAT_PTR(f) == CONCAT_PTR(g))

Definition at line 139 of file bddint.h.

#define BDD_SETUP

(

f

)

bdd CONCAT_PTR(f)=BDD_POINTER(f)

Definition at line 123 of file bddint.h.

#define BDD_SWAP	(	f,
		g		)

Value:

do\
  {\
    bdd _temp;\
    _temp=f;\
    f=g;\
    g=_temp;\
    _temp=CONCAT_PTR(f);\
    CONCAT_PTR(f)=CONCAT_PTR(g);\
    CONCAT_PTR(g)=_temp;\
  }\
while (0)

Definition at line 218 of file bddint.h.

#define BDD_TEMP_DECREFS

(

f

)

Value:

do\
  {\
    if (BDD_REFS(f) < BDD_MAX_REFS)\
      BDD_TEMP_REFS(f)--;\
  }\
while (0)

Definition at line 286 of file bddint.h.

#define BDD_TEMP_INCREFS

(

f

)

Value:

do\
  {\
    if (BDD_REFS(f) < BDD_MAX_REFS)\
      {\
        BDD_TEMP_REFS(f)++;\
        if (BDD_TEMP_REFS(f) == BDD_MAX_TEMP_REFS)\
          {\
            BDD_REFS(f)=BDD_MAX_REFS;\
            BDD_TEMP_REFS(f)=0;\
          }\
      }\
  }\
while (0)

Definition at line 271 of file bddint.h.

#define BDD_TEMP_REFS

(

f

)

(CONCAT_PTR(f)->mark)

Definition at line 131 of file bddint.h.

#define BDD_THEN

(

f

)

((bdd)(BDD_DATA0(f) ^ TAG0(f)))

Definition at line 137 of file bddint.h.

#define BDD_TOP_VAR2	(	top_indexindex,
		bddm,
		f,
		g		)

Value:

do\
  if (BDD_INDEX(bddm, f) < BDD_INDEX(bddm, g))\
    top_indexindex=BDD_INDEXINDEX(f);\
  else\
    top_indexindex=BDD_INDEXINDEX(g);\
while (0)

Definition at line 174 of file bddint.h.

#define BDD_TOP_VAR3	(	top_indexindex,
		bddm,
		f,
		g,
		h		)

Value:

do\
  if (BDD_INDEX(bddm, f) < BDD_INDEX(bddm, g))\
    {\
      top_indexindex=BDD_INDEXINDEX(f);\
      if ((bddm)->indexes[top_indexindex] > BDD_INDEX(bddm, h))\
        top_indexindex=BDD_INDEXINDEX(h);\
    }\
  else\
    {\
      top_indexindex=BDD_INDEXINDEX(g);\
      if ((bddm)->indexes[top_indexindex] > BDD_INDEX(bddm, h))\
        top_indexindex=BDD_INDEXINDEX(h);\
    }\
while (0)

Definition at line 182 of file bddint.h.

#define BDD_ZERO

(

bddm

)

((bddm)->zero)

Definition at line 306 of file bddint.h.

#define BROKEN_CPP

Definition at line 26 of file bddint.h.

#define CACHE_POINTER

(

p

)

((cache_entry)POINTER(p))

Definition at line 54 of file bddint.h.

#define cache_purge_fn_none   ((void (*)(cmu_bdd_manager, cache_entry))0)

Definition at line 665 of file bddint.h.

#define cache_reclaim_fn_none   ((int (*)(cmu_bdd_manager, cache_entry, pointer))0)

Definition at line 666 of file bddint.h.

#define cache_return_fn_none   ((void (*)(cmu_bdd_manager, cache_entry))0)

Definition at line 664 of file bddint.h.

#define CACHE_TYPE_ITE   0x0

Definition at line 325 of file bddint.h.

#define CACHE_TYPE_ONEDATA   0x2

Definition at line 327 of file bddint.h.

#define CACHE_TYPE_TWO   0x1

Definition at line 326 of file bddint.h.

#define CACHE_TYPE_TWODATA   0x3

Definition at line 328 of file bddint.h.

#define CACHE_TYPE_USER1   0x4

Definition at line 329 of file bddint.h.

#define CONCAT_PTR

(

f

)

f##_ptr

Definition at line 118 of file bddint.h.

#define FIREWALL

(

bddm

)

Value:

do\
  {\
    int retcode;\
    (bddm)->allow_reordering=1;\
    (bddm)->nodes_at_start=(bddm)->unique_table.entries;\
    while ((retcode=(setjmp((bddm)->abort.context))))\
      {\
        bdd_cleanup(bddm, retcode);\
        if (retcode == BDD_ABORTED || retcode == BDD_OVERFLOWED)\
          return ((bdd)0);\
        (bddm)->nodes_at_start=(bddm)->unique_table.entries;\
      }\
  }\
while (0)

Definition at line 532 of file bddint.h.

#define FIREWALL1	(	bddm,
		cleanupcode		)

Value:

do\
  {\
    int retcode;\
    (bddm)->allow_reordering=1;\
    (bddm)->nodes_at_start=(bddm)->unique_table.entries;\
    while ((retcode=(setjmp((bddm)->abort.context))))\
      {\
        bdd_cleanup(bddm, retcode);\
        cleanupcode\
        (bddm)->nodes_at_start=(bddm)->unique_table.entries;\
      }\
  }\
while (0)

Definition at line 549 of file bddint.h.

#define FLIP_TAG0

(

p

)

((pointer)((INT_PTR)(p) ^ 0x1))

Definition at line 60 of file bddint.h.

#define FLIP_TAG1

(

p

)

((pointer)((INT_PTR)(p) ^ 0x2))

Definition at line 65 of file bddint.h.

#define FLIP_TAG2

(

p

)

((pointer)((INT_PTR)(p) ^ 0x4))

Definition at line 70 of file bddint.h.

#define HASH_NODE	(	f,
		g		)	(((f) << 1)+(g))

Definition at line 567 of file bddint.h.

#define MAX_REC_SIZE   64

Definition at line 465 of file bddint.h.

#define MIN_REC_SIZE   ALLOC_ALIGNMENT

Definition at line 464 of file bddint.h.

#define OP_CMPTO   200000l

Definition at line 351 of file bddint.h.

#define OP_COFACTOR   100l

Definition at line 341 of file bddint.h.

#define OP_COMP   100000l

Definition at line 350 of file bddint.h.

#define OP_EQUAL   600l

Definition at line 346 of file bddint.h.

#define OP_FWD   300l

Definition at line 343 of file bddint.h.

#define OP_QNT   10000l

Definition at line 347 of file bddint.h.

#define OP_RED   500l

Definition at line 345 of file bddint.h.

#define OP_RELPROD   20000l

Definition at line 348 of file bddint.h.

#define OP_REV   400l

Definition at line 344 of file bddint.h.

#define OP_SATFRAC   200l

Definition at line 342 of file bddint.h.

#define OP_SUBST   30000l

Definition at line 349 of file bddint.h.

#define OP_SWAP   300000l

Definition at line 352 of file bddint.h.

#define OP_SWAPAUX   400000l

Definition at line 353 of file bddint.h.

#define POINTER

(

p

)

((pointer)(((INT_PTR)(p)) & ~(INT_PTR)0x7))

Definition at line 52 of file bddint.h.

#define REC_MGRS   (((MAX_REC_SIZE-MIN_REC_SIZE)/ALLOC_ALIGNMENT)+1)

Definition at line 467 of file bddint.h.

#define RETURN_BDD

(

thing

)

return (bdd_make_external(thing))

Definition at line 299 of file bddint.h.

#define SET_TAG	(	p,
		t		)	((pointer)((INT_PTR)POINTER(p) | (t)))

Definition at line 57 of file bddint.h.

#define TABLE_SIZE

(

size_index

)

(bdd_primes[size_index])

Definition at line 576 of file bddint.h.

#define TAG

(

p

)

((int)(((INT_PTR)(p)) & 0x7))

Definition at line 56 of file bddint.h.

#define TAG0

(

p

)

((int)((INT_PTR)(p) & 0x1))

Definition at line 59 of file bddint.h.

#define TAG0_HI

(

p

)

((pointer)((INT_PTR)(p) | 0x1))

Definition at line 61 of file bddint.h.

#define TAG0_LO

(

p

)

((pointer)((INT_PTR)(p) & ~(INT_PTR)0x1))

Definition at line 62 of file bddint.h.

#define TAG1

(

p

)

((int)((INT_PTR)(p) & 0x2))

Definition at line 64 of file bddint.h.

#define TAG1_HI

(

p

)

((pointer)((INT_PTR)(p) | 0x2))

Definition at line 66 of file bddint.h.

#define TAG1_LO

(

p

)

((pointer)((INT_PTR)(p) & ~(INT_PTR)0x2))

Definition at line 67 of file bddint.h.

#define TAG2

(

p

)

((int)((INT_PTR)(p) & 0x4))

Definition at line 69 of file bddint.h.

#define TAG2_HI

(

p

)

((pointer)((INT_PTR)(p) | 0x4))

Definition at line 71 of file bddint.h.

#define TAG2_LO

(

p

)

((pointer)((INT_PTR)(p) & ~(INT_PTR)0x4))

Definition at line 72 of file bddint.h.

#define USER_ENTRY_TYPES   4

Definition at line 331 of file bddint.h.

---

Typedef Documentation

typedef struct assoc_list_* assoc_list

Definition at line 375 of file bddint.h.

typedef unsigned short bdd_index_type

Definition at line 77 of file bddint.h.

typedef unsigned short bdd_indexindex_type

Definition at line 82 of file bddint.h.

typedef unsigned char bdd_mark_type

Definition at line 84 of file bddint.h.

typedef unsigned char bdd_refcount_type

Definition at line 83 of file bddint.h.

typedef struct cache_ cache

Definition at line 427 of file bddint.h.

typedef struct cache_bin_ cache_bin

Definition at line 397 of file bddint.h.

typedef struct cache_entry_* cache_entry

Definition at line 316 of file bddint.h.

typedef struct hash_rec_* hash_rec

Definition at line 696 of file bddint.h.

typedef struct hash_table_* hash_table

Definition at line 40 of file bddint.h.

typedef struct jump_buf_ jump_buf

Definition at line 478 of file bddint.h.

typedef struct unique_ unique

Definition at line 459 of file bddint.h.

typedef struct var_assoc_* var_assoc

Definition at line 364 of file bddint.h.

typedef struct var_table_* var_table

Definition at line 440 of file bddint.h.

---

Function Documentation

void cmu_bdd_free_hash_table ARGS

(

(hash_table)

)

pointer bdd_lookup_in_hash_table ARGS

(

(hash_table, bdd)

)

void bdd_insert_in_hash_table ARGS

(

(hash_table, bdd, pointer)

)

EXTERN void mem_fatal ARGS

(

(char *)

)

bdd cmu_mtbdd_get_terminal ARGS

(

(cmu_bdd_manager, INT_PTR, INT_PTR)

)

bdd bdd_find ARGS

(

(cmu_bdd_manager, bdd_indexindex_type, bdd, bdd)

)

void bdd_sweep_var_table ARGS

(

(cmu_bdd_manager, long, int)

)

int cmu_bdd_assoc ARGS

(

(cmu_bdd_manager, int)

)

long cmu_bdd_node_limit ARGS

(

(cmu_bdd_manager, long)

)

int bdd_cache_functions ARGS

(

(cmu_bdd_manager, int, int(*) ARGS((cmu_bdd_manager, cache_entry)), void(*) ARGS((cmu_bdd_manager, cache_entry)), void(*) ARGS((cmu_bdd_manager, cache_entry)), int(*) ARGS((cmu_bdd_manager, cache_entry, pointer)))

)

void bdd_flush_cache ARGS

(

(cmu_bdd_manager, int(*) ARGS((cmu_bdd_manager, cache_entry, pointer)), pointer)

)

int bdd_lookup_in_cache13 ARGS

(

(cmu_bdd_manager, int, INT_PTR, INT_PTR *, INT_PTR *, INT_PTR *)

)

int bdd_lookup_in_cache22 ARGS

(

(cmu_bdd_manager, int, INT_PTR, INT_PTR, INT_PTR *, INT_PTR *)

)

int bdd_lookup_in_cache31 ARGS

(

(cmu_bdd_manager, int, INT_PTR, INT_PTR, INT_PTR, INT_PTR *)

)

void bdd_insert_in_cache13 ARGS

(

(cmu_bdd_manager, int, INT_PTR, INT_PTR, INT_PTR, INT_PTR)

)

void cmu_mtbdd_terminal_value_aux ARGS

(

(cmu_bdd_manager, bdd, INT_PTR *, INT_PTR *)

)

void cmu_bdd_reorder ARGS

(

(cmu_bdd_manager)

)

void bdd_block_delta ARGS

(

(block, long)

)

char* bdd_var_name ARGS

(

(cmu_bdd_manager, bdd, char *(*) ARGS((cmu_bdd_manager, bdd, pointer)), pointer)

)

char* bdd_terminal_id ARGS

(

(cmu_bdd_manager, bdd, char *(*) ARGS((cmu_bdd_manager, INT_PTR, INT_PTR, pointer)), pointer)

)

void bdd_number_shared_nodes ARGS

(

(cmu_bdd_manager, bdd, hash_table, long *)

)

bdd cmu_bdd_substitute_step ARGS

(

(cmu_bdd_manager, bdd, long, bdd(*) ARGS((cmu_bdd_manager, bdd, bdd, bdd)), var_assoc)

)

bdd cmu_bdd_exists_temp ARGS

(

(cmu_bdd_manager, bdd, long)

)

bdd mtcmu_bdd_ite ARGS

(

(cmu_bdd_manager, bdd, bdd, bdd)

)

bdd bdd_find_aux ARGS

(

(cmu_bdd_manager, bdd_indexindex_type, INT_PTR, INT_PTR)

)

void bdd_rehash_var_table ARGS

(

(var_table, int)

)

bdd mtcmu_bdd_substitute ARGS

(

(cmu_bdd_manager, bdd)

)

bdd bdd_make_external ARGS

(

(bdd)

)

void bdd_check_array ARGS

(

(bdd *)

)

int bdd_check_arguments ARGS

(

(int,...)

)

---

Variable Documentation

long bdd_primes[]

Definition at line 4 of file bddprimes.c.