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

  FileName    [grabBMC.c]

  PackageName [grab]

  Synopsis    [Check abstract paths on a more concrete model using SAT.]

  Description [Abstract paths are given in an array of MDDs, which
  capture multiple abstract paths at the same time. MDDs are encoded
  as AIG graph to allow the check in the more concrete model.]
    
  Author      [Chao Wang]

  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 "grabInt.h"
#include "bmcInt.h"

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

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

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

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

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

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

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

static bAigEdge_t GrabConvertBddToBaig(bAig_Manager_t *bAigManager, bdd_t *fn, st_table *bddidToNames);
static st_table * GrabBddGetSupportBaigNames(mdd_manager *mddManager, mdd_t *f);
static char * GrabBddIdToBaigNames(mdd_manager *mddManager, int bddid);

/**AutomaticEnd***************************************************************/

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

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

  Synopsis    [Check if the abstract paths exist in the model.]

  Description [Check if the abstract paths exist in the model. The
  paths are given as set of onion rings, where each ring is a set of
  states. The model is defined by the set of latches in absLatches.]

  SideEffects []

******************************************************************************/
boolean
Bmc_AbstractCheckAbstractTraces(
  Ntk_Network_t *network,
  array_t *synOnionRings,
  st_table *absLatches,
  int verbose, 
  int dbgLevel,
  int printInputs)
{
  int               pathLength = array_n(synOnionRings) -1;
  mAig_Manager_t    *maigManager = Ntk_NetworkReadMAigManager(network);
  st_table          *nodeToMvfAigTable = NIL(st_table); 
  BmcCnfClauses_t   *cnfClauses;
  FILE              *cnfFile;
  BmcOption_t       *options;
  array_t           *result;
  int               i;
  boolean           CexExit = FALSE;
  
  nodeToMvfAigTable =
    (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
  if (nodeToMvfAigTable == NIL(st_table)){
    fprintf(vis_stderr, 
	    "** bmc error: please run buid_partiton_maigs first\n");
    return CexExit;
  }

  options = BmcOptionAlloc();
  if (verbose) { 
    options->dbgLevel = dbgLevel;
    options->printInputs = printInputs;
  }
  options->satInFile = BmcCreateTmpFile();
  if (options->satInFile == NIL(char)){
    BmcOptionFree(options);
    return CexExit;
  }

  /* create SAT Solver output file */
  options->satOutFile = BmcCreateTmpFile();
  if (options->satOutFile == NIL(char)){
    BmcOptionFree(options);
    fprintf(vis_stderr, "** bmc error: Cannot allocate a temp file name\n");
    return CexExit;
  }
  cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
  if (cnfFile == NIL(FILE)) {
    BmcOptionFree(options);
    fprintf(vis_stderr, "** bmc error: Cannot create CNF output file %s\n",
	    options->satInFile);
    return CexExit;
  }

  /* Unroll the model exactly 'pathLength' time frames
   */
  cnfClauses = BmcCnfClausesAlloc();
  BmcCnfGenerateClausesForPath(network, 0, pathLength, BMC_INITIAL_STATES,
			       cnfClauses, nodeToMvfAigTable, absLatches);

  /* Generate the constraints from the abstract paths
   *   (1) build a bAigEdge_t (graph) for each ring
   *   (2) add all the cnf clauses that describe this graph
   *   (3) make the output bAigEdge_t equals to 1
  */
  {
    bAigEdge_t  bAigState;
    mdd_manager *mddManager = Ntk_NetworkReadMddManager(network);
    array_t     *clause = array_alloc(int, 1);
    mdd_t       *ring;

    arrayForEachItem(mdd_t *, synOnionRings, i, ring) {
      st_table *bddidTobAigNames;
      bddidTobAigNames = GrabBddGetSupportBaigNames(mddManager, ring);
      bAigState = GrabConvertBddToBaig(maigManager, ring, bddidTobAigNames);
      {
	st_generator *stgen;
	long tmpId;
	char *tmpStr;
	st_foreach_item(bddidTobAigNames, stgen, &tmpId, &tmpStr) {
	  FREE(tmpStr);
	}
	st_free_table(bddidTobAigNames);
      }
      array_insert(int, clause, 0, BmcGenerateCnfFormulaForAigFunction(
                                  maigManager, bAigState, i, cnfClauses));
      BmcCnfInsertClause(cnfClauses, clause);
    } 
   
    array_free(clause);
  } 

  /* Call the SAT solver 
   */
  BmcWriteClauses(maigManager, cnfFile, cnfClauses, options); 
  fclose(cnfFile);
  result = BmcCheckSAT(options);
  if(result != NIL(array_t)){
    if (verbose >= 1 && dbgLevel ==1) {
      fprintf(vis_stdout,"Found Counterexample of length = %d\n", pathLength);
      BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
			     result, pathLength+1, absLatches, options, 
			     NIL(array_t));
    }
    if (verbose >=1 && dbgLevel == 2) {
      BmcPrintCounterExampleAiger(network, nodeToMvfAigTable, cnfClauses,
                             result, pathLength+1, absLatches, options,
                             NIL(array_t));
    }   
    CexExit = TRUE;
  }  

  /* free all used memories */
  BmcCnfClausesFree(cnfClauses);
  array_free(result);
  BmcOptionFree(options);

  return CexExit;
}


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

  Synopsis    [Check if the abstract paths exist in the fine-grain model.]

  Description [Check if the abstract paths exist in the fine-grain
  model. The paths are given as set of onion rings, where each ring is
  a set of states.  The model is defined by the set of latches
  (absLatches) and bnvs (absBnvs). The entire set of bnvs of the
  network are stored in the table coiBnvTable.

  This procedure first build a NEW maig graph (for the fine-grain
  model), then check if the abstract paths exist in the model.

  Before it returns, the previous maig graph is restored.]
  
  SideEffects []

******************************************************************************/
boolean
Bmc_AbstractCheckAbstractTracesWithFineGrain(
  Ntk_Network_t *network,
  st_table *coiBnvTable,
  array_t *synOnionRings,
  st_table *absLatches,
  st_table *absBnvs)
{
  boolean             result;
  mAigManagerState_t  oldMaigState;  /* to store the previous AIG */
  mAig_Manager_t      *maigManager;
  lsGen               lsgen;
  Ntk_Node_t          *node;
  int                 mAigId;
  int                 i;
  st_generator        *stgen;
  st_table            *leaves;
  array_t             *roots, *combInputs;

  /* save the existing maigManager */
  oldMaigState.manager = Ntk_NetworkReadMAigManager(network);
  oldMaigState.nodeToMvfAigTable =  
    (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
  oldMaigState.nodeToMAigIdTable = st_init_table(st_ptrcmp, st_ptrhash);
  Ntk_NetworkForEachNode(network, lsgen, node) {
    mAigId = Ntk_NodeReadMAigId(node);
    st_insert(oldMaigState.nodeToMAigIdTable, node, (char *)(long)mAigId);
    Ntk_NodeSetMAigId(node, ntmaig_UNUSED);
  }

  /* create a new maigManager */
  maigManager = mAig_initAig();
  Ntk_NetworkSetMAigManager(network, maigManager);
  Ntk_NetworkSetApplInfo(network, MVFAIG_NETWORK_APPL_KEY,
	  		 (Ntk_ApplInfoFreeFn) ntmAig_MvfAigTableFreeCallback,
			 (void *) st_init_table(st_ptrcmp, st_ptrhash));

  /* roots are the visible latches, and the visible bnvs (some bnvs
   * may not be in the transitive fan-in cone of the visible latches
   */
  roots = array_alloc(Ntk_Node_t *, 0);
  st_foreach_item(absLatches, stgen, &node, NIL(char *)) {
    array_insert_last(Ntk_Node_t *, roots, Ntk_LatchReadDataInput(node));
    array_insert_last(Ntk_Node_t *, roots, Ntk_LatchReadInitialInput(node));
  }
  st_foreach_item(absBnvs, stgen, &node, NIL(char *)) {
    array_insert_last(Ntk_Node_t *, roots, node);
  }

  combInputs = Ntk_NodeComputeTransitiveFaninNodes(network, roots, 
						   TRUE, /* stopAtLatches */
						   FALSE /* combInputsOnly*/
						   );

  /* leaves are the combinational inputs or the invisible bnvs */
  leaves = st_init_table(st_ptrcmp, st_ptrhash);
  arrayForEachItem(Ntk_Node_t *, combInputs, i, node) {
    if ( Ntk_NodeTestIsCombInput(node) ||
	 ( st_is_member(coiBnvTable, node) &&
	   !st_is_member(absBnvs, node) ) ) {
      st_insert(leaves, node, (char *) ntmaig_UNUSED);
      Ntk_NodeSetMAigId(node, mAig_CreateVar(maigManager,
					     Ntk_NodeReadName(node),
		   Var_VariableReadNumValues(Ntk_NodeReadVariable(node))));
    }
  }
  st_foreach_item(absLatches, stgen, &node, NIL(char *)) {
    if (!st_is_member(leaves, node)) {
      st_insert(leaves, node, (char *) ntmaig_UNUSED);
      Ntk_NodeSetMAigId(node, mAig_CreateVar(maigManager,
					     Ntk_NodeReadName(node),
		   Var_VariableReadNumValues(Ntk_NodeReadVariable(node))));
    }
  }
  array_free(combInputs);

#if 1
  /* THIS SEEMS UNNECESSARY---IT'S HERE TO AVOID ERRORS IN CALLING
   * ntmaig_NetworkBuildMvfAigs()
   */
  Ntk_NetworkForEachCombInput(network, lsgen, node) {
    if (Ntk_NodeReadMAigId(node) == NTK_UNASSIGNED_MAIG_ID) {
      Ntk_NodeSetMAigId(node, mAig_CreateVar(maigManager,
					     Ntk_NodeReadName(node),
		   Var_VariableReadNumValues(Ntk_NodeReadVariable(node))));
    } 
  }
#endif

  /* build the new AIG graph */
  ntmaig_NetworkBuildMvfAigs(network, roots, leaves);

  array_free(roots);
  st_free_table(leaves);


  /* check the existence of the abstract path on the new AIG graph */
  result = Bmc_AbstractCheckAbstractTraces(network,
					   synOnionRings,
					   absLatches,
					   0, 0, 0);

  /* restore the previous maigManager */
  mAig_quit(maigManager);
  Ntk_NetworkFreeApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
  Ntk_NetworkSetMAigManager(network, oldMaigState.manager);
  Ntk_NetworkSetApplInfo(network, MVFAIG_NETWORK_APPL_KEY,
	  		 (Ntk_ApplInfoFreeFn) ntmAig_MvfAigTableFreeCallback,
			 (void *) oldMaigState.nodeToMvfAigTable);
  st_foreach_item(oldMaigState.nodeToMAigIdTable, stgen, &node,
		  &mAigId) {
    Ntk_NodeSetMAigId(node, mAigId);
  }
  st_free_table(oldMaigState.nodeToMAigIdTable);

  return result;
}

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

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

  Synopsis [Build the binary Aig for a given bdd]

  SideEffects [Build the binary Aig for a given bdd.  We assume that
  the return bdd nodes from the foreach_bdd_node are in the order from
  childeren to parent. i.e all the childeren nodes are returned before
  the parent node.

  bddidToNames is a hash table from bddid to its bAigEdge_t name.  If
  provided, this table should contain entiries for all the bddid in
  the support.]

  SideEffects []

  SeeAlso     []
  
******************************************************************************/
static bAigEdge_t
GrabConvertBddToBaig(
   bAig_Manager_t *bAigManager,
   bdd_t          *fn,
   st_table       *bddidToNames)
{
  bdd_gen     *gen;
  bdd_node    *node, *thenNode, *elseNode, *funcNode;
  bdd_manager *bddManager = bdd_get_manager(fn);
  bdd_node    *one  = bdd_read_one(bddManager);
  /*bdd_node    *zero = bdd_read_logic_zero(bddManager);*/
  int         is_complemented;
  int         flag;
  bAigEdge_t  var, left, right, result;
  char        *name;
  st_table    *bddTObaigTable;
  
  bddTObaigTable = st_init_table(st_numcmp, st_numhash);

  if (fn == NULL){
    return bAig_NULL;
  }
  
  st_insert(bddTObaigTable, (char *) (long) bdd_regular(one),  
	    (char *) bAig_One);

  funcNode = bdd_get_node(fn, &is_complemented);
  
  if (bdd_is_constant(funcNode)){
    flag = st_lookup(bddTObaigTable, 
		     (char *) (long) (funcNode),
		     &result);
    assert(flag);
    st_free_table(bddTObaigTable);

    if (is_complemented)
      return bAig_Not(result);
    else
      return result;
  }
  
  foreach_bdd_node(fn, gen, node){
    /* if the node has been processed, skip it. (the constant ONE
     * should be the only node falls into this category).
     */
    if (st_is_member(bddTObaigTable, (char *) (long) bdd_regular(node)))
      continue;
    
    /*  bdd_node_read_index() return the current level's bddId */
    if (bddidToNames) {
      flag = st_lookup(bddidToNames, (char *)(long)bdd_node_read_index(node),
		       &name);
      assert(flag);
      name = util_strsav(name);
    }else {
      char tempString[1024];
      sprintf(tempString, "BDD%d", bdd_node_read_index(node));
      name = util_strsav(tempString);
    }

    /*  Create or Retrieve the bAigEdge_t  w.r.t. 'name' */
    var  = bAig_CreateVarNode(bAigManager, name);
    FREE(name);

    thenNode  = bdd_bdd_T(node);
    flag = st_lookup(bddTObaigTable, (char *) (long) bdd_regular(thenNode),
		     &left);
    assert(flag);
      
    elseNode  = bdd_bdd_E(node);
    flag = st_lookup(bddTObaigTable, (char *) (long) bdd_regular(elseNode),
		      &right);
    assert(flag);

    /* should we test here whether elseNode is complemented arc? */
    if (bdd_is_complement(elseNode))
      right = bAig_Not(right);

    result =  bAig_Or(bAigManager, bAig_And(bAigManager, var, left),
		                   bAig_And(bAigManager, bAig_Not(var), right));
    st_insert(bddTObaigTable, (char *) (long) bdd_regular(node),
	      (char *) (long) result);
  }
  flag = st_lookup(bddTObaigTable, (char *) (long) bdd_regular(funcNode),
		    &result);  
  assert(flag);
  st_free_table(bddTObaigTable);

  if (is_complemented){
    return bAig_Not(result);
  } else {
    return result;
  }
} /* end of bAig_bddtobAig() */


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

Synopsis    [Get a (bddId,baigName) table for the supporting variableS.]

SideEffects [Get a (bddId,baigName) table for the supporting
variableS. The caller should free the returned table as well as the
(char *) of its value field.]

SeeAlso     []
  
******************************************************************************/
static st_table *
GrabBddGetSupportBaigNames(
  mdd_manager *mddManager,
  mdd_t *f)
{
  int        numOfVars = bdd_num_vars(mddManager);
  st_table  *bddidTObaigNames = st_init_table(st_numcmp, st_numhash);
  var_set_t *vset;
  int        i;

  vset = bdd_get_support(f);
  for (i=0; i<numOfVars; i++) {
    if (var_set_get_elt(vset, i) == 1) {
      st_insert(bddidTObaigNames, (char *)(long)i, 
		GrabBddIdToBaigNames(mddManager, i));
    }
  }
  var_set_free(vset);

  return bddidTObaigNames;
}

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

Synopsis    [return the baigName  of a bddid]

SideEffects [The caller should free the returned char *.  This
  function is based on the assumption that MDD and MAIG shares the
  same naming convention (which is true in VIS).]

SeeAlso     []
  
******************************************************************************/
static char *
GrabBddIdToBaigNames(
  mdd_manager *mddManager,
  int            bddid)
{
  array_t *mvar_list = mdd_ret_mvar_list(mddManager);
  array_t *bvar_list = mdd_ret_bvar_list(mddManager);
  bvar_type bv;
  mvar_type mv;
  int     mddid, index, id;
  char    *nodeName;
  char    baigName[1024];

  /* 1. from bddid, get mddid and the index of this bddid in the mddid 
   */
  bv = array_fetch(bvar_type, bvar_list, bddid);
  mddid = bv.mvar_id;
  mv = array_fetch(mvar_type, mvar_list, mddid);
  arrayForEachItem(int, mv.bvars, index, id) {
    if (id == bddid) 
      break;
  }
  assert(index <= mv.encode_length -1);
  
  /* 2. assumptions: (1) mv.name = nodeName,  
   *                 (2) index is the same for MDD and MAIG
   */
  nodeName = mv.name;
  
  /* 3. the baigEdge_t's name is ("%s_%d",nodeName,index)
   */
  sprintf(baigName, "%s_%d", nodeName, index);

  return util_strsav(baigName);
}