src/bmc/bmcUtil.c

Go to the documentation of this file.

#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                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* 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);

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


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

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


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                                          */
/*---------------------------------------------------------------------------*/

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 */


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 */


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


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 */

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


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

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() */



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

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

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

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

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

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 */

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 */


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() */

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() */


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() */


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

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

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


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

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

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

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

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()*/

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() */

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() */

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() */

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() */

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() */

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

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


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() */

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() */

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() */


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

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 */


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                                            */
/*---------------------------------------------------------------------------*/

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

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

} /* end of signatureCompare */




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() */



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() */


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() */