/*---------------------------------------------------------------*
 *
 * File : solvexpNaive.c
 * Author : NTM
 * Created : 09/09/04
 *
 *
 * 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 <stdio.h> // for printing
#include <stdlib.h> // for memory access
#include <string.h> // memset

#include "types.h"  /* MOT */
#include "pools.h" /* nbmotparpool, pool */
#include "signa.h" // getsigvalue, setsigvalue, copysig, setOfSigs
#include "varia.h" // updateVVNegPool, buildInitialVV
#include "distance.h" // DIST_xxx

#include "solvexpNaive.h"

#undef SANITY 
/* #define SANITY to check that lists are sorted in updateVVAllNegPools */


/* NOTE 28/06/06: I've switched from signatures represented
   simply as int*'s to a real signature datatype.
   I don't want to bother cleaning up and updating this method
   accordingly, however... It's only used for a bit of validation
   anyways, because it's so slow.
   So, I'll put some dirty hacks to make the calls to setsigvalue et
   al work, and just change the public function so it has the
   correct profile, ie accepts a signature as input.
*/


/*!
  maximal depth to correct noise (ie, max nb of erroneous
  observations that can be corrected). Never search beyond this
  value, it's too slow... In fact, if n is large (eg 10000), using
  the current value of 20 is probably too slow already, in this case
  decrease to 10 or less, or use a better solvexp method
*/
#define PROFMAX 20


/*! 
   for solvexpNaive: number of parts to use for partitioning
   the negative pools. Testing has shown that 20 is a good
   compromise, you probably shouldn't change this.
   This value only affects the speed, not the result. 
*/
#define NBPARTS 20


/*
  Note: in this method, we explore the neighbour signatures of
  the observed sig. To represent the current neighbour, we use
  both a modified copy of the observed sig (using copysig and
  setsigvalue), and a pair of vectors of ints that store the absolute
  numbers of the modified pools (one for ex-positives and one for 
  ex-negatives): changedPosPools and changedNegPools.
  The first element of these vectors is the number of changed sigs, 
  followed by the SORTED absolute pool numbers whose signatures have 
  been changed.
*/


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

/////////////// DECLARATIONS ///////////////


//////// CHOOSING NEIGHBOUR SIGS /////////

// nextToChange: tabChanged is a vector of ints, of size nbChanged.
// It holds the absolute pool numbers of sig values that must be changed.
// This function modifies tabChanged, as follows:
// tabChanged is seen as the representation of a number in base nbPools;
// this number is incremented, but some numbers are skipped so that
// we always have tabChanged[i] < tabChanged[i+1] for every i.
// Initialization: if tabChanged[0]==-1, tabChanged is initialized
// to {0,1,...,nbChanged-1} (ie the representation of the smallest
// number that respects the rule).
// return value: 1 if tabChanged was successfully changed, 0 otherwise
// (ie, if tabChanged was already maximal).
static int nextToChange(int* tabChanged, int nbChanged, int nbPools) ;

// nextValidToChange:
// tabChanged is a vector of ints, of size nbChanged.
// It holds the absolute pool numbers of sig values that must be changed.
// This function modifies tabChanged, by calling nextToChange
// as many times as necessary so that tabChanged contains
// only potentially erroneous pools: all pools from tabChanged must
// be either negative in sig0, or conflicting positives 
// (ie sig==SIG_NEG, SIG_FAINT, SIG_WEAKCONF or SIG_POSCONF).
// Initialization: if tabChanged[0]==-1, tabChanged will be initialized
// to the first valid-to-change vector.
// return value: 1 if tabChanged was successfully changed to the
// next valid vector, 0 otherwise (ie, no more valid vectors exist).
static int nextValidToChange(signature* sig0, int* tabChanged, int nbChanged) ;

// nextNeighbour:
// sig0 is the observed signature, tabChanged holds the list of
// absolute pool numbers that were changed previously, nbChanged is
// the size of tabChanged (ie, hamming distance between sig0 and the
// previous neighbour examined).
// This function modifies tabChanged so that it contains the next valid
// neighbour (according to nextValidToChange), and fills changedPosPools
// and changedNegPools accordingly. It also generates a newsig, identical
// to sig0 except that changedPosPools are set to SIG_FAINT (instead of SIG_POSCONF
// or SIG_WEAKCONF, since they must have been conflicting for nextValidToChange 
// to select them), and changedNegPools are set to SIG_WEAKCONF instead of SIG_NEG
// or SIG_FAINT (indeed, they may cause a conflict and so we don't tag them as SIG_WEAK).
// an initial value of tabChanged[0]==-1 means this is the first call.
// return value: NULL if no more valid neighbours exist at this distance,
// the neighbour signature otherwise (memory is allocated here).
static signature* nextNeighbour(signature* sig0, int* tabChanged, int nbChanged, 
				int* changedPosPools, int* changedNegPools) ;


//////// WORKING ON NegSVs /////////

// buildNegSV: allocate memory for a "Negative pools' Summary Vector",
// and fill it as necessary.
// The set of all the pools of tabpool are partitioned into "parts" 
// identified by a number in {0,..,nbparts-1}.
// A NegSV is a vector of MOTs, same size as a VV (and also as a pool);
// It represents the knowledge that all negative pools from part are
// negative: if a variable is present in a negative pool of part,
// the 2 bits coding for this variable in the NegSV are 00; otherwise
// the 2 bits are 11.
// Therefore, once a NegSV is built, one can take into account all
// negative pools from part by simply doing a bitwise AND with the 
// NegSV (this happens in updateVVNegSV).
static MOT* buildNegSV(MOT* tabpool, signature* mySig, int part, int nbparts, int n);

// buildAllNegSVs: allocate memory for nbparts pointers to MOTs, and
// fill this vector with pointers to NegSVs (built using buildNegSV).
// This function is called once with the observed signature.
// Subsequently, the NegSVs which have been built will be used for
// decoding (ie resolution of) this observed signature, but also
// any "neighbour" signature if noise-correction is called for and
// if no negative pool from the considered part has been changed
// to positive. Other NegSVs will have to be recalculated, but
// globally this greatly speeds up resolution of noisy observations.
static MOT** buildAllNegSVs(MOT* tabpool, signature* mySig, int nbparts, int n);

// freeAllNegSVs: given a MOT** built by buildAllNegSVs, frees all the
// NegSV memory areas, and then frees allNegSVs itself.
static void freeAllNegSVs(MOT** allNegSVs, int nbparts) ;

// firstPoolInPart: return an int representing the absPoolNum of
// the first pool present in the given part.
// NOTE: must also return a correct value for part==nbparts although this
// part does not exist, because we use it to calculate lastPoolInPart (by 
// decrementing firstPoolInPart(part+1)).
// The only property that must be respected is that a part must be a CONSECUTIVE 
// list of pool numbers.
static int firstPoolInPart(int part, int nbparts, int nbPools);

// updateVVNegSV: update the VV VVtab, to take into account
// the info on negative variables present in NegSV.
static void updateVVNegSV(MOT* VVtab, MOT* NegSV, int n);


//////// WORKING ON VVs /////////

/*! 
  \brief updateVVAllNegPools_NegSVs: update the VV VVtab, taking into account
  all the negative pools (as held in tabsig, changedPosPools and 
  changedNegPools).
  The allNegSVs are built here if changedPosPools[0]==changedNegPools[0]==0,
  and stored statically (using the local function buildAllNegSVs);
  They are then used in the case where at least one signature value has
  been changed.
*/
static void updateVVAllNegPools_NegSVs(MOT* VVtab, MOT* tabpool, signature* mySig, 
				       int* changedPosPools, int* changedNegPools, 
				       int nbparts, int n);


// updateVVandFlagConflicts: update the VV VVtab, to reflect 
// the fact that all positive pools are positive (according to tabsig),
// and also update tabsig by changing sigs of all conflicting
// pospools from SIG_POS to SIG_POSCONF.
// return value: 1 if there is a conflict (ie, if VVtab and tabsig are 
// incompatible), 0 otherwise
// when called, tabsig should hold only values SIG_NEG and SIG_POS (this is checked).
// Note that this function examines every pospool, instead of returning 1
// as soon as a conflict is detected.
// This function should be called with the observed signature, and 
// VVtab should have been updated with negpool info.
// If any conflicts are detected, the signature will have been prepared
// for use by updateVVAllPosPools_CF, which will begin by examining
// only the conflicting pospools, and then use the non-conflicting
// pospools only if no conflicts remained.
static int updateVVandFlagConflicts(MOT* VVtab, MOT* tabpool, signature* mySig, int n);


/*! 
  updateVVAllPosPools_CF: assuming all previously Conflicting
  pos pools have been Flagged (hence CF), update the VV VVtab, to reflect 
  the fact that all positive pools are positive (according to tabsig).
  Return value: 1 if there is still a conflict (ie, if VVtab and tabsig are 
  incompatible), 0 otherwise.
  When called, tabsig should hold values SIG_NEG (pool is neg), SIG_POS (pool is
  pos and causes no conflict with the neg pools), or SIG_POSCONF (pool is
  pos but conflicted with the neg pools in the observed signature).
  VVtab should have 00 (var is in a neg pool) or 01 (var is ambi), ie 
  it must have been processed by updateVVAllNegPools_NegSVs beforehand.
  This function examines the (former) conflicting pospools first, and returns
  as soon as a conflict is detected.
  If no former conflicting pospool causes a conflict, it then deals
  with the former non-conflicting ones (which can allow to change
  some 01 varvalues to 11).
*/
static int updateVVAllPosPools_CF(MOT* VVtab, MOT* tabpool, signature* mySig, int n);


//////// DECODING SIGNATURES /////////

// firstDecoding: try solving the observed signature tabsig.
// This function does updateVVAllNegPools_NegSVs with the observed
// sig (ie, changedPosPools and changedNegPools ={0}). 
// In this context, updateVVAllNegPools_NegSVs builds all the NegSVs, which will 
// be used later if noise is detected.
// It then does updateVVandFlagConflicts, which simultaneously
// finds the deduced VV if the observed signature is conflict-less,
// and updates the signature by flagging all conflicting pospools
// if there are any (by changing their sigs from SIG_POS to SIG_POSCONF). This flagging
// will also be used later if noise is detected.
// return value: NULL if a conflict is detected, a pointer to the 
// deduced VV vector (mem allocated in this func) if the observed sig
// has no conflicts.
static MOT* firstDecoding(MOT* tabpool, signature* mySig, int nbparts, int n) ;


// solveSig: try solving the changed signature newsig.
// newsig is a neighbour of the observed sig, and all changes
// must be listed in changedPosPools and changedNegPools.
// since at least one sig value is changed, updateVVAllNegPools_NegSVs
// will use the allNegSVs (built during firstDecoding) to
// see if newsig is conflicting or not.
// for examining pospools we use updateVVAllPosPools_CF, which
// does not modify the signature and returns as soon as a conflict
// is detected.
// return value: NULL if newsig is conflicting, a pointer to the
// deduced VV (allocated in this function) otherwise.
static MOT* solveSig(MOT* tabpool, signature* newsig, int* changedPosPools,
		     int* changedNegPools, int nbparts, int n) ;



//////////////// BODIES ///////////////////



//////// CHOOSING NEIGHBOUR SIGS /////////

////////////////////////////////////////////////////////////////
// nextToChange: tabChanged is a vector of ints, of size nbChanged.
// It holds the absolute pool numbers of sig values that must be changed.
// This function modifies tabChanged, as follows:
// tabChanged is seen as the representation of a number in base nbPools;
// this number is incremented, but some numbers are skipped so that
// we always have tabChanged[i] < tabChanged[i+1] for every i.
// Initialization: if tabChanged[0]==-1, tabChanged is initialized
// to {0,1,...,nbChanged-1} (ie the representation of the smallest
// number that respects the rule).
// return value: 1 if tabChanged was successfully changed, 0 otherwise
// (ie, if tabChanged was already maximal).
static int nextToChange(int* tabChanged, int nbChanged, int nbPools)
{
  if (tabChanged[0]>=(nbPools-nbChanged))
    { // tabChanged is maximal, cannot increment it in base nbPools
      return 0;
    }
  else if (tabChanged[0]==-1)
    { // initialize
      int i ;
      for (i=0; i<nbChanged; i++)
	{
	  tabChanged[i] = i ;
	}
      return 1 ;
    }
  else
    { // increment tabChanged:
      // indexToChange is the index of the first element of tabChanged 
      // which must be incremented;
      // valmax is the maximal value that this element may take
      // initially, try incrementing the last element of tabChanged
      int indexToChange = (nbChanged-1);
      int valmax = (nbPools-1);

      while(tabChanged[indexToChange]==valmax)
	{
	  // this element of tabChanged is already maximal, must try 
	  // the element of higher weight
	  indexToChange--;
	  valmax--;
	}
  
      //we now have the correct index, increment tabChanged
      tabChanged[indexToChange]++ ;
      indexToChange++ ;
      


      // and correctly set each of the lower weight elements
      {
	int i ;
	for(i=indexToChange; i<nbChanged; i++)
	  {
	    tabChanged[i]=tabChanged[i-1]+1;
	  }
      }
      return 1;
    }
}

///////////////////////////////////////////////////////////////////
// nextValidToChange:
// tabChanged is a vector of ints, of size nbChanged.
// It holds the absolute pool numbers of sig values that must be changed.
// This function modifies tabChanged, by calling nextToChange
// as many times as necessary so that tabChanged contains
// only potentially erroneous pools: all pools from tabChanged must
// be either negative in sig0, or conflicting positives (ie sig==SIG_POSCONF).
// Initialization: if tabChanged[0]==-1, tabChanged will be initialized
// to the first valid-to-change vector.
// return value: 1 if tabChanged was successfully changed to the
// next valid vector, 0 otherwise (ie, no more valid vectors exist).
static int nextValidToChange(signature* sig0, int* tabChanged, int nbChanged)
{
  int nbPools = sig0->nbPools ;

  while(nextToChange(tabChanged, nbChanged, nbPools) == 1)
    { //tabChanged successfully changed, see if it is valid
      int valid = 1 ; // boolean, 1 means valid, 0 means invalid
      
      int i ;
      for(i=0; i<nbChanged; i++)
	{ // examine the sig of each pool from nbChanged
	  int absolutePoolNb = tabChanged[i] ;
	  int sigvalue = getsigvalue(sig0, absolutePoolNb) ;

	  if ((sigvalue == SIG_NEG) || (sigvalue == SIG_FAINT) || 
	      (sigvalue == SIG_POSCONF) || (sigvalue == SIG_WEAKCONF))
	    {
	      // ok, this pool can be changed
	      continue ;
	    }
	  else
	    { // invalid pool, have to try next tabChanged
	      valid = 0 ;
	      break ;
	    }
	}

      if (valid==1)
	{ // current tabChanged is valid, done
	  return 1 ;
	}
      // else try next tabChanged
    }

  // if we get here, no more valid tabChanged exists
  return 0 ;
}


///////////////////////////////////////////////////////////
// nextNeighbour:
// sig0 is the observed signature, tabChanged holds the list of
// absolute pool numbers that were changed previously, nbChanged is
// the size of tabChanged (ie, hamming distance between sig0 and the
// previous neighbour examined).
// This function modifies tabChanged so that it contains the next valid
// neighbour (according to nextValidToChange), and fills changedPosPools
// and changedNegPools accordingly. It also generates a newsig, identical
// to sig0 except that changedPosPools are set to SIG_FAINT (instead of SIG_POSCONF
// or SIG_WEAKCONF, since they must have been conflicting for nextValidToChange 
// to select them), and changedNegPools are set to SIG_WEAKCONF instead of SIG_NEG
// or SIG_FAINT (indeed, they may cause a conflict and so we don't tag them as SIG_WEAK).
// an initial value of tabChanged[0]==-1 means this is the first call.
// return value: NULL if no more valid neighbours exist at this distance,
// the neighbour signature otherwise (memory is allocated here).
static signature* nextNeighbour(signature* sig0, int* tabChanged, int nbChanged, 
				int* changedPosPools, int* changedNegPools)
{
  signature* newsig = copysig(sig0) ; 

  // initialize changedPosPools and changedNegPools
  changedPosPools[0] = 0 ;
  changedNegPools[0] = 0 ;

  if (nextValidToChange(sig0, tabChanged, nbChanged) == 0)
    {
      // no more valid neighbours
      freeSig(newsig) ;
      return NULL ;
    }
  else
    { // OK, tabChanged holds the next valid list of sigs to change
      // fill changedPosPools and changedNegPools, and modify newsig
      int i ;
      for (i=0; i<nbChanged; i++)
	{
	  int absolutePoolNb = tabChanged[i] ;
	  int sigvalue = getsigvalue(newsig, absolutePoolNb) ;
	  if ((sigvalue == SIG_NEG) || (sigvalue == SIG_FAINT))
	    { // this pool was neg or faint, change to weak
	      setsigvalue(newsig, absolutePoolNb, SIG_WEAKCONF) ;
	      changedNegPools[0]++ ;
	      changedNegPools[changedNegPools[0]] = absolutePoolNb ;
	    }
	  else if ((sigvalue == SIG_POSCONF) || (sigvalue == SIG_WEAKCONF))
	    { // this pool was pos or weak, change to faint
	      setsigvalue(newsig, absolutePoolNb, SIG_FAINT) ;
	      changedPosPools[0]++ ;
	      changedPosPools[changedPosPools[0]] = absolutePoolNb ;
	    }
	  else
	    { // should not happen, nextValidToChange should not produce this
	      fprintf(stderr, "in nextNeighbour, a pool's sig is not SIG_NEG, SIG_FAINT, SIG_WEAKCONF or SIG_POSCONF, should not happen\n") ;
	      exit(1) ;
	    }
	}

      return newsig ;
    }
}


//////// WORKING ON NegSVs /////////


///////////////////////////////////////////////////////////////
// buildNegSV: allocate memory for a "Negative pools' Summary Vector",
// and fill it as necessary.
// The set of all the pools of tabpool are partitioned into "parts" 
// identified by a number in {0,..,nbparts-1}.
// A NegSV is a vector of MOTs, same size as a VV (and also as a pool);
// It represents the knowledge that all negative pools from part are
// negative: if a variable is present in a negative pool of part,
// the 2 bits coding for this variable in the NegSV are 00; otherwise
// the 2 bits are 11.
// Therefore, once a NegSV is built, one can take into account all
// negative pools from part by simply doing a bitwise AND with the 
// NegSV (this happens in updateVVNegSV).
static MOT* buildNegSV(MOT* tabpool, signature* mySig, int part, int nbparts, int n)
{
  int NegSVsize = nbmotparpool(n); // number of MOTs in a NegSV
  int nbPools = mySig->nbPools ;

  // allocate memory
  MOT* NegSV = (MOT*)malloc(NegSVsize*sizeof(MOT)) ;
  if(NegSV==NULL)
    {
      fprintf(stderr,"in buildNegSV, no more memory for NegSV\n");
      exit(1);
    }

  // initialize: fill with 1's
  {
    unsigned char inibyte = 255 ; // 255 == 11111111
    memset(NegSV, inibyte, NegSVsize*sizeof(MOT));
  }

  ///////////////////////////
  // replace the 11's by 00's when the variable is in a negative pool from part
  ///////////////////////////
  {
    // absolute<First/Last>PoolNb: int representing the first/last pool of part
    int absoluteFirstPoolNb = firstPoolInPart(part, nbparts, nbPools) ;
    int absoluteLastPoolNb = firstPoolInPart(part+1, nbparts, nbPools) - 1 ;
    int absolutePoolNb ; // loop variable
    for(absolutePoolNb = absoluteFirstPoolNb; absolutePoolNb <= absoluteLastPoolNb ; absolutePoolNb++)
      {
	if ((getsigvalue(mySig, absolutePoolNb) == SIG_NEG) || (getsigvalue(mySig, absolutePoolNb) == SIG_FAINT))
	  { // this pool is negative or faint, update NegSV
	    MOT* currentPool = pool(tabpool, absolutePoolNb, n) ;
	    updateVVNegPool(NegSV, currentPool, n);
	  }
      }
  }

  return NegSV;
}


///////////////////////////////////////////////////////////////
// buildAllNegSVs: allocate memory for nbparts pointers to MOTs, and
// fill this vector with pointers to NegSVs (built using buildNegSV).
// This function is called once with the observed signature.
// Subsequently, the NegSVs which have been built will be used for
// decoding (ie resolution of) this observed signature, but also
// any "neighbour" signature if noise-correction is called for and
// if no negative pool from the considered part has been changed
// to positive. Other NegSVs will have to be recalculated, but
// globally this greatly speeds up resolution of noisy observations.
static MOT** buildAllNegSVs(MOT* tabpool, signature* mySig, int nbparts, int n)
{
  // allocate memory for the table of pointers to NegSVs
  MOT** allNegSVs = (MOT**)malloc(nbparts*sizeof(MOT*)) ;
  if(allNegSVs==NULL)
    {
      fprintf(stderr,"in buildAllNegSVs, non more memory for allNegSVs\n");
      exit(1);
    }

  // fill allNegSVs:
  {
    int part;
    for (part=0; part < nbparts; part++)
      {
	allNegSVs[part] = buildNegSV(tabpool, mySig, part, nbparts, n) ;
      }
  }

  return allNegSVs ;
}



///////////////////////////////////////////////////////////////
// freeAllNegSVs: given a MOT** built by buildAllNegSVs, frees all the
// NegSV memory areas, and then frees allNegSVs itself.
static void freeAllNegSVs(MOT** allNegSVs, int nbparts)
{
  int i ;
  for (i=0; i<nbparts; i++)
    {
      free(allNegSVs[i]) ;
    }
  free(allNegSVs) ;
}

///////////////////////////////////////////////////////////////
// firstPoolInPart: return an int representing the absPoolNum of
// the first pool present in the given part.
// NOTE: must also return a correct value for part==nbparts although this
// part does not exist, because we use it to calculate lastPoolInPart (by 
// decrementing firstPoolInPart(part+1)).
// Currently the partitioning is very simple, we just build
// parts containing equal numbers of pools, but it could be refined
// eg so that each part contains an equal number of NEGATIVE pools.
// This would probably be faster. It would only require modifying
// the body of this function. The only property that must be respected
// is that a part must be a CONSECUTIVE list of pool numbers.
static int firstPoolInPart(int part, int nbparts, int nbPools)
{
  // sanity check: part must be <= nbparts
  if (part > nbparts)
    {
      fprintf(stderr,"in firstPoolInPart, (part=%d) > (nbparts=%d), illegal\n", part, nbparts);
      exit(1);
    }

  {
    if (part==nbparts)
      {
	// special case: the last part must include any pools up to nbPools,
	// beyond nbparts*(nbPools/nbparts) (which can be less than nbPools).
	return(nbPools) ;
      }
    else
      {
	// partsize: number of pools per part (except the last part which must be slightly larger)
	int partsize = nbPools / nbparts ; 
	return(part * partsize) ;
      }
  }
}


///////////////////////////////////////////////////////////////
// updateVVNegSV: update the VV VVtab, to take into account
// the info on negative variables present in NegSV.
// This is very similar to updateVVNegPool, except we don't complement
static void updateVVNegSV(MOT* VVtab, MOT* NegSV, int n)
{
  int nbmots = nbmotparpool(n) ;
  MOT* VVtab_ = VVtab ;
  MOT* NegSV_ = NegSV ;
  int i ;
  for (i=nbmots-1; i >= 0; i--)
    {
      /* VVtab[i] = VVtab[i] & NegSV[i] ; */
      *VVtab_ = (*VVtab_) & (*NegSV_) ;
      VVtab_ ++ ;
      NegSV_ ++ ;
    }
}


//////// WORKING ON VVs /////////

///////////////////////////////////////////////////////////////
/*!
  updateVVAllNegPools_NegSVs: update the VV VVtab, taking into 
  account all the negative pools (as held in tabsig, changedPosPools 
  and changedNegPools, which must be SORTED!) 
  Signature values that have been changed from the observed sig must be 
  listed in changed*Pools, and tabsig must also have been updated. 
  When called on the observed sig, ie if changedPosPools[0]==changedNegPools[0]==0, 
  we buildAllNegSVs and store the resulting allNegSVs statically; 
  otherwise, if at least one sig value is changed: it means that allNegSVs 
  has already been built. This assumes that solvexpNaive will always first 
  try decoding the observed (ie unchanged) signature, and then go on to explore 
  neighbours of the observed sig if it caused conflicts. In this case, we use the 
  statically stored allNegSVs to update VV, except that: 
  - 1. for pools in changedNegPools, the NegSVs cannot be used and have to be 
    rebuilt, using tabsig (which must therefore be up-to-date!); 
  - 2. pools in changedPosPools have to be taken into account individually, 
    by calling updateVVNegPool.
*/
void updateVVAllNegPools_NegSVs(MOT* VVtab, MOT* tabpool, signature* mySig, int* changedPosPools, 
				int* changedNegPools, int nbparts, int n)
{
  static MOT** allNegSVs = NULL ;

  int nbChangedPos = changedPosPools[0] ; // number of changed pos pools
  int nbChangedNeg = changedNegPools[0] ; // number of changed neg pools

  if ((nbChangedPos==0) && (nbChangedNeg==0))
    {
      // no changed sigs, this is the first call with an observed signature
      // we have to build a fresh allNegSVs vector
      if (allNegSVs != NULL)
	{
	  // some other observed signature has been used before, we must free all the SVs
	  freeAllNegSVs(allNegSVs, nbparts) ;
	}
      allNegSVs = buildAllNegSVs(tabpool, mySig, nbparts, n) ;
    }

#ifdef SANITY
  // make sure changedNegPools and changedPosPools are sorted: idem for weak & faint
    {
      int i ;
      for (i=2; i <= nbChangedNeg; i++)
	{
	  if (changedNegPools[i] <= changedNegPools[i-1])
	    {
	      fprintf(stderr, "in updateVVAllNegPools_NegSVs, changedNegPools is not sorted!\n") ;
	      exit(1) ;
	    }
	}
      for (i=2; i <= nbChangedPos; i++)
	{
	  if (changedPosPools[i] <= changedPosPools[i-1])
	    {
	      fprintf(stderr, "in updateVVAllNegPools_NegSVs, changedPosPools is not sorted!\n") ;
	      exit(1) ;
	    }
	}
    }
#endif

  // Now update VV, using allNegSVs except the NegSVs that contain a changedNegPool
  {
    int* changedNeg = changedNegPools + nbChangedNeg ;
    // changedNeg: pointer to current changed negative pool, begin with the last changed neg pool
    int part ; /* loop var */
    for (part=nbparts-1; part>=0; part--)
      {
	if (changedNeg != changedNegPools)
	  { // some changed neg pools remain, see if any are in current part
	    int firstPoolThisPart = firstPoolInPart(part, nbparts, mySig->nbPools);
	    if (firstPoolThisPart <= *changedNeg)
	      { // this part contains at least one changed neg, we must rebuild the NegSV
		// move changedNeg to the last changed neg that is NOT in this part
		changedNeg-- ;
		if (changedNeg != changedNegPools)
		  while(firstPoolThisPart <= *changedNeg)
		    {
		      // current changedNeg is in this part, examine previous changed neg
		      changedNeg-- ;
		      if (changedNeg == changedNegPools)
			break ;
		    }
		// after this while, changedNeg is either changedNegPools, meaning no more changed
		// neg pools remain; or it is the index of the previous changed neg, which does
		// not belong to current part, but must be checked for in the previous parts.
		// in any case, this part contains at least one changed neg, and must
		// therefore be rebuilt
		{
		  MOT* tempNegSV = buildNegSV(tabpool, mySig, part, nbparts, n);
		  
		  // now update VVtab with tempNegSV
		  updateVVNegSV(VVtab, tempNegSV, n);
		  // and free the memory, tempNegSV is no longer needed
		  free(tempNegSV) ;
		}
	      }
	    else
	      {
		// some neg pools remain, but none were in this part
		// we can use the stored NegSV
		MOT* storedNegSV = allNegSVs[part] ;
		updateVVNegSV(VVtab, storedNegSV, n);
	      }
	  }
	else
	  {
	    // changedNeg==changedNegPools, there were no remaining changedNegs
	    // same as above, use the stored NegSV
	    MOT* storedNegSV = allNegSVs[part] ;
	    updateVVNegSV(VVtab, storedNegSV, n);
	  }
      }
  }
  
  /* Finally, take into account all changedPosPools individually.
     This is redundant when a part contained a changed neg, since in this case
     we used tabsig directly to build tempNegSV, but it's not so important...
     just a little extra work! */
  {
    int i ;
    for (i=1; i <= nbChangedPos; i++)
      {
	MOT* currentPool = pool(tabpool, changedPosPools[i], n) ;
	updateVVNegPool(VVtab, currentPool, n);
      }
  }
}






///////////////////////////////////////////////////////////////
// updateVVandFlagConflicts: update the VV VVtab, to reflect 
// the fact that all positive pools are positive (according to tabsig),
// and also update tabsig by changing sigs of all conflicting
// pospools from SIG_POS to SIG_POSCONF and from SIG_WEAK to SIG_WEAKCONF.
// return value: 1 if there is a conflict (ie, if VVtab and tabsig are 
// incompatible), 0 otherwise.
// when called, tabsig should hold only values SIG_NEG, SIG_FAINT, SIG_WEAK  and 
// SIG_POS (this is checked).
// Note that this function examines every pospool, instead of returning 1
// as soon as a conflict is detected.
// This function should be called with the observed signature, and 
// VVtab should have been updated with negpool info.
// If any conflicts are detected, the signature will have been prepared
// for use by updateVVAllPosPools, which will begin by examining
// only the conflicting pospools, and then use the non-conflicting
// pospools only if no conflicts remained.
int updateVVandFlagConflicts(MOT* VVtab, MOT* tabpool, signature* mySig, int n)
{
  int conflict = 0 ; // boolean, ==1 iff at least one conflict detected
  int absolutePoolNb ; // loop variable, the absolute pool number
  int lastAbsolutePoolNb = mySig->nbPools -1 ; // last abs pool number
  for(absolutePoolNb = 0; absolutePoolNb <= lastAbsolutePoolNb; absolutePoolNb++)
    {
      int sigvalue = getsigvalue(mySig, absolutePoolNb) ;
      if (sigvalue == SIG_POS)
	{
	  // this pool is positive, try updating VVtab and see if it 
	  // conflicts. If it does, change it's sig to SIG_POSCONF.
	  MOT* currentPool = pool(tabpool, absolutePoolNb, n) ;
	  if (updateVVPosPool(VVtab, currentPool, n) == 1)
	    { // currentPool causes a conflict, set the sig to SIG_POSCONF
	      setsigvalue(mySig, absolutePoolNb, SIG_POSCONF);
	      conflict = 1 ;
	    }
	}
      else if (sigvalue == SIG_WEAK)
	{
	  // this pool is weak, try updating VVtab and see if it 
	  // conflicts. If it does, change it's sig to SIG_WEAKCONF.
	  MOT* currentPool = pool(tabpool, absolutePoolNb, n) ;
	  if (updateVVPosPool(VVtab, currentPool, n) == 1)
	    { // currentPool causes a conflict, set the sig to SIG_WEAKCONF
	      setsigvalue(mySig, absolutePoolNb, SIG_WEAKCONF);
	      conflict = 1 ;
	    }
	}
      else if ((sigvalue != SIG_NEG) && (sigvalue != SIG_FAINT))
	{
	  fprintf(stderr, 
		  "In updateVVandFlagConflicts: mySig has a value that is not SIG_NEG, SIG_FAINT, SIG_WEAK or SIG_POS.\n") ;
	  exit(1) ;
	}
    }

  // VVtab and tabsig fully updated, return 1 if a conflict was detected
  if (conflict==1)
    return 1 ;
  else
    return 0 ;
}



///////////////////////////////////////////////////////////////
// updateVVAllPosPools_CF: update the VV VVtab, to reflect 
// the fact that all positive pools are positive (according to tabsig).
// return value: 1 if there is a conflict (ie, if VVtab and tabsig are 
// incompatible), 0 otherwise
// when called, tabsig should hold values SIG_NEG (pool is neg), SIG_FAINT 
// (pool is faint), SIG_WEAK (pool is weak and causes no conflict with the
//  neg pools),SIG_WEAKCONF (pool is pos but conflicted with the former neg
// pools), SIG_POS (pool is pos and causes no conflict with the neg pools), 
// or SIG_POSCONF (pool is pos but conflicted with the former neg pools)
// VVtab should have 00 (var is in a neg pool) or 01 (var is ambi), ie 
// it must have been processed by updateVVAllNegPools beforehand.
// This function examines the (former) conflicting pospools first, and returns
// as soon as a conflict is detected.
// If no former conflicting pospool causes a conflict, it then deals
// with the former non-conflicting ones (which can allow to change
// some 01 varvalues to 11).
int updateVVAllPosPools_CF(MOT* VVtab, MOT* tabpool, signature* mySig, int n)
{
  int absolutePoolNb ; // loop variable, the absolute pool number
  int lastAbsolutePoolNb = mySig->nbPools -1 ; // last abs pool number
  for(absolutePoolNb = lastAbsolutePoolNb; absolutePoolNb >= 0; absolutePoolNb--)
    {
      int sigvalue = getsigvalue(mySig, absolutePoolNb);
      if ((sigvalue == SIG_POSCONF) || (sigvalue == SIG_WEAKCONF))
	{ 
	  // this pool is positive and was conflicting in the observed signature,
	  // try updating VVtab and see if it still conflicts
	  MOT* currentPool = pool(tabpool, absolutePoolNb, n) ;
	  if (updateVVPosPool(VVtab, currentPool, n) == 1)
	    { // currentPool causes a conflict
	      return 1 ;
	    }
	}
    }
  // okey dokey, all positive pools examined and no conflict detected
  // now update VVtab by taking into account the non-conflicting PosPools
  for(absolutePoolNb = lastAbsolutePoolNb; absolutePoolNb >= 0; absolutePoolNb--)
    {
      int sigvalue = getsigvalue(mySig, absolutePoolNb);
      if ((sigvalue == SIG_POS) || (sigvalue == SIG_WEAK) )
	{ 
	  // this pool is a non-conflicting positive, update VVtab
	  MOT* currentPool = pool(tabpool, absolutePoolNb, n) ;
	  if (updateVVPosPool(VVtab, currentPool, n) == 1)
	    { // currentPool causes a conflict, should never happen!
	      fprintf(stderr, 
		      "in updateVVAllPosPools_CF, a non-conflicting PosPool (abs number %d) causes a conflict!\n",
		      absolutePoolNb);
	      exit(1);
	    }
	}
    }

  // VVtab is now fully updated, return 0
  return 0 ;
}

//////// DECODING SIGNATURES /////////

///////////////////////////////////////////////////////////////
// firstDecoding: try solving the observed signature mySig.
// This function does updateVVAllNegPools_NegSVs with the observed
// sig (ie, changedPosPools and changedNegPools ={0}). 
// In this context, updateVVAllNegPools_NegSVs builds all the NegSVs, which will 
// be used later if noise is detected.
// It then does updateVVandFlagConflicts, which simultaneously
// finds the deduced VV if the observed signature is conflict-less,
// and updates the signature by flagging all conflicting pospools
// if there are any (by changing their sigs from SIG_POS to SIG_POSCONF). This flagging
// will also be used later if noise is detected.
// return value: NULL if a conflict is detected, a pointer to the 
// deduced VV vector (mem allocated in this func) if the observed sig
// has no conflicts.
static MOT* firstDecoding(MOT* tabpool, signature* mySig, int nbparts, int n)
{
  // VVtab: stores the VV which might be returned (initiated with 01's).
  // memory is allocated in buildInitialVV, we must free it if a conflict is detected
  MOT* VVtab ;
  int changedPools[1] = {0} ; // no changedPools here

  VVtab = buildInitialVV(n,85) ; // initialize VVtab with 01's

  updateVVAllNegPools_NegSVs(VVtab, tabpool, mySig, changedPools, changedPools, nbparts, n) ;
  
  if (updateVVandFlagConflicts(VVtab, tabpool, mySig, n) == 1)
    { // conflict detected. mySig has been correctly updated, discard VVtab
      free(VVtab) ;
      VVtab = NULL ;
    }

  return VVtab;
}


///////////////////////////////////////////////////////////////
// solveSig: try solving the changed signature newsig.
// newsig is a neighbour of the observed sig, and all changes
// must be listed in changedPosPools and changedNegPools.
// since at least one sig value is changed, updateVVAllNegPools_NegSVs
// will use the allNegSVs (built during firstDecoding) to
// see if newsig is conflicting or not.
// for examining pospools we use updateVVAllPosPools_CF, which
// does not modify the signature and returns as soon as a conflict
// is detected.
// return value: NULL if newsig is conflicting, a pointer to the
// deduced VV (allocated in this function) otherwise.
static MOT* solveSig(MOT* tabpool, signature* newsig, int* changedPosPools, 
		     int* changedNegPools, int nbparts, int n)
{
  // VVtab: stores the VV which might be returned (initiated with 01's).
  // memory is allocated in buildInitialVV, we must free it if a conflict is detected
  MOT* VVtab = buildInitialVV(n,85) ;

  updateVVAllNegPools_NegSVs(VVtab, tabpool, newsig, changedPosPools, changedNegPools, nbparts, n) ;

  if (updateVVAllPosPools_CF(VVtab, tabpool, newsig, n) == 1)
    { // conflict detected, discard VVtab
      free(VVtab) ;
      VVtab = NULL ;
    }

  return VVtab;
}



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


/*!
  \brief Given an observation mySig, find all nearest coherent
  signatures and return them in a setOfSigs.
  This function uses a naive algorithm, and stops if no coherent sigs were 
  found at a distance <= PROFMAX (defined in solvexpNaive.c). In this case, 
  the returned setOfSigs has distance==PROFMAX and nbOfSigs==0.
  NOTES:
  - this function only works with the Hamming distance, ie DIST_xxx = 1 forall xxx.
  - mySig is an observation: it can have only SIG_POS, SIG_WEAK,
  SIG_FAINT or SIG_NEG (no SIG_xxxCONF).
  - The returned setOfSigs is a set of interpretations, it only has
  SIG_POS or SIG_NEG.
  - mySig used to be modified by this function, but this no longer happens.

  Algorithm is:
  - examine if mySig is coherent;
  - if it is not, ie some conflicts are detected, examine the neighbours
  of mySig of increasing distance to mySig (the maximal distance 
  considered is PROFMAX).
  If a coherent interpretation is found at a given distance d, find all
  the coherent interpretations at this distance but do not try increasing
  d anymore.
  Finally, return a setOfSigs holding all nearest coherent interpretations,
  along with their number and distance to tabsig.
*/
setOfSigs solvexpNaive(MOT* tabpool, signature* mySig, int n)
{
  /* before anything else, make sure we are dealing with the Hamming
     distance. This algo hasn't been generalized to arbitrary distances. */
  if ((DIST_NEG != 1) || (DIST_FAINT != 1) || (DIST_WEAK != 1) || (DIST_POS != 1))
    {
      fprintf(stderr, "solvexpNaive called but distance is not Hamming! dying.\n") ;
      exit(1) ;
    }

  /* immediately copy mySig to a fresh signature:
     this is done because the signature gets modified in firstDecoding,
     and we don't want to change mySig.
     Remember to free copiedSig before returning. */
  signature* copiedSig = copysig(mySig) ;
      
  // coherentSigs: structure that will be returned.
  setOfSigs coherentSigs = buildEmptySetOfSigs() ;

  /* just always use the constant NBPARTS value */
  int nbparts = NBPARTS ;

  /////////////////////////////////////////////////////
  // start decoding: try with the observed sig first
  MOT* VVtab = firstDecoding(tabpool, copiedSig, nbparts, n) ;
  
  if (VVtab != NULL)
    { /* the observed sig is coherent, add the canonical
	 interpretation, free copiedSig and return */
      signature* goodSig = canonicalInterp(copiedSig) ;
      freeSig(copiedSig) ;
      addSigToSet(&coherentSigs, goodSig) ;
      free(VVtab) ; // discard VVtab, we just keep the signature
      return(coherentSigs) ;
    }

  else
    { // observed sig is not coherent, examine neighbours of copiedSig
      // copiedSig has been updated to tag conflicting pospools, we can use solveSig
      
      signature* newsig; // will store the current neighbour signature

      int* tabChanged ; 
      // tabChanged: will hold the list of changed absolute pool numbers
      int* changedPosPools ; 
      // will hold the number of changed pospools (POS and WEAK) at index 0, followed 
      // by the sorted abs pool numbers
      int* changedNegPools ;
      // idem for changed negpools 

      // allocate memory for these 3 vectors
      tabChanged = (int*) malloc(PROFMAX * sizeof(int)) ;
      if (tabChanged == NULL)
	{
	  fprintf(stderr, "in solvexpNaive, no more memory for tabChanged\n") ;
	  exit(1) ;
	}
      changedPosPools = (int*) malloc((PROFMAX+1) * sizeof(int)) ;
      if (changedPosPools == NULL)
	{
	  fprintf(stderr, "in solvexpNaive, no more memory for changedPosPools\n") ;
	  exit(1) ;
	}
      changedNegPools = (int*) malloc((PROFMAX+1) * sizeof(int)) ;
      if (changedNegPools == NULL)
	{
	  fprintf(stderr, "in solvexpNaive, no more memory for changedNegPools\n") ;
	  exit(1) ;
	}
      
      // initialize them to 0 (for safety)
      memset(tabChanged, 0, PROFMAX * sizeof(int)) ;
      memset(changedPosPools, 0, (PROFMAX+1) * sizeof(int)) ;
      memset(changedNegPools, 0, (PROFMAX+1) * sizeof(int)) ;
      
      int distance ;
      for (distance = 1; distance <= PROFMAX; distance++)
	{ // examine neighbours of copiedSig, starting at distance 1
	  // initialize tabChanged
	  tabChanged[0] = -1 ;

	  while ((newsig = nextNeighbour(copiedSig, tabChanged, distance, 
					 changedPosPools, changedNegPools))
		 != NULL)
	    {
	      
	      VVtab = solveSig(tabpool, newsig, changedPosPools, changedNegPools, nbparts, n) ;

	      if (VVtab != NULL)
		{ // current sig is coherent, save newsig
		  
		  
		  // newsig has ex-conflicting pospools flagged, change them
		  // to regular non-conflicting status (ie, SIG_POS)
		  {
		    int absPoolNb ;
		    int nbPools = mySig->nbPools ;
		    for (absPoolNb=0; absPoolNb < nbPools; absPoolNb++)
		      {
			if (getsigvalue(newsig, absPoolNb) == SIG_POSCONF)
			  setsigvalue(newsig, absPoolNb, SIG_POS) ;
			if (getsigvalue(newsig, absPoolNb) == SIG_WEAKCONF)
			  setsigvalue(newsig, absPoolNb, SIG_WEAK) ;
		      }
		  }
		  
		  /* build corresponding interpretation */
		  signature* goodsig = canonicalInterp(newsig) ;
		  freeSig(newsig) ;

		  // check if the signature is not already in allSigs
		  int valid = 1 ;
		  int i ;// loop indice
		  for (i=0 ; i<coherentSigs.nbOfSigs; i++) 
		    {
		      if (equalSigs(goodsig, coherentSigs.allSigs[i]))
			valid = 0;
		    }
		  
		  if (valid == 1) 
		    addSigToSet(&coherentSigs,goodsig) ;
		  else
		    // goodsig is redundant, free it
		    freeSig(goodsig) ;
		  free(VVtab);// VVtab is discarded, we just keep the signatures now
		}
	      else
		{ // newsig is not coherent, free it
		  freeSig(newsig) ;
		}
	    }

	  // no more neighbours at current distance
	  if (coherentSigs.nbOfSigs > 0)
	    {
	      // at least one good sig was found, done
	      free(tabChanged) ;
	      free(changedPosPools) ;
	      free(changedNegPools) ;
	      coherentSigs.distance = distance ;
	      goto done ;
	    }
	  // else increase distance
	}

      // if we get here, no coherent neighbour at distance <= PROFMAX was found
      // return setOfSigs with nbOfSigs==0, distance==PROFMAX, and allSigs==NULL
      free(tabChanged) ;
      free(changedPosPools) ;
      free(changedNegPools) ;
      coherentSigs.distance = distance ;
      goto done ;
    }

  
 done:

  freeSig(copiedSig) ; // copiedSig was the copy of mySig, discard it
  return coherentSigs ;

}

