src/bmc/bmcCirCUsUtil.c

Go to the documentation of this file.

#include "bmcInt.h"
#include "sat.h"

static char rcsid[] UNUSED = "$Id: bmcCirCUsUtil.c,v 1.22 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 char * getBddName(bdd_manager *bddManager, bdd_node *node);
static bAigEdge_t getAigAtTimeFrame(bAig_Manager_t *manager, bAigEdge_t node, int i, int withInitialState);
static bAigEdge_t getAigOfBddAtState(Ntk_Network_t *network, bdd_node *node, int state, int withInitialState);

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

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

void
BmcCirCUsAutLtlCheckTerminalAutomaton(
  Ntk_Network_t            *network,
  bAig_Manager_t           *aigManager,
  st_table                 *nodeToMvfAigTable,
  BmcCheckForTermination_t *terminationStatus,
  st_table                 *coiIndexTable,
  BmcOption_t              *options)
{
  long            startTime, endTime;
  int             k = terminationStatus->k;
  int             returnStatus = 0;
  Ltl_Automaton_t *automaton = terminationStatus->automaton;
  satInterface_t  *tInterface, *etInterface;
  bAigEdge_t      autPath, property;
  array_t         *objArray;
  array_t         *previousResultArray;

  startTime = util_cpu_ctime();

  if (options->verbosityLevel == BmcVerbosityMax_c) {
    (void) fprintf(vis_stdout, "\nBMC: Check for termination\n");
  }
  etInterface = 0;
  tInterface  = 0;
    /*
    Hold objects
  */
  objArray = array_alloc(bAigEdge_t, 2);
  previousResultArray    = array_alloc(bAigEdge_t, 0);
  returnStatus = 0;

  autPath = BmcCirCUsCreateAigForSimpleCompositePath(network, aigManager, automaton,
                                                     0, k+1, nodeToMvfAigTable,
                                                     coiIndexTable,
                                                     BMC_NO_INITIAL_STATES);

  property = bAig_Not(
    BmcCirCUsBdd2Aig(network, automaton->fairSets, k, -1,
                     automaton, aigManager,  BMC_NO_INITIAL_STATES));

  property = bAig_And(aigManager, property,
                      BmcCirCUsBdd2Aig(network, automaton->fairSets, k+1, -1,
                                       automaton, aigManager,  BMC_NO_INITIAL_STATES));
  options->cnfPrefix = k+1;
  array_insert(bAigEdge_t, objArray, 0, property);
  array_insert(bAigEdge_t, objArray, 1, autPath);
  tInterface = BmcCirCUsInterfaceWithObjArr(aigManager, network, objArray,
                                            previousResultArray, options, tInterface);
  if(tInterface->status == SAT_UNSAT){
     returnStatus = 1;
  }

  /* ===========================
     Early termination condition
     ===========================
  */
  if ((options->earlyTermination)&&(returnStatus ==0)) {
    if (options->verbosityLevel == BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout, "\nChecking the early termination at k= %d\n", k);
    }

    autPath = BmcCirCUsCreateAigForSimpleCompositePath(network, aigManager, automaton,
                                                       0, k+1, nodeToMvfAigTable,
                                                       coiIndexTable,
                                                       BMC_INITIAL_STATES);
    array_insert(bAigEdge_t, objArray, 0, autPath);
    array_insert(bAigEdge_t, objArray, 1, bAig_One);
    options->cnfPrefix = k+1;
    etInterface = BmcCirCUsInterfaceWithObjArr(aigManager, network, objArray,
                                               previousResultArray, options, etInterface);

    if(etInterface->status == SAT_UNSAT){
      (void) fprintf(vis_stdout, "# BMC: by early termination\n");
      returnStatus = 1;
    }
  } /* Early termination */

  if (options->verbosityLevel != BmcVerbosityNone_c) {
    endTime = util_cpu_ctime();
    fprintf(vis_stdout, "-- Check for termination time time = %10g\n",
            (double)(endTime - startTime) / 1000.0);
  }
  array_free(objArray);
  array_free(previousResultArray);

  terminationStatus->action = returnStatus;

} /* BmcCirCUsAutLtlCheckTerminalAutomaton */



bAigEdge_t
BmcCirCUsBdd2Aig(
  Ntk_Network_t   *network,
  bdd_t           *function,
  int             current,
  int             next,
  Ltl_Automaton_t *automaton,
  bAig_Manager_t  *aigManager,
  int             withInitialState)
{
  bdd_manager *bddManager;
  bdd_node    *node;
  bdd_gen     *gen;

  array_t     *cube;
  int         i, value;
  int         state = current;
  bAigEdge_t  aigFunction, andFunction, aigNode;

  if (function == NULL){
    return bAig_NULL;
  }
  /*
    If BDD represents a constant value
   */
  if(bdd_is_tautology(function, 0)){
    return bAig_Zero;
  }
  if(bdd_is_tautology(function, 1)){
    return bAig_One;
  }

  bddManager = bdd_get_manager(function);
  aigFunction = bAig_Zero;
  foreach_bdd_cube(function, gen, cube){
    andFunction = bAig_One;
    arrayForEachItem(int, cube, i, value){
      if (value != 2){
        int j;
        /*
          If the BDD varaible is a next state varaible, we use the corresponding
          current state varaible but with next state index.
        */
        if (next != -1 && st_lookup_int(automaton->nsPsTable, (char *)(long)i, &j)){
          node = bdd_bdd_ith_var(bddManager, j);
          state = next;
        } else {
          node = bdd_bdd_ith_var(bddManager, i);
          state = current;
        }
        aigNode = getAigOfBddAtState(network, node, state, withInitialState);
        if (value == 0){
          aigNode = bAig_Not(aigNode);
        }
        andFunction = bAig_And(aigManager, andFunction, aigNode);
      }
    }
    aigFunction = bAig_Or(aigManager, aigFunction, andFunction);
  }/* foreach_bdd_cube */

  return aigFunction;
} /* BmcCirCUsBdd2Aig */


bAigEdge_t
BmcCirCUsAutCreateAigForPath(
  Ntk_Network_t   *network,
  bAig_Manager_t  *aigManager,
  Ltl_Automaton_t *automaton,
  int             fromState,
  int             toState,
  int             initialState)
{
  int        k;
  bAigEdge_t result, aigFunction = bAig_One;

  if(initialState){
    result = BmcCirCUsBdd2Aig(network, automaton->initialStates, 0, -1,
                              automaton, aigManager, initialState);
    aigFunction = result;
  }
  for(k=fromState; k<toState; k++){
   result = BmcCirCUsBdd2Aig(network, automaton->transitionRelation, k, k+1,
                              automaton, aigManager, initialState);
    aigFunction = bAig_And(aigManager , aigFunction, result);
  }
  return aigFunction;

} /* BmcCirCUsAutCreateAigForPath */

bAigEdge_t
BmcCirCUsAutCreateAigForSimplePath(
  Ntk_Network_t   *network,
  bAig_Manager_t  *aigManager,
  Ltl_Automaton_t *automaton,
  int             fromState,
  int             toState,
  int             initialState)
{
  int        i, j, bddID;
  bAigEdge_t result, aigFunction, next, current;
  mdd_manager        *bddManager = Ntk_NetworkReadMddManager(network);
  st_generator       *stGen;

  bdd_node           *node;



  aigFunction = BmcCirCUsAutCreateAigForPath(network, aigManager, automaton,
                                             fromState, toState, initialState);
  /*
    The path is simple path
  */
  for(i = fromState + 1; i <= toState; i++){
    for(j=fromState; j < i; j++){
      result = bAig_Zero;
      st_foreach_item(automaton->psNsTable, stGen,&bddID, NULL) {
        node = bdd_bdd_ith_var(bddManager, bddID);

        current = getAigOfBddAtState(network, node, i, initialState);
        next    = getAigOfBddAtState(network, node, j, initialState);

        result = bAig_Or(aigManager, result,
                         bAig_Not(bAig_Eq(aigManager, current, next)));
      }
      aigFunction = bAig_And(aigManager, aigFunction, result);
    }
  }

  return aigFunction;

} /* BmcCirCUsAutCreateAigForSimplePath */

bAigEdge_t
BmcCirCUsCreateAigForSimpleCompositePath(
  Ntk_Network_t   *network,
  bAig_Manager_t  *aigManager,
  Ltl_Automaton_t *automaton,
  int             fromState,
  int             toState,
  st_table        *nodeToMvfAigTable,
  st_table        *coiIndexTable,
  int             initialState)
{
  int        i, j, bddID;
  bAigEdge_t         result, aigFunction, next, current;
  mdd_manager        *bddManager = Ntk_NetworkReadMddManager(network);
  st_generator       *stGen;

  bdd_node           *node;



  /*
    Build a path in the original model
   */
  bAig_ExpandTimeFrame(network, aigManager, toState+1, initialState);
  /*
    Build a path in the automaton
   */
  aigFunction = BmcCirCUsAutCreateAigForPath(network, aigManager, automaton,
                                             fromState, toState, initialState);
  /*
    Constrains the two paths to be simple paths
  */
  for(i = fromState + 1; i <= toState; i++){
    for(j=fromState; j < i; j++){
      result = bAig_Zero;

      /*
        Unique states in the automaton
       */
      st_foreach_item(automaton->psNsTable, stGen, &bddID, NULL) {
        node = bdd_bdd_ith_var(bddManager, bddID);

        current = BmcCirCUsBdd2Aig(network, bdd_construct_bdd_t(bddManager, node), i, -1,
                                   automaton, aigManager,
                                   initialState);
        next    = BmcCirCUsBdd2Aig(network, bdd_construct_bdd_t(bddManager,node), j, -1,
                                   automaton, aigManager,
                                   initialState);
        /*
          next    = BmcCirCUsBdd2Aig(network, bdd_construct_bdd_t(bddManager,node), i, j,
                                   automaton, aigManager,
                                   initialState);

          result = bAig_Or(aigManager, result,
                                   bAig_Not(next));
        */
        result = bAig_Or(aigManager, result,
                         bAig_Not(bAig_Eq(aigManager, current, next)));
      }
      /*
        Unique states in the original model
      */
      result = bAig_Or(aigManager, result,
                       bAig_Not(BmcCirCUsConnectFromStateToState(network, i-1, j,
                                                                 nodeToMvfAigTable,
                                                                 coiIndexTable,
                                                                 initialState)));
      aigFunction = bAig_And(aigManager, aigFunction, result);
    }
  }

  return aigFunction;

} /* BmcCirCUsCreateAigForSimpleCompositePath */



void
BmcCirCUsAutLtlCheckForTermination(
  Ntk_Network_t            *network,
  bAig_Manager_t           *aigManager,
  st_table                 *nodeToMvfAigTable,
  BmcCheckForTermination_t *terminationStatus,
  st_table                 *coiIndexTable,
  BmcOption_t              *options)
{
  long            startTime, endTime;
  int             k = terminationStatus->k;
  int             returnStatus = 0;
  Ltl_Automaton_t *automaton = terminationStatus->automaton;
  Ctlsp_Formula_t *externalConstraints = terminationStatus->externalConstraints;
  satInterface_t  *tInterface, *etInterface;
  bAigEdge_t      autPath, property, tmp;
  array_t         *objArray;
  array_t         *previousResultArray;
  array_t         *previousResultArrayWOI;

  /*
    If checkLevel == 0 -->  check for beta' and beta'' only and if either UNSAT, m=k and chekLevel =1
    If checkLevel == 1 -->  check for beta  only and if UNSAT, checkLevel = 2.
    If checkLevel == 2 -->  check for alpha only and if UNSAT, n=k and checkLevel = 3.
    If gama is UNSAT up to (m+n-1) and checkLvel = 3, formula passes.
    checkLevel = 4 if (m+n-1) > maxK;
   */
  startTime = util_cpu_ctime();

  etInterface = 0;
  tInterface  = 0;
    /*
    Hold objects
  */
  objArray = array_alloc(bAigEdge_t, 2);

  previousResultArray    = array_alloc(bAigEdge_t, 0);
  previousResultArrayWOI = array_alloc(bAigEdge_t, 0);

  /* ===========================
     Early termination condition
     ===========================
  */
  if (options->earlyTermination) {
    if (options->verbosityLevel == BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout, "\nChecking the early termination at k= %d\n", k);
    }

    autPath = BmcCirCUsCreateAigForSimpleCompositePath(network, aigManager, automaton,
                                                       0, k, nodeToMvfAigTable,
                                                       coiIndexTable,
                                                       BMC_INITIAL_STATES);
    array_insert(bAigEdge_t, objArray, 0, autPath);
    array_insert(bAigEdge_t, objArray, 1, bAig_One);
    options->cnfPrefix = k;
    etInterface = BmcCirCUsInterfaceWithObjArr(aigManager, network, objArray,
                                     previousResultArray, options, etInterface);

    if(etInterface->status == SAT_UNSAT){
      (void) fprintf(vis_stdout, "# BMC: by early termination\n");
      terminationStatus->action = 3;
      return;
    }
  } /* Early termination */
  if((!automaton->fairSets) &&
     (terminationStatus->checkLevel == 0)) {
    /*
      All the automaton states are fair states. So, beta' and beta are always UNSAT.
    */
    terminationStatus->m = 0;
    printf("Value of m = %d\n", terminationStatus->m);
    terminationStatus->checkLevel = 2;
  }

   /*
    Check \beta''(k)
  */
  if(terminationStatus->checkLevel == 0){
    int i;

    if (options->verbosityLevel == BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout, "# BMC: Check Beta''\n");
    }
    autPath = BmcCirCUsCreateAigForSimpleCompositePath(network, aigManager, automaton,
                                                       0, k+1, nodeToMvfAigTable,
                                                       coiIndexTable, BMC_NO_INITIAL_STATES);
    property = bAig_One;
    for(i=1; i<=k+1; i++){
      tmp = BmcCirCUsBdd2Aig(network, automaton->fairSets, i, -1,
                             automaton, aigManager,
                             BMC_NO_INITIAL_STATES);

      if(externalConstraints){
        tmp = bAig_Or(aigManager, tmp,
                      BmcCirCUsCreatebAigOfPropFormula(network, aigManager, i,
                                                       externalConstraints,
                                                       BMC_NO_INITIAL_STATES));
      }
      property = bAig_And(aigManager, property, bAig_Not(tmp));
    }

    tmp = BmcCirCUsBdd2Aig(network, automaton->fairSets, 0, -1,
                           automaton, aigManager,  BMC_NO_INITIAL_STATES);
    if(externalConstraints){
      tmp = bAig_Or(aigManager, tmp,
                    BmcCirCUsCreatebAigOfPropFormula(network, aigManager, 0,
                                                     externalConstraints,
                                                     BMC_NO_INITIAL_STATES));
    }
    property = bAig_And(aigManager, property, tmp);

    options->cnfPrefix = k+1;
    array_insert(bAigEdge_t, objArray, 0, property);
    array_insert(bAigEdge_t, objArray, 1, autPath);
    tInterface = BmcCirCUsInterfaceWithObjArr(aigManager, network, objArray,
                                    previousResultArray, options, tInterface);
    if(tInterface->status == SAT_UNSAT){
      terminationStatus->m = k;
      (void)fprintf(vis_stderr,"m = %d\n", terminationStatus->m);
      terminationStatus->checkLevel = 1;
    }
  } /* Check for Beta'' */

  /*
    Check \beta'(k)
  */
  if(terminationStatus->checkLevel == 0){
    int i;

    if (options->verbosityLevel == BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout, "# BMC: Check Beta'\n");
    }
    autPath = BmcCirCUsCreateAigForSimpleCompositePath(network, aigManager, automaton,
                                                       0, k+1, nodeToMvfAigTable,
                                                       coiIndexTable, BMC_NO_INITIAL_STATES);
    property = bAig_One;
    for(i=0; i<=k; i++){
      tmp = BmcCirCUsBdd2Aig(network, automaton->fairSets, i, -1,
                             automaton, aigManager,
                             BMC_NO_INITIAL_STATES);
      if(externalConstraints){
        tmp = bAig_Or(aigManager, tmp,
                      BmcCirCUsCreatebAigOfPropFormula(network, aigManager, i,
                                                       externalConstraints,
                                                       BMC_NO_INITIAL_STATES));
      }
      property = bAig_And(aigManager, property, bAig_Not(tmp));
    }
    tmp = BmcCirCUsBdd2Aig(network, automaton->fairSets, k+1, -1,
                           automaton, aigManager,
                           BMC_NO_INITIAL_STATES);
    if(externalConstraints){
      tmp = bAig_Or(aigManager, tmp,
                    BmcCirCUsCreatebAigOfPropFormula(network, aigManager, k+1,
                                                     externalConstraints,
                                                     BMC_NO_INITIAL_STATES));
    }
    property = bAig_And(aigManager, property, tmp);

    options->cnfPrefix = k+1;
    array_insert(bAigEdge_t, objArray, 0, property);
    array_insert(bAigEdge_t, objArray, 1, autPath);
    tInterface = BmcCirCUsInterfaceWithObjArr(aigManager, network, objArray,
                                    previousResultArray, options, tInterface);
    if(tInterface->status == SAT_UNSAT){
      terminationStatus->m = k;
      (void)fprintf(vis_stderr,"m = %d\n", terminationStatus->m);
      terminationStatus->checkLevel = 1;
    }
  } /* Check for Beta' */

  /*
    Check for Beta.
  */
  if(terminationStatus->checkLevel == 1){

    if (options->verbosityLevel == BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout, "# BMC: Check Beta\n");
    }
    autPath = BmcCirCUsCreateAigForSimpleCompositePath(network, aigManager, automaton,
                                                       0, k+1, nodeToMvfAigTable,
                                                       coiIndexTable, BMC_NO_INITIAL_STATES);
    property = bAig_One;

    tmp = BmcCirCUsBdd2Aig(network, automaton->fairSets, k, -1,
                           automaton, aigManager,  BMC_NO_INITIAL_STATES);

    if(externalConstraints){
      tmp = bAig_Or(aigManager, tmp,
                    BmcCirCUsCreatebAigOfPropFormula(network, aigManager, k,
                                                     externalConstraints,
                                                     BMC_NO_INITIAL_STATES));
    }
    property = bAig_And(aigManager, property, bAig_Not(tmp));

    tmp = BmcCirCUsBdd2Aig(network, automaton->fairSets, k+1, -1,
                           automaton, aigManager,  BMC_NO_INITIAL_STATES);
    if(externalConstraints){
      tmp = bAig_Or(aigManager, tmp,
                    BmcCirCUsCreatebAigOfPropFormula(network, aigManager, k+1,
                                                     externalConstraints,
                                                     BMC_NO_INITIAL_STATES));
    }
    property = bAig_And(aigManager, property, tmp);

    options->cnfPrefix = k+1;
    array_insert(bAigEdge_t, objArray, 0, property);
    array_insert(bAigEdge_t, objArray, 1, autPath);
    tInterface = BmcCirCUsInterfaceWithObjArr(aigManager, network, objArray,
                                    previousResultArray, options, tInterface);
    if(tInterface->status == SAT_UNSAT){
      terminationStatus->checkLevel = 2;
    }
  } /* Check Beta*/

  if(terminationStatus->checkLevel == 2){ /* we check Alpha if Beta is unsatisfiable */

    if (options->verbosityLevel == BmcVerbosityMax_c) {
      (void) fprintf(vis_stdout, "# BMC: Check Alpha \n");
    }
    autPath = BmcCirCUsCreateAigForSimpleCompositePath(network, aigManager, automaton,
                                                       0, k, nodeToMvfAigTable,
                                                       coiIndexTable,
                                                       BMC_INITIAL_STATES);
    array_insert(bAigEdge_t, objArray, 1, bAig_One);
    property = bAig_Zero;
    if(automaton->fairSets){
      property =  BmcCirCUsBdd2Aig(network, automaton->fairSets, k, -1,
                                   automaton, aigManager,  BMC_INITIAL_STATES);
      array_insert(bAigEdge_t, objArray, 1, property);
    }
    if(externalConstraints){
      property = bAig_Or(aigManager, property,
                         BmcCirCUsCreatebAigOfPropFormula(network, aigManager, k,
                                                          externalConstraints,
                                                          BMC_INITIAL_STATES));
      array_insert(bAigEdge_t, objArray, 1, property);
    }
    options->cnfPrefix = k;
    array_insert(bAigEdge_t, objArray, 0, autPath);
    tInterface = 0;
    tInterface = BmcCirCUsInterfaceWithObjArr(aigManager, network,
                                              objArray, previousResultArray,
                                              options, tInterface);
    if(tInterface->status == SAT_UNSAT){
      terminationStatus->n = k;
      terminationStatus->checkLevel = 3;
      (void)fprintf(vis_stdout,"Value of m=%d  n=%d\n",terminationStatus->m,terminationStatus->n);
      if ((terminationStatus->m+terminationStatus->n-1) <= options->maxK){
        terminationStatus->k = terminationStatus->m+terminationStatus->n-1;
        if(k==0){
          /*
            By induction, the property passes.
           */
          terminationStatus->k = 0;
        }
        returnStatus = 1;
      } else {
        terminationStatus->checkLevel = 4;
        returnStatus = 2;
      }
    }
  }/* Chek for Alpha */

  if (options->verbosityLevel != BmcVerbosityNone_c) {
    endTime = util_cpu_ctime();
    fprintf(vis_stdout, "-- Check for termination time time = %10g\n",
            (double)(endTime - startTime) / 1000.0);
  }

  terminationStatus->action = returnStatus;

} /* BmcAutLtlCheckForTermination */


char *
BmcCirCUsCallCirCUs(
  BmcOption_t *options)
{
  satOption_t  *satOption;
  satManager_t *cm;
  int          maxSize;
  char         *fileName = NIL(char);

  satOption          = sat_InitOption();
  satOption->verbose = options->verbosityLevel-1;

  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 << 8;
  cm->nodesArray = ALLOC(bAigEdge_t, maxSize);
  cm->maxNodesArraySize = maxSize;
  cm->nodesArraySize = satNodeSize;

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

    if(!(cm->stdOut = fopen(options->satOutFile, "w"))) {
      fprintf(stdout, "ERROR : Can't open file %s\n", options->satOutFile);
      cm->stdOut = stdout;
      cm->stdErr = stderr;
    }
    sat_PrintSatisfyingAssignment(cm);
    fileName = options->satOutFile;
  }
  sat_FreeManager(cm);

  return fileName;
} /* BmcCallCirCUs */

char *
BmcCirCUsCallCusp(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;
  char        *fileName = NIL(char);

  /*
    Prepare to call external CNF SAT solver
   */
  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(char);
    }
    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 external sat solver.  It may not be in your path.  Status = %d\n", satStatus);
    options->satSolverError = TRUE;
    return NIL(char);
  }

  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(char);
  }
  /* 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(char);
      }
      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;
    }
    (void) fclose(fp);
    fp = Cmd_FileOpen(options->satOutFile, "w", NIL(char *), 0);
    for(num=0; num < array_n(result); num++){
      fprintf(fp,"%d ", array_fetch(int, result, num));
      if(((num+1) %10) == 0){
        fprintf(fp,"\n");
      }
    }
    array_free(result);
    (void) fclose(fp);
    fileName = options->satOutFile;
  } 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);

  return fileName;
} /* BmcCirCUsCallCusp */


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

static char *
getBddName(
  bdd_manager *bddManager,
  bdd_node *node)
{
  array_t   *mvar_list  = mdd_ret_mvar_list(bddManager);
  array_t   *bvar_list  = mdd_ret_bvar_list(bddManager);
  char      name[100];
  bvar_type bv;
  mvar_type mv;
  int       nodeIndex = bdd_node_read_index(node);
  int       index, rtnNodeIndex;

  /*
    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);
    sprintf(name, "%s_%d", mv.name, index);
  } else {
    sprintf(name, "Bdd_%d", nodeIndex);
  }
  return util_strsav(name);
}

static bAigEdge_t
getAigAtTimeFrame(
  bAig_Manager_t *manager,
  bAigEdge_t node,
  int        i,
  int withInitialState)
{
  bAigTimeFrame_t *timeframe;
  bAigEdge_t     result, *li;
  int            index;

  result = bAig_NULL;

  if(withInitialState) timeframe = manager->timeframe;
  else                 timeframe = manager->timeframeWOI;

  if(st_lookup_int(timeframe->li2index, (char *)node, &index)) {
    li = timeframe->latchInputs[i];
    result = bAig_GetCanonical(manager, li[index]);
  }
  else if(st_lookup_int(timeframe->o2index, (char *)node, &index)) {
    li = timeframe->outputs[i];
    result = bAig_GetCanonical(manager, li[index]);
  }
  else if(st_lookup_int(timeframe->i2index, (char *)node, &index)) {
    li = timeframe->internals[i];
    result = bAig_GetCanonical(manager, li[index]);
  }
  else if(st_lookup_int(timeframe->bli2index, (char *)node, &index)) {
    li = timeframe->blatchInputs[i];
    result = bAig_GetCanonical(manager, li[index]);
  }
  else if(st_lookup_int(timeframe->bpi2index, (char *)node, &index)) {
    li = timeframe->binputs[i];
    result = bAig_GetCanonical(manager, li[index]);
  }
  return result;
}

static bAigEdge_t
getAigOfBddAtState(
  Ntk_Network_t   *network,
  bdd_node        *node,
  int             state,
  int             withInitialState)
{
  mdd_manager      *bddManager = Ntk_NetworkReadMddManager(network);
  mAig_Manager_t   *aigManager = Ntk_NetworkReadMAigManager(network);

  char        *nodeName, *nameKey;
  char        tmpName[100];
  bAigEdge_t  aigNode, rtnAig;

  nodeName = getBddName(bddManager, bdd_regular(node));
  aigNode  = bAig_FindNodeByName(aigManager, nodeName);
  if(aigNode == bAig_NULL){
    sprintf(tmpName, "%s_%d_%d", nodeName, withInitialState, state);
    nameKey = util_strsav(tmpName);
    aigNode  = bAig_FindNodeByName(aigManager, nameKey);
    if(aigNode == bAig_NULL){
      aigNode = bAig_CreateVarNode(aigManager, nameKey);
    } else {
      FREE(nameKey);
    }
    rtnAig = aigNode;
  } else {
    aigNode = bAig_GetCanonical(aigManager, aigNode);
    rtnAig  = getAigAtTimeFrame(aigManager, aigNode, state, withInitialState);
    if(rtnAig == bAig_NULL){
      rtnAig = bAig_CreateNode(aigManager, bAig_NULL, bAig_NULL);
    }
  }
  return bAig_GetCanonical(aigManager, rtnAig);
} /* getAigOfBddAtState */