00001
00002
00003
00004 #include "bddint.h"
00005
00006
00007 void
00008 bdd_mark_shared_nodes(cmu_bdd_manager bddm, bdd f)
00009 {
00010 BDD_SETUP(f);
00011 f=BDD_OUTPOS(f);
00012 if (BDD_IS_CONST(f) || cmu_bdd_type_aux(bddm, f) == BDD_TYPE_POSVAR)
00013 return;
00014 if (BDD_MARK(f))
00015 {
00016 if (BDD_MARK(f) == 1)
00017 BDD_MARK(f)=2;
00018 return;
00019 }
00020 BDD_MARK(f)=1;
00021 bdd_mark_shared_nodes(bddm, BDD_THEN(f));
00022 bdd_mark_shared_nodes(bddm, BDD_ELSE(f));
00023 }
00024
00025
00026 void
00027 bdd_number_shared_nodes(cmu_bdd_manager bddm, bdd f, hash_table h, long *next)
00028 {
00029 BDD_SETUP(f);
00030 if (BDD_IS_CONST(f) || ((1 << cmu_bdd_type_aux(bddm, f)) & ((1 << BDD_TYPE_POSVAR) | (1 << BDD_TYPE_NEGVAR))))
00031 return;
00032 if (BDD_MARK(f) == 0)
00033 return;
00034 if (BDD_MARK(f) == 2)
00035 {
00036 bdd_insert_in_hash_table(h, f, (pointer)next);
00037 ++*next;
00038 }
00039 BDD_MARK(f)=0;
00040 bdd_number_shared_nodes(bddm, BDD_THEN(f), h, next);
00041 bdd_number_shared_nodes(bddm, BDD_ELSE(f), h, next);
00042 }
00043
00044
00045 static char default_terminal_id[]="terminal XXXXXXXXXX XXXXXXXXXX";
00046 static char default_var_name[]="var.XXXXXXXXXX";
00047
00048
00049 char *
00050 bdd_terminal_id(cmu_bdd_manager bddm, bdd f, char *(*terminal_id_fn)(cmu_bdd_manager, INT_PTR, INT_PTR, pointer), pointer env)
00051 {
00052 char *id;
00053 INT_PTR v1, v2;
00054
00055 cmu_mtbdd_terminal_value_aux(bddm, f, &v1, &v2);
00056 if (terminal_id_fn)
00057 id=(*terminal_id_fn)(bddm, v1, v2, env);
00058 else
00059 id=0;
00060 if (!id)
00061 {
00062 if (f == BDD_ONE(bddm))
00063 return ("1");
00064 if (f == BDD_ZERO(bddm))
00065 return ("0");
00066 sprintf(default_terminal_id, "terminal %ld %ld", (long)v1, (long)v2);
00067 id=default_terminal_id;
00068 }
00069 return (id);
00070 }
00071
00072
00073 char *
00074 bdd_var_name(cmu_bdd_manager bddm, bdd v, char *(*var_naming_fn)(cmu_bdd_manager, bdd, pointer), pointer env)
00075 {
00076 char *name;
00077
00078 if (var_naming_fn)
00079 name=(*var_naming_fn)(bddm, v, env);
00080 else
00081 name=0;
00082 if (!name)
00083 {
00084 BDD_SETUP(v);
00085 sprintf(default_var_name, "var.%d", BDD_INDEX(bddm, v));
00086 name=default_var_name;
00087 }
00088 return (name);
00089 }
00090
00091
00092 void
00093 cmu_mtbdd_terminal_value_aux(cmu_bdd_manager bddm, bdd f, INT_PTR *value1, INT_PTR *value2)
00094 {
00095 BDD_SETUP(f);
00096 if (BDD_IS_OUTPOS(f))
00097 {
00098 *value1=BDD_DATA0(f);
00099 *value2=BDD_DATA1(f);
00100 }
00101 else
00102 (*bddm->transform_fn)(bddm, BDD_DATA0(f), BDD_DATA1(f), value1, value2, bddm->transform_env);
00103 }
