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 | } |
---|