#include "Debug.h"

void mdd_GetState_Values(
mdd_manager *mgr ,
mdd_t *  top, 
FILE  * f) 
{
  mdd_t * T;
  mdd_t * E;
  int    id;
  array_t * val = array_alloc(int, 4); 
  static int level;
  char c = ' ' ;

  level++;

  id = bdd_top_var_id(top);

  mvar_type mv =  
array_fetch(mvar_type, mdd_ret_mvar_list((mgr)),(id));
 // fprintf(f,"(");

  // Pour le Then
  T=bdd_then(top);
 
 //variable belongs to what we are looking for
// if(strstr(mv.name,var_name) !=NULL)
  if(bdd_is_tautology(T,1)){
    //array_insert(type, array, position, object)
    fprintf(f,"%s = 1 ",mv.name);
    //c = '+';
  } else
    if(!bdd_is_tautology(T,0)){
      fprintf(f,"%s = 1 * ",mv.name);
      //mdd_FunctionPrint(mgr, T,f);
     // c = '+';
    }

  mdd_free(T);
  
  //pour le Else
  E=bdd_else(top);
  if(bdd_is_tautology(E,0)){
    goto fin;
  }
  
  if(bdd_is_tautology(E,1)){
    fprintf(f,"%c %s = 0",c, mv.name);
    goto fin;
  }
  
  fprintf(f,"%c %s = 0 * ",c, mv.name);
  /*
  mdd_FunctionPrint(mgr, E,f);
  mdd_free(E);
*/
 fin:
  fprintf(f,")");
  level--;
  return;
}