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

  FileName    [puresat.c]

  PackageName [puresat]

  Synopsis    [Abstraction refinement for large scale invariant checking.]

  Description [This file contains the functions to check invariant properties
  by the PureSAT abstraction refinement algorithm, which is entirely based on
  SAT solver, the input of which could be either CNF or AIG. It has several
  parts:

  * Localization-reduction base Abstraction
  * K-induction or interpolation to prove the truth of a property
  * Bounded Model Checking to find bugs
  * Incremental concretization based methods to verify abstract bugs
  * Incremental SAT solver to improve efficiency
  * UNSAT proof based method to obtain refinement
  * AROSAT to bring in only necessary latches into unsat proofs
  * Bridge abstraction to get compact coarse refinement
  * Refinement minization to guarrantee minimal refinements
  * Unsat proof-based refinement minimization to eliminate multiple candidate
    by on SAT test
  * Refinement prediction to decrease the number of refinement iterations
  * Dynamic switching to redistribute computional resources to improve
    efficiency
  
  For more information, please check the BMC'03, ICCAD'04, STTT'05 and TACAS'05
  paper of Li et al., "A satisfiability-based appraoch to abstraction
  refinement in model checking", " Abstraction in symbolic model checking
  using satisfiability as the only decision procedure", "Efficient computation
  of small abstraction refinements", and "Efficient abstraction refinement in
  interpolation-based unbounded model checking"]
  
  Author      [Bing Li]

  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado.
  All rights reserved.

  Permission is hereby granted, without written agreement and without
  license or royalty fees, to use, copy, modify, and distribute this
  software and its documentation for any purpose, provided that the
  above copyright notice and the following two paragraphs appear in
  all copies of this software.]

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

#include "puresatInt.h"

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

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

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

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

static jmp_buf timeOutEnv;

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

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

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

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

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

  Synopsis    [Initializes the puresat package. The added command is for
  testing purpose only; the same algorithm can be activated by the
  check_invariant command.]

  Description [Initializes the puresat package. The added command is for
  testing purpose only; the same algorithm can be activated by the
  check_invariant command.]

  SideEffects []

  SeeAlso     [PureSat_End]

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


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

  Synopsis    [Ends the puresat package.]

  Description [Ends the puresat package.]
   
  SideEffects []

  SeeAlso     [PureSat_Init]

******************************************************************************/
void
PureSat_End(void)
{

}

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


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


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

  Synopsis    [time out function]

  Description [time out function]

  SideEffects []

  SeeAlso     []

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


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

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

  Synopsis    [Check invariant formulae with abstraction refinement method
  PureSat.]

  Description [Check invariant formulae with abstraction refinement method
  PureSat.]

  SideEffects []

  SeeAlso     []

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