[27] | 1 | #include "Debug.h" |
---|
| 2 | |
---|
| 3 | void mdd_GetState_Values( |
---|
| 4 | mdd_manager *mgr , |
---|
| 5 | mdd_t * top, |
---|
| 6 | FILE * f) |
---|
| 7 | { |
---|
| 8 | mdd_t * T; |
---|
| 9 | mdd_t * E; |
---|
| 10 | int id; |
---|
| 11 | array_t * val = array_alloc(int, 4); |
---|
| 12 | static int level; |
---|
| 13 | char c = ' ' ; |
---|
| 14 | |
---|
| 15 | level++; |
---|
| 16 | |
---|
| 17 | id = bdd_top_var_id(top); |
---|
| 18 | |
---|
| 19 | mvar_type mv = |
---|
| 20 | array_fetch(mvar_type, mdd_ret_mvar_list((mgr)),(id)); |
---|
| 21 | // fprintf(f,"("); |
---|
| 22 | |
---|
| 23 | // Pour le Then |
---|
| 24 | T=bdd_then(top); |
---|
| 25 | |
---|
| 26 | //variable belongs to what we are looking for |
---|
| 27 | // if(strstr(mv.name,var_name) !=NULL) |
---|
| 28 | if(bdd_is_tautology(T,1)){ |
---|
| 29 | //array_insert(type, array, position, object) |
---|
| 30 | fprintf(f,"%s = 1 ",mv.name); |
---|
| 31 | //c = '+'; |
---|
| 32 | } else |
---|
| 33 | if(!bdd_is_tautology(T,0)){ |
---|
| 34 | fprintf(f,"%s = 1 * ",mv.name); |
---|
| 35 | //mdd_FunctionPrint(mgr, T,f); |
---|
| 36 | // c = '+'; |
---|
| 37 | } |
---|
| 38 | |
---|
| 39 | mdd_free(T); |
---|
| 40 | |
---|
| 41 | //pour le Else |
---|
| 42 | E=bdd_else(top); |
---|
| 43 | if(bdd_is_tautology(E,0)){ |
---|
| 44 | goto fin; |
---|
| 45 | } |
---|
| 46 | |
---|
| 47 | if(bdd_is_tautology(E,1)){ |
---|
| 48 | fprintf(f,"%c %s = 0",c, mv.name); |
---|
| 49 | goto fin; |
---|
| 50 | } |
---|
| 51 | |
---|
| 52 | fprintf(f,"%c %s = 0 * ",c, mv.name); |
---|
| 53 | /* |
---|
| 54 | mdd_FunctionPrint(mgr, E,f); |
---|
| 55 | mdd_free(E); |
---|
| 56 | */ |
---|
| 57 | fin: |
---|
| 58 | fprintf(f,")"); |
---|
| 59 | level--; |
---|
| 60 | return; |
---|
| 61 | } |
---|
| 62 | |
---|