src/cmuBdd/bddcproject.c File Reference

#include "bddint.h"
Include dependency graph for bddcproject.c:

Go to the source code of this file.

Defines

#define OP_CPROJ   5000001

Functions

bdd cmu_bdd_project (cmu_bdd_manager, bdd)
static bdd cmu_bdd_smooth_g_step (cmu_bdd_manager bddm, bdd f, long op, var_assoc vars, long id)
static bdd cmu_bdd_smooth_g (cmu_bdd_manager bddm, bdd f, long id)
static bdd cmu_bdd_project_step (cmu_bdd_manager bddm, bdd f, long op, var_assoc vars)

Variables

static char vcid [] = "bddcproject.c,v 1.2 1994/06/02 02:36:30 shiple Exp"

Define Documentation

#define OP_CPROJ   5000001

Definition at line 20 of file bddcproject.c.

Function Documentation

bdd cmu_bdd_project ( cmu_bdd_manager  bddm,
bdd  f 
)

Definition at line 175 of file bddcproject.c.

00176 {
00177     long op;
00178 
00179     if (bdd_check_arguments(1, f))
00180         {
00181             FIREWALL(bddm);
00182             if (bddm->curr_assoc_id == -1)
00183                 op=bddm->temp_op--;
00184             else
00185                 op=OP_CPROJ+bddm->curr_assoc_id;
00186             RETURN_BDD(cmu_bdd_project_step(bddm, f, op, bddm->curr_assoc));
00187         }
00188     return ((bdd)0);
00189 }

static bdd cmu_bdd_project_step ( cmu_bdd_manager  bddm,
bdd  f,
long  op,
var_assoc  vars 
) [static]

Definition at line 102 of file bddcproject.c.

00104 {
00105     bdd temp1, temp2;
00106     bdd sm, pr;
00107     bdd result;
00108     int quantifying;
00109 
00110     BDD_SETUP(f);
00111     if ((long)BDD_INDEX(bddm, f) > vars->last)
00112         {
00113             BDD_TEMP_INCREFS(f);
00114             return (f);
00115         }
00116     if (bdd_lookup_in_cache1(bddm, op, f, &result))
00117         return (result);
00118     quantifying=(vars->assoc[BDD_INDEXINDEX(f)] != 0);
00119 
00120     if (quantifying)
00121         {
00122 
00123             sm  = cmu_bdd_smooth_g(bddm,BDD_THEN(f),(long)BDD_INDEXINDEX(f)); 
00124             if (sm == BDD_ONE(bddm))
00125                 {
00126                     pr  = cmu_bdd_project_step(bddm, BDD_THEN(f), op, vars);
00127                     {
00128                     BDD_SETUP(pr);
00129                     result = bdd_find(bddm, BDD_INDEXINDEX(f), pr,BDD_ZERO(bddm));
00130                    BDD_TEMP_DECREFS(pr);
00131                     }
00132                     
00133                 }
00134       else if (sm == BDD_ZERO(bddm))
00135                 {
00136                     pr = cmu_bdd_project_step(bddm, BDD_ELSE(f), op, vars);
00137                     {
00138                     BDD_SETUP(pr);
00139                     result = bdd_find(bddm, BDD_INDEXINDEX(f), BDD_ZERO(bddm), pr);
00140                    BDD_TEMP_DECREFS(pr);
00141                     }
00142                     
00143                 }
00144             else 
00145                 {
00146                     temp1 = cmu_bdd_project_step(bddm, BDD_THEN(f), op, vars);
00147                     temp2 = cmu_bdd_project_step(bddm, BDD_ELSE(f),op, vars);
00148                     {
00149                     BDD_SETUP(temp1);
00150                     BDD_SETUP(temp2);
00151                     pr = cmu_bdd_ite_step(bddm, sm, BDD_ZERO(bddm), temp2);
00152                     bddm->op_cache.cache_level++;
00153                     result = bdd_find(bddm, BDD_INDEXINDEX(f), temp1, pr);
00154                     BDD_TEMP_DECREFS(temp1);
00155                     BDD_TEMP_DECREFS(temp2);
00156                     bddm->op_cache.cache_level--;
00157                     }
00158             
00159                 }
00160         }
00161   
00162     else
00163         {
00164             temp1=cmu_bdd_project_step(bddm, BDD_THEN(f), op, vars);
00165             temp2=cmu_bdd_project_step(bddm, BDD_ELSE(f), op, vars);
00166             result=bdd_find(bddm, BDD_INDEXINDEX(f), temp1, temp2);
00167 
00168         }
00169   
00170     bdd_insert_in_cache1(bddm, op, f, result);
00171     return (result);
00172 }

static bdd cmu_bdd_smooth_g ( cmu_bdd_manager  bddm,
bdd  f,
long  id 
) [static]

Definition at line 80 of file bddcproject.c.

00081 {
00082     long op;
00083     
00084             if (bddm->curr_assoc_id == -1)
00085                 op=bddm->temp_op--;
00086             else
00087                 op=OP_QNT+bddm->curr_assoc_id;
00088             RETURN_BDD(cmu_bdd_smooth_g_step(bddm, f, op, bddm->curr_assoc,id));
00089   }

static bdd cmu_bdd_smooth_g_step ( cmu_bdd_manager  bddm,
bdd  f,
long  op,
var_assoc  vars,
long  id 
) [static]

Definition at line 34 of file bddcproject.c.

00035 {
00036     bdd temp1, temp2;
00037     bdd result;
00038     int quantifying;
00039 
00040     BDD_SETUP(f);
00041     if ((long)BDD_INDEX(bddm, f) > vars->last)
00042         {
00043             BDD_TEMP_INCREFS(f);
00044             return (f);
00045         }
00046     if (bdd_lookup_in_cache1(bddm, op, f, &result))
00047         return (result);
00048     quantifying=(vars->assoc[BDD_INDEXINDEX(f)] != 0);
00049 
00050     temp1=cmu_bdd_smooth_g_step(bddm, BDD_THEN(f), op, vars,id);
00051 
00052     if ((quantifying && temp1 == BDD_ONE(bddm))&&((long)BDD_INDEX(bddm, f) > id ))
00053 
00054         result=temp1;
00055     else
00056         {
00057             temp2=cmu_bdd_smooth_g_step(bddm, BDD_ELSE(f), op, vars,id);
00058             if (quantifying)
00059                 {
00060                     BDD_SETUP(temp1);
00061                     BDD_SETUP(temp2);
00062                     bddm->op_cache.cache_level++;
00063                     result=cmu_bdd_ite_step(bddm, temp1, BDD_ONE(bddm), temp2);
00064                     BDD_TEMP_DECREFS(temp1);
00065                     BDD_TEMP_DECREFS(temp2);
00066                     bddm->op_cache.cache_level--;
00067                 }
00068             else
00069                 result=bdd_find(bddm, BDD_INDEXINDEX(f), temp1, temp2);
00070         }
00071     bdd_insert_in_cache1(bddm, op, f, result);
00072 
00073    
00074     return (result);
00075 }

Variable Documentation

char vcid[] = "bddcproject.c,v 1.2 1994/06/02 02:36:30 shiple Exp" [static]

Definition at line 15 of file bddcproject.c.

Generated on Tue Jan 12 13:57:14 2010 for glu-2.2 by  doxygen 1.6.1