source: vis_dev/vis-2.3/src/bmc/bmcUtil.c @ 33

/**CFile***********************************************************************

  FileName    [bmcUtil.c]

  PackageName [bmc]

  Synopsis    [Utilities for BMC package]

  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 "bmcInt.h"
#include "sat.h"
#include "baig.h"

static char rcsid[] UNUSED = "$Id: bmcUtil.c,v 1.82 2010/04/10 04:07:06 fabio Exp $";

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

#define MAX_LENGTH 320 /* Max. length of a string while reading a file     */

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


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


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


/**AutomaticStart*************************************************************/

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

static int StringCheckIsInteger(char *string, int *value);
static int nameCompare(const void * name1, const void * name2);
static void printValue(mAig_Manager_t *manager, Ntk_Network_t *network, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *varNames, st_table *resultTable, int state, int *prevValue);
static void printValueAiger(mAig_Manager_t *manager, Ntk_Network_t *network, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *varNames, st_table *resultTable, int state, int *prevValue);
static void printValueAigerInputs(mAig_Manager_t *manager, Ntk_Network_t *network, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *varNames, st_table *resultTable, int state, int *prevValue);

/**AutomaticEnd***************************************************************/

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


/**Function********************************************************************

  Synopsis [Compute cube that is close to target states.]

  SideEffects []

******************************************************************************/
mdd_t *
Bmc_ComputeCloseCube( 
  mdd_t *states,
  mdd_t *target,
  int   *dist,
  Fsm_Fsm_t *modelFsm)
{
  array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
  mdd_manager *mddMgr = Ntk_NetworkReadMddManager( Fsm_FsmReadNetwork( modelFsm ) ); 
  mdd_t *result = BmcComputeCloseCube( states, target, dist, PSVars, mddMgr );

  return result;
}

/**Function********************************************************************

  Synopsis [Build multi-valued function for a given node.]

  SideEffects [The mvf of this node is a function of combinational input
  nodes.]

******************************************************************************/
MvfAig_Function_t *
Bmc_NodeBuildMVF(
  Ntk_Network_t *network,
  Ntk_Node_t    *node)
{
  MvfAig_Function_t * MvfAig; 
  lsGen tmpGen;
  Ntk_Node_t *tmpNode;
  array_t    *mvfArray;
  array_t    *tmpRoots = array_alloc(Ntk_Node_t *, 0);
  st_table   *tmpLeaves = st_init_table(st_ptrcmp, st_ptrhash);
  array_insert_last(Ntk_Node_t *, tmpRoots, node);

  Ntk_NetworkForEachCombInput(network, tmpGen, tmpNode) {
    st_insert(tmpLeaves, (char *) tmpNode, (char *) ntmaig_UNUSED);
  }

  mvfArray = ntmaig_NetworkBuildMvfAigs(network, tmpRoots, tmpLeaves);
  MvfAig   = array_fetch(MvfAig_Function_t *, mvfArray, 0);
  array_free(tmpRoots);
  st_free_table(tmpLeaves);
  array_free(mvfArray);
  return MvfAig;
}


/**Function********************************************************************

  Synopsis [Returns MvfAig corresponding to a node; returns NIL if node not in
  table.]

  SideEffects [None]

******************************************************************************/
MvfAig_Function_t *
Bmc_ReadMvfAig(
  Ntk_Node_t * node,
  st_table   * nodeToMvfAigTable)
{
  MvfAig_Function_t *result;
  if (st_lookup(nodeToMvfAigTable, node, &result)){
     return result;
  }
  return NIL(MvfAig_Function_t);
}


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

/**Function********************************************************************

  Synopsis    [Evaluate states satisfying X target]

  Description [Evaluate states satisfying X target.]

  SideEffects []

******************************************************************************/
mdd_t *
BmcFsmEvaluateX(
  Fsm_Fsm_t *modelFsm,
  mdd_t     *targetMdd)
{
  mdd_t *fromLowerBound;
  mdd_t *fromUpperBound;
  mdd_t *result;
  Img_ImageInfo_t * imageInfo;
  mdd_t           *careStates;
  array_t         *careStatesArray = array_alloc(array_t *, 0);  

  imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);

  /*
   * The lower bound is the conjunction of the fair states,
   * and the target states.
   */
  fromLowerBound = mdd_dup(targetMdd);
  /*
   * The upper bound is the same as the lower bound.
   */
  fromUpperBound = mdd_dup(fromLowerBound);
  /*
    careSet is the set of all unreachabel states.
  */
  careStates = mdd_one(Fsm_FsmReadMddManager(modelFsm));
  array_insert(mdd_t *, careStatesArray, 0, careStates);
  
  result = Img_ImageInfoComputePreImageWithDomainVars(imageInfo,
                fromLowerBound, fromUpperBound, careStatesArray);
  mdd_free(fromLowerBound);
  mdd_free(fromUpperBound);
  
  return result;

} /* BmcFsmEvaluateX */


/**Function********************************************************************

  Synopsis [Compute cube that is close to target states. Support
  is an array of mddids representing the total support; that is, all
  the variables on which aSet may depend. It dos the function only
  if CUDD is the BDD package.]

  SideEffects []

******************************************************************************/
mdd_t *
BmcComputeCloseCube(
  mdd_t *aSet,
  mdd_t *target,
  int   *dist,
  array_t *Support,
  mdd_manager *mddMgr)
{
  if (bdd_get_package_name() == CUDD && target != NIL(mdd_t)) {
    mdd_t *range;             /* range of Support             */
    mdd_t *legalSet;          /* aSet without the don't cares */
    mdd_t *closeCube;

    
    /* Check that support of set is contained in Support. 
    assert(SetCheckSupport(aSet, Support, mddMgr)); */ 
    assert(!mdd_is_tautology(aSet, 0));
    range      = mdd_range_mdd(mddMgr, Support);
    legalSet   = bdd_and(aSet, range, 1, 1);
    mdd_free(range);
    closeCube = mdd_closest_cube(legalSet, target, dist);

    mdd_free(legalSet);
    
    return closeCube;
  } else {
    return aSet;
    /*return BMC_ComputeAMinterm(aSet, Support, mddMgr);*/
  }/* if CUDD */

} /* BmcComputeCloseCube */


/**Function********************************************************************

  Synopsis [Build AND/INV graph for intial states]

  Description [Build AND/INV graph for intial states. Returns bAig Id
  of the bAig Function that represents the intial states.

  The initial states are computed as follows. For each latch i, the relation
  (x_i = g_i(u)) is built, where x_i is the present state variable of latch i,
  and g_i(u) is the multi-valued initialization function of latch i, in terms
  of the input variables u.  These relations are then conjuncted.
  ]

  SideEffects []

  SeeAlso     []
  
******************************************************************************/
mAigEdge_t
BmcCreateMaigOfInitialStates(
  Ntk_Network_t   *network,
  st_table        *nodeToMvfAigTable,
  st_table        *CoiTable)
{
  mAig_Manager_t  *manager = Ntk_NetworkReadMAigManager(network);
  st_generator    *stGen;
  
  Ntk_Node_t         *latch, *latchInit;
  MvfAig_Function_t  *initMvfAig, *latchMvfAig;
 
  bAigEdge_t         resultAnd = bAig_One;
  bAigEdge_t         resultOr;
  int                i;

  st_foreach_item(CoiTable, stGen, &latch, NULL) {
    
    
    latchInit  = Ntk_LatchReadInitialInput(latch);
    
    /* Get the multi-valued function for each node*/
    initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
    if (initMvfAig ==  NIL(MvfAig_Function_t)){
      (void) fprintf(vis_stdout, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchInit));
      return bAig_NULL;
   }
   latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
   if (latchMvfAig ==  NIL(MvfAig_Function_t)){
     latchMvfAig = Bmc_NodeBuildMVF(network, latch);
     array_free(latchMvfAig);
     latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
   }
   resultOr  = bAig_Zero;
   for(i=0; i<array_n(initMvfAig); i++){
     resultOr = mAig_Or(manager, resultOr,
                        bAig_Eq(manager,
                                bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(initMvfAig,  i)),
                                bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i))
                                )
                        );
     if(resultOr == bAig_One){
       break;
     }
   }
   resultAnd = mAig_And(manager, resultAnd, resultOr);
   if(resultAnd == bAig_Zero){
     break;
   }
  }/* for each latch*/

  return resultAnd;
}


/**Function********************************************************************

  Synopsis [Builds AND/INVERTER graph (aig) for a propsitional formula]

  Description [Builds AND/INVERTER graph for a propsitional formula.
  Returns bAig ID of the function that is quivalent to the propositional
  fomula]

  SideEffects []

  SeeAlso     []

******************************************************************************/

mAigEdge_t
BmcCreateMaigOfPropFormula(
  Ntk_Network_t   *network,
  mAig_Manager_t  *manager,
  Ctlsp_Formula_t *formula)
{
  mAigEdge_t left, right, result;

  if (formula == NIL(Ctlsp_Formula_t)) {
    return mAig_NULL;
  }
  if (formula->type == Ctlsp_TRUE_c){
    return mAig_One;
  }
  if (formula->type == Ctlsp_FALSE_c){
    return mAig_Zero;
  }
  
  assert(Ctlsp_isPropositionalFormula(formula));
  
  if (formula->type == Ctlsp_ID_c){
      char *nodeNameString  = Ctlsp_FormulaReadVariableName(formula);
      char *nodeValueString = Ctlsp_FormulaReadValueName(formula);
      Ntk_Node_t *node      = Ntk_NetworkFindNodeByName(network, nodeNameString);

      Var_Variable_t *nodeVar;
      int             nodeValue;

      MvfAig_Function_t  *tmpMvfAig;
      st_table           *nodeToMvfAigTable; /* maps each node to its mvfAig */
      
      if (node == NIL(Ntk_Node_t)) {
          (void) fprintf(vis_stderr, "bmc error: Could not find node corresponding to the name\t %s\n", nodeNameString);
          return mAig_NULL;
      }
      nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
      if (nodeToMvfAigTable == NIL(st_table)){
         (void) fprintf(vis_stderr, "bmc error: please run build_partiton_maigs first");
         return mAig_NULL;
      }
      tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
      if (tmpMvfAig ==  NIL(MvfAig_Function_t)){
          tmpMvfAig = Bmc_NodeBuildMVF(network, node);
          array_free(tmpMvfAig);
          tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
      }
      nodeVar = Ntk_NodeReadVariable(node);
      if (Var_VariableTestIsSymbolic(nodeVar)) {
        nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
        if ( nodeValue == -1 ) {
          (void) fprintf(vis_stderr, "Value specified in RHS is not in domain of variable\n");
          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
          return mAig_NULL;
        }
      }
      else { 
        int check;    
         check = StringCheckIsInteger(nodeValueString, &nodeValue);
         if( check == 0 ) {
          (void) fprintf(vis_stderr,"Illegal value in the RHS\n");
          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
          return mAig_NULL;
         }
         if( check == 1 ) {
          (void) fprintf(vis_stderr,"Value in the RHS is out of range of int\n");
          (void) fprintf(vis_stderr,"%s = %s", nodeNameString, nodeValueString);
          return mAig_NULL;
         }
         if ( !(Var_VariableTestIsValueInRange(nodeVar, nodeValue))) {
          (void) fprintf(vis_stderr,"Value specified in RHS is not in domain of variable\n");
          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
          return mAig_NULL;

         }
      }
      result = MvfAig_FunctionReadComponent(tmpMvfAig, nodeValue);
      return bAig_GetCanonical(manager, result);
  }
  /*
    right can be mAig_NULL for unery operators, but left can't be mAig_Null
   */
  left  = BmcCreateMaigOfPropFormula(network, manager, formula->left);
  if (left == mAig_NULL){
    return mAig_NULL;
  }  
  right = BmcCreateMaigOfPropFormula(network, manager, formula->right);

  switch(formula->type) {
    case Ctlsp_NOT_c:
      result = mAig_Not(left);
      break;
    case Ctlsp_OR_c:
      result = mAig_Or(manager, left, right);
      break;
    case Ctlsp_AND_c:
      result = mAig_And(manager, left, right);
      break;
    case Ctlsp_THEN_c:
      result = mAig_Then(manager, left, right); 
      break;
    case Ctlsp_EQ_c:
      result = mAig_Eq(manager, left, right);
      break;
    case Ctlsp_XOR_c:
      result = mAig_Xor(manager, left, right);
      break;
    default:
      fail("Unexpected LTL type");
  }
  return result;
} /* BmcCreateMaigOfPropFormula */

/**Function********************************************************************

  Synopsis [Build MDD for safety property in form of AG(p).  Where p is either a
  propositional formula or a path formula contains only the temporal property X.]

  Description [Build MDD for a safety formula. Returns NIL if the conversion
  fails. The calling application is responsible for freeing the returned MDD.]

  SideEffects []

  SeeAlso     [Ctlsp_FormulaReadClass]

******************************************************************************/
mdd_t *
BmcCreateMddOfSafetyProperty(
  Fsm_Fsm_t       *fsm,
  Ctlsp_Formula_t *formula)
{
 
  mdd_manager   *manager = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(fsm));
  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 0
  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);
  }
#endif
  /*
    Atomic proposition.
   */
  if (formula->type == Ctlsp_ID_c){
    return BmcModelCheckAtomicFormula(fsm, formula);
  }
  /*
    right can be NIL(mdd_t) for unery operators, but left can't be  NIL(mdd_t)
   */
  left  = BmcCreateMddOfSafetyProperty(fsm, formula->left);
  if (left == NIL(mdd_t)){
    return NIL(mdd_t);
  }  
  right = BmcCreateMddOfSafetyProperty(fsm, 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;
  case Ctlsp_X_c:
      result = BmcFsmEvaluateX(fsm, left);
      break;
  default:
    /*
      return NIL(mdd_t) if the type is not supported
     */
     return NIL(mdd_t);
     /*
      fail("Unexpected type");
     */
  }
  return result;
}


/**Function********************************************************************

  Synopsis    [Generate the CNF formula of a given function represented by
               AND/INVERTER graph]

  Description [Generate an array of clausese for a function represented in
  AND/INVERETER graph structure. 
  
  the CNF formula of node to the output file specifies by cnfFile.
               It stores CNF index for each node in the cnfIndexTable. The generated CNF
               is in dimacs format.
               It is an error to call this function on a constand zero/one node.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
BmcGenerateCnfFormulaForAigFunction(
   bAig_Manager_t *manager,
   bAigEdge_t      node,
   int             k,
   BmcCnfClauses_t *cnfClauses)
{
  int        leftIndex, rightIndex, nodeIndex;
  array_t    *clause;

  assert( (node != bAig_One) && (node != bAig_Zero));
  
  if(bAig_IsInverted(node)){
    /*
      The generated clauses are in dimacs formate that uses negative number to indicate complement
     */
    return -1*BmcGenerateCnfFormulaForAigFunction(manager, bAig_NonInvertedEdge(node), k, cnfClauses);
  }
  if (BmcCnfReadOrInsertNode(cnfClauses, bAig_NodeReadName(manager, node), k, &nodeIndex)){
    return nodeIndex;
  }
  if (bAig_isVarNode(manager, node)){
    return nodeIndex;
  }
  leftIndex  = BmcGenerateCnfFormulaForAigFunction(manager,
                                                   bAig_GetCanonical(manager, leftChild(node)),
                                                   k, cnfClauses);
  rightIndex = BmcGenerateCnfFormulaForAigFunction(manager,
                                                   bAig_GetCanonical(manager, rightChild(node)),
                                                   k, cnfClauses);
  clause  = array_alloc(int, 3);
  array_insert(int, clause, 0, -leftIndex );
  array_insert(int, clause, 1, -rightIndex);
  array_insert(int, clause, 2,  nodeIndex );
  BmcCnfInsertClause(cnfClauses, clause);
  array_free(clause);
  
  clause  = array_alloc(int, 2);
  array_insert(int, clause, 0,  leftIndex);
  array_insert(int, clause, 1, -nodeIndex);
  BmcCnfInsertClause(cnfClauses, clause);
  array_free(clause);
  
  clause  = array_alloc(int, 2);
  array_insert(int, clause, 0,  rightIndex);
  array_insert(int, clause, 1, -nodeIndex);
  BmcCnfInsertClause(cnfClauses, clause);  
  array_free(clause);
  
  return(nodeIndex);
}

/**Function********************************************************************

  Synopsis [Generate CNF for bdd function]

  Description [
    The function of each node f = var*thenChild + -var*elseChild
    var is the variable at this node.
    For each node there are four cases:
      - both childeren are constant -> do nothing.
      - the then child is constant 1 -> generate clauses for f = var + elseChild.
      - the else child is constant 0 -> generate clauses for f = var * thenChild.
      - the else child is constant 1 -> generate clauses for f = -var + thenChild.
      - else -> generate clauses for f = var*thenChild + -var*elseChild.
  ------------------------------------------------
    function        |        clauses
  ------------------------------------------------  
    c = a*b         | (-a + -b + c)*(a + -c)*(b + -c)
    c = a+b         | (a + b + -c)*(-a + c)*(-b + c)
    f = c*a + -c*b  | (-a + -c + f)*(a + -c + -f)*
                    | (-b +  c + f)*(b +  c + -f)

  return the cnf index of the bdd function
  ]
  
  SideEffects []

  SeeAlso     []
  
******************************************************************************/
int 
BmcGenerateCnfFormulaForBdd(
   bdd_t          *bddFunction,
   int             k,
   BmcCnfClauses_t *cnfClauses)
{
  bdd_manager *bddManager = bdd_get_manager(bddFunction);
  bdd_node    *node, *thenNode, *elseNode, *funcNode;
  int         is_complemented;
  int         nodeIndex=0, thenIndex, elseIndex;
  bdd_gen     *gen;
  int         varIndex, flag; 
  array_t     *tmpClause;
  
  st_table    *bddToCnfIndexTable;
  
  bdd_t       *currentBddNode;
  int         cut = 5;
  
  if (bddFunction == NULL){
    return 0;
  }
  funcNode = bdd_get_node(bddFunction, &is_complemented);
  if (bdd_is_constant(funcNode)){
    if (is_complemented){
      /* add an empty clause to indicate FALSE (un-satisfiable)*/
      BmcAddEmptyClause(cnfClauses);
    }
    return 0;
  }
  if(bdd_size(bddFunction) <= cut){
    return BmcGenerateCnfFormulaForBddOffSet(bddFunction, k, cnfClauses);
  }
  
  bddToCnfIndexTable = st_init_table(st_numcmp, st_numhash);
  foreach_bdd_node(bddFunction, gen, node){
    if (bdd_is_constant(node)){ /* do nothing */
      continue;
    }

    /*
      bdd_size() returns 1 if bdd is constant one.
    */
    /*
      Use offset method to generate CNF if the size of the node <= cut (include the constant 1 node).
    */
    /*#if 0*/    
    if(bdd_size(currentBddNode = bdd_construct_bdd_t(bddManager, bdd_regular(node))) <= cut){
      if (bdd_size(currentBddNode) == cut){
        nodeIndex = BmcGenerateCnfFormulaForBddOffSet(currentBddNode, k, cnfClauses);
        st_insert(bddToCnfIndexTable, (char *) (long) bdd_regular(node),  (char *) (long)nodeIndex);
        continue;
      }
      continue;
    }
    /*#endif*/    
    varIndex  = BmcGetCnfVarIndexForBddNode(bddManager, bdd_regular(node), k, cnfClauses);
    nodeIndex = varIndex;
    
    thenNode = bdd_bdd_T(node);
    elseNode = bdd_bdd_E(node);

    if (!((bdd_is_constant(thenNode)) && (bdd_is_constant(elseNode)))){
      nodeIndex = cnfClauses->cnfGlobalIndex++;   /* index of the function of this node */
      
      if (bdd_is_constant(thenNode)){ /* the thenNode can be only constant one*/
        flag = st_lookup_int(bddToCnfIndexTable, bdd_regular(elseNode), &elseIndex);
        assert(flag);
        /*
          test if the elseNode is complemented arc?
        */
        if (bdd_is_complement(elseNode)){
          elseIndex = -1*elseIndex;
        }  
        BmcCnfGenerateClausesForOR(elseIndex, varIndex, nodeIndex, cnfClauses);
      } else if (bdd_is_constant(elseNode)){ /* one or zero */
        flag = st_lookup_int(bddToCnfIndexTable, bdd_regular(thenNode), &thenIndex);
        assert(flag);
        /*
          test if the elseNode is complemented arc?
        */
        if (bdd_is_complement(elseNode)){  /* Constant zero */
         BmcCnfGenerateClausesForAND(thenIndex, varIndex, nodeIndex, cnfClauses);
        } else { /* Constant one */
         BmcCnfGenerateClausesForOR(thenIndex, -varIndex, nodeIndex, cnfClauses);
        }
      } else {
        flag = st_lookup_int(bddToCnfIndexTable, bdd_regular(thenNode), &thenIndex);
        if(flag == 0){
          thenIndex = BmcGenerateCnfFormulaForBddOffSet(bdd_construct_bdd_t(bddManager, bdd_regular(thenNode)), k, cnfClauses);
          st_insert(bddToCnfIndexTable, (char *) (long) bdd_regular(thenNode),  (char *) (long)thenIndex);
        }
        /*assert(flag);*/
        
        flag = st_lookup_int(bddToCnfIndexTable, bdd_regular(elseNode), &elseIndex);
        if(flag == 0){
          elseIndex = BmcGenerateCnfFormulaForBddOffSet( bdd_construct_bdd_t(bddManager, bdd_regular(elseNode)), k, cnfClauses);
          st_insert(bddToCnfIndexTable, (char *) (long) bdd_regular(elseNode),  (char *)(long) elseIndex);
        }
        /*assert(flag);*/
        /*
          test if the elseNode is complemented arc?
        */
        if (bdd_is_complement(elseNode)){
          elseIndex = -1*elseIndex;
        }      
        tmpClause = array_alloc(int, 3);

        assert(abs(thenIndex) <= cnfClauses->cnfGlobalIndex);
        assert(abs(varIndex) <= cnfClauses->cnfGlobalIndex);
        assert(abs(nodeIndex) <= cnfClauses->cnfGlobalIndex);
          
        array_insert(int, tmpClause, 0, -thenIndex);
        array_insert(int, tmpClause, 1, -varIndex);
        array_insert(int, tmpClause, 2, nodeIndex);
        BmcCnfInsertClause(cnfClauses, tmpClause);
        
        array_insert(int, tmpClause, 0, thenIndex);
        array_insert(int, tmpClause, 1, -varIndex);
        array_insert(int, tmpClause, 2, -nodeIndex);
        BmcCnfInsertClause(cnfClauses, tmpClause);
        
        array_insert(int, tmpClause, 0, -elseIndex);
        array_insert(int, tmpClause, 1, varIndex);
        array_insert(int, tmpClause, 2, nodeIndex);
        BmcCnfInsertClause(cnfClauses, tmpClause);
        
        array_insert(int, tmpClause, 0, elseIndex);
        array_insert(int, tmpClause, 1, varIndex);
        array_insert(int, tmpClause, 2, -nodeIndex);
        BmcCnfInsertClause(cnfClauses, tmpClause);  
        
        array_free(tmpClause);
      }
    }
    st_insert(bddToCnfIndexTable, (char *) (long) bdd_regular(node),  (char *) (long) nodeIndex);
  } /* foreach_bdd_node() */
  st_free_table(bddToCnfIndexTable);
  return (is_complemented? -nodeIndex: nodeIndex);
} /* BmcGenerateCnfFormulaForBdd() */



/**Function********************************************************************

  Synopsis [Generate CNF for bdd function based on the off set of the
  bdd function]

  Description [Express the negation of bdd function in disjunctive
  normal form(DNF), and generate a clause for each disjunct in the
  DNF.]
  
  SideEffects []

  SeeAlso     []
  
******************************************************************************/
int 
BmcGenerateCnfFormulaForBddOffSet(
   bdd_t          *bddFunction,
   int             k,
   BmcCnfClauses_t *cnfClauses)
{
  bdd_manager *bddManager = bdd_get_manager(bddFunction);
  bdd_node    *node, *funcNode;
  int         is_complemented;
  bdd_gen     *gen;
  int         varIndex; 
  array_t     *tmpClause;
  array_t     *cube;
  int         i, value;
  bdd_t       *newVar;
  
  if (bddFunction == NULL){
    return 0;
  }
  /*
    Because the top node of bddFunction represents a variable in
    bddFunction, newVar is used to represent the function of
    bddFunction.  Setting the cnfIndex of newVar to 1(0) is like
    setting the function of bddFunction to 1(0).
  */
  newVar = bdd_create_variable(bddManager);
  bddFunction = bdd_xnor(newVar, bddFunction);
  funcNode = bdd_get_node(bddFunction, &is_complemented);
  if (bdd_is_constant(funcNode)){
    if (is_complemented){
      /* add an empty clause to indicate FALSE (un-satisfiable)*/
      BmcAddEmptyClause(cnfClauses);
    }
    return 0;
  }
  bddFunction = bdd_not(bddFunction);

  foreach_bdd_cube(bddFunction, gen, cube){
    tmpClause = array_alloc(int,0);
    arrayForEachItem(int, cube, i, value) {
      if (value != 2){
        node = bdd_bdd_ith_var(bddManager, i);
        varIndex  = BmcGetCnfVarIndexForBddNode(bddManager, bdd_regular(node), k, 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)),
                                       k, cnfClauses);
  return (varIndex);
} /* BmcGenerateCnfFormulaForBddOffSet() */

#if 0
/**Function********************************************************************

  Synopsis    [Generate the CNF formula of a given function represented by
               AND/INVERTER graph]

  Description [Generate an array of clausese for a function represented in
  AND/INVERETER graph structure. 
  
  the CNF formula of node to the output file specifies by cnfFile.
               It stores CNF index for each node in the cnfIndexTable. The generated CNF
               is in dimacs format.
               It is an error to call this function on a constand zero/one node.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
BmcGenerateCnfForAigFunction(
   bAig_Manager_t  *manager,
   Ntk_Network_t   *network,
   bAigEdge_t      node,
   int             k,
   BmcCnfClauses_t *cnfClauses)
{
  int        leftIndex, rightIndex, nodeIndex;
  array_t    *clause;

  if(bAig_IsInverted(node)){
    /*
      The generated clauses are in dimacs formate that uses negative number to indicate complement
     */
    return -1*BmcGenerateCnfFormulaForAigFunction(manager, bAig_NonInvertedEdge(node), k, cnfClauses);
  }
  {
    char *name   = bAig_NodeReadName(manager, node);
    char *found  = strchr(name, '=');
    
    if (found != NIL(char)){
      int value = atoi(found+1);
      int length = found-name;
      char toName[length+1];
      Ntk_Node_t *node;
      
      toName[length] = '\0';
      strncpy(toName, name, length);
      node = Ntk_NetworkFindNodeByName(network, toName);
      if ((node != NIL( Ntk_Node_t)) && Ntk_NodeTestIsLatch(node)){
        MvfAig_Function_t  *tmpMvfAig;
        st_table *nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
        bAigEdge_t mAigNode;

        if (nodeToMvfAigTable == NIL(st_table)){
          (void) fprintf(vis_stderr, "bmc error: please run build_partiton_maigs first");
          return mAig_NULL;
        }
        if (k==0){
          node = Ntk_LatchReadInitialInput(node);
        } else {
          node = Ntk_LatchReadDataInput(node);
          k--;
        }
        tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
        if (tmpMvfAig ==  NIL(MvfAig_Function_t)){
          tmpMvfAig = Bmc_NodeBuildMVF(network, node);
          array_free(tmpMvfAig);
          tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
        }
        mAigNode = MvfAig_FunctionReadComponent(tmpMvfAig, value);
        BmcGenerateCnfForAigFunction(manager, network, mAigNode, k, cnfClauses);
      }
    }
  }
  if (BmcCnfReadOrInsertNode(cnfClauses, bAig_NodeReadName(manager, node), k, &nodeIndex)){
    return nodeIndex;
  }
  if (bAig_isVarNode(manager, node)){
    return nodeIndex;
  }
  leftIndex  = BmcGenerateCnfForAigFunction(manager, network, leftChild(node),  k, cnfClauses);
  rightIndex = BmcGenerateCnfForAigFunction(manager, network, rightChild(node), k, cnfClauses);
 
  clause  = array_alloc(int, 3);
  array_insert(int, clause, 0, -leftIndex );
  array_insert(int, clause, 1, -rightIndex);
  array_insert(int, clause, 2,  nodeIndex );
  BmcCnfInsertClause(cnfClauses, clause);
  array_free(clause);
  
  clause  = array_alloc(int, 2);
  array_insert(int, clause, 0,  leftIndex);
  array_insert(int, clause, 1, -nodeIndex);
  BmcCnfInsertClause(cnfClauses, clause);
  array_free(clause);
  
  clause  = array_alloc(int, 2);
  array_insert(int, clause, 0,  rightIndex);
  array_insert(int, clause, 1, -nodeIndex);
  BmcCnfInsertClause(cnfClauses, clause);  
  array_free(clause);

  return(nodeIndex);

}
#endif
/**Function********************************************************************

  Synopsis [
               c = a <-> b = (a=0)*(b=0) + (a=1)*(b=1) ....
           For a given term (a=i)*(b=i), if either is Zero,  don't generate
                                         clauses for this term.
                                         if both are One, don't generate clauses
                                         for c.
  ]

  SideEffects []

******************************************************************************/
void
BmcGenerateClausesFromStateTostate(
   bAig_Manager_t  *manager,
   bAigEdge_t      *fromAigArray,
   bAigEdge_t      *toAigArray,
   int             mvfSize, 
   int             fromState,
   int             toState,
   BmcCnfClauses_t *cnfClauses,
   int             outIndex) 
{
  array_t    *clause, *tmpclause;
  int        toIndex, fromIndex, cnfIndex;
  int        i;

  /* used to turn off the warning messages: might be left uninitialized.
     We are sure that these two variables will not be used uninitialized.
  */
  toIndex =0;
  fromIndex = 0;
  
  for(i=0; i< mvfSize; i++){
    if ((fromAigArray[i] == bAig_One) && (toAigArray[i] == bAig_One)){
      return;   /* the clause is always true */
    }
  }
  clause  = array_alloc(int, 0);
  for(i=0; i< mvfSize; i++){
    if ((fromAigArray[i] != bAig_Zero) && (toAigArray[i] != bAig_Zero)){
      if (toAigArray[i] != bAig_One){ 
         /* to State */

         toIndex = BmcGenerateCnfFormulaForAigFunction(manager,toAigArray[i],
                                                       toState,cnfClauses);
      }
      if (fromAigArray[i] != bAig_One){ 
         /* from State */
         fromIndex = BmcGenerateCnfFormulaForAigFunction(manager,
                                                         fromAigArray[i],
                                                         fromState,
                                                         cnfClauses);
      }
     /*
      Create new var for the output of this node. We don't create variable for this node, we only
      use its index number.
     */
     cnfIndex = cnfClauses->cnfGlobalIndex++;  /* index of the output of the OR of T(from, to) */
     
     assert(abs(cnfIndex) <= cnfClauses->cnfGlobalIndex);
     assert(abs(fromIndex) <= cnfClauses->cnfGlobalIndex);
     assert(abs(toIndex) <= cnfClauses->cnfGlobalIndex);
     
     if (toAigArray[i] == bAig_One){       
       tmpclause  = array_alloc(int, 2);
       array_insert(int, tmpclause, 0, -fromIndex);
       array_insert(int, tmpclause, 1, cnfIndex);
       BmcCnfInsertClause(cnfClauses, tmpclause);
       array_free(tmpclause); 

       tmpclause  = array_alloc(int, 2);
       array_insert(int, tmpclause, 0, fromIndex);
       array_insert(int, tmpclause, 1, -cnfIndex);
       BmcCnfInsertClause(cnfClauses, tmpclause);
       array_free(tmpclause);       

     } else if (fromAigArray[i] == bAig_One){
       tmpclause  = array_alloc(int, 2);
       array_insert(int, tmpclause, 0, -toIndex);
       array_insert(int, tmpclause, 1, cnfIndex);
       BmcCnfInsertClause(cnfClauses, tmpclause);
       array_free(tmpclause);

       tmpclause  = array_alloc(int, 2);
       array_insert(int, tmpclause, 0, toIndex);
       array_insert(int, tmpclause, 1, -cnfIndex);
       BmcCnfInsertClause(cnfClauses, tmpclause);
       array_free(tmpclause);
       
     } else {
       tmpclause  = array_alloc(int, 3);
       array_insert(int, tmpclause, 0, -toIndex);
       array_insert(int, tmpclause, 1, -fromIndex);
       array_insert(int, tmpclause, 2,  cnfIndex);
       BmcCnfInsertClause(cnfClauses, tmpclause);
       array_free(tmpclause);

       tmpclause  = array_alloc(int, 2);
       array_insert(int, tmpclause, 0, toIndex);
       array_insert(int, tmpclause, 1, -cnfIndex);
       BmcCnfInsertClause(cnfClauses, tmpclause);
       array_free(tmpclause);

       tmpclause  = array_alloc(int, 2);
       array_insert(int, tmpclause, 0, fromIndex);
       array_insert(int, tmpclause, 1, -cnfIndex);
       BmcCnfInsertClause(cnfClauses, tmpclause);
       array_free(tmpclause);
     }
     array_insert_last(int, clause, cnfIndex);
    } /* if */
  } /* for i loop */
  if (outIndex != 0 ){
    array_insert_last(int, clause, -outIndex);
  }
  BmcCnfInsertClause(cnfClauses, clause);
  array_free(clause);
  
  return;
}

/**Function********************************************************************

  Synopsis [Write the set of clauses in diamacs format to the output file.]

  SideEffects []

******************************************************************************/
void
BmcWriteClauses(
   mAig_Manager_t  *maigManager,
   FILE            *cnfFile,
   BmcCnfClauses_t *cnfClauses,
   BmcOption_t     *options)
{
  st_generator *stGen;
  char         *name;
  int          cnfIndex, i, k;

  if (options->verbosityLevel == BmcVerbosityMax_c) {      
    fprintf(vis_stdout,
            "Number of Variables = %d Number of Clauses = %d\n",
            cnfClauses->cnfGlobalIndex-1,  cnfClauses->noOfClauses);
  }
  st_foreach_item_int(cnfClauses->cnfIndexTable, stGen, &name, &cnfIndex) {
    fprintf(cnfFile, "c %s %d\n",name, cnfIndex);
  }
  (void) fprintf(cnfFile, "p cnf %d %d\n", cnfClauses->cnfGlobalIndex-1,
                 cnfClauses->noOfClauses);
  if (cnfClauses->clauseArray != NIL(array_t)) {
    for (i = 0; i < cnfClauses->nextIndex; i++) {
      k = array_fetch(int, cnfClauses->clauseArray, i);
      (void) fprintf(cnfFile, "%d%c", k, (k == 0) ? '\n' : ' ');
    }
  }
  return;
}

/**Function********************************************************************

  Synopsis [Check the satisfiability of CNF formula written in file]

  Description [Run SAT solver on input file]

  SideEffects []

******************************************************************************/
array_t *
BmcCheckSAT(BmcOption_t *options)
{
  array_t     *result = NIL(array_t);
  

  if(options->satSolver == cusp){
    result = BmcCallCusp(options);
  }
  if(options->satSolver == CirCUs){
    result = BmcCallCirCUs(options);
  }
  /* Adjust alarm if timeout in effect.  This is necessary because the
   * alarm may have gone off while the SAT solver is running.  Since
   * the CPU time of a child process is charged to the parent only when
   * the child terminates, the SIGALRM handler assumes that more time
   * is left than it is in reality.  We could do this adjustment right
   * after calling the SAT solver, but we prefer to give ourselves the
   * extra time to report the result even if this means using more time
   * than we are allotted.
   */
  if (options->timeOutPeriod > 0) {
    int residualTime = options->timeOutPeriod -
      (util_cpu_ctime() - options->startTime) / 1000;
    /* Make sure we do not cancel the alarm if no time is left. */
    if (residualTime <= 0) {
      residualTime = 1;
    }
    (void) alarm(residualTime);
  }

  return result;
}

/**Function********************************************************************

  Synopsis [Check the satisfiability of CNF formula written in file]

  Description [Run CirCUs on input file]

  SideEffects []

******************************************************************************/
array_t *
BmcCallCirCUs(
  BmcOption_t *options)
{
  satOption_t  *satOption;
  array_t      *result = NIL(array_t);
  satManager_t *cm;
  int          maxSize;

  satOption = sat_InitOption();
  satOption->verbose = options->verbosityLevel;
    satOption->verbose = 0;
  
  cm = sat_InitManager(0);
  cm->comment = ALLOC(char, 2);
  cm->comment[0] = ' ';
  cm->comment[1] = '\0';
  cm->stdOut = stdout;
  cm->stdErr = stderr;

  cm->option = satOption;
  cm->each = sat_InitStatistics();

  cm->unitLits = sat_ArrayAlloc(16);
  cm->pureLits = sat_ArrayAlloc(16);

  maxSize = 10000 << (bAigNodeSize-4);
  cm->nodesArray = ALLOC(bAigEdge_t, maxSize);
  cm->maxNodesArraySize = maxSize;
  cm->nodesArraySize = bAigNodeSize;

  sat_AllocLiteralsDB(cm);

  sat_ReadCNF(cm, options->satInFile);

  if (options->verbosityLevel == BmcVerbosityMax_c) {
    (void)fprintf(vis_stdout,"Calling SAT solver (CirCUs) ...");
    (void) fflush(vis_stdout);
  }
  sat_Main(cm);
  if (options->verbosityLevel == BmcVerbosityMax_c) {
    (void) fprintf(vis_stdout," done ");
    (void) fprintf(vis_stdout, "(%g s)\n", cm->each->satTime);
  }
  if(cm->status == SAT_UNSAT) {
    if (options->verbosityLevel != BmcVerbosityNone_c){
      (void) fprintf(vis_stdout, "# SAT: Counterexample not found\n");
      
    }
    fflush(cm->stdOut);
  } else if(cm->status == SAT_SAT) {
    if (options->verbosityLevel != BmcVerbosityNone_c){
      (void) fprintf(vis_stdout, "# SAT: Counterexample found\n");
    }
    if (options->verbosityLevel == BmcVerbosityMax_c){
      sat_ReportStatistics(cm, cm->each);
    }
    fflush(cm->stdOut);
    result = array_alloc(int, 0);
    {
      int i, size, value;
      
      size = cm->initNumVariables * bAigNodeSize;
      for(i=bAigNodeSize; i<=size; i+=bAigNodeSize) {
        value = SATvalue(i);
        if(value == 1) {
          array_insert_last(int, result, SATnodeID(i));
        }
        else if(value == 0) {
          array_insert_last(int, result, -(SATnodeID(i)));
        }
      }
    }
  }
  //Bing: To avoid SEVERE memory leakage
  FREE(cm->nodesArray);
  
  sat_FreeManager(cm);

  return result;
} /* BmcCallCirCUs */

/**Function********************************************************************

  Synopsis [Check the satisfiability of CNF formula written in file]

  Description [Run external solver on input file]

  SideEffects []

******************************************************************************/
array_t *
BmcCallCusp(BmcOption_t *options)
{
  FILE        *fp;
  static char parseBuffer[1024];
  int         satStatus;
  char        line[MAX_LENGTH];
  int         num = 0;
  array_t     *result = NIL(array_t);
  char        *tmpStr, *tmpStr1, *tmpStr2;
  long        solverStart;
  int         satTimeOutPeriod = 0;

  strcpy(parseBuffer,"cusp -distill -velim -cnf ");
  options->satSolverError = FALSE;  /* assume no error*/
  if (options->timeOutPeriod > 0) {
    /* Compute the residual CPU time and subtract a little time to
       give vis a chance to clean up before its own time out expires.
    */
    satTimeOutPeriod = options->timeOutPeriod - 1 -
      (util_cpu_ctime() - options->startTime) / 1000;
    if (satTimeOutPeriod <= 0){ /* no time left to run SAT solver*/
      options->satSolverError=TRUE;
      return NIL(array_t);
    }
    tmpStr2 = util_inttostr(satTimeOutPeriod);
    tmpStr1 = util_strcat3(options->satInFile," -t ", tmpStr2);
    tmpStr = util_strcat3(tmpStr1, " >", options->satOutFile);
    FREE(tmpStr1);
    FREE(tmpStr2);
  } else {
    tmpStr = util_strcat3(options->satInFile, " >", options->satOutFile);
  }
  strcat(parseBuffer, tmpStr);
  FREE(tmpStr);
  
  if (options->verbosityLevel == BmcVerbosityMax_c) {
    (void)fprintf(vis_stdout,"Calling SAT solver (cusp) ...");
    (void) fflush(vis_stdout);
    solverStart = util_cpu_ctime();
  } else { /* to remove uninitialized variables warning */
    solverStart = 0;
  }
  /* Call Sat Solver*/
  satStatus = system(parseBuffer);
  if (satStatus != 0){
    (void) fprintf(vis_stderr, "Can't run cusp. It may not be in your path. Status = %d\n", satStatus);
    options->satSolverError = TRUE;
    return NIL(array_t);
  }
  
  if (options->verbosityLevel == BmcVerbosityMax_c) {
    (void) fprintf(vis_stdout," done ");
    (void) fprintf(vis_stdout, "(%g s)\n",
                   (double) (util_cpu_ctime() - solverStart)/1000.0);
  }
  fp = Cmd_FileOpen(options->satOutFile, "r", NIL(char *), 0);
  if (fp == NIL(FILE)) {
    (void) fprintf(vis_stderr, "** bmc error: Cannot open the file %s\n",
                   options->satOutFile);
    options->satSolverError = TRUE;
    return NIL(array_t);
  }
  /* Skip the lines until the result */
  while(1) {
    if (fgets(line, MAX_LENGTH - 1, fp) == NULL) break;
    if(strstr(line,"UNSATISFIABLE") ||
       strstr(line,"SATISFIABLE") ||
       strstr(line,"MEMOUT") ||
       strstr(line,"TIMEOUT"))
      break;
  }

  if(strstr(line,"UNSATISFIABLE") != NIL(char)) {
    if (options->verbosityLevel != BmcVerbosityNone_c){
      (void) fprintf(vis_stdout, "# SAT: Counterexample not found\n");
      
    }
  } else if(strstr(line,"SATISFIABLE") != NIL(char)) {
    if (options->verbosityLevel != BmcVerbosityNone_c){
      (void) fprintf(vis_stdout, "# SAT: Counterexample found\n");
    }
    /* Skip the initial v of the result line */
    result = array_alloc(int, 0);
    while (fgets(line, MAX_LENGTH - 1, fp) != NULL) {
      char *word;
      if (line[0] != 'v') {
        (void) fprintf(vis_stderr,
                       "** bmc error: Cannot find assignment in file %s\n",
                       options->satOutFile);
        options->satSolverError = TRUE;
        return NIL(array_t);
      }
      word = strtok(&(line[1])," \n");
      while (word != NIL(char)) {
        num = atoi(word);
        if (num == 0) break;
        array_insert_last(int, result, num);
        word = strtok(NIL(char)," \n");
      }
      if (num == 0) break;
    }
  } else if(strstr(line,"MEMOUT") != NIL(char)) {
    (void) fprintf(vis_stdout,"# SAT: SAT Solver Memory out\n");
    options->satSolverError = TRUE;
  } else if(strstr(line,"TIMEOUT") != NIL(char)) {
    (void) fprintf(vis_stdout,
                   "# SAT: SAT Solver Time out occurred after %d seconds.\n",
                   satTimeOutPeriod);
    options->satSolverError = TRUE;
  } else {
    (void) fprintf(vis_stdout, "# SAT: SAT Solver failed, try again\n");
    options->satSolverError = TRUE;
  }
  (void) fflush(vis_stdout);
  (void) fclose(fp);

  return result;
} /* BmcCallCusp */


/**Function********************************************************************

  Synopsis [Print CounterExample.]

  SideEffects [Print a counterexample that was returned from the SAT
  solver in term of an array of integer "result". The counterexample
  starts from state 0 and of lenght eqaual to "length". If loopClause
  is not empty, this function print a loopback from the last state to
  a state in loopClause that exist in "result".]

******************************************************************************/
void
BmcPrintCounterExample(
  Ntk_Network_t   *network,
  st_table        *nodeToMvfAigTable,
  BmcCnfClauses_t *cnfClauses,
  array_t         *result,
  int             length,
  st_table        *CoiTable,
  BmcOption_t     *options,
  array_t         *loopClause)
{
  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
  lsGen             gen;
  st_generator      *stGen;
  Ntk_Node_t        *node;
  int               k;
  array_t           *latches = array_alloc(int, 0);
  int               *prevValueLatches;
  array_t           *inputs  = array_alloc(int, 0);
  int               *prevValueInputs;
  int               tmp;
  int               loop;
  st_table          *resultTable = st_init_table(st_numcmp, st_numhash);

  /*
    Initialize resultTable from the result to speed up the search in the result array.
   */
  for(k=0; k< array_n(result); k++){
    st_insert(resultTable, (char *) (long) array_fetch(int, result, k),  (char *) 0);
  }
  /* sort latches by name */
  st_foreach_item(CoiTable, stGen, &node, NULL) {
      array_insert_last(char*, latches, Ntk_NodeReadName(node));
  }
  array_sort(latches, nameCompare);
  /*
    Use to store the last value of each latch. If the current value of a latch
    differs from its corresponding value in this array, we will print the new values.
   */
  prevValueLatches = ALLOC(int, array_n(latches));
  prevValueInputs = 0;
  if(options->printInputs == TRUE){
    /* sort inputs by name */
    Ntk_NetworkForEachInput(network, gen, node){
      array_insert_last(char*, inputs, Ntk_NodeReadName(node));
    }
    array_sort(inputs, nameCompare);
    prevValueInputs = ALLOC(int, array_n(inputs));
  }
  loop = -1; /* no loop back */
  if(loopClause != NIL(array_t)){
    for(k=0; k < array_n(loopClause); k++){
      /*  if (searchArray(result, array_fetch(int, loopClause, k)) > -1){ */
      if (st_lookup_int(resultTable, (char *)(long)array_fetch(int, loopClause, k), &tmp)){
        loop = k;
        break;
      }
    }
  }
  /*
  Ntk_NetworkForEachPrimaryOutput(network, gen, node){
    array_insert_last(char*, outputs, Ntk_NodeReadName(node));
  }
  array_sort(outputs, nameCompare);
  */
  for (k=0; k<= length; k++){
    if (k == 0){
      (void) fprintf(vis_stdout, "\n--State %d:\n", k);
    } else {
      (void) fprintf(vis_stdout, "\n--Goes to state %d:\n", k);
    }
    /*
      Print the current values of the latches if they are different form their
      previous values.
     */
    printValue(manager, network, nodeToMvfAigTable, cnfClauses,
               latches, resultTable,  k, prevValueLatches);  
#if 0
    (void) fprintf(vis_stdout, "--Primary output:\n");
    printValue(manager, network, nodeToMvfAigTable, cnfClauses, outputs, result, k);
#endif
    if((options->printInputs == TRUE) && (k !=0)) {
      (void) fprintf(vis_stdout, "--On input:\n");
      printValue(manager, network, nodeToMvfAigTable, cnfClauses,
                 inputs, resultTable,   k-1, prevValueInputs);   
    }
  } /* for k loop */
  if(loop != -1){
    (void) fprintf(vis_stdout, "\n--Goes back to state %d:\n", loop);
    printValue(manager, network, nodeToMvfAigTable, cnfClauses,
               latches, resultTable,  loop, prevValueLatches);
    if((options->printInputs == TRUE)) {
      (void) fprintf(vis_stdout, "--On input:\n");
      printValue(manager, network, nodeToMvfAigTable, cnfClauses,
                 inputs, resultTable, length, prevValueInputs);   
    }
  }
  array_free(latches);
  FREE(prevValueLatches);
  if(options->printInputs == TRUE){
    array_free(inputs);
    FREE(prevValueInputs);
  }
  st_free_table(resultTable);
  return;
} /* BmcPrintCounterExample() */

/**Function********************************************************************

  Synopsis [Print CounterExample in Aiger format.]

  SideEffects [Print a counterexample that was returned from the SAT
  solver in term of an array of integer "result". The counterexample
  starts from state 0 and of lenght eqaual to "length". If loopClause
  is not empty, this function print a loopback from the last state to
  a state in loopClause that exist in "result".]

******************************************************************************/
void
BmcPrintCounterExampleAiger(
  Ntk_Network_t   *network,
  st_table        *nodeToMvfAigTable,
  BmcCnfClauses_t *cnfClauses,
  array_t         *result,
  int             length,
  st_table        *CoiTable,
  BmcOption_t     *options,
  array_t         *loopClause)
{
  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
  lsGen             gen;
  st_generator      *stGen;
  Ntk_Node_t        *node;
  int               k;
  array_t           *latches = array_alloc(int, 0);
  int               *prevValueLatches;
  array_t           *inputs  = array_alloc(int, 0);
  array_t           *outputs = array_alloc(int, 0);
  int               *prevValueInputs;
  int               *prevValueOutputs;
  int               tmp;
  int               loop;
  st_table          *resultTable = st_init_table(st_numcmp, st_numhash);
  char              *nodeName;

  /*
    Initialize resultTable from the result to speed up the search in the result array.
   */
  for(k=0; k< array_n(result); k++){
    st_insert(resultTable, (char *) (long) array_fetch(int, result, k),  (char *) 0);
  }
  /* sort latches by name */
  st_foreach_item(CoiTable, stGen, &node, NULL) {
      array_insert_last(char*, latches, Ntk_NodeReadName(node));
  }
  /*
    Use to store the last value of each latch. If the current value of a latch
    differs from its corresponding value in this array, we will print the new values.
   */

  /* the file generation needs to be removed for final vis release */

  FILE *order = Cmd_FileOpen("inputOrder.txt", "w", NIL(char *), 0);
  for (k=0; k< array_n(latches); k++)
  {
    nodeName = array_fetch(char *, latches, k);
    if((nodeName[0] == '$') && (nodeName[1] == '_'))
    {
      fprintf(order, "%s\n", &nodeName[2]);
    }
  }
  fclose(order);

  prevValueLatches = ALLOC(int, array_n(latches));
  Ntk_NetworkForEachInput(network, gen, node){
    array_insert_last(char*, inputs, Ntk_NodeReadName(node));
  }

  prevValueInputs = ALLOC(int, array_n(inputs));
  loop = -1; /* no loop back */
  if(loopClause != NIL(array_t)){
    for(k=0; k < array_n(loopClause); k++){
      /*  if (searchArray(result, array_fetch(int, loopClause, k)) > -1){ */
      if (st_lookup_int(resultTable, (char *)(long)array_fetch(int, loopClause, k), &tmp)){
        loop = k;
        break;
      }
    }
  }
 
  Ntk_NetworkForEachPrimaryOutput(network, gen, node){
    array_insert_last(char*, outputs, Ntk_NodeReadName(node));
  }
  prevValueOutputs = ALLOC(int, array_n(outputs));

  for (k=0; k< length; k++){
    /* This will print latches whose name doesn't start with $_. The latches whose
       name starts with $_ are latches added to the model by the aigtoblif translator.
     */
    printValueAiger(manager, network, nodeToMvfAigTable, cnfClauses,
               latches, resultTable,  k, prevValueLatches); 
    fprintf(vis_stdout, " ");
#if 0
    (void) fprintf(vis_stdout, "--Primary output:\n");
    printValue(manager, network, nodeToMvfAigTable, cnfClauses, outputs, result, k);
#endif

    if((loop<0)||(k<length))
    {

      /* we augment the original .mv model with latches in front of inputs and hence
         instead of inputs we print out the value of latches, this would have to be
         restored in the final release */

      printValueAigerInputs(manager, network, nodeToMvfAigTable, cnfClauses,
                 latches, resultTable,   k, prevValueInputs);   
      fprintf(vis_stdout, " ");

      /* the sat-solver doesn't propagate the values to output so we generate the output
         1 knowing when ouptut would be 1, we will have to remove this for vis release */

      if((k+1)==length)
      {
        fprintf(vis_stdout, "1 ");
      }
      else
      {
        fprintf(vis_stdout, "0 ");
      }

      printValueAiger(manager, network, nodeToMvfAigTable, cnfClauses,
               latches, resultTable,  k+1, prevValueLatches); 
    }
    if((loop < 0)||(k!=length))
    {
      fprintf(vis_stdout, "\n");
    }

  } /* for k loop */
  if(loop != -1){
    (void) fprintf(vis_stdout, "\n--Goes back to state %d:\n", loop);
    printValueAiger(manager, network, nodeToMvfAigTable, cnfClauses,
               latches, resultTable,  loop, prevValueLatches);
    (void) fprintf(vis_stdout, "--On input:\n");
    printValueAiger(manager, network, nodeToMvfAigTable, cnfClauses,
                 inputs, resultTable, length, prevValueInputs);   
  }
  array_free(latches);
  FREE(prevValueLatches);
  if(options->printInputs == TRUE){
    array_free(inputs);
    FREE(prevValueInputs);
  }
  st_free_table(resultTable);
  return;
} /* BmcPrintCounterExampleAiger() */


/**Function********************************************************************

  Synopsis [Print CounterExample.]

  SideEffects [Print a counterexample that was returned from the SAT
  solver in term of an array of integer "result". The counterexample
  starts from state 0 and of lenght eqaual to "length". If loopClause
  is not empty, this function print a loopback from the last state to
  a state in loopClause that exist in "result".]

******************************************************************************/
void
BmcAutPrintCounterExample(
  Ntk_Network_t   *network,
  Ltl_Automaton_t *automaton,
  st_table        *nodeToMvfAigTable,
  BmcCnfClauses_t *cnfClauses,
  array_t         *result,
  int             length,
  st_table        *CoiTable,
  BmcOption_t     *options,
  array_t         *loopClause)
{
  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
  lsGen             gen;
  st_generator      *stGen;
  Ntk_Node_t        *node;
  int               k;
  array_t           *latches = array_alloc(int, 0);
  int               *prevValueLatches;
  array_t           *inputs  = array_alloc(int, 0);
  int               *prevValueInputs;
  int               tmp;
  int               loop;
  st_table          *resultTable = st_init_table(st_numcmp, st_numhash);

  /*
    Initialize resultTable from the result to speed up the search in the result array.
   */
  for(k=0; k< array_n(result); k++){
    st_insert(resultTable, (char *) (long) array_fetch(int, result, k),  (char *) 0);
  }
  /* sort latches by name */
  st_foreach_item(CoiTable, stGen, &node, NULL) {
      array_insert_last(char*, latches, Ntk_NodeReadName(node));
  }
  array_sort(latches, nameCompare);
  /*
    Use to store the last value of each latch. If the current value of a latch
    differs from its corresponding value in this array, we will print the new values.
   */
  prevValueLatches = ALLOC(int, array_n(latches));
  prevValueInputs = 0;
  if(options->printInputs == TRUE){
    /* sort inputs by name */
    Ntk_NetworkForEachInput(network, gen, node){
      array_insert_last(char*, inputs, Ntk_NodeReadName(node));
    }
    array_sort(inputs, nameCompare);
    prevValueInputs = ALLOC(int, array_n(inputs));
  }
  loop = -1; /* no loop back */
  if(loopClause != NIL(array_t)){
    for(k=0; k < array_n(loopClause); k++){
      /*  if (searchArray(result, array_fetch(int, loopClause, k)) > -1){ */
      if (st_lookup_int(resultTable, (char *)(long)array_fetch(int, loopClause, k), &tmp)){
        loop = k;
        break;
      }
    }
  }
  /*
  Ntk_NetworkForEachPrimaryOutput(network, gen, node){
    array_insert_last(char*, outputs, Ntk_NodeReadName(node));
  }
  array_sort(outputs, nameCompare);
  */
  for (k=0; k<= length; k++){
    if (k == 0){
      (void) fprintf(vis_stdout, "\n--State %d:\n", k);
    } else {
      (void) fprintf(vis_stdout, "\n--Goes to state %d:\n", k);
    }
    /*
      Print the current values of the latches if they are different form their
      previous values.
     */
    printValue(manager, network, nodeToMvfAigTable, cnfClauses,
               latches, resultTable,  k, prevValueLatches);

    {
      lsGen               lsGen;
      vertex_t            *vtx;
      Ltl_AutomatonNode_t *state;
      int                 stateIndex;
      bdd_node            *node;
      int                 is_complemented;
      
       
      foreach_vertex(automaton->G, lsGen, vtx) {
        state = (Ltl_AutomatonNode_t *) vtx->user_data;
        
        node = bdd_get_node(state->Encode, &is_complemented);
        
        stateIndex  = state->cnfIndex[k];



        
        if (st_lookup_int(resultTable, (char *)(long)stateIndex, &tmp)){
          (void) fprintf(vis_stdout,"n%d \n", state->index);
        }
      }
    }
#if 0
    (void) fprintf(vis_stdout, "--Primary output:\n");
    printValue(manager, network, nodeToMvfAigTable, cnfClauses, outputs, result, k);
#endif
    if((options->printInputs == TRUE) && (k !=0)) {
      (void) fprintf(vis_stdout, "--On input:\n");
      printValue(manager, network, nodeToMvfAigTable, cnfClauses,
                 inputs, resultTable,   k-1, prevValueInputs);   
    }
  } /* for k loop */
  if(loop != -1){
    (void) fprintf(vis_stdout, "\n--Goes back to state %d:\n", loop);
    printValue(manager, network, nodeToMvfAigTable, cnfClauses,
               latches, resultTable,  loop, prevValueLatches);
    if((options->printInputs == TRUE)) {
      (void) fprintf(vis_stdout, "--On input:\n");
      printValue(manager, network, nodeToMvfAigTable, cnfClauses,
                 inputs, resultTable, length, prevValueInputs);   
    }
  }
  array_free(latches);
  FREE(prevValueLatches);
  if(options->printInputs == TRUE){
    array_free(inputs);
    FREE(prevValueInputs);
  }
  st_free_table(resultTable);
  return;
} /* BmcPrintCounterExample() */


/**Function********************************************************************

  Synopsis    [Generate CNF formula for a path from state 'from' to state 'to']

  Description [Unfold the transition relation 'k' states (k = to-from +1), and
  generate clauses for each state.
  
           For a multi-valued latch of 4 vlaues. Two binary variables are used 
           to rpresent X, x1 and x0. For this latch, there exist three multi-valued 
           functions.
           One for the binary reoresentation of the variable. For example the
           second entry of the mvf = 1, iff ~x1 and x0. 
           The second mfv is for the data input of the latch. If the And/Inv graph 
           attached to an entry of this mvf equal to 1, X equal to the binary 
           representation corresponding to this entry. For example, if the And/
           INV graph attached to the first entry =1, then X = ~x1 & ~x0. 
           To generate the CNF to the transition relation, first generate CNF to
           next state varaible using mvf of the latch.  Then, generate CNF for 
           latch data input using current state variavles. Finaly, generate CNF
           for the AND of these two MVF.  This for every entry of the MVF. Then 
           OR the results.
           The third MVF is for the initial value of the latch.  It is treat the
           same as the latch data input except if the initial value is constant. 
   
  The initialState value may be either BMC_INITIAL_STATES to generate the clause for the intial states.
  BMC_NO_INITIAL_STATES otherwise.
  ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
BmcCnfGenerateClausesForPath(
   Ntk_Network_t   *network,
   int             from,
   int             to,
   int             initialState,
   BmcCnfClauses_t *cnfClauses,
   st_table        *nodeToMvfAigTable,
   st_table        *CoiTable)
{
  mAig_Manager_t  *manager   = Ntk_NetworkReadMAigManager(network);
  st_generator    *stGen;
  
  Ntk_Node_t         *latch, *latchData, *latchInit;
  MvfAig_Function_t  *initMvfAig, *dataMvfAig, *latchMvfAig;
  bAigEdge_t         *initBAig, *latchBAig, *dataBAig;
  
  int        i, k, mvfSize;

  st_foreach_item(CoiTable, stGen, &latch, NULL) {
    
 
   latchInit  = Ntk_LatchReadInitialInput(latch);
   latchData  = Ntk_LatchReadDataInput(latch);

   /* Get the multi-valued function for each node*/
   initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
   if (initMvfAig ==  NIL(MvfAig_Function_t)){
     (void) fprintf(vis_stdout, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchInit));
     return;
   } 
   dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
   if (dataMvfAig ==  NIL(MvfAig_Function_t)){
     (void) fprintf(vis_stdout, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchData));
     return;
   }
   latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
   if (latchMvfAig ==  NIL(MvfAig_Function_t)){
     latchMvfAig = Bmc_NodeBuildMVF(network, latch);
     array_free(latchMvfAig);
     latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
   }
      
   mvfSize   = array_n(initMvfAig);
   initBAig  = ALLOC(bAigEdge_t, mvfSize);
   dataBAig  = ALLOC(bAigEdge_t, mvfSize);
   latchBAig = ALLOC(bAigEdge_t, mvfSize);   

   for(i=0; i< mvfSize; i++){
     dataBAig[i]  = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(dataMvfAig,  i));
     latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i));
     initBAig[i]  = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(initMvfAig,  i));
   }
   /*
   if (from == 0){
   */
   if (initialState == BMC_INITIAL_STATES){
   /* Generate the CNF for the initial state of the latch */
     BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
   }
   /* Generate the CNF for the transition functions */   
   for (k=from; k < to; k++){
     BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
   } /* for k state loop */

   FREE(initBAig);
   FREE(dataBAig);
   FREE(latchBAig);
  }/* For each latch loop*/
  
  return;
}

/**Function********************************************************************

  Synopsis    [Generate CNF formula for a loop-free path]

  Description [This function generates CNF formula for a loop-free path from
  state fromState to state toState. A loop free path is a path from a state S0
  to state Sn such that every state in the path is distinct. i.e for all states
  in the path Si != Sj for 0<= i < j <= n.
           
  The initialState value may be either BMC_INITIAL_STATES to generate the clause
  for the intial states. BMC_NO_INITIAL_STATES otherwise.
  ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
BmcCnfGenerateClausesForLoopFreePath(
   Ntk_Network_t   *network,
   int             fromState,
   int             toState,
   int             initialState,
   BmcCnfClauses_t *cnfClauses,
   st_table        *nodeToMvfAigTable,
   st_table        *CoiTable)
{
  int state;
  
  /*
    Generate clauses for a path from fromState to toState.
  */
  BmcCnfGenerateClausesForPath(network, fromState, toState, initialState, cnfClauses, nodeToMvfAigTable, CoiTable);
  
  /*
    Restrict the above path to be loop-free path.
  */
  /*
    for(state=0; state< toState; state++){
  */
  /*
    Don't include the last state because we know it is not equal any of the previous states.
    The property fails at this state, and true at all other states.
   */
  /*
  for(state=1; state < toState; state++){
  */
  for(state= fromState + 1; state <= toState; state++){
    BmcCnfGenerateClausesForNoLoopToAnyPreviouseStates(network, fromState, state, cnfClauses, nodeToMvfAigTable, CoiTable);
  }

  return;
}

/**Function********************************************************************

  Synopsis    [Generate Clauses for no loop from last state to any of the
  previouse states]

  Description [Generate Clauses for no loop from last state (toState) to
  any of the previous states starting from fromState. It generates the CNF
  clauses such that the last state of the path is not equal to any of the
  path previous states. 
  ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
BmcCnfGenerateClausesForNoLoopToAnyPreviouseStates(
   Ntk_Network_t   *network,
   int             fromState,
   int             toState,
   BmcCnfClauses_t *cnfClauses,
   st_table        *nodeToMvfAigTable,
   st_table        *CoiTable)
{
  mAig_Manager_t  *manager   = Ntk_NetworkReadMAigManager(network);
  st_generator    *stGen;
  
  Ntk_Node_t         *latch;
  MvfAig_Function_t  *latchMvfAig;
  bAigEdge_t         *latchBAig;
  array_t            *orClause;
  int                lastIndex, prevIndex, andIndex1, andIndex2;  
  int                i, k, mvfSize;

  /*
    Generates the clauses to check if the toState is not equal to any previouse states starting
    from fromState.
    
    Assume there are two state varaibles a and b. To check if Si != Sj, we must generate clauses
    for the formula ( ai != aj + bi != bj). 
  */
  for(k=fromState; k < toState; k++){
    orClause = array_alloc(int,0);
    st_foreach_item(CoiTable, stGen, &latch, NULL) {
      
  
      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
      if (latchMvfAig ==  NIL(MvfAig_Function_t)){
        latchMvfAig = Bmc_NodeBuildMVF(network, latch);
        array_free(latchMvfAig);
        latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
      } 
      mvfSize   = array_n(latchMvfAig);
      latchBAig = ALLOC(bAigEdge_t, mvfSize);   
      
      for(i=0; i< mvfSize; i++){
        latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i));
      }

      for (i=0; i< mvfSize; i++){
        prevIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], k       ,cnfClauses);
        lastIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], toState ,cnfClauses);     
        andIndex1 = cnfClauses->cnfGlobalIndex++;
        BmcCnfGenerateClausesForAND(prevIndex, -lastIndex, andIndex1, cnfClauses);
        andIndex2 = cnfClauses->cnfGlobalIndex++;
        BmcCnfGenerateClausesForAND(-prevIndex, lastIndex, andIndex2, cnfClauses);

        array_insert_last(int, orClause, andIndex1);
        array_insert_last(int, orClause, andIndex2);
      }
      FREE(latchBAig);
    }/* For each latch loop*/
    BmcCnfInsertClause(cnfClauses, orClause);
    array_free(orClause);
  } /* foreach k*/
  return;
}


/**Function********************************************************************

  Synopsis    [Generate Clauses for last state equal to any of the
  previouse states]

  Description [ Change it!
  Generate Clauses for no loop from last state (toState) to
  any of the previous states starting from fromState. It generates the CNF
  clauses such that the last state of the path is not equal to any of the
  path previous states. 
  ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
BmcCnfGenerateClausesForLoopToAnyPreviouseStates(
   Ntk_Network_t   *network,
   int             fromState,
   int             toState,
   BmcCnfClauses_t *cnfClauses,
   st_table        *nodeToMvfAigTable,
   st_table        *CoiTable)
{
  mAig_Manager_t  *manager   = Ntk_NetworkReadMAigManager(network);
  st_generator    *stGen;
  
  Ntk_Node_t         *latch;
  MvfAig_Function_t  *latchMvfAig;
  bAigEdge_t         *latchBAig;
  array_t            *orClause;
  int                lastIndex, prevIndex, andIndex1, andIndex2;  
  int                i, k, mvfSize;

  /*
    Generates the clauses to check if the toState is not equal to any previouse states starting
    from fromState.
    
    Assume there are two state varaibles a and b. To check if Si != Sj, we must generate clauses
    for the formula ( ai != aj + bi != bj). 
  */
  for(k=fromState; k < toState; k++){
    orClause = array_alloc(int,0);
    st_foreach_item(CoiTable, stGen, &latch, NULL) {
      
  
      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
      if (latchMvfAig ==  NIL(MvfAig_Function_t)){
        latchMvfAig = Bmc_NodeBuildMVF(network, latch);
        array_free(latchMvfAig);
        latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
      } 
      mvfSize   = array_n(latchMvfAig);
      latchBAig = ALLOC(bAigEdge_t, mvfSize);   
      
      for(i=0; i< mvfSize; i++){
        latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i));
      }

      for (i=0; i< mvfSize; i++){
        prevIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], k       ,cnfClauses);
        lastIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], toState ,cnfClauses);     
        andIndex1 = cnfClauses->cnfGlobalIndex++;
        BmcCnfGenerateClausesForAND(prevIndex, lastIndex, andIndex1, cnfClauses);
        andIndex2 = cnfClauses->cnfGlobalIndex++;
        BmcCnfGenerateClausesForAND(-prevIndex, -lastIndex, andIndex2, cnfClauses);

        array_insert_last(int, orClause, andIndex1);
        array_insert_last(int, orClause, andIndex2);
      }
      FREE(latchBAig);
    }/* For each latch loop*/
    BmcCnfInsertClause(cnfClauses, orClause);
    array_free(orClause);
  } /* foreach k*/
  return;
}

/**Function********************************************************************

  Synopsis    [Generate CNF formula for a path from state 'from' to state 'to']

  Description [Unfold the transition relation 'k' states (k = to-from +1), and
  generate clauses for each state.
           For a multi-valued latch of 4 vlaues. Two binary variables are used 
           to rpresent X, x1 and x0. For this latch, there exist three multi-valued 
           functions.
           One for the binary reoresentation of the variable. For example the
           second entry of the mvf = 1, iff ~x1 and x0. 
           The second mfv is for the data input of the latch. If the And/Inv graph 
           attached to an entry of this mvf equal to 1, X equal to the binary 
           representation corresponding to this entry. For example, if the And/
           INV graph attached to the first entry =1, then X = ~x1 & ~x0. 
           To generate the CNF to the transition relation, first generate CNF to
           next state varaible using mvf of the latch.  Then, generate CNF for 
           latch data input using current state variavles. Finaly, generate CNF
           for the AND of these two MVF.  This for every entry of the MVF. Then 
           OR the results.
           The third MVF is for the initial value of the latch.  It is treat the
           same as the latch data input except if the initial value is constant.         
           ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
BmcCnfGenerateClausesFromStateToState(
   Ntk_Network_t   *network,
   int             from,
   int             to,
   BmcCnfClauses_t *cnfClauses,
   st_table        *nodeToMvfAigTable,
   st_table        *CoiTable,
   int             loop)
{
  mAig_Manager_t  *manager   = Ntk_NetworkReadMAigManager(network);
  st_generator    *stGen;
  Ntk_Node_t         *latch, *latchData;
  MvfAig_Function_t  *dataMvfAig, *latchMvfAig;
  bAigEdge_t         *latchBAig, *dataBAig;
  int        i, mvfSize;

  st_foreach_item(CoiTable, stGen, &latch, NULL) {
    latchData  = Ntk_LatchReadDataInput(latch);
    
    dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
    if (dataMvfAig ==  NIL(MvfAig_Function_t)){
      (void) fprintf(vis_stdout,
                     "No multi-valued function for this node %s \n",
                     Ntk_NodeReadName(latchData));
      return;
    }
    latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
    if (latchMvfAig ==  NIL(MvfAig_Function_t)){
      latchMvfAig = Bmc_NodeBuildMVF(network, latch);
    }
    mvfSize   = array_n(dataMvfAig);
    dataBAig  = ALLOC(bAigEdge_t, mvfSize);
    latchBAig = ALLOC(bAigEdge_t, mvfSize);
    for(i=0; i< mvfSize; i++){
      dataBAig[i]  = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(dataMvfAig,  i));
      latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i));
    }
    BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize,
                                       from, to, cnfClauses, loop);
    FREE(dataBAig);
    FREE(latchBAig);
  } /* For each latch loop*/  
  return;
}

/**Function********************************************************************

  Synopsis    [Generate CNF clauses for the AND gate]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void 
BmcCnfGenerateClausesForAND(
   int             a,
   int             b,
   int             c,
   BmcCnfClauses_t *cnfClauses)
{
  array_t     *tmpClause;
    
  tmpClause = array_alloc(int, 3);
  array_insert(int, tmpClause, 0, -a);
  array_insert(int, tmpClause, 1, -b);
  array_insert(int, tmpClause, 2, c);
  BmcCnfInsertClause(cnfClauses, tmpClause);
  array_free(tmpClause);
  
  tmpClause = array_alloc(int, 2);
  
  array_insert(int, tmpClause, 0, a);
  array_insert(int, tmpClause, 1, -c);
  BmcCnfInsertClause(cnfClauses, tmpClause);
  
  array_insert(int, tmpClause, 0, b);
  BmcCnfInsertClause(cnfClauses, tmpClause);
       
  array_free(tmpClause);
  return;
}

/**Function********************************************************************

  Synopsis    [Generate CNF clauses for the OR gate]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void 
BmcCnfGenerateClausesForOR(
   int             a,
   int             b,
   int             c,
   BmcCnfClauses_t *cnfClauses)
{
  array_t     *tmpClause;
    
  tmpClause = array_alloc(int, 3);
  array_insert(int, tmpClause, 0, a);
  array_insert(int, tmpClause, 1, b);
  array_insert(int, tmpClause, 2, -c);
  BmcCnfInsertClause(cnfClauses, tmpClause);
  array_free(tmpClause);
  
  tmpClause = array_alloc(int, 2);
  array_insert(int, tmpClause, 0, -a);
  array_insert(int, tmpClause, 1, c);
  BmcCnfInsertClause(cnfClauses, tmpClause);
  
  array_insert(int, tmpClause, 0, -b);
  BmcCnfInsertClause(cnfClauses, tmpClause);
       
  array_free(tmpClause);
  return;
}

/**Function********************************************************************

  Synopsis [Alloc Memory for BmcCnfClauses_t]

  SideEffects []

  SeeAlso []
******************************************************************************/
BmcCnfClauses_t *
BmcCnfClausesAlloc(void)
{
  BmcCnfClauses_t *result = ALLOC(BmcCnfClauses_t, 1);
  
  if (!result){
    return result;
  }
  result->clauseArray    = array_alloc(int, 0);
  result->cnfIndexTable  = st_init_table(strcmp, st_strhash);
  result->freezedKeys    = array_alloc(nameType_t *, 0);
  
  result->nextIndex      = 0;
  result->noOfClauses    = 0;
  result->cnfGlobalIndex = 1;  
  result->emptyClause    = FALSE;
  result->freezed        = FALSE;

  return result;
} /*BmcCnfClausesAlloc()*/

/**Function********************************************************************

  Synopsis [Free Memory for BmcCnfClauses_t]

  SideEffects []

  SeeAlso []
******************************************************************************/
void 
BmcCnfClausesFree(
  BmcCnfClauses_t *cnfClauses)
{
  st_generator *stGen;
  char         *name;
  int          cnfIndex;

  array_free(cnfClauses->clauseArray);
  array_free(cnfClauses->freezedKeys);

  if (cnfClauses->cnfIndexTable != NIL(st_table)){
    st_foreach_item_int(cnfClauses->cnfIndexTable, stGen, (char **) &name, &cnfIndex) {
      FREE(name);
    }
    st_free_table(cnfClauses->cnfIndexTable);
  }
  FREE(cnfClauses);
  cnfClauses = NIL(BmcCnfClauses_t);
} /* BmcCnfClausesFree() */

/**Function********************************************************************

  Synopsis [Freeze the current state of CNF]

  Description [The current state of CNF is stored in the structure BmcCnfStates_t.
  This information may use later to store CNF to this state by calling
  BmcCnfClausesRestore().]

  SideEffects []

  SeeAlso [BmcCnfClausesRestore() BmcCnfClausesUnFreeze() ]
******************************************************************************/
BmcCnfStates_t *
BmcCnfClausesFreeze(
  BmcCnfClauses_t * cnfClauses)
{
  BmcCnfStates_t *state = ALLOC(BmcCnfStates_t, 1);

  state->nextIndex      = cnfClauses->nextIndex;
  state->noOfClauses    = cnfClauses->noOfClauses;
  state->cnfGlobalIndex = cnfClauses->cnfGlobalIndex;

  /* This variable is used when deleting any new entries in cnfClauses->freezedKeys
   that will be added after CNF is freezed.*/
  state->freezedKeySize = array_n(cnfClauses->freezedKeys);
  
  state->emptyClause    = cnfClauses->emptyClause;
  state->freezed        = cnfClauses->freezed;
  cnfClauses->freezed   = TRUE;
  return state;
} /* mcCnfClausesFreeze() */

/**Function********************************************************************

  Synopsis [Unfreeze CNF]

  Description [Keeps the current state of CNF]

  SideEffects []

  SeeAlso []
******************************************************************************/
void 
BmcCnfClausesUnFreeze(
  BmcCnfClauses_t *cnfClauses,
  BmcCnfStates_t  *state)
{
  int i;

  cnfClauses->freezed = FALSE;
  if (array_n(cnfClauses->freezedKeys) != 0){
    int freezedKeySize = array_n(cnfClauses->freezedKeys);
    
    for (i=0; i< (freezedKeySize-state->freezedKeySize); i++){
      (cnfClauses->freezedKeys)->num--;
    }
  }
} /* BmcCnfClausesUnFreeze() */

/**Function********************************************************************

  Synopsis [Restore the CNF to its previouse state]

  Description [Restore the CNF to its previouse state that CNF was when
  BmcCnfClausesFreeze() was last called]

  SideEffects []
  
  SeeAlso []
******************************************************************************/
void 
BmcCnfClausesRestore(
  BmcCnfClauses_t *cnfClauses,
  BmcCnfStates_t  *state)
{
  int        i, index;
  nameType_t *key;

  cnfClauses->nextIndex      = state->nextIndex;
  cnfClauses->noOfClauses    = state->noOfClauses;
  cnfClauses->cnfGlobalIndex = state->cnfGlobalIndex;
  cnfClauses->emptyClause    = state->emptyClause;
  cnfClauses->freezed        = state->freezed;
  
  if (array_n(cnfClauses->freezedKeys) != 0){
    int freezedKeySize = array_n(cnfClauses->freezedKeys);
                       
    for (i=0; i< (freezedKeySize-state->freezedKeySize); i++){
      key = array_fetch_last(nameType_t *, cnfClauses->freezedKeys);
      if (st_delete_int(cnfClauses->cnfIndexTable, &key, &index)){
        FREE(key);
      } 
      (cnfClauses->freezedKeys)->num--;
    }
  }
} /* BmcCnfClausesRestore() */

/**Function********************************************************************

  Synopsis [Add clause to the clauseArray]

  Description [Add a clause to the clause array.  clause is of type array_t.
  The user must free clause.]

  SideEffects []
  
  SeeAlso []
******************************************************************************/
void 
BmcCnfInsertClause(
  BmcCnfClauses_t *cnfClauses,
  array_t         *clause)
{
  int  i, lit;

  if (clause != NIL(array_t)){
    if (array_n(clause) == 0){ /* empty clause */
      cnfClauses->emptyClause = TRUE;
      return;
    }
    for (i=0; i< array_n(clause); i++){
      lit = array_fetch(int, clause, i);
      array_insert(int, cnfClauses->clauseArray, cnfClauses->nextIndex++, lit);
    }
    array_insert(int, cnfClauses->clauseArray, cnfClauses->nextIndex++, 0); /*End Of clause*/
    cnfClauses->noOfClauses++;
    cnfClauses->emptyClause = FALSE;
  }
  return;
}/* BmcCnfInsertClause() */

/**Function********************************************************************

  Synopsis [Add an empty clause]

  SideEffects []

  SeeAlso []
******************************************************************************/
void
BmcAddEmptyClause(
  BmcCnfClauses_t *cnfClauses)
{
  cnfClauses->emptyClause = TRUE;
}/* BmcAddEmptyClause() */

/**Function********************************************************************

  Synopsis [Return the cnfIndex of the node]

  Description [If CNF was generated for this node, return its cnfIndex, otherwise
  insert the name of this node in the cnfIndexTable, and return its cnfIndex. The
  key to the cnfIndexTable is (nodeName_state).] 

  SideEffects []
******************************************************************************/
int
BmcCnfReadOrInsertNode(
   BmcCnfClauses_t *cnfClauses,
   nameType_t      *nodeName,
   int             state,
   int             *nodeIndex)
{
  nameType_t *varName;
  int        index;
  char       *stateStr = util_inttostr(state);

  varName  = util_strcat3(nodeName, "_", stateStr);
  FREE(stateStr);
  if (!st_lookup_int(cnfClauses->cnfIndexTable, varName, &index)) {
    index = cnfClauses->cnfGlobalIndex++;
    st_insert(cnfClauses->cnfIndexTable, varName, (char*) (long) index);
    if(cnfClauses->freezed == TRUE){
      array_insert_last(nameType_t *, cnfClauses->freezedKeys, varName);
    }
    *nodeIndex = index;
    return 0; /* Inserted */
  }
  else { /* The node has been visited */
    *nodeIndex = index;
    FREE(varName);
    return 1;     
  }
}


/**Function********************************************************************

  Synopsis    [Find the Cone of Influnce (COI) for an LTL formula]

  Description [Return a list of state variables (latches) that are in the COI of the
  LTL formula.]

  SideEffects []

******************************************************************************/
void
BmcGetCoiForLtlFormula(
  Ntk_Network_t   *network,
  Ctlsp_Formula_t *formula,
  st_table        *ltlCoiTable)
{
  st_table *visited = st_init_table(st_ptrcmp, st_ptrhash);
  
  BmcGetCoiForLtlFormulaRecursive(network, formula, ltlCoiTable, visited);
  st_free_table(visited);
  return;
} /* BmcGetCoiForLtlFormula() */

/**Function********************************************************************

  Synopsis    [Recursive function to find the COI of a network node.]

  Description []

  SideEffects []

******************************************************************************/
void
BmcGetCoiForLtlFormulaRecursive(
  Ntk_Network_t   *network,
  Ctlsp_Formula_t *formula,
  st_table        *ltlCoiTable,
  st_table        *visited)
{
  if (formula == NIL(Ctlsp_Formula_t)) {
    return;
  }
  /* leaf node */
  if (formula->type == Ctlsp_ID_c){
    char       *name = Ctlsp_FormulaReadVariableName(formula);
    Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, name);
    int        tmp;

    if (st_lookup_int(visited, (char *) node, &tmp)){
      /* Node already visited */
      return;
    }
    BmcGetCoiForNtkNode(node, ltlCoiTable, visited);
    return;
  }
  BmcGetCoiForLtlFormulaRecursive(network, formula->left,  ltlCoiTable, visited);
  BmcGetCoiForLtlFormulaRecursive(network, formula->right, ltlCoiTable, visited);

  return;
} /* BmcGetCoiForLtlFormulaRecursive() */

/**Function********************************************************************

  Synopsis    [Genrate COI for a non-latch network node]

  Description [For each fanins of the given node, if its latch, add it
  to the CoiTable and return. If it is not latch, call this function to
  look for any latches in the fanins of this node.]

  SideEffects []

******************************************************************************/
void
BmcGetCoiForNtkNode(
  Ntk_Node_t  *node,
  st_table    *CoiTable,
  st_table    *visited)
{
  int        i, j;
  Ntk_Node_t *faninNode;

  if(node == NIL(Ntk_Node_t)){
    return;
  }
  if (st_lookup_int(visited, (char *) node, &j)){
    /* Node already visited */
    return;
  }
  st_insert(visited, (char *) node, (char *) 0);
  if (Ntk_NodeTestIsLatch(node)){
    st_insert(CoiTable, (char *) node, (char *) 0);
  }
  Ntk_NodeForEachFanin(node, i, faninNode) {
    BmcGetCoiForNtkNode(faninNode, CoiTable, visited);
  }
  return;
} /* BmcGetCoiForNtkNode() */


/**Function********************************************************************

  Synopsis    [Find Mdd for states satisfying Atomic Formula.]

  Description [An atomic formula defines a set of states in the following
  way: it states a designated ``net'' (specified by the full path name)
  takes a certain value. The net should be purely a function of latches;
  as a result an evaluation of the net yields a set of states.]

  SideEffects []

******************************************************************************/

mdd_t *
BmcModelCheckAtomicFormula(
  Fsm_Fsm_t *modelFsm,
  Ctlsp_Formula_t *ctlFormula)
{
  mdd_t * resultMdd;
  mdd_t *tmpMdd;
  Ntk_Network_t *network = Fsm_FsmReadNetwork(modelFsm);
  char *nodeNameString = Ctlsp_FormulaReadVariableName(ctlFormula);
  char *nodeValueString = Ctlsp_FormulaReadValueName(ctlFormula);
  Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, nodeNameString);

  Var_Variable_t *nodeVar;
  int nodeValue;

  graph_t *modelPartition;
  vertex_t *partitionVertex;
  Mvf_Function_t *MVF;

  nodeVar = Ntk_NodeReadVariable(node);
  if (Var_VariableTestIsSymbolic(nodeVar)) {
    nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
  }
  else {
    nodeValue = atoi(nodeValueString);
  }

  modelPartition = Part_NetworkReadPartition(network);
  if (!(partitionVertex = Part_PartitionFindVertexByName(modelPartition,
                                                         nodeNameString))) {
    lsGen tmpGen;
    Ntk_Node_t *tmpNode;
    array_t *mvfArray;
    array_t *tmpRoots = array_alloc(Ntk_Node_t *, 0);
    st_table *tmpLeaves = st_init_table(st_ptrcmp, st_ptrhash);
    array_insert_last(Ntk_Node_t *, tmpRoots, node);

    Ntk_NetworkForEachCombInput(network, tmpGen, tmpNode) {
      st_insert(tmpLeaves, (char *) tmpNode, (char *) NTM_UNUSED);
    }

    mvfArray =  Ntm_NetworkBuildMvfs(network, tmpRoots, tmpLeaves,
                                      NIL(mdd_t));
    MVF = array_fetch(Mvf_Function_t *, mvfArray, 0);
    array_free(tmpRoots);
    st_free_table(tmpLeaves);
    array_free(mvfArray);

    tmpMdd = Mvf_FunctionReadComponent(MVF, nodeValue);
    resultMdd = mdd_dup(tmpMdd);
    Mvf_FunctionFree(MVF);
  }
  else {
    MVF = Part_VertexReadFunction(partitionVertex);
    tmpMdd = Mvf_FunctionReadComponent(MVF, nodeValue);
    resultMdd = mdd_dup(tmpMdd);
  }
  if (Part_PartitionReadMethod(modelPartition) == Part_Frontier_c &&
      Ntk_NodeTestIsCombOutput(node)) {
    array_t     *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
    mdd_manager *mgr = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(modelFsm));
    array_t     *supportList;
    st_table    *supportTable = st_init_table(st_numcmp, st_numhash);
    int         i, j;
    int         existIntermediateVars;
    int         mddId;
    Mvf_Function_t      *mvf;
    vertex_t    *vertex;
    array_t     *varBddRelationArray, *varArray;
    mdd_t       *iv, *ivMdd, *relation;

    for (i = 0; i < array_n(psVars); i++) {
      mddId = array_fetch(int, psVars, i);
      st_insert(supportTable, (char *)(long)mddId, NULL);
    }

    existIntermediateVars = 1;
    while (existIntermediateVars) {
      existIntermediateVars = 0;
      supportList = mdd_get_support(mgr, resultMdd);
      for (i = 0; i < array_n(supportList); i++) {
        mddId = array_fetch(int, supportList, i);
        if (!st_lookup(supportTable, (char *)(long)mddId, NULL)) {
          vertex = Part_PartitionFindVertexByMddId(modelPartition, mddId);
          mvf = Part_VertexReadFunction(vertex);
          varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mgr, mddId, mvf);
          varArray = mdd_id_to_bdd_array(mgr, mddId);
          assert(array_n(varBddRelationArray) == array_n(varArray));
          for (j = 0; j < array_n(varBddRelationArray); j++) {
            iv = array_fetch(mdd_t *, varArray, j);
            relation = array_fetch(mdd_t *, varBddRelationArray, j);
            ivMdd = bdd_cofactor(relation, iv);
            mdd_free(relation);
            tmpMdd = resultMdd;
            resultMdd = bdd_compose(resultMdd, iv, ivMdd);
            mdd_free(tmpMdd);
            mdd_free(iv);
            mdd_free(ivMdd);
          }
          array_free(varBddRelationArray);
          array_free(varArray);
          existIntermediateVars = 1;
        }
      }
      array_free(supportList);
    }
    st_free_table(supportTable);
  }
  return resultMdd;
}

/**Function********************************************************************

  Synopsis    [Read fairness constraints from file and check for errors.]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
array_t *
BmcReadFairnessConstraints(
  FILE *fp /* pointer to the fairness constraint file */)
{
  array_t *constraintArray;     /* raw fairness constraints */
  array_t *ltlConstraintArray;  /* constraints converted to LTL */

  if (fp == NIL(FILE) ) {
    /* Nothing to be done. */
    return NIL(array_t);
  }

  /* Read constraints from file and check for errors. */
  constraintArray = Ctlsp_FileParseFormulaArray(fp);
  if (constraintArray == NIL(array_t)) {
    (void) fprintf(vis_stderr,
                   "** ctlsp error: error reading fairness constraints.\n");
    return NIL(array_t);
  }
  if (array_n(constraintArray) == 0) {
    (void) fprintf(vis_stderr, "** ctlsp error: fairness file is empty.\n");
    return NIL(array_t);
  }
  /*
   * Check that each constraint is an LTL formula.
   */
  ltlConstraintArray = Ctlsp_FormulaArrayConvertToLTL(constraintArray);
  Ctlsp_FormulaArrayFree(constraintArray);
  if (ltlConstraintArray == NIL(array_t)) {
    (void) fprintf(vis_stderr,
                   "** ctlsp error: fairness constraints are not LTL formulae.\n");
    return NIL(array_t);
  }

  return ltlConstraintArray;

} /* BmcReadFairnessConstraints */


/**Function********************************************************************

  Synopsis [return the cnf index for a bdd node]

  SideEffects []

******************************************************************************/
int
BmcGetCnfVarIndexForBddNode(
  bdd_manager *bddManager,
  bdd_node *node,
  int      state,
  BmcCnfClauses_t *cnfClauses)
{
  array_t     *mvar_list  = mdd_ret_mvar_list(bddManager);
  array_t     *bvar_list  = mdd_ret_bvar_list(bddManager);  
  
  char      name[100];
  char      *nodeName;
  bvar_type bv;
  mvar_type mv;
  int nodeIndex = bdd_node_read_index(node);
  int index, rtnNodeIndex, rtnCode;


  /*
    If the node is for a multi-valued varaible.
  */
  if (nodeIndex < array_n(bvar_list)){
    bv = array_fetch(bvar_type, bvar_list, nodeIndex);
    /*
      get the multi-valued varaible.
    */
    mv = array_fetch(mvar_type, mvar_list, bv.mvar_id);
    arrayForEachItem(int, mv.bvars, index, rtnNodeIndex) {
      if (nodeIndex == rtnNodeIndex){
        break;
      }
    }
    assert(index < mv.encode_length);
    /*
      printf("Name of bdd node %s %d\n", mv.name, index);
    */
    sprintf(name, "%s_%d", mv.name, index);
  } else {
    sprintf(name, "Bdd_%d", nodeIndex);
  }
  nodeName = util_strsav(name);
  rtnCode = BmcCnfReadOrInsertNode(cnfClauses, nodeName, state, &nodeIndex);
  if(rtnCode == 1) {
    FREE(nodeName);
  }
  return nodeIndex;
}

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

/**Function********************************************************************

  Synopsis [Test that the given string is an integer. Returns 0 if string is
  not an integer, 1 if the integer is too big for int, and 2 if integer fits
  in int.]

  SideEffects [Sets the pointer value if the string is an integer small enough
  for int.]

******************************************************************************/
static int
StringCheckIsInteger(
  char *string,
  int *value)
{
  char *ptr;
  long l;
  
  l = strtol (string, &ptr, 0) ;
  if(*ptr != '\0')
    return 0;
  if ((l > MAXINT) || (l < -1 - MAXINT))
    return 1 ;
  *value = (int) l;
  return 2 ;
}

/**Function********************************************************************

  Synopsis    [Compare procedure for name comparison.]

  Description [Compare procedure for name comparison.]

  SideEffects []

******************************************************************************/
static int
nameCompare(
  const void * name1,
  const void * name2)
{
    return(strcmp(*(char**)name1, *(char **)name2));

} /* end of signatureCompare */




/**Function********************************************************************

  Synopsis    [Print the valuse of variables in the variable list "varNames".]

  Description [For each variable in the variable list, this functions prints its
  value in the resultTable if it is different for its value in prevValue. If this
  variable is a symbolic variable, this function prints its symbolic value.]

  SideEffects []

******************************************************************************/
static void
printValue(
  mAig_Manager_t  *manager,
  Ntk_Network_t   *network,
  st_table        *nodeToMvfAigTable,
  BmcCnfClauses_t *cnfClauses,
  array_t         *varNames,
  st_table        *resultTable,
  int             state,
  int             *prevValue)
{
  Ntk_Node_t        *node;
  int               i, j;
  bAigEdge_t        bAigId;
  nameType_t        *varName, *nodeName;
  int               value, index;
  MvfAig_Function_t *MvfAig;
  int               changed = 0;
  int               tmp;

  for (j=0; j< array_n(varNames); j++) {
    if (state == 0){
      prevValue[j] = -1;
    }
    nodeName = array_fetch(char *, varNames, j);
    /*
      Fetch the node corresponding to this node name.
    */
    node = Ntk_NetworkFindNodeByName(network, nodeName);
    /*
      Get the multi-valued function for each node
    */
    MvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
    /*
      In case of the multi-valued function is not build for this node, do nothing.
      We may notify the user.
     */
    if (MvfAig ==  NIL(MvfAig_Function_t)){
      continue;
    }
    /*
      No CNF index for this variable at time "state in the "
     */
    value = -1;
    for (i=0; i< array_n(MvfAig); i++) {
      bAigId = MvfAig_FunctionReadComponent(MvfAig, i);
      /*
        constant value
       */
      if (bAigId == bAig_One){
        /*
          This variable equal the constant i.
         */
        value = i;
        break;
      }
      if (bAigId != bAig_Zero){
        char        *tmpStr;
        
        nodeName = bAig_NodeReadName(manager, bAigId);
        /*
          Build the variable name at state "state".
         */
        tmpStr = util_inttostr(state);
        varName  = util_strcat3(nodeName, "_", tmpStr);
        if (st_lookup_int(cnfClauses->cnfIndexTable, varName, &index)) {
          if (bAig_IsInverted(bAigId)){
            index = -index;
          }
          /*if (searchArray(result, index) > -1){*/
          if (st_lookup_int(resultTable, (char *)(long)index, &tmp)){
            value = i;
            break;
          }
        } /* if st_lookup_int()  */
        FREE(tmpStr);
        FREE(varName);
      } /* if (bAigId != bAig_Zero) */
    }
    if (value >= 0){
      if (value != prevValue[j]){
        Var_Variable_t *nodeVar = Ntk_NodeReadVariable(node);

        prevValue[j] = value;
        changed = 1;
        if (Var_VariableTestIsSymbolic(nodeVar)) {
          char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value);

          (void) fprintf(vis_stdout,"%s:%s\n",  Ntk_NodeReadName(node), symbolicValue);
        }
        else {
          (void) fprintf(vis_stdout,"%s:%d\n",  Ntk_NodeReadName(node), value);
        }
      }
    } else {
      /*
        This variable does not have value in the current time frame. It means its value
        is not important at this time frame.
       */
      (void) fprintf(vis_stdout,"%s:X\n",  Ntk_NodeReadName(node));
    }
  } /* for j loop */
  if (changed == 0){
    fprintf( vis_stdout, "<Unchanged>\n");
  }

}/* end of printValue() */



/**Function********************************************************************

  Synopsis    [Print the valuse of variables in the variable list "varNames".]

  Description [For each variable in the variable list, this functions prints the 
               values of names, which do not start with $_ as these are true
               latches of the model. Since this is in aiger format, hence all
               the values are printed even if they didn't change from the 
               previous values.]

  SideEffects []

******************************************************************************/
static void
printValueAiger(
  mAig_Manager_t  *manager,
  Ntk_Network_t   *network,
  st_table        *nodeToMvfAigTable,
  BmcCnfClauses_t *cnfClauses,
  array_t         *varNames,
  st_table        *resultTable,
  int             state,
  int             *prevValue)
{
  Ntk_Node_t        *node;
  int               i, j;
  bAigEdge_t        bAigId;
  nameType_t        *varName, *nodeName;
  int               value, index;
  MvfAig_Function_t *MvfAig;
  int               tmp;
  char *            NodeName;

  for (j=0; j< array_n(varNames); j++) {
    if (state == 0){
      prevValue[j] = -1;
    }
    nodeName = array_fetch(char *, varNames, j);
    /*
      Fetch the node corresponding to this node name.
    */
    node = Ntk_NetworkFindNodeByName(network, nodeName);
    /*
      Get the multi-valued function for each node
    */
    MvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
    /*
      In case of the multi-valued function is not build for this node, do nothing.
      We may notify the user.
     */
    if (MvfAig ==  NIL(MvfAig_Function_t)){
      continue;
    }
    /*
      No CNF index for this variable at time "state in the "
     */
    value = -1;
    for (i=0; i< array_n(MvfAig); i++) {
      bAigId = MvfAig_FunctionReadComponent(MvfAig, i);
      /*
        constant value
       */
      if (bAigId == bAig_One){
        /*
          This variable equal the constant i.
         */
        value = i;
        break;
      }
      if (bAigId != bAig_Zero){
        char        *tmpStr;
        
        nodeName = bAig_NodeReadName(manager, bAigId);
        /*
          Build the variable name at state "state".
         */
        tmpStr = util_inttostr(state);
        varName  = util_strcat3(nodeName, "_", tmpStr);
        if (st_lookup_int(cnfClauses->cnfIndexTable, varName, &index)) {
          if (bAig_IsInverted(bAigId)){
            index = -index;
          }
          /*if (searchArray(result, index) > -1){*/
          if (st_lookup_int(resultTable, (char *)(long)index, &tmp)){
            value = i;
            break;
          }
        } /* if st_lookup_int()  */
        FREE(tmpStr);
        FREE(varName);
      } /* if (bAigId != bAig_Zero) */
    }
    NodeName = Ntk_NodeReadName(node); 
    if(!((NodeName[0] == '$') && (NodeName[1] == '_')))
    {
      if (value >= 0){
        Var_Variable_t *nodeVar = Ntk_NodeReadVariable(node);
        
        prevValue[j] = value;
        if (Var_VariableTestIsSymbolic(nodeVar)) {
          char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value);
          
          (void) fprintf(vis_stdout,"%s",   symbolicValue);
        } 
        else {
          (void) fprintf(vis_stdout,"%d",  value);
        }
      } else {
      /*
        This variable does not have value in the current time frame. It means its value
        is not important at this time frame.
       */
        (void) fprintf(vis_stdout,"x" );
      }
    } /* these nodes are latches in front of inputs so they will be printed out as inputs */
  } /* for j loop */
}/* end of printValueAiger() */


/**Function********************************************************************

  Synopsis    [Print the valuse of variables in the variable list "varNames".]

  Description [For each variable in the variable list, this functions checks if
               the name starts with $_, which means that those latches are 
               actually storing the value of inputs. This modification to the
               model is externally done and not done by VIS so this method is
               only specific to certain type of model, the output of aigtoblif
               translator.]

  SideEffects []

******************************************************************************/
static void
printValueAigerInputs(
  mAig_Manager_t  *manager,
  Ntk_Network_t   *network,
  st_table        *nodeToMvfAigTable,
  BmcCnfClauses_t *cnfClauses,
  array_t         *varNames,
  st_table        *resultTable,
  int             state,
  int             *prevValue)
{
  Ntk_Node_t        *node;
  int               i, j;
  bAigEdge_t        bAigId;
  nameType_t        *varName, *nodeName;
  int               value, index;
  MvfAig_Function_t *MvfAig;
  int               tmp;
  char *            NodeName;

  for (j=0; j< array_n(varNames); j++) {
    if (state == 0){
      prevValue[j] = -1;
    }
    nodeName = array_fetch(char *, varNames, j);
    /*
      Fetch the node corresponding to this node name.
    */
    node = Ntk_NetworkFindNodeByName(network, nodeName);
    /*
      Get the multi-valued function for each node
    */
    MvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
    /*
      In case of the multi-valued function is not build for this node, do nothing.
      We may notify the user.
     */
    if (MvfAig ==  NIL(MvfAig_Function_t)){
      continue;
    }
    /*
      No CNF index for this variable at time "state in the "
     */
    value = -1;
    for (i=0; i< array_n(MvfAig); i++) {
      bAigId = MvfAig_FunctionReadComponent(MvfAig, i);
      /*
        constant value
       */
      if (bAigId == bAig_One){
        /*
          This variable equal the constant i.
         */
        value = i;
        break;
      }
      if (bAigId != bAig_Zero){
        char        *tmpStr;
        
        nodeName = bAig_NodeReadName(manager, bAigId);
        /*
          Build the variable name at state "state".
         */
        tmpStr = util_inttostr(state);
        varName  = util_strcat3(nodeName, "_", tmpStr);
        if (st_lookup_int(cnfClauses->cnfIndexTable, varName, &index)) {
          if (bAig_IsInverted(bAigId)){
            index = -index;
          }
          /*if (searchArray(result, index) > -1){*/
          if (st_lookup_int(resultTable, (char *)(long)index, &tmp)){
            value = i;
            break;
          }
        } /* if st_lookup_int()  */
        FREE(tmpStr);
        FREE(varName);
      } /* if (bAigId != bAig_Zero) */
    }
    NodeName = Ntk_NodeReadName(node); 
    if((NodeName[0] == '$') && (NodeName[1] == '_'))
    {
      if (value >= 0){
        Var_Variable_t *nodeVar = Ntk_NodeReadVariable(node);
        
        prevValue[j] = value;
        if (Var_VariableTestIsSymbolic(nodeVar)) {
          char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value);
          
          (void) fprintf(vis_stdout,"%s",   symbolicValue);
        } 
        else {
          (void) fprintf(vis_stdout,"%d",  value);
        }
      } else {
      /*
        This variable does not have value in the current time frame. It means its value
        is not important at this time frame.
       */
        (void) fprintf(vis_stdout,"x" );
      }
    } /* these nodes are latches in front of inputs so they will be printed out as inputs */
  } /* for j loop */
}/* end of printValueAigerInputs() */