src/bmc/bmcAutUtil.c

Go to the documentation of this file.

#include "bmc.h"
#include "bmcInt.h"

static char rcsid[] UNUSED = "$Id: bmcAutUtil.c,v 1.18 2005/05/18 18:11:52 jinh Exp $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static st_table * AutomatonVertexGetImg(graph_t *G, vertex_t *vtx);
static st_table * AutomatonVertexGetPreImg(graph_t *G, vertex_t *vtx);
static int stIntersect(st_table *tbl1, st_table *tbl2);
static int NoOfBitEncode(int n);
static bdd_t * encodeOfInteger(mdd_manager *manager, array_t *varArray, int val);

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

void
BmcAutEncodeAutomatonStates(
  Ntk_Network_t   *network,
  Ltl_Automaton_t *automaton)
{
  mdd_manager         *manager = Ntk_NetworkReadMddManager(network);
  lsGen               lsGen, lsGen1;
  vertex_t            *vtx;
  Ltl_AutomatonNode_t *node, *node1;
  Ctlsp_Formula_t     *F;
  mdd_t               *label;
  
  int                 i;

  /*
    Build the mdd of the labels of each automaton node
   */
  foreach_vertex(automaton->G, lsGen, vtx) {
    node = (Ltl_AutomatonNode_t *) vtx->user_data;
    if (node->Labels) {
      label =  mdd_one(manager);
      for (i=0; i<array_n(automaton->labelTable); i++) {
        if (LtlSetGetElt(node->Labels, i)) {
          F = array_fetch(Ctlsp_Formula_t *, automaton->labelTable, i);
          label = mdd_and(label, BmcAutBuildMddForPropositionalFormula(network, automaton, F), 1, 1);
        }
      }
      node->Encode = label;
    }
  }
  /*
    Encode automaton labels
   */
  foreach_vertex(automaton->G, lsGen, vtx) {
    bdd_t *newVar = NULL;
    
    node = (Ltl_AutomatonNode_t *) vtx->user_data;
    foreach_vertex(automaton->G, lsGen1, vtx) {
      node1 = (Ltl_AutomatonNode_t *) vtx->user_data;
      if(node != node1){
        if(newVar == NULL){
          newVar = bdd_create_variable(manager);
          node->Encode = bdd_and(node->Encode, newVar, 1, 1);
        }
        node1->Encode = bdd_and(node1->Encode, bdd_not(newVar), 1, 1);
      }
    }
  }
} /* BmcAutEncodeAutomatonStates() */


void
BmcAutEncodeAutomatonStates2(
  Ntk_Network_t   *network,
  Ltl_Automaton_t *automaton)
{
  mdd_manager         *manager = Ntk_NetworkReadMddManager(network);
  lsGen               lsGen, lsGen1;
  vertex_t            *vtx;
  Ltl_AutomatonNode_t *node, *node1;
  Ctlsp_Formula_t     *F;
  mdd_t               *label;
  
  int                 i;
 
  /*
    Build the mdd for the labels of each automaton node.
   */
  foreach_vertex(automaton->G, lsGen, vtx) {
    node = (Ltl_AutomatonNode_t *) vtx->user_data;
    if (node->Labels) {
      label =  mdd_one(manager);
      for (i=0; i<array_n(automaton->labelTable); i++) {
        if (LtlSetGetElt(node->Labels, i)) {
          F = array_fetch(Ctlsp_Formula_t *, automaton->labelTable, i); 
          label = mdd_and(label, BmcAutBuildMddForPropositionalFormula(network, automaton, F), 1, 1);
        }
      }
      node->Encode = label;
    }
  }
  /*
    Three cases:
      1- node and node1 are both = 1
      2- node1 = 1
      3- neither node nor nod1 equal to 1
   */
  foreach_vertex(automaton->G, lsGen, vtx) {
    bdd_t *newVar = NULL;
    st_table        *preState, *preState1;
   
    node = (Ltl_AutomatonNode_t *) vtx->user_data;
    preState  = AutomatonVertexGetPreImg(automaton->G, vtx);

    foreach_vertex(automaton->G, lsGen1, vtx) {  
      node1 = (Ltl_AutomatonNode_t *) vtx->user_data;
      if(node != node1){
        if (!mdd_is_tautology(mdd_and(node->Encode, node1->Encode, 1,1),0)){
          preState1 = AutomatonVertexGetPreImg(automaton->G, vtx);
          if (stIntersect(preState, preState1)){
            if(mdd_equal(node->Encode, mdd_one(manager)) && !mdd_equal(node1->Encode, mdd_one(manager))){
              node->Encode = bdd_not(node1->Encode);
            } else
              if(mdd_equal(node1->Encode, mdd_one(manager)) && !mdd_equal(node->Encode, mdd_one(manager))){
                node1->Encode = bdd_not(node->Encode);
              } else {
                if(newVar == NULL){
                  newVar = bdd_create_variable(manager);
                }
                node1->Encode = bdd_and(node1->Encode, bdd_not(newVar), 1, 1);
                node->Encode = bdd_and(node->Encode, bdd_not(node1->Encode), 1, 1);
              }
          } else {
            if(newVar == NULL){
              newVar = bdd_create_variable(manager);
              node->Encode = bdd_and(node->Encode, newVar, 1, 1);
            }
            node1->Encode = bdd_and(node1->Encode,  bdd_not(newVar), 1, 1);
          }
        }
      }
    }
  }

#if 0  
  /*
    Encode the automaton labels
   */
  foreach_vertex(automaton->G, lsGen, vtx) {
    bdd_t               *newVar = NULL;
    st_table            *nextStates;
    Ltl_AutomatonNode_t *nextState;
    st_generator        *stGen;
    
    node       = (Ltl_AutomatonNode_t *) vtx->user_data;
    nextStates = AutomatonVertexGetImg(automaton->G, vtx);
    
    st_foreach_item(nextStates, stGen, (char **)&vtx, NIL(char *)) {
      nextState = (Ltl_AutomatonNode_t *) vtx->user_data;

      if(node != nextState){
        if (!mdd_is_tautology(mdd_and(node->Encode, nextState->Encode, 1,1),0)){
          printf("n%d intersects n%d\n", node->index, nextState->index);
          if(newVar == NULL){
            newVar = bdd_create_variable(manager);
            /*node->Encode = bdd_and(node->Encode, newVar, 1, 1);*/
          }
          nextState->Encode = bdd_and(nextState->Encode, bdd_not(newVar), 1, 1);
          node->Encode = bdd_and(node->Encode, bdd_not(nextState->Encode), 1, 1);
        }
      }
    }
  }
#endif
  
} /* BmcAutEncodeAutomatonStates2() */

void
BmcAutEncodeAutomatonStates3(
  Ntk_Network_t   *network,
  Ltl_Automaton_t *automaton)
{
  mdd_manager         *manager = Ntk_NetworkReadMddManager(network);
  lsGen               lsGen;
  st_generator        *stGen, *stGen1;
  vertex_t            *vtx, *vtx1;
  Ltl_AutomatonNode_t *node, *node1;
  Ctlsp_Formula_t     *F;
  bdd_t               *label;
  
  int                 i;
  int                 noOfStates=0;
  int                 noOfBits;
  array_t             *varArray = array_alloc(bdd_t*,0);

  /*
    Build the bdd for the labels of each automaton node.
   */
  foreach_vertex(automaton->G, lsGen, vtx) {
    node = (Ltl_AutomatonNode_t *) vtx->user_data;
    if (node->Labels) {
      noOfStates++;
      label =  bdd_one(manager);
      for (i=0; i<array_n(automaton->labelTable); i++) {
        if (LtlSetGetElt(node->Labels, i)) {
          F = array_fetch(Ctlsp_Formula_t *, automaton->labelTable, i); 
          label = bdd_and(label, BmcAutBuildMddForPropositionalFormula(network, automaton, F), 1, 1);
        }
      }
      node->Encode = label;
    }
  }

  st_foreach_item(automaton->Init, stGen, &vtx, NULL) {
    node = (Ltl_AutomatonNode_t *) vtx->user_data;
    st_foreach_item(automaton->Init, stGen1, &vtx1, NULL) {
      node1 = (Ltl_AutomatonNode_t *) vtx1->user_data;
      if(node != node1){
        if(mdd_equal(node->Encode, mdd_one(manager)) && !mdd_equal(node1->Encode, mdd_one(manager))){
              node->Encode = bdd_not(node1->Encode);
        } else
          if(mdd_equal(node1->Encode, mdd_one(manager)) && !mdd_equal(node->Encode, mdd_one(manager))){
            node1->Encode = bdd_not(node->Encode);
          }
      }
    }
  }

  noOfBits = NoOfBitEncode(noOfStates);
  for(i=0; i< noOfBits; i++){ 
    array_insert_last(bdd_t*, varArray, bdd_create_variable(manager));
  }
  i=0;
  foreach_vertex(automaton->G, lsGen, vtx) {
    node = (Ltl_AutomatonNode_t *) vtx->user_data;
    if (node->Labels) {
      node->Encode = bdd_and(node->Encode, encodeOfInteger(manager, varArray, i), 1, 1);
      i++;
    }
  }
} /* BmcAutEncodeAutomatonStates3() */


void
BmcAutBuildTransitionRelation(
  Ntk_Network_t   *network,
  Ltl_Automaton_t *automaton)
{
  mdd_manager         *manager = Ntk_NetworkReadMddManager(network);
  lsGen               lsGen;
  st_generator        *stGen;
  vertex_t            *vtx, *vtx1;
  Ltl_AutomatonNode_t *state, *nextState;
 
  
  
  bdd_t               *nextStateBdd, *transitionRelation;
  bdd_t               *initialState, *fairSet, *fairState;
  int                 i;
  bdd_t               *bddVar;
  st_table            *nextStates;
  var_set_t           *psSupport, *nsSupport;
  st_table            *FairSet = 0;
  array_t             *fairSetArray;

  /*
    psNsTable  (Bdd Id, bdd_t*)
   */
  st_table            *psNsTable = st_init_table(st_numcmp, st_numhash);
  /*
    nsPsTable  (BDD Id, BDD Id)
   */
  st_table            *nsPsTable = st_init_table(st_numcmp, st_numhash);

  boolean             isComplemented;
  int                 nodeIndex;
  
  /*
    Initialization
   */
  transitionRelation = bdd_zero(manager);

  /*
    Build the transition relation 
   */
  foreach_vertex(automaton->G, lsGen, vtx) {
    state = (Ltl_AutomatonNode_t *) vtx->user_data;
    /*
      support is the set of the bddId of the bdd node in the support of the bdd function. 
    */
    psSupport = bdd_get_support(state->Encode);
    for(i=0; i<psSupport->n_elts; i++) {
      if (var_set_get_elt(psSupport, i) == 1) {
        /*
          i is the bdd Id of the variable in the support of the function.
        */
        if (!st_lookup(psNsTable, (char *)(long) i, NULL)){
          bddVar =  bdd_create_variable(manager);
          nodeIndex = bdd_node_read_index(bdd_get_node(bddVar, &isComplemented));
          st_insert(psNsTable, (char *) (long) i,         (char *) bddVar);
          st_insert(nsPsTable, (char *) (long) nodeIndex, (char *) (long)i);
        }
      }
    }
    /*
      Get the next states.
     */
    nextStates = AutomatonVertexGetImg(automaton->G, vtx);
    st_foreach_item(nextStates, stGen, &vtx1, NULL) {
      nextState = (Ltl_AutomatonNode_t *) vtx1->user_data;

      nextStateBdd = bdd_dup(nextState->Encode);
      nsSupport = bdd_get_support(nextStateBdd);
      for(i=0; i<nsSupport->n_elts; i++) {
        if (var_set_get_elt(nsSupport, i) == 1) {
          bdd_t *tmp;

          if (!st_lookup(psNsTable, (char *)(long)i, &bddVar)){
            bddVar =  bdd_create_variable(manager);
            nodeIndex = bdd_node_read_index(bdd_get_node(bddVar, &isComplemented));
            st_insert(psNsTable, (char *) (long) i,         (char *) bddVar);
            st_insert(nsPsTable, (char *) (long) nodeIndex, (char *) (long)i);
          }       
          tmp = nextStateBdd;
          nextStateBdd = bdd_compose(nextStateBdd, bdd_get_variable(manager, i), bddVar);
          bdd_free(tmp);
        }
      }
      transitionRelation = bdd_or(transitionRelation, bdd_and(state->Encode, nextStateBdd,1 ,1) ,1 ,1);
      
    } /* for each next states*/
  } /* for each present state */

  fairSetArray = array_alloc(bdd_t*, 0);
  fairSet = 0;
  if (lsLength(automaton->Fair) != 0) {
    fairSet = bdd_zero(manager);
    lsForEachItem(automaton->Fair, lsGen, FairSet) {
      fairState = bdd_zero(manager);
      st_foreach_item(FairSet, stGen, &vtx, NULL) {
        state = (Ltl_AutomatonNode_t *) vtx->user_data;
        fairState = bdd_or(fairState, state->Encode,1,1);
      }
      array_insert_last(bdd_t*, fairSetArray, fairState); 
      fairSet = bdd_or(fairSet, fairState,1,1);
    }
  }
  initialState = bdd_zero(manager);
  st_foreach_item(automaton->Init, stGen, &vtx, NULL) {
    state = (Ltl_AutomatonNode_t *) vtx->user_data;
    initialState = bdd_or(initialState, state->Encode, 1, 1);
  }
  automaton->transitionRelation  = transitionRelation;
  automaton->initialStates       = initialState;
  automaton->fairSets            = fairSet;
  automaton->psNsTable           = psNsTable;
  automaton->nsPsTable           = nsPsTable;
  automaton->fairSetArray        = fairSetArray;
  
} /* BmcAutBuildTransitionRelation() */


mdd_t *
BmcAutBuildMddForPropositionalFormula(
   Ntk_Network_t   *network,
   Ltl_Automaton_t *automaton,
   Ctlsp_Formula_t *formula)
{
  mdd_manager     *manager = Ntk_NetworkReadMddManager(network);
  mdd_t           *left, *right, *result;
  

  if (formula == NIL(Ctlsp_Formula_t)) {
    return NIL(mdd_t);
  }
  if (formula->type == Ctlsp_TRUE_c){
    return bdd_one(manager);
  }
  if (formula->type == Ctlsp_FALSE_c){
    return  mdd_zero(manager);
  }
  
  if (!Ctlsp_isPropositionalFormula(formula)) {
    (void) fprintf(vis_stderr, "bmc error: Only propositional formula can be converted to bdd \n");
    fprintf(vis_stdout, "\nFormula: ");
    Ctlsp_FormulaPrint(vis_stdout, formula);
    fprintf(vis_stdout, "\n");
    return NIL(mdd_t);
  }
  /*
    Atomic proposition.
   */
  if (formula->type == Ctlsp_ID_c){
    int       is_complemented;
    bdd_node  *funcNode;
    
    result   =  BmcModelCheckAtomicFormula(Fsm_NetworkReadOrCreateFsm(network), formula);
    funcNode = bdd_get_node(result, &is_complemented);
    if(is_complemented){
      funcNode = bdd_not_bdd_node(funcNode);
    }
    return result;
  }
  /*
    right can be NIL(mdd_t) for unery operators, but left can't be  NIL(mdd_t)
   */
  left  = BmcAutBuildMddForPropositionalFormula(network, automaton, formula->left);
  if (left == NIL(mdd_t)){
    return NIL(mdd_t);
  }  
  right = BmcAutBuildMddForPropositionalFormula(network, automaton, formula->right);
  /*assert(right !=  NIL(mdd_t)); */
  switch(formula->type) {
    case Ctlsp_NOT_c:
      result = mdd_not(left);
      break;
    case Ctlsp_OR_c:
      result = mdd_or(left, right, 1, 1);
      break;
    case Ctlsp_AND_c:
      result = mdd_and(left, right, 1, 1);
      break;
    case Ctlsp_THEN_c:
      result = mdd_or(left, right, 0, 1); 
      break;
    case Ctlsp_EQ_c:
      result = mdd_xnor(left, right);
      break;
    case Ctlsp_XOR_c:
      result = mdd_xor(left, right);
      break;
  default:
    /*
      return NIL(mdd_t) if the type is not supported
     */
    fail("Unexpected type");
  }
  return result;
}

int 
BmcAutGenerateCnfForBddOffSet(
   bdd_t          *function,
   int             current,
   int             next,
   BmcCnfClauses_t *cnfClauses,
   st_table        *nsPsTable)
{
  bdd_manager *bddManager = bdd_get_manager(function);
  bdd_node    *node, *funcNode;
  int         is_complemented;
  bdd_gen     *gen;
  int         varIndex; 
  array_t     *tmpClause;
  array_t     *cube;
  int         i, value;
  int         state = current;
  bdd_t       *bddFunction;
  bdd_t       *newVar;

  int         total=0, ndc=0;
  float       per;

  if (function == NULL){
    return 0;
  }
 
  funcNode = bdd_get_node(function, &is_complemented);
 
  if (bdd_is_constant(funcNode)){
    if (is_complemented){
      /* add an empty clause to indicate FALSE (un-satisfiable)*/
      BmcAddEmptyClause(cnfClauses);
    }
    /*bdd_free(bddFunction);
      bdd_free(newVar);*/
    return 0;
  }

  newVar = bdd_create_variable(bddManager);
  bddFunction = bdd_xnor(newVar, function);
  bddFunction = bdd_not(bddFunction);

  foreach_bdd_cube(bddFunction, gen, cube){
    tmpClause = array_alloc(int,0);
    arrayForEachItem(int, cube, i, value) {
      total++;
      if (value != 2){
        int j;

        ndc++;
        /*
          If the BDD varaible is a next state varaible, we use the corresponding
          current state varaible but with next state index.
         */
        
        if (nsPsTable && st_lookup_int(nsPsTable, (char *)(long)i, &j)){
          node = bdd_bdd_ith_var(bddManager, j);
          state = next;
        } else {
          node = bdd_bdd_ith_var(bddManager, i);
          state = current;
        }
        varIndex  = BmcGetCnfVarIndexForBddNode(bddManager, bdd_regular(node), state, cnfClauses);
        if (value == 1){
          varIndex = -varIndex; 
        }
        array_insert_last(int, tmpClause, varIndex);
      }
    }
    BmcCnfInsertClause(cnfClauses, tmpClause);
    array_free(tmpClause);
  }/* foreach_bdd_cube() */
  varIndex  = BmcGetCnfVarIndexForBddNode(bddManager,
                                       bdd_regular(bdd_get_node(newVar, &is_complemented)),
                                       current, cnfClauses);
  per = ((float) ((float)ndc/(float)total))*100; 
  return (varIndex);
} /* BmcAutGenerateCnfForBddOffSet() */


BmcCheckForTermination_t *
BmcAutTerminationAlloc(
  Ntk_Network_t   *network,
  Ctlsp_Formula_t *ltlFormula,
  array_t         *constraintArray)
{
  BmcCheckForTermination_t  *result = ALLOC(BmcCheckForTermination_t, 1);
  Ltl_Automaton_t           *automaton;
  LtlMcOption_t             *ltlOptions = LtlMcOptionAlloc();
  
  if (!result){
    return result;
  }
  /*
    Build the Buechi Automaton for the negation of the LTL formula.
  */
  ltlOptions->algorithm    = Ltl2Aut_WRING_c;
  ltlOptions->rewriting    = TRUE;
  ltlOptions->prunefair    = TRUE;
  ltlOptions->iocompatible = TRUE;
  ltlOptions->directsim    = TRUE;
  ltlOptions->reversesim   = TRUE;
  ltlOptions->verbosity    = McVerbosityNone_c;
  ltlOptions->noStrengthReduction = 1;
  
  automaton  = LtlMcFormulaToAutomaton(network, ltlFormula, ltlOptions, 0);
  assert(automaton != NIL(Ltl_Automaton_t));
  
  /*BmcAutEncodeAutomatonStates(network, automaton); */
  /*mcAutEncodeAutomatonStates2(network, automaton);*/
  BmcAutEncodeAutomatonStates3(network, automaton);
  BmcAutBuildTransitionRelation(network, automaton);
    
  LtlMcOptionFree(ltlOptions);

  result->k = 0;
  result->m = -1;
  result->n = -1;
  result->checkLevel = 0;
  result->action = 0;
  result->automaton = automaton;

  result->externalConstraints  = NIL(Ctlsp_Formula_t);
  if(constraintArray != NIL(array_t)){
    Ctlsp_Formula_t *formula1, *formula2;
    int              j;
    
    formula1 = NIL(Ctlsp_Formula_t);
    arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula2) {
      formula2 = Ctlsp_FormulaDup(formula2);
      if(formula1 == NIL(Ctlsp_Formula_t)) {
        formula1 = formula2;
      } else {
        formula1 =  Ctlsp_FormulaCreate(Ctlsp_OR_c, formula1, formula2);
      }
    }
    result->externalConstraints = formula1;
  }
  result->internalConstraints = automaton->fairSets;
  return result;
}

Ltl_Automaton_t *
BmcAutLtlToAutomaton(
  Ntk_Network_t   *network,
  Ctlsp_Formula_t *ltlFormula)
{
  Ltl_Automaton_t  *automaton;
  LtlMcOption_t    *ltlOptions = LtlMcOptionAlloc();
  
  /*
    Build the Buechi Automaton for the negation of the LTL formula.
  */
  ltlOptions->algorithm    = Ltl2Aut_WRING_c;
  ltlOptions->rewriting    = TRUE;
  ltlOptions->prunefair    = TRUE;
  ltlOptions->iocompatible = TRUE;
  ltlOptions->directsim    = TRUE;
  ltlOptions->reversesim   = TRUE;
  ltlOptions->verbosity    = McVerbosityNone_c;
  ltlOptions->noStrengthReduction = 1;
  
  automaton  = LtlMcFormulaToAutomaton(network, ltlFormula, ltlOptions, 0);
  assert(automaton != NIL(Ltl_Automaton_t));
 
  return automaton;
}


void
BmcAutTerminationFree(
  BmcCheckForTermination_t *result)
{
  LtlTableau_t    *tableau;
  Ltl_Automaton_t *automaton = result->automaton;
    
  tableau = automaton->tableau; 
  Ltl_AutomatonFree((gGeneric) automaton);
  LtlTableauFree(tableau);
  if(result->externalConstraints  != NIL(Ctlsp_Formula_t)){
    Ctlsp_FormulaFree(result->externalConstraints);
  }
  
  FREE(result);
}


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/

static st_table *
AutomatonVertexGetImg(
  graph_t *G,
  vertex_t *vtx)
{
  lsList Img;
  lsGen lsgen;
  edge_t *e;
  vertex_t *s;
  st_table *uTable;

  Img = g_get_out_edges(vtx);

  uTable = st_init_table(st_ptrcmp, st_ptrhash);
  lsForEachItem(Img, lsgen, e) {
    s = g_e_dest(e);
    st_insert(uTable, (char *) s, (char *) s);
  }

  return uTable;
}

static st_table *
AutomatonVertexGetPreImg(
  graph_t *G,
  vertex_t *vtx)
{
  lsList preImg;
  lsGen lsgen;
  edge_t *e;
  vertex_t *s;
  st_table *uTable;

  preImg = g_get_in_edges(vtx);

  uTable = st_init_table(st_ptrcmp, st_ptrhash);
  lsForEachItem(preImg, lsgen,  e) {
    s = g_e_source(e);
    st_insert(uTable, (char *) s, (char *) s);
  }
  
  return uTable;
}

static int
stIntersect(
  st_table *tbl1,
  st_table *tbl2)
{
  st_generator *stgen;
  vertex_t *vtx;

  st_foreach_item(tbl1, stgen, &vtx, NULL) {
    if (st_is_member(tbl2,(char *)vtx)) {
      st_free_gen(stgen);
      return 1;
    }
  }
  return 0;
}

static int
NoOfBitEncode(
   int n)
{
    int i = 0;
    int j = 1;

    if (n < 2) return 1; /* Takes care of value <= 1 */

    while (j < n) {
        j = j * 2;
        i++;
    }
    return i;
}

static bdd_t *
encodeOfInteger(
  mdd_manager *manager,
  array_t *varArray,
  int val)
{
  int i;
  bdd_t *returnValue =  mdd_one(manager);
  int tmp = val;
  bdd_t  *var;

  for(i=0; i< array_n(varArray); i++){
    var = array_fetch(bdd_t*, varArray, i);
    if(tmp%2 == 0){
      returnValue = bdd_and(returnValue, var, 1, 0); 
    } else {
      returnValue = bdd_and(returnValue, var, 1, 1);
    }
    tmp = tmp / 2;
  }
  return returnValue;
}