src/cmuBdd/bddswap.c File Reference

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

Go to the source code of this file.

Functions

static bdd cmu_bdd_swap_vars_aux_step (cmu_bdd_manager bddm, bdd f, bdd g, bdd h, bdd_indexindex_type h_indexindex, long op)
static bdd cmu_bdd_swap_vars_step (cmu_bdd_manager bddm, bdd f, bdd_indexindex_type g_indexindex, bdd h, long op)
bdd cmu_bdd_swap_vars_temp (cmu_bdd_manager bddm, bdd f, bdd g, bdd h)
bdd cmu_bdd_swap_vars (cmu_bdd_manager bddm, bdd f, bdd g, bdd h)

Function Documentation

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

Definition at line 127 of file bddswap.c.

00128 {
00129   bdd_index_type g_index, h_index;
00130 
00131   if (bdd_check_arguments(3, f, g, h))
00132     {
00133       BDD_SETUP(f);
00134       BDD_SETUP(g);
00135       BDD_SETUP(h);
00136       if (cmu_bdd_type_aux(bddm, g) != BDD_TYPE_POSVAR || cmu_bdd_type_aux(bddm, h) != BDD_TYPE_POSVAR)
00137         {
00138           cmu_bdd_warning("cmu_bdd_swap_vars: second and third arguments are not both positive variables");
00139           BDD_INCREFS(f);
00140           return (f);
00141         }
00142       FIREWALL(bddm);
00143       g_index=BDD_INDEX(bddm, g);
00144       h_index=BDD_INDEX(bddm, h);
00145       if (g_index == h_index)
00146         {
00147           BDD_INCREFS(f);
00148           return (f);
00149         }
00150       if (g_index > h_index)
00151         RETURN_BDD(cmu_bdd_swap_vars_step(bddm, f, BDD_INDEXINDEX(h), g, OP_SWAP+BDD_INDEXINDEX(h)));
00152       else
00153         RETURN_BDD(cmu_bdd_swap_vars_step(bddm, f, BDD_INDEXINDEX(g), h, OP_SWAP+BDD_INDEXINDEX(g)));
00154     }
00155   return ((bdd)0);
00156 }

static bdd cmu_bdd_swap_vars_aux_step ( cmu_bdd_manager  bddm,
bdd  f,
bdd  g,
bdd  h,
bdd_indexindex_type  h_indexindex,
long  op 
) [static]

Definition at line 9 of file bddswap.c.

00010 {
00011   bdd_indexindex_type top_indexindex;
00012   bdd_index_type f_index, g_index;
00013   bdd f1, f2;
00014   bdd g1, g2;
00015   bdd temp1, temp2;
00016   bdd result;
00017 
00018   BDD_SETUP(f);
00019   BDD_SETUP(g);
00020   f_index=BDD_INDEX(bddm, f);
00021   g_index=BDD_INDEX(bddm, g);
00022   if (f_index == bddm->indexes[h_indexindex])
00023     {
00024       if (op & 1)
00025         f=BDD_THEN(f);
00026       else
00027         f=BDD_ELSE(f);
00028       BDD_RESET(f);
00029     }
00030   if (g_index == bddm->indexes[h_indexindex])
00031     {
00032       if (op & 1)
00033         g=BDD_THEN(g);
00034       else
00035         g=BDD_ELSE(g);
00036       BDD_RESET(g);
00037     }
00038   if (f == g)
00039     {
00040     if (op & 1)
00041       return (cmu_bdd_compose_temp(bddm, f, h, BDD_ONE(bddm)));
00042     else
00043       return (cmu_bdd_compose_temp(bddm, f, h, BDD_ZERO(bddm)));
00044     }
00045   if (f_index >= bddm->indexes[h_indexindex] && g_index >= bddm->indexes[h_indexindex])
00046     {
00047       BDD_TEMP_INCREFS(f);
00048       BDD_TEMP_INCREFS(g);
00049       return (bdd_find(bddm, h_indexindex, f, g));
00050     }
00051   if (bdd_lookup_in_cache2(bddm, op, f, g, &result))
00052     return (result);
00053   BDD_TOP_VAR2(top_indexindex, bddm, f, g);
00054   BDD_COFACTOR(top_indexindex, f, f1, f2);
00055   BDD_COFACTOR(top_indexindex, g, g1, g2);
00056   temp1=cmu_bdd_swap_vars_aux_step(bddm, f1, g1, h, h_indexindex, op);
00057   temp2=cmu_bdd_swap_vars_aux_step(bddm, f2, g2, h, h_indexindex, op);
00058   result=bdd_find(bddm, top_indexindex, temp1, temp2);
00059   bdd_insert_in_cache2(bddm, op, f, g, result);
00060   return (result);
00061 }

static bdd cmu_bdd_swap_vars_step ( cmu_bdd_manager  bddm,
bdd  f,
bdd_indexindex_type  g_indexindex,
bdd  h,
long  op 
) [static]

Definition at line 66 of file bddswap.c.

00067 {
00068   bdd_index_type f_index;
00069   bdd temp1, temp2;
00070   bdd result;
00071 
00072   BDD_SETUP(f);
00073   if (BDD_IS_CONST(f))
00074     return (f);
00075   if (bdd_lookup_in_cache2(bddm, op, f, h, &result))
00076     return (result);
00077   f_index=BDD_INDEX(bddm, f);
00078   if (f_index > bddm->indexes[g_indexindex])
00079     {
00080       temp1=cmu_bdd_compose_temp(bddm, f, h, BDD_ONE(bddm));
00081       temp2=cmu_bdd_compose_temp(bddm, f, h, BDD_ZERO(bddm));
00082       result=bdd_find(bddm, g_indexindex, temp1, temp2);
00083     }
00084   else if (f_index < bddm->indexes[g_indexindex])
00085     {
00086       temp1=cmu_bdd_swap_vars_step(bddm, BDD_THEN(f), g_indexindex, h, op);
00087       temp2=cmu_bdd_swap_vars_step(bddm, BDD_ELSE(f), g_indexindex, h, op);
00088       result=bdd_find(bddm, BDD_INDEXINDEX(f), temp1, temp2);
00089     }
00090   else
00091     {
00092       BDD_SETUP(h);
00093       temp1=cmu_bdd_swap_vars_aux_step(bddm, BDD_THEN(f), BDD_ELSE(f), h, BDD_INDEXINDEX(h), OP_SWAPAUX+2*BDD_INDEXINDEX(h)+1);
00094       temp2=cmu_bdd_swap_vars_aux_step(bddm, BDD_THEN(f), BDD_ELSE(f), h, BDD_INDEXINDEX(h), OP_SWAPAUX+2*BDD_INDEXINDEX(h));
00095       result=bdd_find(bddm, g_indexindex, temp1, temp2);
00096     }
00097   bdd_insert_in_cache2(bddm, op, f, h, result);
00098   return (result);
00099 }

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

Definition at line 103 of file bddswap.c.

00104 {
00105   bdd_index_type g_index, h_index;
00106 
00107   BDD_SETUP(f);
00108   BDD_SETUP(g);
00109   BDD_SETUP(h);
00110   g_index=BDD_INDEX(bddm, g);
00111   h_index=BDD_INDEX(bddm, h);
00112   if (g_index == h_index)
00113     {
00114       BDD_TEMP_INCREFS(f);
00115       return (f);
00116     }
00117   if (g_index > h_index)
00118     return (cmu_bdd_swap_vars_step(bddm, f, BDD_INDEXINDEX(h), g, OP_SWAP+BDD_INDEXINDEX(h)));
00119   else
00120     return (cmu_bdd_swap_vars_step(bddm, f, BDD_INDEXINDEX(g), h, OP_SWAP+BDD_INDEXINDEX(g)));
00121 }

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