src/cmuBdd/bddmisc.c File Reference
#include "bddint.h"
Include dependency graph for bddmisc.c:
Go to the source code of this file.
Functions | |
| void | bdd_mark_shared_nodes (cmu_bdd_manager bddm, bdd f) |
| void | bdd_number_shared_nodes (cmu_bdd_manager bddm, bdd f, hash_table h, long *next) |
| char * | bdd_terminal_id (cmu_bdd_manager bddm, bdd f, char *(*terminal_id_fn)(cmu_bdd_manager, INT_PTR, INT_PTR, pointer), pointer env) |
| char * | bdd_var_name (cmu_bdd_manager bddm, bdd v, char *(*var_naming_fn)(cmu_bdd_manager, bdd, pointer), pointer env) |
| void | cmu_mtbdd_terminal_value_aux (cmu_bdd_manager bddm, bdd f, INT_PTR *value1, INT_PTR *value2) |
Variables | |
| static char | default_terminal_id [] = "terminal XXXXXXXXXX XXXXXXXXXX" |
| static char | default_var_name [] = "var.XXXXXXXXXX" |
Function Documentation
| void bdd_mark_shared_nodes | ( | cmu_bdd_manager | bddm, | |
| bdd | f | |||
| ) |
Definition at line 8 of file bddmisc.c.
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 }
| void bdd_number_shared_nodes | ( | cmu_bdd_manager | bddm, | |
| bdd | f, | |||
| hash_table | h, | |||
| long * | next | |||
| ) |
Definition at line 27 of file bddmisc.c.
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 }
| char* bdd_terminal_id | ( | cmu_bdd_manager | bddm, | |
| bdd | f, | |||
| char *(*)(cmu_bdd_manager, INT_PTR, INT_PTR, pointer) | terminal_id_fn, | |||
| pointer | env | |||
| ) |
Definition at line 50 of file bddmisc.c.
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 }
| char* bdd_var_name | ( | cmu_bdd_manager | bddm, | |
| bdd | v, | |||
| char *(*)(cmu_bdd_manager, bdd, pointer) | var_naming_fn, | |||
| pointer | env | |||
| ) |
Definition at line 74 of file bddmisc.c.
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 }
| void cmu_mtbdd_terminal_value_aux | ( | cmu_bdd_manager | bddm, | |
| bdd | f, | |||
| INT_PTR * | value1, | |||
| INT_PTR * | value2 | |||
| ) |
Definition at line 93 of file bddmisc.c.
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 }
Variable Documentation
char default_terminal_id[] = "terminal XXXXXXXXXX XXXXXXXXXX" [static] |
char default_var_name[] = "var.XXXXXXXXXX" [static] |
