src/bmc/bmcCmd.c

Go to the documentation of this file.

#include "bmcInt.h"

static char rcsid[] UNUSED = "$Id: bmcCmd.c,v 1.83 2010/04/09 23:50:57 fabio Exp $";

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

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


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


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/
static jmp_buf timeOutEnv;
static int bmcTimeOut;          /* timeout value */
static long alarmLapTime;       /* starting CPU time for timeout */

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

static BmcOption_t * ParseBmcOptions(int argc, char **argv);
static int CommandBmc(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static void TimeOutHandle(void);
static void DispatchBmcCommand(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, array_t *constraintArray, BmcOption_t *options);
static int CommandCnfSat(Hrc_Manager_t ** hmgr, int argc, char ** argv);

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

void
Bmc_Init(void)
{
  Cmd_CommandAdd("bounded_model_check", CommandBmc, /* doesn't change network */  0);
  
  Cmd_CommandAdd("cnf_sat", CommandCnfSat, /* doesn't change network */  0); 
}

void
Bmc_End(void)
{
}

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


static BmcOption_t *
ParseBmcOptions(
  int argc,
  char **argv)
{
  BmcOption_t  *options = BmcOptionAlloc();
  char *ltlFileName     = NIL(char);
  unsigned int i;
  int          c;
  
  if (!options){
    return NIL(BmcOption_t);
  }
  
  options->dbgOut = 0;
  /*
   * Parse command line options.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "E:C:S:F:O::I:hiv:m:k:s:o:t:d:r:e")) != EOF) {
    switch(c) {
    case 'F':
      options->fairFile = Cmd_FileOpen(util_optarg, "r", NIL(char *), 0);
      if (options->fairFile == NIL(FILE)) {
        (void) fprintf(vis_stdout,
                       "** bmc error: Cannot open the file %s\n",
                       util_optarg);
        BmcOptionFree(options);
        return NIL(BmcOption_t);
      }
      break;
    case 'O':
      options->dbgOut = Cmd_FileOpen(util_optarg, "w", NIL(char *), 0);
      if(options->dbgOut == NIL(FILE)) {
        (void) fprintf(vis_stdout, "**bmc error: Cannot open %s for debug information.\n", util_optarg);
         BmcOptionFree(options);
         return NIL(BmcOption_t);
      } 
      break;
    case 'm':
      for (i = 0; i < strlen(util_optarg); i++) {
        if (!isdigit((int)util_optarg[i])) {
          goto usage;
        }
      }
      options->minK = atoi(util_optarg);
      break;
    case 'k':
      for (i = 0; i < strlen(util_optarg); i++) {
        if (!isdigit((int)util_optarg[i])) {
          goto usage;
        }
      }
      options->maxK = atoi(util_optarg);
      break;
    case 's':
      for (i = 0; i < strlen(util_optarg); i++) {
        if (!isdigit((int)util_optarg[i])) {
          goto usage;
        }
      }
      options->step = atoi(util_optarg);
      break;
    case 'r':
      for (i = 0; i < strlen(util_optarg); i++) {
        if (!isdigit((int)util_optarg[i])) {
          goto usage;
        }
      }
      options->inductiveStep = atoi(util_optarg);
      break;
    case 'e':
      options->earlyTermination = TRUE;
      break;    
    case 'd':
      for (i = 0; i < strlen(util_optarg); i++) {
        if (!isdigit((int)util_optarg[i])) {
          goto usage;
        }
      }
      options->dbgLevel = atoi(util_optarg);
      break;    
    case 't' :
      options->timeOutPeriod = atoi(util_optarg);
        break;
    case 'i':
      options->printInputs = TRUE;
      break;    
    case 'h':
      goto usage;
    case 'v':
      for (i = 0; i < strlen(util_optarg); i++) {
        if (!isdigit((int)util_optarg[i])) {
          goto usage;
        }
      }
      options->verbosityLevel = (Bmc_VerbosityLevel) atoi(util_optarg);
      break;
    case 'o':
      options->cnfFileName = util_strsav(util_optarg);
      break;    
    case 'I' :
      options->incremental = atoi(util_optarg);
      break;
    case 'E':
      for (i = 0; i < strlen(util_optarg); i++) {
        if (!isdigit((int)util_optarg[i])) {
          goto usage;
        }
      }
      options->encoding = atoi(util_optarg);
      if((options->encoding < 0) || (options->encoding > 2)){
        goto usage;
      }
      break;
    case 'S':
      for (i = 0; i < strlen(util_optarg); i++) {
        if (!isdigit((int)util_optarg[i])) {
          goto usage;
        }
      }
      options->satSolver = atoi(util_optarg);
      if((options->satSolver < 0) || (options->satSolver > 1)){
        goto usage;
      }
      break;
    case 'C':
      for (i = 0; i < strlen(util_optarg); i++) {
        if (!isdigit((int)util_optarg[i])) {
          goto usage;
        }
      }
      options->clauses = atoi(util_optarg);
      if((options->clauses < 0) || (options->clauses > 2)){
        goto usage;
      }
      break;
    default:
      goto usage;
    }
  }
  if (options->minK > options->maxK){
    (void) fprintf(vis_stderr, "** bmc error: value for -m option must not be greater than vlaue for -k option\n");    
    goto usage;
  }
  /*
   * Open the ltl file.
   */
  if (argc - util_optind == 0) {
    (void) fprintf(vis_stderr, "** bmc error: file containing ltl formulae not provided\n");
    goto usage;
  }
  else if (argc - util_optind > 1) {
    (void) fprintf(vis_stderr, "** bmc error: too many arguments\n");
    goto usage;
  }
  ltlFileName = util_strsav(argv[util_optind]);
  
  /* Read LTL Formulae */
  if (!ltlFileName) 
      goto usage;

  options->ltlFile = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0);
  if (options->ltlFile == NIL(FILE)) {
    (void) fprintf(vis_stdout,"** bmc error: Cannot open the file %s\n", ltlFileName);
    FREE(ltlFileName);
    BmcOptionFree(options);
    return NIL(BmcOption_t);
  }
  FREE(ltlFileName);
  /* create SAT Solver input file */
  if (options->cnfFileName == NIL(char)) {
    options->satInFile = BmcCreateTmpFile(); 
    if (options->satInFile == NIL(char)){
      BmcOptionFree(options);
      return NIL(BmcOption_t);
    }
  } else {
    options->satInFile = options->cnfFileName;
  }
  /* create SAT Solver output file */
  options->satOutFile = BmcCreateTmpFile();
  if (options->satOutFile == NIL(char)){
    BmcOptionFree(options);
    return NIL(BmcOption_t);
  }
  return options;
  
 usage:
  (void) fprintf(vis_stderr, "usage: bmc [-h][-m minimum_length][-k maximum_length][-s step][-r inductive_step][-e][-F <fairness_file>][-d debug_level][-E <encoding>][-C <clauses>][-S <sat_solver>][-O <debug_file>][-I <level>][-v verbosity_level][-t period][-o <cnf_file>] <ltl_file>\n");
  (void) fprintf(vis_stderr, "   -h \tprint the command usage\n");
  (void) fprintf(vis_stderr, "   -m \tminimum length of counterexample to be checked (default is 0)\n");  
  (void) fprintf(vis_stderr, "   -k \tmaximum length of counterexample to be checked (default is 1)\n");
  (void) fprintf(vis_stderr, "   -s \tincrementing value of counterexample length (default is 1)\n");
  (void) fprintf(vis_stderr, "   -r \tUse check for termination at each inductive_step to check if the property passes (default is 0).\n");
  (void) fprintf(vis_stderr, "   -e \tUse early termination to check if the property passes. Valid only with -r \n"); 
  (void) fprintf(vis_stderr, "   -F <fairness_file>\n");
  (void) fprintf(vis_stderr, "   -d <debug_level>\n");
  (void) fprintf(vis_stderr, "       debug_level = 0 => No debugging performed (Default)\n");
  (void) fprintf(vis_stderr, "       debug_level = 1 => Debugging with minimal output: generate counter-example if the LTL formula fails.\n");
  (void) fprintf(vis_stderr, "       debug_level = 2 => Debugging with full output in Aiger format: generate counter-example if the LTL formula fails.\n");
  (void) fprintf(vis_stderr, "   -O <debug_file>\n");
  (void) fprintf(vis_stderr, "   -i \tPrint input values in debug traces.\n");
  (void) fprintf(vis_stderr, "   -v <verbosity_level>\n");
  (void) fprintf(vis_stderr, "       verbosity_level = 0 => no feedback (Default)\n");
  (void) fprintf(vis_stderr, "       verbosity_level = 1 => code status\n");
  (void) fprintf(vis_stderr, "       verbosity_level = 2 => code status and CPU usage profile\n");
  (void) fprintf(vis_stderr, "   -t <period> time out period\n");
  (void) fprintf(vis_stderr, "   -E <encoding>\n");
  (void) fprintf(vis_stderr, "       encoding = 0 => Original BMC encoding (Default)\n");
  (void) fprintf(vis_stderr, "       encoding = 1 => SNF encoding\n");
  (void) fprintf(vis_stderr, "       encoding = 2 => Fixpoint encoding\n");
  /*
  (void) fprintf(vis_stderr, "       encoding = 3 => FNF encoding\n");
  */
  (void) fprintf(vis_stderr, "   -S <sat_solver>\n");
  (void) fprintf(vis_stderr, "       sat_solver = 0 => CirCUs (Default)\n");
  (void) fprintf(vis_stderr, "       sat_solver = 1 => cusp\n");
  (void) fprintf(vis_stderr, "   -C <clauses>\n");
  (void) fprintf(vis_stderr, "       clauses = 0 => Apply CirCUs on circuit (Default)\n");
  (void) fprintf(vis_stderr, "       clauses = 1 => Apply SAT solver on CNF (new)\n");
  (void) fprintf(vis_stderr, "       clauses = 2 => Apply SAT solver on CNF (old)\n");
  (void) fprintf(vis_stderr, "   -I <level>\n");
  (void) fprintf(vis_stderr, "       level = 1 => Trace Objective\n");
  (void) fprintf(vis_stderr, "       level = 2 => Distill\n");
  (void) fprintf(vis_stderr, "       level = 3 => Trace Objective + Distill\n");
  (void) fprintf(vis_stderr, "   -o <cnf_file> contains CNF of the counterexample\n");
  (void) fprintf(vis_stderr, "   <ltl_file> The input file containing LTL formulae to be checked.\n");

  BmcOptionFree(options);
  return NIL(BmcOption_t);
}

BmcOption_t *
BmcOptionAlloc(void)
{
  BmcOption_t *result = ALLOC(BmcOption_t, 1);
  
  if (!result){
    return result;
  }
  result->ltlFile = NIL(FILE);
  result->fairFile = NIL(FILE);
  result->cnfFileName = NIL(char);
  result->minK = 0;
  result->maxK = 1;
  result->step = 1;
  result->timeOutPeriod  = 0;
  result->startTime = 0;
  result->verbosityLevel = BmcVerbosityNone_c;
  result->dbgLevel       = 0;
  result->inductiveStep  = 0;
  result->printInputs    = FALSE;
  result->satSolverError = FALSE;
  result->satInFile  = NIL(char);
  result->satOutFile = NIL(char);
  result->incremental = 0;
  result->earlyTermination = 0;
  result->satSolver = CirCUs;  /* default is 0 */
  result->clauses   = 0;  /* default is 0 */
  result->encoding  = 0;  /* default is 0 */
  return result;
}

void
BmcOptionFree(
  BmcOption_t *result)
{
  if (result->ltlFile != NIL(FILE)){
    fclose(result->ltlFile);
  }
  if (result->cnfFileName != NIL(char)){
    FREE(result->cnfFileName);
  } else if (result->satInFile != NIL(char)) {
    unlink(result->satInFile);
    FREE(result->satInFile);
  }
  if (result->fairFile != NIL(FILE)){
    fclose(result->fairFile);
  }
  if (result->satOutFile != NIL(char)) {
    unlink(result->satOutFile);
    FREE(result->satOutFile);
  }
  FREE(result);
}

char *
BmcCreateTmpFile(void)
{
#if HAVE_MKSTEMP && HAVE_CLOSE  
  char   cnfFileName[] = "/tmp/vis.XXXXXX";
  int    fd;
#else
  char   *cnfFileName;
  char   buffer[512];
#endif

#if HAVE_MKSTEMP && HAVE_CLOSE    
  fd = mkstemp(cnfFileName);
  if (fd == -1){
#else
  cnfFileName = util_strsav(tmpnam(buffer));
  if (cnfFileName == NIL(char)){
#endif       
    (void)fprintf(vis_stderr,"** bmc error: Can not create temporary file. ");
    (void)fprintf(vis_stderr,"Clean up /tmp and try again.\n");
    return NIL(char);
  }
#if HAVE_MKSTEMP && HAVE_CLOSE
  close(fd);
#endif   
  return util_strsav(cnfFileName);
} /* createTmpFile() */

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


static int
CommandBmc(
  Hrc_Manager_t ** hmgr,
  int              argc,
  char          ** argv)
{
  Ntk_Network_t     *network;
  BmcOption_t       *options;
  int               i;
  array_t           *formulaArray;
  array_t           *LTLformulaArray;
  bAig_Manager_t    *manager;
  array_t           *constraintArray = NIL(array_t);

  /*
   * Parse command line options.
   */
  if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) {
      return 1;
  }
  /*
   * Read the network
   */
  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
  if (network == NIL(Ntk_Network_t)) {
    (void) fprintf(vis_stdout, "** bmc error: No network\n");
    BmcOptionFree(options);
    return 1;
  }
  manager = Ntk_NetworkReadMAigManager(network);
  if (manager == NIL(mAig_Manager_t)) {
    (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n");
    BmcOptionFree(options);
    return 1;
  }
  /*
    We need the bdd when building the transition relation of the automaton
  */
  if(options->inductiveStep !=0){
    Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t);
 
    designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
    if (designFsm == NIL(Fsm_Fsm_t)) {
      return 1;
    }
  }
  /* time out */
  if (options->timeOutPeriod > 0) {
    /* Set the static variables used by the signal handler. */
    bmcTimeOut = options->timeOutPeriod;
    alarmLapTime = options->startTime = util_cpu_ctime();
    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
    (void) alarm(options->timeOutPeriod);
    if (setjmp(timeOutEnv) > 0) {
      (void) fprintf(vis_stdout,
                     "\n# BMC: timeout occurred after %d seconds.\n",
                     options->timeOutPeriod);
      (void) fprintf(vis_stdout, "# BMC: data may be corrupted.\n");
      BmcOptionFree(options);
      alarm(0);
      return 1;
    }
  }
  formulaArray  = Ctlsp_FileParseFormulaArray(options->ltlFile);
  if (formulaArray == NIL(array_t)) {
    (void) fprintf(vis_stderr,
                   "** bmc error: error in parsing CTL* Fromula from file\n");
    BmcOptionFree(options);
    return 1;
  }
  if (array_n(formulaArray) == 0) {
    (void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
    BmcOptionFree(options);
    Ctlsp_FormulaArrayFree(formulaArray);
    return 1;
  }
  LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
  Ctlsp_FormulaArrayFree(formulaArray);
  if (LTLformulaArray ==  NIL(array_t)){
    (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
    BmcOptionFree(options);
    return 1;
  }
  if (options->fairFile != NIL(FILE)) {
    constraintArray = BmcReadFairnessConstraints(options->fairFile);
    if(constraintArray == NIL(array_t)){
      Ctlsp_FormulaArrayFree(LTLformulaArray);
      BmcOptionFree(options);
      return 1;
    }
    if(!Ctlsp_LtlFormulaArrayIsPropositional(constraintArray)){
      Ctlsp_FormulaArrayAddLtlFairnessConstraints(LTLformulaArray,
                                                  constraintArray);
      Ctlsp_FormulaArrayFree(constraintArray);
      constraintArray = NIL(array_t);
    }
  }
  /*
    Call a proper BMC function based on LTL formula.
  */
  for (i = 0; i < array_n(LTLformulaArray); i++) { 
    Ctlsp_Formula_t *ltlFormula     = array_fetch(Ctlsp_Formula_t *,
                                                  LTLformulaArray, i);
    
    DispatchBmcCommand(network, ltlFormula, constraintArray, options);
  }
  /*
    Free used memeory
  */
  if (constraintArray != NIL(array_t)){
    Ctlsp_FormulaArrayFree(constraintArray);
  }
  Ctlsp_FormulaArrayFree(LTLformulaArray);
  BmcOptionFree(options);
  fflush(vis_stdout);
  fflush(vis_stderr);
  alarm(0);
  return 0;

}/* CommandBmc() */

static void
TimeOutHandle(void)
{
  int seconds = (int) ((util_cpu_ctime() - alarmLapTime) / 1000);

  if (seconds < bmcTimeOut) {
    unsigned slack = (unsigned) (bmcTimeOut - seconds);
    (void) signal(SIGALRM, (void(*)(int)) TimeOutHandle);
    (void) alarm(slack);
  } else {
    longjmp(timeOutEnv, 1);
  }
} /* TimeOutHandle */


static void
DispatchBmcCommand(
  Ntk_Network_t   *network,
  Ctlsp_Formula_t *ltlFormula,
  array_t         *constraintArray,
  BmcOption_t     *options)
{
  Ctlsp_Formula_t *negLtlFormula = Ctlsp_LtllFormulaNegate(ltlFormula);
  st_table        *CoiTable      = st_init_table(st_ptrcmp, st_ptrhash);

  assert(ltlFormula != NIL(Ctlsp_Formula_t));
  assert(network != NIL(Ntk_Network_t));
 
  /*
    print out the given LTL formula
  */
  fprintf(vis_stdout, "Formula: ");
  Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
  fprintf(vis_stdout, "\n");
  if (options->verbosityLevel >= BmcVerbosityMax_c){
    fprintf(vis_stdout, "Negated formula: ");
    Ctlsp_FormulaPrint(vis_stdout, negLtlFormula);
    fprintf(vis_stdout, "\n");
  }
  /*
    Compute the cone of influence of the LTL formula
  */
  BmcGetCoiForLtlFormula(network, negLtlFormula, CoiTable);

  if(options->clauses == 2){
    /*
      Generate clauses for each time frame.  This is the old way of generating
      clauses in BMC.
    */
    if (constraintArray != NIL(array_t)){
      BmcLtlVerifyGeneralLtl(network, negLtlFormula, CoiTable,
                             constraintArray, options);
    } else /*
             If the LTL formula is propositional.
           */
      if(Ctlsp_isPropositionalFormula(negLtlFormula)){
        BmcLtlVerifyProp(network, negLtlFormula, CoiTable, options);
      } else /*
               If the LTL formula is of type G(p) (its negation is
               of type F(q)), where p and q are propositional.
             */
        if(Ctlsp_LtlFormulaIsFp(negLtlFormula)){
          BmcLtlVerifyGp(network, negLtlFormula, CoiTable, options);
        } else /*
                 If the LTL formula is of type F(p) (its negation is
                 of type G(q)), where p and q are propositional.
               */
          if (Ctlsp_LtlFormulaIsGp(negLtlFormula)){
            BmcLtlVerifyFp(network, negLtlFormula, CoiTable, options);
          } else /*
                   If the depth of the LTL formula (the maximum level
                   of nesting temporal operators) = 1
                 */
            /*
            if (Ctlsp_LtlFormulaDepth(negLtlFormula) == 1){
              BmcLtlVerifyUnitDepth(network, negLtlFormula, CoiTable, options);
            } else
            */
              /* 
                 If the LTL formula is of type FG(p) (its negation is
                 of type GF(q)), where p and q are propositional.
              */
              if(Ctlsp_LtlFormulaIsGFp(negLtlFormula)){
                BmcLtlVerifyFGp(network, negLtlFormula, CoiTable, options);
              } else
                /*
                  All other LTL formulae
                */
                BmcLtlVerifyGeneralLtl(network, negLtlFormula, CoiTable,
                                       NIL(array_t), options);
  } else {
    /*
     Build AIG for each time frame.
     */
    if (constraintArray != NIL(array_t)){
      if(options->encoding == 0){
       BmcCirCUsLtlVerifyGeneralLtl(network, negLtlFormula,
                                    CoiTable,
                                   constraintArray, options, 0);
      } else 
        if(options->encoding == 1){
          BmcCirCUsLtlVerifyGeneralLtl(network, negLtlFormula,
                                          CoiTable,
                                          constraintArray, options, 1);
        } else 
          if(options->encoding == 2){
            BmcCirCUsLtlVerifyGeneralLtlFixPoint(network, negLtlFormula,
                                                 CoiTable,
                                                 constraintArray, options);
          }
    } else
      /*
        If the LTL formula is propositional.
      */
      if(Ctlsp_isPropositionalFormula(negLtlFormula)){
        BmcCirCUsLtlVerifyProp(network, negLtlFormula, CoiTable, options);
      } else
        /*
          If the LTL formula is of type G(p) (its negation is
          of type F(q)), where p and q are propositional.
        */
        if(Ctlsp_LtlFormulaIsFp(negLtlFormula)){
          BmcCirCUsLtlVerifyGp(network, negLtlFormula, CoiTable, options);
        } else
          /*
            If the LTL formula is of type F(p) (its negation is
            of type G(q)), where p and q are propositional.
          */
          if (Ctlsp_LtlFormulaIsGp(negLtlFormula)){
            BmcCirCUsLtlVerifyFp(network, negLtlFormula, CoiTable, options);
          } else
            /*
              If the depth of the LTL formula (the maximum level
              of nesting temporal operators) = 1
              
              if (Ctlsp_LtlFormulaDepth(negLtlFormula) == 1){
              BmcLtlVerifyUnitDepth(network, negLtlFormula, CoiTable, options);
              } else
               
              If the LTL formula is of type FG(p) (its negation is
              of type GF(q)), where p and q are propositional.
            */
            if(Ctlsp_LtlFormulaIsGFp(negLtlFormula)){
              BmcCirCUsLtlVerifyFGp(network, negLtlFormula, CoiTable, options);
            } else
              if(Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(negLtlFormula) ||
                 (Ltl_AutomatonGetStrength(BmcAutLtlToAutomaton(network,ltlFormula)) == 0))
                {
                  BmcCirCUsLtlCheckSafety(network, negLtlFormula, options, CoiTable);
                }
              else {
                /*
                  All other LTL formulae
                */
                if(options->encoding == 0){
                  BmcCirCUsLtlVerifyGeneralLtl(network, negLtlFormula,
                                               CoiTable,
                                               NIL(array_t), options, 0);
                } else 
                  if(options->encoding == 1){
                    BmcCirCUsLtlVerifyGeneralLtl(network, negLtlFormula,
                                                    CoiTable,
                                                    NIL(array_t), options, 1);
                  } else 
                    if(options->encoding == 2){
                      BmcCirCUsLtlVerifyGeneralLtlFixPoint(network, negLtlFormula,
                                                 CoiTable,
                                                           NIL(array_t), options);
                    }
              } 
  }
  
  st_free_table(CoiTable);
  Ctlsp_FormulaFree(negLtlFormula);
} /* DispatchBmcCommand() */


static int
CommandCnfSat(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  satOption_t *option;
  char *filename, c;
  char *forcedAssignFilename;
  int timeOutPeriod, i;

  option = sat_InitOption();
  timeOutPeriod = -1;
  forcedAssignFilename = 0;
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "a:bf:ht:v:c:")) != EOF) {
    switch(c) {
      case 'h':
        goto usage;
      case 'b' :
        option->BDDMonolithic = 1;
        break;
      case 'f' :
        option->outFilename = strdup(util_optarg);
        break;
      case 'a' :
        forcedAssignFilename = strdup(util_optarg);
        break;
      case 't' :
        timeOutPeriod = atoi(util_optarg);
        break;
      case 'v':
        for (i = 0; i < (int)(strlen(util_optarg)); i++) {
          if (!isdigit((int)util_optarg[i])) {
            goto usage;
          }
        }
        option->verbose = (Bmc_VerbosityLevel) atoi(util_optarg);
        break;

        //Bing: for unsat core
      case 'c':
        option->coreGeneration = 1;
        option->unsatCoreFileName = strdup(util_optarg);
        option->minimizeConflictClause = 0;
        option->clauseDeletionHeuristic = 0;
        break;
      default:
        goto usage;
    }
  }

  if (argc - util_optind == 0) {
    (void) fprintf(vis_stderr, "** ERROR : file containing cnf file not provided\n");
    goto usage;
  }
  else if (argc - util_optind > 1) {
    (void) fprintf(vis_stderr, "** ERROR : too many arguments\n");
    goto usage;
  }
  filename = util_strsav(argv[util_optind]);

  if(forcedAssignFilename)
    option->forcedAssignArr = sat_ReadForcedAssignment(forcedAssignFilename);

  if (timeOutPeriod > 0) {
    bmcTimeOut = timeOutPeriod;
    alarmLapTime = util_cpu_ctime();
    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
    (void) alarm(timeOutPeriod);
    if (setjmp(timeOutEnv) > 0) {
      (void) fprintf(vis_stderr,
                "** ERROR : timeout occurred after %d seconds.\n", timeOutPeriod);
      alarm(0);
      return 1;
    }
  }

  sat_CNFMain(option, filename);

  return 0;

  usage:
  (void) fprintf(vis_stderr, "usage: cnf_sat [-h] [-v verboseLevel] [-t timeout] <cnf_file>\n");
  (void) fprintf(vis_stderr, "   -h \tprint the command usage\n");
  (void) fprintf(vis_stderr, "   -a <filename> \tto make forced assignment\n");
  (void) fprintf(vis_stderr, "   -f <filename> \twrite log to the file\n");
  (void) fprintf(vis_stderr, "   -b \tuse BDD based method\n");
  (void) fprintf(vis_stderr, "   -v <verbosity_level>\n");
  (void) fprintf(vis_stderr, "   -t <period> time out period\n");
  (void) fprintf(vis_stderr, "   -c <filename> UNSAT core generation\n");
  (void) fprintf(vis_stderr, "   <cnf_file> CNF file to be checked.\n");
  return 1;
}


#if 0

int
CommandBddSat(
  Hrc_Manager_t ** hmgr,
  int              argc,
  char          ** argv)
{
  Ntk_Network_t     *network;
  BmcOption_t       *options;
  array_t           *formulaArray;
  bAig_Manager_t    *mAigManager;
  Fsm_Fsm_t         *fsm;
  mdd_manager       *mddManager;
  int               startTime;


  /*
   * Parse command line options.
   */
  if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) {
      return 1;
  }
  /* Read the network */
  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
  if (network == NIL(Ntk_Network_t)) {
    (void) fprintf(vis_stdout, "** bdd_sat error: No network\n");
    BmcOptionFree(options);
    return 1;
  }
  /* read fsm */
  fsm = Fsm_NetworkReadOrCreateFsm(network);
  if (fsm == NIL(Fsm_Fsm_t)) {
    (void) fprintf(vis_stdout, "** bdd_sat error: Can't read or create fsm\n");
    BmcOptionFree(options);
    return 1;
  }
  mddManager = Fsm_FsmReadMddManager(fsm); /* mdd manager */
  
  mAigManager = Ntk_NetworkReadMAigManager(network);
  if (mAigManager == NIL(mAig_Manager_t)) {
    (void) fprintf(vis_stdout, "** bdd_sat error: run build_partition_maigs command first\n");
    BmcOptionFree(options);
    return 1;
  }
  formulaArray = Ctlsp_FileParseFormulaArray(options->ltlFile);
  if (formulaArray == NIL(array_t)) {
    (void) fprintf(vis_stderr,
                   "** bdd_sat error: Error in parsing CTL* Fromula from file\n");
    BmcOptionFree(options);
    return 1;
  }
  if (array_n(formulaArray) == 0) {
    (void) fprintf(vis_stderr, "** bdd_sat error: No formula in file\n");
    BmcOptionFree(options);
    array_free(formulaArray);
    return 1;
  }
  /* time out */
  if (options->timeOutPeriod > 0) {
    /* Set the static variables used by the signal handler. */
    bmcTimeOut = options->timeOutPeriod;
    alarmLapTime = options->startTime = util_cpu_ctime();
    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
    (void) alarm(options->timeOutPeriod);
    if (setjmp(timeOutEnv) > 0) {
      (void) fprintf(vis_stdout,
                     "\n# bdd_sat: timeout occurred after %d seconds.\n",
                     options->timeOutPeriod);
      (void) fprintf(vis_stdout, "# bdd_sat: data may be corrupted.\n");
      BmcOptionFree(options);
      alarm(0);
      return 1;
    }
  }
  /* bdd and sat to model check the LTL property.*/
  BmcBddSat(network, formulaArray, options);

  Ctlsp_FormulaArrayFree(formulaArray);
  fflush(vis_stdout);
  fflush(vis_stderr);
  BmcOptionFree(options);
  alarm(0);
  return 0; /* normal exit */
}/* CommandBddSat() */
#endif