src/puresat/puresat.c

Go to the documentation of this file.

#include "puresatInt.h"

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

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

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

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

static jmp_buf timeOutEnv;

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/
static int CommandPureSatAbRf( Hrc_Manager_t ** hmgr,int  argc, char ** argv);
static void TimeOutHandle(void);
/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

void
PureSat_Init(void)
{
  /*
   * Add a command to the global command table.  By using the leading
   * underscore, the command will be listed under "help -a" but not "help".
   */
  Cmd_CommandAdd("_puresat_test", CommandPureSatAbRf,  0);
}


void
PureSat_End(void)
{

}

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


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


static void
TimeOutHandle()
{
  longjmp(timeOutEnv, 1);
}

static int
CommandPureSatAbRf(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  Ntk_Network_t * network;
  
  FILE * ltlFile;
  array_t * formulaArray;
  boolean re;
  int i;

  PureSat_Manager_t *pm;
  int timeOutPeriod;

  pm = PureSatManagerAlloc();
  timeOutPeriod = pm->timeOutPeriod;
  PureSatCmdParse(argc, argv,pm);
  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
  fprintf(vis_stdout, "Num of latches is %d\n",Ntk_NetworkReadNumLatches(network));
  if (network == NIL(Ntk_Network_t)) {
      fprintf(vis_stderr,
              "No network, please read in the circuit, and init_verify\n");
      return 1;
  }
 
  ltlFile = Cmd_FileOpen(pm->ltlFileName, "r", NIL(char *), 0);
  if (ltlFile == NIL(FILE)) {
    fprintf(vis_stdout,"Cannot open LTL file %s\n", pm->ltlFileName);
    exit(1);
  }
  
  formulaArray = Ctlsp_FileParseFormulaArray(ltlFile);
  if(!array_n(formulaArray))
    {fprintf(vis_stderr,"ltlfile doesn't contain any formula \n");
    exit (1);}

  /*timeout*/
  if (timeOutPeriod > 0) {
    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
    fprintf(vis_stdout, "signal\n");
    (void) alarm(timeOutPeriod);
    if (setjmp(timeOutEnv) > 0) {
      (void) fprintf(vis_stdout,
                     "# PURESAT: timeout occurred after %d seconds.\n", timeOutPeriod);
      (void) fprintf(vis_stdout, "# PURESAT: data may be corrupted.\n");
      alarm(0);
      return 1;
    }
  }

  for (i = 0; i < array_n(formulaArray); i++) {
    Ctlsp_Formula_t *ltlFormula = array_fetch(Ctlsp_Formula_t *, formulaArray, i);
    re = PureSatCheckInv_SSS(network,ltlFormula,pm);
    if(re)
      fprintf(vis_stdout,"formula #%d is true\n",i);
    else
      fprintf(vis_stdout,"formula #%d is False\n",i);
  }
  return 0;
}