/**CFile*********************************************************************** FileName [bmcAutUtil.c] PackageName [bmc] Synopsis [Utility file for BMC_Automaton] Author [Mohammad Awedh] Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.] ******************************************************************************/ #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 */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* 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); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Encode the states of the Automaton.] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ 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; ilabelTable); 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() */ /**Function******************************************************************** Synopsis [Encode the states of the Automaton.] Description [The labels of each node in the automaton are propositional and are asserted by state variables in the original model. So, we uses these labels as part of the state encoding of the automaton. If two nodes cannot be uniquely specified, then we use new variables] SideEffects [] SeeAlso [] ******************************************************************************/ 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; ilabelTable); 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() */ /**Function******************************************************************** Synopsis [Encode the states of the Automaton.] Description [The labels of each node in the automaton are propositional and are asserted by state variables in the original model. So, we uses these labels as part of the state encoding of the automaton. If two nodes cannot be uniquely specified, then we use new variables] SideEffects [] SeeAlso [] ******************************************************************************/ 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; ilabelTable); 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() */ /**Function******************************************************************** Synopsis [Build BDD of the transition relation of the Automaton.] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ 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; in_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; in_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() */ /**Function******************************************************************** Synopsis [Build MDD for a propositional formula.] Description [Build MDD for a propositional formula. Returns NIL if the conversion fails. The calling application is responsible for freeing the returned MDD.] SideEffects [] SeeAlso [] ******************************************************************************/ 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; } /**Function******************************************************************** Synopsis [Generate CNF for a given BDD function.] Description [Generate CNF for a BDD function. This function first negates the BDD function, and then generates the CNF corresponding to the OFF-set of the negated function. If the BDD node is a next state variable, we use the BDD index of the present state variable corresponding to this variable. We could do this by searching the nsPSTable. If trans ==1, this function generates a CNF for a transition from current state to next state, otherwise it generates CNF for NO transition. The function calling this function must add a unit clause to set the returned value to positive (for function to be true) or negative (for function to be false). ] SideEffects [] SeeAlso [] ******************************************************************************/ 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() */ /**Function******************************************************************** Synopsis [Alloc Memory for BmcCheckForTermination_t] SideEffects [] SeeAlso [] ******************************************************************************/ 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; } /**Function******************************************************************** Synopsis [Convert LTL to Automaton] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ 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; } /**Function******************************************************************** Synopsis [Free BmcCheckForTermination_t.] SideEffects [] SeeAlso [] ******************************************************************************/ 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 */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Return the image of the given vertex in the hash table.] SideEffects [Result should be freed by the caller.] ******************************************************************************/ 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; } /**Function******************************************************************** Synopsis [Return the pre-image of the given vertex in the hash table.] SideEffects [Result should be freed by the caller.] ******************************************************************************/ 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; } /**Function******************************************************************** Synopsis [Return 1 if tbl1 and tbl2 two intersects.] SideEffects [] ******************************************************************************/ 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; } /**Function******************************************************************** Synopsis [Returns no. of Bit encoding needed for n] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ 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; } /**Function******************************************************************** Synopsis [Returns no. of Bit encoding needed for n] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ 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; }