src/cmuBdd/bddreduce.c File Reference

#include "bddint.h"

Include dependency graph for bddreduce.c:

Functions
static bdd	cmu_bdd_reduce_step (cmu_bdd_manager bddm, bdd f, bdd c)
bdd	cmu_bdd_reduce (cmu_bdd_manager bddm, bdd f, bdd c)
static bdd	cmu_bdd_cofactor_step (cmu_bdd_manager bddm, bdd f, bdd c)
bdd	cmu_bdd_cofactor (cmu_bdd_manager bddm, bdd f, bdd c)

Function Documentation

bdd cmu_bdd_cofactor	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	c
	)

Definition at line 128 of file bddreduce.c.

00129 {
00130   if (bdd_check_arguments(2, f, c))
00131     {
00132       if (c == BDD_ZERO(bddm))
00133         {
00134           cmu_bdd_warning("cmu_bdd_cofactor: second argument is false");
00135           return (BDD_ONE(bddm));
00136         }
00137       FIREWALL(bddm);
00138       RETURN_BDD(cmu_bdd_cofactor_step(bddm, f, c));
00139     }
00140   return ((bdd)0);
00141 }

static bdd cmu_bdd_cofactor_step	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	c
	)			`[static]`

Definition at line 83 of file bddreduce.c.

00084 {
00085   bdd_indexindex_type top_indexindex;
00086   bdd f1, f2;
00087   bdd c1, c2;
00088   bdd temp1, temp2;
00089   bdd result;
00090 
00091   BDD_SETUP(f);
00092   BDD_SETUP(c);
00093   if (BDD_IS_CONST(c))
00094     {
00095       if (c == BDD_ZERO(bddm))
00096         return ((bdd)0);
00097       BDD_TEMP_INCREFS(f);
00098       return (f);
00099     }
00100   if (BDD_IS_CONST(f))
00101     return (f);
00102   if (bdd_lookup_in_cache2(bddm, OP_COFACTOR, f, c, &result))
00103     return (result);
00104   BDD_TOP_VAR2(top_indexindex, bddm, f, c);
00105   BDD_COFACTOR(top_indexindex, f, f1, f2);
00106   BDD_COFACTOR(top_indexindex, c, c1, c2);
00107   temp1=cmu_bdd_cofactor_step(bddm, f1, c1);
00108   temp2=cmu_bdd_cofactor_step(bddm, f2, c2);
00109   if (!temp1)
00110     result=temp2;
00111   else if (!temp2)
00112     result=temp1;
00113   else
00114     result=bdd_find(bddm, top_indexindex, temp1, temp2);
00115   bdd_insert_in_cache2(bddm, OP_COFACTOR, f, c, result);
00116   return (result);
00117 }

bdd cmu_bdd_reduce	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	c
	)

Definition at line 65 of file bddreduce.c.

00066 {
00067   bdd result;
00068 
00069   if (bdd_check_arguments(2, f, c))
00070     {
00071       FIREWALL(bddm);
00072       result=cmu_bdd_reduce_step(bddm, f, c);
00073       if (!result)
00074         return (BDD_ZERO(bddm));
00075       RETURN_BDD(result);
00076     }
00077   return ((bdd)0);
00078 }

static bdd cmu_bdd_reduce_step	(	cmu_bdd_manager	bddm,
		bdd	f,
		bdd	c
	)			`[static]`

Definition at line 9 of file bddreduce.c.

00010 {
00011   bdd_indexindex_type top_indexindex;
00012   bdd f1, f2;
00013   bdd c1, c2;
00014   bdd temp1, temp2;
00015   bdd result;
00016 
00017   BDD_SETUP(f);
00018   BDD_SETUP(c);
00019   if (BDD_IS_CONST(c))
00020     {
00021       if (c == BDD_ZERO(bddm))
00022         return ((bdd)0);
00023       BDD_TEMP_INCREFS(f);
00024       return (f);
00025     }
00026   if (BDD_IS_CONST(f))
00027     return (f);
00028   if (bdd_lookup_in_cache2(bddm, OP_RED, f, c, &result))
00029     return (result);
00030   BDD_TOP_VAR2(top_indexindex, bddm, f, c);
00031   BDD_COFACTOR(top_indexindex, f, f1, f2);
00032   BDD_COFACTOR(top_indexindex, c, c1, c2);
00033   if (f == f1)
00034     {
00035       bddm->op_cache.cache_level++;
00036       temp1=cmu_bdd_ite_step(bddm, c1, BDD_ONE(bddm), c2);
00037       bddm->op_cache.cache_level--;
00038       result=cmu_bdd_reduce_step(bddm, f, temp1);
00039       {
00040         BDD_SETUP(temp1);
00041         BDD_TEMP_DECREFS(temp1);
00042       }
00043     }
00044   else
00045     {
00046       temp1=cmu_bdd_reduce_step(bddm, f1, c1);
00047       temp2=cmu_bdd_reduce_step(bddm, f2, c2);
00048       if (!temp1)
00049         result=temp2;
00050       else if (!temp2)
00051         result=temp1;
00052       else
00053         result=bdd_find(bddm, top_indexindex, temp1, temp2);
00054     }
00055   bdd_insert_in_cache2(bddm, OP_RED, f, c, result);
00056   return (result);
00057 }

src/cmuBdd/bddreduce.c File Reference

Functions

Function Documentation