00001
00002
00003
00004 #include "bddint.h"
00005
00006
00007 static
00008 int
00009 bdd_fraction_compare(cmu_bdd_manager bddm, bdd f, bdd g)
00010 {
00011 double f_frac, g_frac;
00012
00013 bddm->op_cache.cache_level++;
00014 f_frac=cmu_bdd_satisfying_fraction_step(bddm, f);
00015 g_frac=cmu_bdd_satisfying_fraction_step(bddm, g);
00016 bddm->op_cache.cache_level--;
00017 if (f_frac < g_frac)
00018 return (-1);
00019 if (f_frac > g_frac)
00020 return (1);
00021 return (0);
00022 }
00023
00024
00025 static
00026 int
00027 cmu_bdd_compare_step(cmu_bdd_manager bddm, bdd f, bdd g, bdd_indexindex_type v_indexindex, long op)
00028 {
00029 bdd f1, f2;
00030 bdd g1, g2;
00031 bdd_indexindex_type top_indexindex;
00032 INT_PTR result;
00033
00034 BDD_SETUP(f);
00035 BDD_SETUP(g);
00036 if (f == g)
00037 return (0);
00038 if (BDD_IS_CONST(f) || BDD_IS_CONST(g))
00039 {
00040 if (f == BDD_ZERO(bddm) || g == BDD_ONE(bddm))
00041 return (-1);
00042 return (1);
00043 }
00044 if (bdd_lookup_in_cache2d(bddm, op, f, g, &result))
00045 return ((int)result);
00046 BDD_TOP_VAR2(top_indexindex, bddm, f, g);
00047 if (bddm->indexes[top_indexindex] > bddm->indexes[v_indexindex])
00048 result=bdd_fraction_compare(bddm, f, g);
00049 else
00050 {
00051 BDD_COFACTOR(top_indexindex, f, f1, f2);
00052 BDD_COFACTOR(top_indexindex, g, g1, g2);
00053 if (!(result=cmu_bdd_compare_step(bddm, f2, g2, v_indexindex, op)))
00054 result=cmu_bdd_compare_step(bddm, f1, g1, v_indexindex, op);
00055 }
00056 bdd_insert_in_cache2d(bddm, op, f, g, result);
00057 return ((int)result);
00058 }
00059
00060
00061 int
00062 cmu_bdd_compare_temp(cmu_bdd_manager bddm, bdd f, bdd g, bdd v)
00063 {
00064 BDD_SETUP(v);
00065 return (cmu_bdd_compare_step(bddm, f, g, BDD_INDEXINDEX(v), OP_CMPTO+BDD_INDEXINDEX(v)));
00066 }
00067
00068
00069 int
00070 cmu_bdd_compare(cmu_bdd_manager bddm, bdd f, bdd g, bdd v)
00071 {
00072 if (bdd_check_arguments(3, f, g, v))
00073 {
00074 BDD_SETUP(v);
00075 if (cmu_bdd_type_aux(bddm, v) != BDD_TYPE_POSVAR)
00076 {
00077 cmu_bdd_warning("cmu_bdd_compare: third argument is not a positive variable");
00078 return (0);
00079 }
00080 return (cmu_bdd_compare_step(bddm, f, g, BDD_INDEXINDEX(v), OP_CMPTO+BDD_INDEXINDEX(v)));
00081 }
00082 return (0);
00083 }
