/*-----------------------------------------------------------------*
 *
 * File : varia.c
 * Author : NTM
 * Created : 30/09/03
 *
 *
 * 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> // printf(stderr,)
#include <stdlib.h> // malloc etc..., and qsort
#include <math.h> // rint
#include <string.h> // memset

#include "pools.h" // nbmotparpool
#include "fonc.h" // compInts
#include "myrand.h" // myrandom
#include "varia.h"


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

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


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


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


/*!
  Allocates memory for a VV vector, and fills it with inibyte. 
  Useful value: 85 (==01010101, meaning "all variables are unknown").
  I also use 0 occasionally.

  NOTE: this function calls nbmotparpool which caches it's result
  in a static; therefore it is more efficient to only use one 
  value for n (it should always be the number of variables, which 
  is constant in one simulation batch). <br>
  An exception is if you want a single MOT initialized with eg 01's, 
  you can call buildInitialVV with n==1 and it will not call
  nbmotparpool, therefore it won't disrupt the static caching system.
*/
MOT* buildInitialVV(int n, unsigned char inibyte)
{
  int VVsize = 1 ;
  if (n!=1)
    VVsize = nbmotparpool(n); // number of MOTs in a VV

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

  // initialize: fill with inibyte
  memset(VV, inibyte, VVsize * sizeof(MOT));

  // NOTE: if inibyte=85, the final MOT of VV contains 01's even 
  // beyond the last variable, keep this in mind when manipulating 
  // the MOTs of VVs (eg in updateVVPosPool)

  return VV;
}




/*!
  Update the VV VVtab, to reflect the fact that pool is negative.
  every variable present in the pool is known to be negative (value set to 
  00 in VVtab).<br>
  n is the total number of variables<br>
  This function exploits the fact that the VV vectors and the pools
  have been designed with an identical structure, and uses bitwise operations
  on MOTs to achieve high performance<br>
  NOTE: from JL: added q and k as params, required for tabpoolsize,
  which is used when tabpool is double-sized and contains ~ in second
  half, see below. 
*/
void updateVVNegPool(MOT* VVtab, MOT* pool, int n)
{
  int nbmotpool = nbmotparpool(n) ;
  int i ;
  for (i = nbmotpool-1; i>=0; i--)
    {
      *VVtab = (*VVtab) & (~(*pool)) ;
      VVtab++ ;
      pool++ ;
    }
}

/*
  Update the VV VVtab, to reflect the fact that pool is positive:
  If at least one variable present in pool is marked positive in VVtab,
  or if at least 2 variables are marked ambiguous, do nothing and return 0;<br>
  else, if no variables are marked positive and exactly one variable
  is marked ambiguous, mark this variable as positive and return 0;<br>
  else: there is a conflict, this pool being positive is incompatible
  with the current VV vector; in this case return 1.<br>
  n is the total number of variables
*/
int updateVVPosPool(MOT* VVtab, MOT* pool, int n)
{
  int nbmotpool = nbmotparpool(n) ;

  int nbvarparmot = sizeof(MOT) * 4 ; /* number of variables' values in a MOT, 
					 2 bits per variable => 4 variables per byte */

  int vartochange = -1; // variable vartochange must be set to 11
  // (value -1 means no ambiguous variable has been found yet)

  int motindex ;
  for (motindex=0; motindex < nbmotpool; motindex++)
    {
      MOT varvaluesinpool = VVtab[motindex] & pool[motindex] ;
      // WATCH IT! when motindex==nbmotpool-1, it is crucial that the last
      // MOT of VVtab or of pool have been padded with 0's after the last variable.
      // This is the case for all pools (it is done in STD/3, see pools.c), but
      // not for VVtab (see buildInitialVV/1 above).

      if (varvaluesinpool == 0)
	{ 
	  // all variables from pool in this MOT are negative
	  continue;
	}
      else
	{ 
	  // at least one non-negative variable in this MOT
	  if (vartochange >= 0)
	    {
	      //another non-negative variable has already been found for this pool
	      // do nothing and return 0 (no conflict for this pool but nothing can be deduced)
	      return 0 ;
	    }
	  else
	    {
	      // il faut descendre au niveau des variables
	      // les variables stockees dans le mot d'indice i sont [varmin..varmax[, avec:
	      int varmin = nbvarparmot * motindex ;
	      int varmax = nbvarparmot * (motindex+1) ;
	      int var ; /* loop var */
	      if (varmax > n)
		{ 
		  // la valeur max est toujours < n
		  varmax = n;
		}
	      for (var = varmin ; var < varmax ; var++)
		{
		  // I could still work directly on varvaluesinpool, using the following algorithm:
		  // consider the 2 bits coding for var in varvaluesinpool, and do:
		  // 1. if ==00, continue (ie, examine next var)
		  // 2. else if ==11, return 0 (cannot conclude anything)
		  // 3. else if ==01: if vartochange==0, vartochange=var and continue
		  //                       else return 0 (this is the second 01 var in this mot)
		  //
		  // However, the current algo simply gets 2 MOTs more than would be necessary,
		  // so I will keep it for now (accessing the 2 bits coding for
		  // var in varvaluesinpool would require using a trick, instead
		  // of the currently used getpoolvalue, and would therefore be
		  // more messy).

		  // varinpool: 0 si var absente du pool, 11 si presente
		  int varinpool = getpoolvalue(pool, var) ;
		  if (varinpool==0)
		    {
		      // cette var n'est pas dans le pool
		      continue ;
		    }
		  else if (varinpool==11)
		    {
		      // var est dans pool, regarder dans VVtab
		      // varvalue: 0 si var est marquee fausse, 1 si ambi et 11 si marquee bonne
		      int varvalue = getpoolvalue(VVtab, var) ;
		      if (varvalue == 11)
			{ // cette var est deja marquee vraie, on ne peut rien conclure de ce pool
			  return 0 ;
			}
		      else if (varvalue==0)
			{
			  // var est marquee fausse, var suivante
			  continue ;
			}
		      else if (varvalue==1)
			{
			  // varvalue == 1, cette var est marquee ambi
			  if (vartochange >= 0)
			    {
			      // une autre var avait deja ete identifiee a changer, ca fait
			      // donc au moins 2, on ne peut rien conclure
			      return 0 ;
			    }
			  else
			    {
			      // premiere var ambi rencontree, on fixe vartochange
			      vartochange = var ;
			    }
			}
		      else
			{ // in VVtab, values other than 0, 1 or 11 are not allowed
			  fprintf(stderr, "in updateVVPosPool, var %d has an illegal value in VVtab\n", var);
			  exit(1);
			}
		    }
		  else
		    { // varinpool should be 0 or 11, die
		      fprintf(stderr, 
			      "in updateVVPosPool, the value of var %d in a pool is neither 0 nor 11\n", 
			      var);
		      exit(1);
		    }
		} // end for(var..), done examining the current MOT
	    }
	}
    }
  // si on arrive ici (sans avoir fait return), soit vartochange contient l'unique var ambi
  // de ce pool, qu'il faut fixer a 11 dans VVtab; soit vartochange == -1, ce qui veut
  // dire qu'il y a conflit
  if (vartochange == -1)
    { 
      // conflict
      return 1 ;
    }
  else
    { 
      // this pool proves that vartochange is positive, update VVtab
      setpoolvalue(VVtab,vartochange,11);
      return 0;
    }
}


/*!
  Return TRUE if pool contains a variable that is not marked 00 in VVtab.
  \param pool: a pool (vars present must be marked 11, absents are 00)
  \param VVtab: a VV (same size as a pool)
  \param n: the number of variables
  \return true if pool contains a variable that is not marked 00 in VVtab.
  
  NOTE: make sure the extra bits at the end of the last MOT, which
  do not correspond to any variables, are set to 0 (in at least one
  of the 2 vectors). Pools built by STD are OK.
*/
bool hasANonNegVar(MOT* pool, MOT *VVtab, int n)
{
  int indexmot ;
  for (indexmot = nbmotparpool(n) - 1 ; indexmot >= 0 ; indexmot--)	
    {
      if ( ((*pool) & (*VVtab)) != 0)
	return (TRUE) ;
      pool++ ;
      VVtab++ ;
    }
  return (FALSE);
}



/*!
  This function updates the VVtab to VVtab | pool (bitwise).
*/
void naivePosUpdate(MOT* VVtab, MOT* pool, int n)
{
  int indexmot;
  for (indexmot = nbmotparpool(n)-1; indexmot >= 0 ; indexmot--)
    {
      *VVtab = (*VVtab) | (*pool) ;
      VVtab++ ;
      pool++ ;      	
    }
}



/*!
  Generate a set of simulated values for the n Boolean variables {0,..,n-1}.
  nbPosVars is the number of positive variables (there used to be avposvars
  and varposvars but this has been removed 25/06/04).<br>
  contraint: nbPosVars must be >=0 (this is checked for).<br>
  This function returns a vector of ints of size nbPosVars+1,
  in a memory area allocated in the function itself.<br>
  The vector holds: nbPosVars at index 0, followed by the SORTED positive 
  variables starting at index 1.
*/
int* simulateVars(int n, int nbPosVars)
{
  // sanity checks
  if (nbPosVars < 0)
    {
      fprintf(stderr, 
	      "in simulateVars, nbPosVars must be positive (current value: %d)\n", nbPosVars) ;
      exit(1);
    }

  // commenting out this output: all output should happen in higher-level functions
  // printf("nb of posvars=%d, ",nbPosVars);
  
  //------------------------------------------------------------------
  // randomly choose nbPosVars variables in {0,..,n-1}
  //-------------------------------------------------------------------

  // allocate memory for the vector of positive variables
  int* posvars;

  // size of the posvars vector: nbPosVars+1 because posvars[0]==nbPosVars
  int sizeposvars = nbPosVars + 1 ;

  // allocate memory for posvars
  posvars = (int*)malloc(sizeposvars * sizeof(int));
  if (posvars==NULL)
    {
      fprintf(stderr,"in simulateVars, no more memory for malloc\n");
      exit(1);
    }
  /* initialize memory with 0 */
  memset(posvars, 0, sizeposvars*sizeof(int)) ;

  // store nbPosVars at index 0
  posvars[0]=nbPosVars;

  int nbchosen = 0; // number of already chosen variables

  // randomly choose nbPosVars in {0,..,n-1}
  while(nbchosen < nbPosVars)
    { 
      int positvar = myrandom(n);
      
      // see if positvar has already been selected
      int chosenbefore=0; // has this var been chosen before? (1 if yes, 0 if no)
      int posvarsindex;
      for (posvarsindex=1; posvarsindex < nbchosen+1; posvarsindex++)
	{
	  if (positvar==posvars[posvarsindex])
	    {
	      // positvar was previously chosen, pick another variable
	      chosenbefore=1;
	      break;
	    }
	}

      if (chosenbefore==0)
	{
	  // ok, this variable has not been chosen before, add it to posvars
	  posvars[nbchosen+1] = positvar;
	  nbchosen++;
	}
    }
  // now sort the vector:
  // place -1 at index 0 to make sure it remains there
  posvars[0] = -1 ;
  qsort((void*)posvars, nbPosVars+1, sizeof(int), compInts) ;
  // now set nbPosVars instead of the bogus -1
  if (posvars[0] == -1)
    posvars[0] = nbPosVars ;
  else
    { // sanity check, -1 should have remained the first element
      fprintf(stderr, "in simulateVars, after qsort something is bloody wrong!\n") ;
      exit(1) ;
    }
  // and return it
  return posvars;
}


