/*----------------------------------------------------------------*
 *
 * File : sigsToVVs.c
 * Author : NTM
 * Created : 01/04/05
 *
 *
 * Copyright (C) Nicolas Thierry-Mieg, 2006.
 *
 *
 * This file is part of InterPool, written by 
 * Nicolas Thierry-Mieg (CNRS, France) Nicolas.Thierry-Mieg@imag.fr
 *
 * InterPool is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * InterPool is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with InterPool; if not, write to the Free Software
 * Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA
 *
 *-----------------------------------------------------------------*/

#include <stdlib.h> /* free, exit, ... */
#include <stdio.h> /* printf and friends */

#include "types.h" /* MOT */
#include "pools.h" /* nbmotparpool */
#include "varia.h" /* buildInitialVV */
#include "signa.h" /* setOfSigs */
#include "solveSigSimple.h" /* solveSigSimple */

#include "sigsToVVs.h"



/************************************************************************
 ******************* LOCAL FUNCTIONS ************************************
 ************************************************************************/

/********************** DECLARATIONS ************************************/

/*! 
  \brief Update summaryVV by merging newVV into it, as follows:
  if a variable is pos in both summaryVV and newVV, it stays pos (in summaryVV);
  else, if it is neg in both summaryVV and newVV, it stays neg;
  else: it becomes ambiguous (in summaryVV).
  This seems to be the most prudent merging we can apply.
*/
static void mergeVVs(MOT* summaryVV, MOT* newVV, int n) ;


/************************ BODIES ***************************************/


/*!
  mergeVVs: update summaryVV by merging newVV into it, as follows:
  if a variable is pos in both summaryVV and newVV, it stays pos (in summaryVV);
  else, if it is neg in both summaryVV and newVV, it stays neg;
  else: it becomes ambiguous (in summaryVV).
  This seems to be the most prudent merging we can apply.
  NOTE: watch out for the nonexistant variables in the last MOT of 
  the VVs: their values will also be updated. Make sure you don't use them.

  \param summaryVV a VV summarizing all sigs examined up to now; summaryVV
  gets updated by taking into account newVV.
  \param newVV the VV corresponding to a new sig.
  \param n number of variables.
*/
static void mergeVVs(MOT* summaryVV, MOT* newVV, int n)
{

  /* parameter verification: both vectors should be non-null */
  if ((summaryVV==NULL) || (newVV==NULL))
    {
      fprintf(stderr, "in mergeVVs, at least one of the VVs is NULL, shouldn't happen!\n") ;
      exit(1) ;
    }

  int VVsize = nbmotparpool(n) ;

  {
    int i ;
    // use buildInitialVV with n=1 to build a single MOT filled with 01's
    MOT* VVmot01 = buildInitialVV(1, 85) ;
    for (i=0; i < VVsize; i++)
      {
	/* algorithm: for each index, we use the following operations on
	   MOTs to obtain the desired result (you can verify that this works
	   by simply writing out the truth table for each pair of bits 
	   of summaryVV and newVV).
	   Easy optimization when mergeVVs will be successively called on many
	   newVV's: you can calculate the OR and the AND of all the VVs at
	   each index, and then apply the ( (01 & bigOR) | bigAND) operation.
	*/
	summaryVV[i] = ( (*VVmot01 & (summaryVV[i] | newVV[i])) 
			 | (summaryVV[i] & newVV[i]) ) ;

      }
    free(VVmot01) ;
  }
}


/************************************************************************
 ******************* EXPORTED FUNCTIONS *********************************
 ************************************************************************/


/*!
  \brief Given a set of coherent sigs, build the deduced VV by merging the VVs
  corresponding to all the sigs (using a prudent merge, see mergeVVs).
  Also checks that every sig from the set is coherent.
  Returns the deduced VV (allocated here), or NULL (if coherentSigs 
  is empty).
  
  \param coherentSigs a set of signatures (typically, the set of nearest 
  coherent signatures obtained after resolving an observed sig).
  \param tabpool the pools used.
  \param n number of variables.

  NOTE: if profiling reveals this function to be significant, I can
  easily speed it up by saving all the thisVV's in a vector of
  VVs, and merging them all in a single mergeAllVVs at the end
  (instead of merging each VV with the deducedVV as soon as I obtain
  it by solveSigSimple). This should increase performance because
  merging a single or many VVs should take almost the same amount of 
  time... see mergeVV for details.
  However, the number of coherent sigs should generally be small
  (ideally 1), so this shouldn't pose a problem (and it's cleaner).
*/
MOT* buildDeducedVV(setOfSigs coherentSigs, MOT* tabpool, int n)
{
  MOT* deducedVV ; // will be returned

  int nbOfSigs = coherentSigs.nbOfSigs ; // number of sigs

  if (nbOfSigs <= 0)
    // no signatures in coherentSigs, strange?
    deducedVV = NULL ;
  else
    {
      int signum = 0 ;
      
      // initialize deducedVV with the VV of the first sig
      deducedVV = solveSigSimple(tabpool, coherentSigs.allSigs[signum], n) ;

      /* check that the first sig was coherent */
      if (deducedVV==NULL)
	{
	  fprintf(stderr, "in buildDeducedVV, first sig is not coherent, shouldn't happen!\n") ;
	  exit(1) ;
	}

      // now update deducedVV with all remaining sigs
      for (signum = 1; signum < nbOfSigs; signum++)
	{
	  signature* thisSig = coherentSigs.allSigs[signum];
	  
	  // solve this sig
	  MOT* thisVV = solveSigSimple(tabpool, thisSig, n) ;
	  /* check that it was coherent */
	  if (thisVV==NULL)
	    {
	      fprintf(stderr, "in buildDeducedVV, sig %d is not coherent, shouldn't happen!\n", signum) ;
	      exit(1) ;
	    }

	  mergeVVs(deducedVV, thisVV, n) ;

	  // except for the first VV, which is saved in deducedVV and will
	  // be returned, all other VVs must be freed:
	  free(thisVV) ;
	}
    }

  return deducedVV;
}
