/*----------------------------------------------------------------*
 *
 * File : unitClosures.h
 * Author : NTM
 * Created : 12/01/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
 *
 *-----------------------------------------------------------------*/

#ifndef _unitClosures_h_
#define _unitClosures_h_

#include "types.h" /* MOT */
#include "closure.h" /* closure */

/*!
  \file unitClosures.h
  \brief This file holds the unitClosures type definition and methods.
  This is part of the reimplementation of Gilles stuff.
*/


/******************************************************************
 ****** unitClosures type and low-level primitives
 ******************************************************************/

/*!
  \brief Datatype to store unit closures

  Type to represent a set of unit closures.<br>
  A unit closure can hold at most one 1 per layer (with STD, but
  also with any other transversal design).<br>
  This type is very different from setOfClosures: the data is
  stored in a few large chunks of memory; obtaining a regular
  closure from this is not immediate, but on the other
  hand this should greatly accelerate operations applied to every
  unit closure in a set, such as substracting a closure from
  all unit closures, or copying the set of unitClosures...

  structure of negPools (and posPools) is:
  - table holds nbOfClosures successive blocks (one block for each conflicting var);
  - each block has the same structure as a negPools and posPools vector
  from the closure type (see closure.h).
*/
typedef struct
{
  int nbOfClosures; /*!< number of unit closures in the set */
  int nbValid; /*!< number of valid unit closures */
  MOT* negPools; /*!< large table to store the neg conflicting Pools of each var */
  MOT* faintPools; /*!< large table to store the faint conflicting Pools of each var */
  int* negPoolCosts; /*!< vector (of nbOfClosures ints) holding the cost of neg and 
		       faint conflicting pools that contain each conflicting var */
  MOT* weakPools; /*!< large table to store the weak conf Pools of each var */
  MOT* posPools; /*!< large table to store the pos conf Pools of each var */
  int* scores; /*!< vector of nbOfClosures ints holding the "score" of each variable
		 (this is a lower bound on the real score of the negPools, since some 
		 posPools could become non-conflicting because of another var) */
  bool* valid; /*!< nbOfClosures bools; valid[i] is FALSE if unit closure i should be ignored */
} unitClosures;


/*!
  \brief free all memory from myClosuresP
*/
void freeUnitClosures(unitClosures* myClosuresP) ;

/*!
  \brief return a copy of myClosuresP
*/
unitClosures* copyUnitClosures(unitClosures* myClosuresP, int nbPools) ;

/*!
  \brief return a copy of myUnitsP->valid. mem is allocated here.
*/
bool* copyValidVector(unitClosures* myUnitsP) ;


/*!
  \brief Perform expensive checks on myUnitsP:
  - Compare nbValid with the number of TRUE's in valid;
  - Count the number of non-zero bits in each unit's negPools
  and faintPools, and multiply by corresponding DIST_xxx: 
  this should be equal to the unit's negPoolCosts.
  Die with error message if a discrepancy is found.
  This is for sanity-checking.
  NOTE: this function relies on the fact that xxxPools are
  padded with 0's
*/
void checkUnits(unitClosures* myUnitsP, int nbPools) ;


/*!
  \brief Given an enriched observation sig, build all the unit closures
  (ie the closures of each single conflicting variable), sort them 
  in an a priori favorable order (as specified in sortClosuresForSearch), 
  and return them in a (ptr to a) unitClosures.
  pre-condition: there must be at least one conflicting var in sig.
*/
unitClosures* buildUnitClosures(MOT* tabpool, signature* sig, int n) ;


/*!
  \brief Copy sourceClosureP's negPools, negPoolsCost and score into 
  destClosureP,squashing previous content.
  Then update these 3 fields from destClosureP by doing the union with
  the negPools and faintPools for unit vector unitNum.
  NOTE: after the call, destClosureP is no longer coherent: it's posPools
  contains garbage, and destClosureP->score is in reality:
  <cost of sourceClosureP->posPools> - destClosureP->negPoolsCost.
  You must either discard *destClosureP, or call finishUnionWithUnit using
  the same params.
  This is somewhat ugly, but it allows to examine destClosureP->negPoolsCost
  for potential pruning before copying and doing the union with the unit's
  posPools and weakPools...
*/
void beginUnionWithUnit(closure* destClosureP, closure* sourceClosureP, 
			unitClosures* myUnitsP, int unitNum, int nbPools) ;


/*!
  \brief Finish filling destClosureP with the union of sourceClosureP 
  with unit closureunitNum: copy sourceClosureP's posPools into 
  destClosureP, do the union with the unit closure's posPools and
  weakPools, and update score accordingly.
  This function should only be called after beginUnionWithUnit, 
  on the same args.
*/
void finishUnionWithUnit(closure* destClosureP, closure* sourceClosureP, 
			 unitClosures* myUnitsP, int unitNum, int nbPools) ;


/*!
  Return a unitClosures, where every unit marked invalid in myUnitsP
  is TRASHED (it doesn't exist in the returned unitClosures); and where:
  - nbOfCLosures and nbValid are set correctly ;
  - negPools and faintPools are the result of substracting 
    currentClosureP->negPools from each valid unit closure's 
    negPools and faintPools in myUnits;
  - negPoolCosts and scores are copies of myUnits, but updated 
    to reflect the currentClosureP->negPools substractions;
  - posPools and weakPools are simply copied from myUnitsP;
  - valid is initially all TRUE (since any invalid units in 
    myUnits are trashed), but is then updated as follows:
    - If any unit's negPoolCosts is (still) > maxNegPoolCost, 
      invalidate it;
    - Else if any unit's negPools+faintPools becomes empty, 
      update currentClosureP->posPools and currentClosureP->score 
      by doing the union with this unit's posPools and weakPools, 
      then invalidate the unit.
  In fact, the 2 invalidations just described are implemented 
  so that the invalidated units get overwritten: they are trashed 
  and don't exist in the returned unitClosures, just like the units 
  which were already invalid in myUnitsP.
  Therefore, all units in the returned unitClosures are VALID!

  NOTE: this function can modify currentClosureP (by adding some 
  pos pools and updating the score).
*/
unitClosures* substractNegPoolsFromUnits(closure* currentClosureP, unitClosures* myUnitsP, 
					 int maxNegPoolCost, int nbPools) ;

/*!
  \brief Return a unitClosures, where every unit marked invalid in myUnitsP
  is TRASHED (it doesn't exist in the returned unitClosures).
  This function does exactly the same as substractNegPoolsFromUnits, 
  but in addition it performs inclusion-invalidation:<br>
  if any valid unit in myUnitsP contains the negPools+faintPools for 
  unit unitNum in myUnitsP, mark it as invalid in myUnitsP.<br>
  If you use this function, myUnitsP MUST BE substracted! (whereas with
  substractNegPoolsFromUnits, it doesn't matter).
  NOTE: this function modifies both currentClosureP (adds some posPools) and
  myUnitsP (invalidates some units, updates nbValid accordingly).
*/
unitClosures* substractNegPoolsFromUnitsInclInval(closure* currentClosureP, unitClosures* myUnitsP, 
						  int unitNum,
						  int maxNegPoolCost, int nbPools) ;


/*!
  \brief Substract currentClosureP->posPools from each valid unit's posPools.
  If any unit's posPools becomes empty, invalidate it.
  This function should be called after substractNegPoolsFromUnits, on the
  unitClosures produced by it.
  If myUnitsP->nbOfClosures==0, it's OK, nothing happens.
*/
void substractPosPoolsFromUnits(closure* currentClosureP, unitClosures* myUnitsP, int nbPools) ;


#endif
