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

  FileName    [puresatMain.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                                                     */
/*---------------------------------------------------------------------------*/

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

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

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

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

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

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


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

  Synopsis    [PURESAT command interface function]

  Description [PURESAT command interface function]

  SideEffects []

  SeeAlso     []

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

void
PureSat_CheckInvariant(
  Ntk_Network_t *network,
  array_t *InvariantFormulaArray,
  int verbosity,
  int dbgLevel,
  FILE *dbgOut,
  boolean printInputs,
  boolean incremental,
  boolean sss,
  boolean flatIP,
  int speed)
{
  int result,i;
  Ctlp_Formula_t  *invFormula;
  Ctlsp_Formula_t *invFormula_sp;
  PureSat_Manager_t * pm = PureSatManagerAlloc();

  pm->incre = incremental;
  pm->verbosity = verbosity;
  pm->dbgLevel = dbgLevel;
  pm->sss = sss;
  pm->printInputs = printInputs;
  pm->dbgOut = dbgOut;

  switch(speed){
  case 0:
    break;
  case 1:
    pm->Switch = 0;
    break;
  case 2:
    pm->Switch = 0;
    pm->CoreRefMin = 0;
    break;
  case 3:
    pm->Switch = 0;
    pm->CoreRefMin = 0;
    pm->RefPredict = 0;
    break;
  case 4:
    pm->Switch = 0;
    pm->CoreRefMin = 0;
    pm->RefPredict = 0;
    pm->Arosat = 0;
    break;
  default:
    pm->Switch = 0;
    pm->CoreRefMin = 0;
    pm->RefPredict = 0;
    pm->Arosat = 0;
    break;
  }
    
  arrayForEachItem(Ctlp_Formula_t *, InvariantFormulaArray, i, invFormula) {
    /* if(Ctlsp_isCtlFormula(invFormula))*/
    invFormula_sp = Ctlsp_CtlFormulaToCtlsp(invFormula);
    if(sss)
      /*SSS-base Puresat algorithm*/
      result = PureSatCheckInv_SSS(network,invFormula_sp,pm);
    else
      if(flatIP)
	/*Interpolation algorithm without abstraction refinement*/
	result = PureSatCheckInv_FlatIP(network,invFormula_sp,pm);
      else
	/*Interpolation-based Puresat algorithm*/
	result = PureSatCheckInv_IP(network,invFormula_sp,pm);
    if(result){
        (void) fprintf(vis_stdout, "# INV: formula passed --- ");
        Ctlsp_FormulaPrint(vis_stdout, (invFormula_sp));
        fprintf(vis_stdout, "\n");
    }
    else{
      if(pm->dbgLevel != 2)
      {
        (void) fprintf(vis_stdout, "# INV: formula failed --- ");
        Ctlsp_FormulaPrint(vis_stdout, (invFormula_sp));
        fprintf(vis_stdout, "\n");
      }
    }
  }
  PureSatManagerFree(pm);
}



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

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

  Synopsis    [Main procedure of K-induction based PURESAT algorithm]

  Description [Main procedure of K-induction based PURESAT algorithm]

  SideEffects []

  SeeAlso     []

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


boolean PureSatCheckInv_SSS(Ntk_Network_t * network,
			Ctlsp_Formula_t *ltlFormula,
			PureSat_Manager_t *pm)
{
  lsGen     gen;
  st_generator      *stGen;
  int NumofCurrentLatch=0,Length=0,tmp=0,NumofLatch=0,i,j,k;
  int addtoAbs=0,latchThreshHold=10000,RingPosition=0;
  int oldLength=0, beginPosition=0;
  int NumInSecondLevel =0;
  array_t * visibleArray = array_alloc(char *,0);
  array_t * invisibleArray = array_alloc(char *,0);
  array_t * refinement = array_alloc(char*,0);
  array_t * CoiArray,* ConClsArray;
  array_t * arrayRC = NULL;
  array_t *tmpRefinement;
  array_t *tmpRefinement1;
  char * nodeName;
  Ntk_Node_t * node, *latch;
  boolean ExistSimplePath = TRUE,ExistACE = FALSE;
  boolean realRefine=TRUE;
  boolean needSorting = FALSE, firstTime = TRUE;
  mAig_Manager_t    *maigManager;
  BmcOption_t * options;
  BmcCnfStates_t    *cnfstate;
  bAigEdge_t        property;
  st_table * nodeToMvfAigTable;
  double t1,t2, t0,t3;
  long *space;
  PureSat_IncreSATManager_t * pism1,*pism2;
  satArray_t *saved;

  pm->supportTable = st_init_table(st_ptrcmp,st_ptrhash);
  pm->CoiTable = st_init_table(st_ptrcmp,st_ptrhash);
  pm->vertexTable = st_init_table(strcmp, st_strhash);
  pism1 = PureSatIncreSATManagerAlloc(pm);
  pism2 = PureSatIncreSATManagerAlloc(pm);
  t0 = util_cpu_ctime();

  options = BmcOptionAlloc();
  options->satInFile = BmcCreateTmpFile();
  options->satOutFile = BmcCreateTmpFile();
  NumofCurrentLatch=0;
  t1 = util_cpu_ctime();
  PureSatBmcGetCoiForLtlFormula(network, ltlFormula,pm->CoiTable);
  PureSatGenerateSupportTable(network,pm);
  t2 = util_cpu_ctime();
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"Generate DFS: %g\n",(double)((t2-t1)/1000.0));
  
  pm->vertexTable = (st_table *)PureSatCreateInitialAbstraction(network,ltlFormula,&NumofCurrentLatch,pm);
 
  pm->AbsTable = st_init_table(st_ptrcmp,st_ptrhash);
  
  Ntk_NetworkForEachLatch(network, gen, node){
    if (st_lookup_int(pm->CoiTable, node, &tmp)){
      NumofLatch++;
      nodeName = Ntk_NodeReadName(node);
      if(st_lookup(pm->vertexTable,nodeName,NIL(char *)))
	{
	  array_insert_last(char *,visibleArray,nodeName);
	  latch = Ntk_NetworkFindNodeByName(network,nodeName);
	  PureSatComputeTableForLatch(network,pm->AbsTable,latch);
	}
      else
	array_insert_last(char *,invisibleArray,nodeName);
    }
   }
  if(pm->verbosity>=1){
    fprintf(vis_stdout,"visiblearray has %d latches\n",array_n(visibleArray));
    fprintf(vis_stdout,"invisibleArray has %d latches\n",array_n(invisibleArray));
  }
  CoiArray = array_dup(visibleArray);
  array_append(CoiArray,invisibleArray);
   
  maigManager = Ntk_NetworkReadMAigManager(network);
  if (maigManager == NIL(mAig_Manager_t)) {
    (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n");
    BmcOptionFree(options);
    return 1;
  }
 nodeToMvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
							 MVFAIG_NETWORK_APPL_KEY);
  
 /*build property clauses*/
 if (Ctlsp_isPropositionalFormula(ltlFormula))
   property = BmcCreateMaigOfPropFormula(network, maigManager, ltlFormula);
 else
   property = BmcCreateMaigOfPropFormula(network, maigManager, ltlFormula->left);
 
 if (property == mAig_NULL){
   fprintf(vis_stderr,"property = NULL\n");
   exit(0);
 }
 
 property = bAig_Not(property);
 
 while(NumofCurrentLatch < NumofLatch)
   {
     t3 = util_cpu_ctime();
     if(pm->verbosity>=1)
       fprintf(vis_stdout,"Current Latches: %d, COI latches:%d,NEW Length:%d,\n",
	       NumofCurrentLatch,NumofLatch,pm->Length);
     if(pm->verbosity>=2)
       fprintf(vis_stdout,"General time: %g\n",(double)((t3-t0)/1000.0));
     //tmpRefinement1 = array_alloc(char *,0);
     firstTime = TRUE;
     pm->SufAbsTable = st_init_table(st_ptrcmp,st_ptrhash);
     if(realRefine){
       arrayForEachItem(char *,refinement,i,nodeName)
	 {
	   latch = Ntk_NetworkFindNodeByName(network,nodeName);
	   PureSatComputeTableForLatch(network,pm->AbsTable,latch);
	 }
       array_append(visibleArray,refinement);
       latchThreshHold=(int)((double)(array_n(CoiArray)-array_n(visibleArray))/(double)4)+1;
       
       addtoAbs =(int)((double)(array_n(CoiArray)-array_n(visibleArray))/(double)5)+1;
       addtoAbs = addtoAbs >50 ? 50: addtoAbs;
       
       array_free(invisibleArray);
       invisibleArray = array_alloc(char *,0);
       st_foreach_item_int(pm->CoiTable,stGen,&latch,&i)
	 {
	   nodeName = Ntk_NodeReadName(latch);
	   if(!st_lookup(pm->vertexTable,nodeName,0))
	     array_insert_last(char *,invisibleArray,nodeName);
	 }
       t1 = util_cpu_ctime();
       PureSatGetCoiForVisibleArray_Ring(network, visibleArray,RingPosition, pm->CoiTable);
       RingPosition = array_n(visibleArray);
       arrayRC = PureSatGenerateRingFromAbs(network,pm,invisibleArray,&NumInSecondLevel);
       if(pm->verbosity>=2){
	 fprintf(vis_stdout,"NumInSecondLevel is %d  ",NumInSecondLevel);
	 fprintf(vis_stdout,"latchThreshHold is %d\n",latchThreshHold);
       }
       latchThreshHold = (latchThreshHold <= NumInSecondLevel) ? latchThreshHold:NumInSecondLevel;
       if(pm->verbosity>=2){
	 fprintf(vis_stdout,"New latchThreshHold is %d\n",latchThreshHold);
       }
       t2 = util_cpu_ctime();
       if(pm->verbosity>=2){
	 fprintf(vis_stdout,"Generate Ring: %g\n",(double)((t2-t1)/1000.0));
       }
       array_free(refinement);
     }/* if(realRefine)*/
     
     realRefine =FALSE; /* means no ref, just Length++.*/
     t1 = util_cpu_ctime();
     if((ExistSimplePath =
	PureSatExistASimplePath(network,pism1,visibleArray,property,pm)))
       {
	 t2 = util_cpu_ctime();
	 if(pm->verbosity>=2)
	   fprintf(vis_stdout,"Solve on Simple Path: %g\n",(double)((t2-t1)/1000.0));
	 pism1->oldLength = pm->Length;
	 pism1->Length = pm->Length;
	 pism1->beginPosition = array_n(visibleArray);
	 if(pm->verbosity>=1)
	   fprintf(vis_stdout, "Simple Path Exists, length = %d\n",pm->Length);
	 
	 /*check Abs Model*/
	 t1 = util_cpu_ctime();
	 ExistACE = PureSatIncreExistCE(network,pism2,visibleArray,property,pm);
	 if(pm->verbosity>=2)
	   fprintf(vis_stdout,"beginPosition2: %d, oldLength2 %d\n",pism2->beginPosition, pism2->oldLength);
	 t2 = util_cpu_ctime();
	 if(pm->verbosity>=2)
	   fprintf(vis_stdout,"Solve on Abs model: %g\n",(double)((t2-t1)/1000.0));
	 pism2->oldLength = pm->Length;
	 pism2->Length = pm->Length;
	 pism2->beginPosition = array_n(visibleArray);
	 needSorting = FALSE;
	 
	 /*keep a record of previous position for refine's use*/
	 oldLength = pism2->oldLength;
	 beginPosition = pism2->beginPosition;
	 
	 /* while(ExistACE)
	     loop until find sufficient set*/
	 if(ExistACE)
	   {
	     if(pm->verbosity>=1)
	       fprintf(vis_stdout,"found Abstract Counterexample at length %d\n", pm->Length);
	     cnfstate = BmcCnfClausesFreeze(pism2->cnfClauses);
	     pism2->propertyPos = cnfstate->nextIndex;
	     
	     /*store the conflict clauses*/
	     ConClsArray = array_alloc(int,0);
	     
	     /*if incremental */
	     if(pm->incre){
	       if(pism2->cm->savedConflictClauses){
		 saved = pism2->cm->savedConflictClauses;
		 for(i=0, space=saved->space; i<saved->num; i++, space++){
		   array_insert_last(int,ConClsArray,*space);
		 }
	       }
	     }
	     realRefine = TRUE;
	     
	     /*incrementally check Concrete Model*/
	     tmpRefinement = array_alloc(char *,0);
	     if(pm->verbosity>=2)
	       fprintf(vis_stdout,"Begin building a new abstract model\n");
	     for(i=0;i<array_n(arrayRC);i=i+latchThreshHold)
	       {
		 if(i>0)
		   latchThreshHold = array_n(arrayRC)-latchThreshHold;
		 for(j=0;j<latchThreshHold;j++)
		   {
		     if((i+j)<array_n(arrayRC))
		       {
			 nodeName = array_fetch(char *,arrayRC,i+j);
			 array_insert_last(char *,tmpRefinement,nodeName);
			 if(pm->verbosity>=2)
			   fprintf(vis_stdout, "picking %s\n",nodeName);
		       }
		     else
		       break;
		   }/* for(j=0;*/
		 tmpRefinement1=array_dup(visibleArray);
		 array_append(tmpRefinement1,tmpRefinement);
		 
		 t1 = util_cpu_ctime();
		 pism2->cm->option->incAll = 1;
		 pism2->cm->option->incTraceObjective = 0;
		 pism2->cm->option->incPreserveNonobjective = 0;
		 if(PureSatIncreExistCEForRefineOnAbs(network,pism2,tmpRefinement1,property,firstTime,pm)) {
		   t2 = util_cpu_ctime();
		   if(pm->verbosity>=2)
		     fprintf(vis_stdout,"time for finding a sufficient set on model: %g\n",(double)((t2-t1)/1000.0));
		   if((i+j)>=array_n(arrayRC)){
		     if(pm->verbosity>=1)
		       fprintf(vis_stdout,"found real counterexamples\n");
		     if(pm->dbgLevel>=1){
		       options->printInputs = TRUE;
		       BmcPrintCounterExample(network, nodeToMvfAigTable, pism2->cnfClauses,
					      pm->result, pm->Length, pm->CoiTable, options, 
					      NIL(array_t));
		       array_free(pm->result);
		       pm->result = NIL(array_t);
		     }
		     array_free(tmpRefinement1);
		     array_free(tmpRefinement);
		     BmcOptionFree(options);
		     PureSatIncreSATManagerFree(pm,pism1);
		     PureSatIncreSATManagerFree(pm,pism2);
		     /*PureSatManagerFree(pm);*/
		     array_free(CoiArray);
		     array_free(visibleArray);
		     return FALSE;
		   }
		   else{
		     if(pm->result!=NIL(array_t)){
		       array_free(pm->result);
		       pm->result = NIL(array_t);
		     }
		   }
		 }
		 else{
		   t2 = util_cpu_ctime();
		   if(pm->verbosity>=1)
		     fprintf(vis_stdout,"found a sufficient model\n");
		   if(pm->verbosity>=2)
		     fprintf(vis_stdout,"time for finding a sufficient set on model: %g\n",(double)((t2-t1)/1000.0));
		   firstTime = FALSE;
		   arrayForEachItem(char *,tmpRefinement1,k,nodeName){
		     node = Ntk_NetworkFindNodeByName(network, nodeName);
		     if(!st_lookup(pm->SufAbsTable,node,NIL(char *)))
		       st_insert(pm->SufAbsTable,node, (char *)0);
		     else{
		       fprintf(vis_stderr,"wrong in sufabstable \n");
		       exit(0);
		     }
		   }
		   pism2->beginPosition = array_n(tmpRefinement1);
		   pism2->oldLength = Length;
		   array_free(tmpRefinement1);
		   break;
		 }
		 pism2->beginPosition = array_n(tmpRefinement1);
		 array_free(tmpRefinement1);
		 pism2->oldLength = Length;
	       } /*for(i=0;i<array_n(arrayRC)*/
	     
	     /*recover the conflict clauses and incremental SAT option*/
	     pism2->cm->option->incAll = 0;
	     pism2->cm->option->incTraceObjective = 1;
	     pism2->cm->option->incPreserveNonobjective = 1;
	     
	     /*if incremental*/
	     if(pm->incre){
	       if(pism2->cm->savedConflictClauses)
		 sat_ArrayFree(pism2->cm->savedConflictClauses);
	       pism2->cm->savedConflictClauses = sat_ArrayAlloc(16);
	       arrayForEachItem(int, ConClsArray,i,tmp)
		 sat_ArrayInsert(pism2->cm->savedConflictClauses,tmp);
	     }
	     array_free(tmpRefinement);
	     t1 = util_cpu_ctime();
	     refinement = PureSatRefineOnAbs(network,pm,property,addtoAbs);
	     t2 = util_cpu_ctime();
	     if(pm->verbosity>=2)
	       fprintf(vis_stdout,"time for RefOnAbs: %g\n",(double)((t2-t1)/1000.0));
	     st_free_table(pm->SufAbsTable);
	     pm->SufAbsTable = NIL(st_table);
	     
	     /*adjust parameters*/
	     NumofCurrentLatch+=array_n(refinement);
	     pm->Length++;
	     pism1->Length++;
	     pism2->Length++;
	     BmcCnfClausesRestore(pism2->cnfClauses, cnfstate);
	     pism2->beginPosition = beginPosition;
	     pism2->oldLength = oldLength;
	     FREE(cnfstate);
	   }/* if(pism2->cm->status == SAT_SAT)*/
	 else /*if(pism2->cm->status != SAT_SAT)*/
	   {
	     if(pm->verbosity>=1)
	       fprintf(vis_stdout,"no Abstract Counterexample at length %d \n",pm->Length);
	     pm->Length++;
	     pism1->Length++;
	     pism2->Length++;
	     st_free_table(pm->SufAbsTable);
	     pm->SufAbsTable = NIL(st_table);
	   }
       } /*if(ExistSimplePath)*/
     else /* if no simple path*/
       {
	 t2 = util_cpu_ctime();
	 if(pm->verbosity>=2)
	   fprintf(vis_stdout,"Solve on Simple Path: %g\n",(double)((t2-t1)/1000.0));
	 if(pm->verbosity>=1)
	   fprintf(vis_stdout,"simple Path doesn't exist, exit\n");
	 BmcOptionFree(options);
	 PureSatIncreSATManagerFree(pm,pism1);
	 PureSatIncreSATManagerFree(pm,pism2);
	 PureSatManagerFree(pm);
	 array_free(CoiArray);
	 array_free(visibleArray);
	 return TRUE;
       }
   }/* while(NumofCurrentLatch < NumofLatch)*/
 /*st_free_table(AbsTable);*/
 
 /*Now go to the concrete model*/
 if(pm->verbosity>=1)
   fprintf(vis_stdout,"reach concrete model\n");
 array_append(visibleArray,refinement);
 array_free(refinement);
 while(PureSatExistASimplePath(network,pism1,visibleArray,property,pm))
   {
     pism1->oldLength = pism1->Length;
     pism1->beginPosition = array_n(visibleArray);
     if(PureSatExistCE(network,pism2,options,visibleArray,property,pm,1)) {
       if(pm->verbosity>=1)
	 fprintf(vis_stdout,"found real counterexample of length:%d\n",pm->Length);
       if(pm->dbgLevel>=1){
	 options->printInputs = TRUE;
	 BmcPrintCounterExample(network, nodeToMvfAigTable, pism2->cnfClauses,
				pm->result, pm->Length, pm->CoiTable, options, 
				NIL(array_t));
       }
       BmcOptionFree(options);
       PureSatIncreSATManagerFree(pm,pism1);
       PureSatIncreSATManagerFree(pm,pism2);
       /*PureSatManagerFree(pm);*/
       array_free(CoiArray);
       array_free(visibleArray);
       return FALSE;
     }
     else
       {
	 pism2->oldLength = Length;
	 pm->Length++;
	 pism1->Length++;
	 pism2->Length++;
	 pism2->beginPosition = array_n(visibleArray);
       }
   }
 
 BmcOptionFree(options);
 PureSatIncreSATManagerFree(pm,pism1);
 PureSatIncreSATManagerFree(pm,pism2);  
 /*PureSatManagerFree(pm);*/
 array_free(CoiArray);
 array_free(visibleArray);
 return TRUE;
}

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

  Synopsis    [PURESAT command parser]

  Description [PURESAT command parser]

  SideEffects []

  SeeAlso     []

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



void PureSatCmdParse(int argc,
		     char **argv,
		     PureSat_Manager_t *pm)

{
  int c, incre;
  
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "t:i:h:v:I:")) != EOF) {
    switch(c) {
      case 'i':
	strcpy(pm->ltlFileName,util_strsav(util_optarg));
        break;	
      case 't' :
	pm->timeOutPeriod = atoi(util_optarg);
        break;	
      case 'v':
        pm->verbosity = atoi(util_optarg);
        break;
      case 'I':
	incre = atoi(util_optarg);
        pm->incre = (incre==0)? FALSE:TRUE;
        break;
      case 'h':
	goto usage;
      default:
	goto usage;
    }
  }
  return;
 usage:
  (void) fprintf(vis_stderr, "usage: abrf [-h][-i ltlfile][-t timeout]\n");
  (void) fprintf(vis_stderr, "   -i \tName of LTL file.\n");
  (void) fprintf(vis_stderr, "   -t \ttimeout.\n");
  (void) fprintf(vis_stderr, "   -v \tverbosity for more information. \n");
  (void) fprintf(vis_stderr, "   -I \tincremental SAT switch. \n");
  (void) fprintf(vis_stderr, "\t\t0 for non-incremental, other values for incremental\n");
  (void) fprintf(vis_stderr, "   -h \tprint the command usage\n");

}

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