src/cmuBdd/mtbdd.c File Reference

#include "bddint.h"

Include dependency graph for mtbdd.c:

Functions
void	mtbdd_transform_closure (cmu_bdd_manager bddm, int(canonical_fn)(cmu_bdd_manager, INT_PTR, INT_PTR, pointer), void(transform_fn)(cmu_bdd_manager, INT_PTR, INT_PTR, INT_PTR , INT_PTR , pointer), pointer transform_env)
void	mtcmu_bdd_one_data (cmu_bdd_manager bddm, INT_PTR value1, INT_PTR value2)
void	cmu_mtbdd_free_terminal_closure (cmu_bdd_manager bddm, void(*free_terminal_fn)(cmu_bdd_manager, INT_PTR, INT_PTR, pointer), pointer free_terminal_env)
bdd	cmu_mtbdd_get_terminal (cmu_bdd_manager bddm, INT_PTR value1, INT_PTR value2)
void	cmu_mtbdd_terminal_value (cmu_bdd_manager bddm, bdd f, INT_PTR value1, INT_PTR value2)
static bdd	mtcmu_bdd_ite_step (cmu_bdd_manager bddm, bdd f, bdd g, bdd h)
bdd	mtcmu_bdd_ite (cmu_bdd_manager bddm, bdd f, bdd g, bdd h)
bdd	mtcmu_bdd_substitute (cmu_bdd_manager bddm, bdd f)
static bdd	cmu_mtbdd_equal_step (cmu_bdd_manager bddm, bdd f, bdd g)
bdd	cmu_mtbdd_equal (cmu_bdd_manager bddm, bdd f, bdd g)

Function Documentation

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

Definition at line 220 of file mtbdd.c.

00221 {
00222   if (bdd_check_arguments(2, f, g))
00223     {
00224       FIREWALL(bddm);
00225       RETURN_BDD(cmu_mtbdd_equal_step(bddm, f, g));
00226     }
00227   return ((bdd)0);
00228 }

static bdd cmu_mtbdd_equal_step	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	g
	)			`[static]`

Definition at line 187 of file mtbdd.c.

00188 {
00189   bdd_indexindex_type top_indexindex;
00190   bdd f1, f2;
00191   bdd g1, g2;
00192   bdd temp1, temp2;
00193   bdd result;
00194 
00195   BDD_SETUP(f);
00196   BDD_SETUP(g);
00197   if (f == g)
00198     return (BDD_ONE(bddm));
00199   if (BDD_IS_CONST(f) && BDD_IS_CONST(g))
00200     return (BDD_ZERO(bddm));
00201   if (BDD_OUT_OF_ORDER(f, g))
00202     BDD_SWAP(f, g);
00203   if (bdd_lookup_in_cache2(bddm, OP_EQUAL, f, g, &result))
00204     return (result);
00205   BDD_TOP_VAR2(top_indexindex, bddm, f, g);
00206   BDD_COFACTOR(top_indexindex, f, f1, f2);
00207   BDD_COFACTOR(top_indexindex, g, g1, g2);
00208   temp1=cmu_mtbdd_equal_step(bddm, f1, g1);
00209   temp2=cmu_mtbdd_equal_step(bddm, f2, g2);
00210   result=bdd_find(bddm, top_indexindex, temp1, temp2);
00211   bdd_insert_in_cache2(bddm, OP_EQUAL, f, g, result);
00212   return (result);
00213 }

void cmu_mtbdd_free_terminal_closure	(	cmu_bdd_manager	bddm,
		void(*)(cmu_bdd_manager, INT_PTR, INT_PTR, pointer)	free_terminal_fn,
		pointer	free_terminal_env
	)

Definition at line 58 of file mtbdd.c.

00061 {
00062   bddm->unique_table.free_terminal_fn=free_terminal_fn;
00063   bddm->unique_table.free_terminal_env=free_terminal_env;
00064 }

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

Definition at line 71 of file mtbdd.c.

00072 {
00073   FIREWALL(bddm);
00074   RETURN_BDD(bdd_find_terminal(bddm, value1, value2));
00075 }

void cmu_mtbdd_terminal_value	(	cmu_bdd_manager	bddm,
		bdd	f,
		INT_PTR *	value1,
		INT_PTR *	value2
	)

Definition at line 82 of file mtbdd.c.

00083 {
00084   if (bdd_check_arguments(1, f))
00085     {
00086       BDD_SETUP(f);
00087       if (!BDD_IS_CONST(f))
00088         {
00089           cmu_bdd_warning("mtbdd_terminal_data: argument is terminal node");
00090           *value1=0;
00091           *value2=0;
00092           return;
00093         }
00094       cmu_mtbdd_terminal_value_aux(bddm, f, value1, value2);
00095     }
00096 }

void mtbdd_transform_closure	(	cmu_bdd_manager	bddm,
		int(*)(cmu_bdd_manager, INT_PTR, INT_PTR, pointer)	canonical_fn,
		void()(cmu_bdd_manager, INT_PTR, INT_PTR, INT_PTR , INT_PTR *, pointer)	transform_fn,
		pointer	transform_env
	)

Definition at line 17 of file mtbdd.c.

00021 {
00022   bddm->transform_fn=transform_fn;
00023   bddm->transform_env=transform_env;
00024   bddm->canonical_fn=canonical_fn;
00025 }

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

Definition at line 154 of file mtbdd.c.

00155 {
00156   if (bdd_check_arguments(3, f, g, h))
00157     {
00158       FIREWALL(bddm);
00159       RETURN_BDD(mtcmu_bdd_ite_step(bddm, f, g, h));
00160     }
00161   return ((bdd)0);
00162 }

static bdd mtcmu_bdd_ite_step	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	g,
		bdd	h
	)			`[static]`

Definition at line 101 of file mtbdd.c.

00102 {
00103   bdd_indexindex_type top_indexindex;
00104   bdd f1, f2;
00105   bdd g1, g2;
00106   bdd h1, h2;
00107   bdd temp1, temp2;
00108   bdd result;
00109 
00110   BDD_SETUP(f);
00111   BDD_SETUP(g);
00112   BDD_SETUP(h);
00113   if (BDD_IS_CONST(f))
00114     {
00115       if (f == BDD_ONE(bddm))
00116         {
00117           BDD_TEMP_INCREFS(g);
00118           return (g);
00119         }
00120       BDD_TEMP_INCREFS(h);
00121       return (h);
00122     }
00123   /* f is not constant. */
00124   if (g == h)
00125     {
00126       BDD_TEMP_INCREFS(g);
00127       return (g);
00128     }
00129   /* f is not constant, g and h are distinct. */
00130   if (!BDD_IS_OUTPOS(f))
00131     {
00132       f=BDD_NOT(f);
00133       BDD_SWAP(g, h);
00134     }
00135   /* f is now an uncomplemented output pointer. */
00136   if (bdd_lookup_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)h, (INT_PTR *)&result))
00137     return (result);
00138   BDD_TOP_VAR3(top_indexindex, bddm, f, g, h);
00139   BDD_COFACTOR(top_indexindex, f, f1, f2);
00140   BDD_COFACTOR(top_indexindex, g, g1, g2);
00141   BDD_COFACTOR(top_indexindex, h, h1, h2);
00142   temp1=mtcmu_bdd_ite_step(bddm, f1, g1, h1);
00143   temp2=mtcmu_bdd_ite_step(bddm, f2, g2, h2);
00144   result=bdd_find(bddm, top_indexindex, temp1, temp2);
00145   bdd_insert_in_cache31(bddm, CACHE_TYPE_ITE, (INT_PTR)f, (INT_PTR)g, (INT_PTR)h, (INT_PTR)result);
00146   return (result);
00147 }

void mtcmu_bdd_one_data	(	cmu_bdd_manager	bddm,
		INT_PTR	value1,
		INT_PTR	value2
	)

Definition at line 32 of file mtbdd.c.

00033 {
00034   var_table table;
00035   long hash;
00036 
00037   table=bddm->unique_table.tables[BDD_CONST_INDEXINDEX];
00038   if (table->entries != 1)
00039     cmu_bdd_fatal("mtcmu_bdd_one_data: other terminal nodes already exist");
00040   hash=HASH_NODE(bddm->one->data[0], bddm->one->data[1]);
00041   BDD_REDUCE(hash, table->size);
00042   table->table[hash]=0;
00043   bddm->one->data[0]=value1;
00044   bddm->one->data[1]=value2;
00045   hash=HASH_NODE(bddm->one->data[0], bddm->one->data[1]);
00046   BDD_REDUCE(hash, table->size);
00047   table->table[hash]=bddm->one;
00048 }

bdd mtcmu_bdd_substitute	(	cmu_bdd_manager	bddm,
		bdd	f
	)

Definition at line 168 of file mtbdd.c.

00169 {
00170   long op;
00171 
00172   if (bdd_check_arguments(1, f))
00173     {
00174       FIREWALL(bddm);
00175       if (bddm->curr_assoc_id == -1)
00176         op=bddm->temp_op--;
00177       else
00178         op=OP_SUBST+bddm->curr_assoc_id;
00179       RETURN_BDD(cmu_bdd_substitute_step(bddm, f, op, mtcmu_bdd_ite_step, bddm->curr_assoc));
00180     }
00181   return ((bdd)0);
00182 }

src/cmuBdd/mtbdd.c File Reference

Functions

Function Documentation