00001
00002
00003
00004 #include "bddint.h"
00005
00006
00007 static
00008 bdd
00009 cmu_bdd_swap_vars_aux_step(cmu_bdd_manager bddm, bdd f, bdd g, bdd h, bdd_indexindex_type h_indexindex, long op)
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 }
00062
00063
00064 static
00065 bdd
00066 cmu_bdd_swap_vars_step(cmu_bdd_manager bddm, bdd f, bdd_indexindex_type g_indexindex, bdd h, long op)
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 }
00100
00101
00102 bdd
00103 cmu_bdd_swap_vars_temp(cmu_bdd_manager bddm, bdd f, bdd g, bdd h)
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 }
00122
00123
00124
00125
00126 bdd
00127 cmu_bdd_swap_vars(cmu_bdd_manager bddm, bdd f, bdd g, bdd h)
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 }
