// FILE. . . . . /home/hak/hlt/src/hlt/osf/exec/Taxonomy.java
// EDIT BY . . . Hassan Ait-Kaci
// ON MACHINE. . Hp-Dv7
// STARTED ON. . Mon Nov 05 18:05:54 2012

/**
 * @version     Last modified on Fri Aug 30 11:59:48 2013 by hak
 * @author      <a href="mailto:hak@acm.org">Hassan A&iuml;t-Kaci</a>
 * @copyright   &copy; <a href="http://www.hassan-ait-kaci.net/">by the author</a>
 */

package hlt.osf.exec;

import java.util.HashSet;
import java.util.Iterator;

import java.io.PrintStream;
import java.io.IOException;
import java.io.FileNotFoundException;

import hlt.osf.io.TaxonomyLoader;
import hlt.osf.io.BadTokenException;

import hlt.osf.base.Sort;
import hlt.osf.io.DisplayManager;
import hlt.osf.util.BitCode;
import hlt.osf.util.Decoded;
import hlt.osf.util.LockedBitCodeException;

import hlt.language.tools.Misc;
import hlt.language.tools.Debug;
import hlt.language.util.ArrayList;
import hlt.language.util.IntArrayList;
import hlt.language.util.IntIterator;

/**
 * This is a class extending ArrayList for storing Sort objects.
 */
public class Taxonomy extends ArrayList implements Contextable
  {
    /* ************************************************************************ */

    /**
     * Construct a taxonomy.
     */
    public Taxonomy ()
    {
      super();
    }

    /**
     * Construct a taxonomy of the specified initial capaciity.
     */
    public Taxonomy (int initialCapacity)
    {
      super(initialCapacity);
    }

    /**
     * Construct a taxonomy with the specified Context.
     */
    public Taxonomy (Context context)
    {
      this();
      _context = context;
    }

    /**
     * Construct a taxonomy of the specified initial capaciity and the specified Context.
     */
    public Taxonomy (int initialCapacity, Context context)
    {
      this(initialCapacity);
      _context = context;
    }

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

    /**
     * This taxonomy's operational context.
     */
    private Context _context;

    /**
     * Returns this taxonomy's operational context.
     */    
    public Context context ()
    {
      return _context;
    }

    /**
     * Set this taxonomy's operational context to the specified one.
     */    
    public Taxonomy setContext (Context context)
    {
      _context = context;
      return this;
    }

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

    /**
     * This returns the sort with specified index in this taxonomy.
     */
    public Sort getSort (int index)
    {
      return (Sort)get(index);
    }

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

    /**
     * This is false as long as the current sort taxonomy has not been
     * encoded; true otherwise.
     */
    private static boolean _isLocked = false;

    /**
     * Returns true iff the current sort taxonomy has been been encoded.
     */
    public static boolean isLocked ()
    {
      return _isLocked;
    }

    /**
     * Locks this taxonomy. This is <i>private</i> because it should not be
     * accessible from outside this <tt>Taxonomy</tt>.
     */
    private void _lock ()
    {
      _isLocked = true;
    }

    /**
     * Unlocks this taxonomy.  This is <i>public</i> because it may be
     * accessible from outside this <tt>Taxonomy</tt>.
     */
    public void unlock ()
    {
      _isLocked = false;
    }

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

    /**
     * Encodes all the sorts of this taxonomy and initializes it.
     */
    public void encodeSorts () throws AnomalousSituationException
    {
      // encode all the defined sorts in this sort code array:
      encodeSorts(0,size()-1);
      _initialize();
    }

    /**
     * Locks this taxonomy, initializes the top sort to have the correct
     * number of bits set, sets the top and bottom sorts to have the
     * right context and registers them in the named sort array and the
     * code cache.
     */
    private void _initialize () throws AnomalousSituationException
    {
      // sets the sort code size to be the size of this code array + 1
      // to account for top (added further down in this method):
      Sort.setCodeSize(size()+1);

      // lock this code array:
      _lock();

      // add the top sort at the highest index in this sort code array
      // and set its bit code to be all ones for the relevant bit code
      // width:
      add(Sort.top());
      Sort.top().setIndex(size()-1).code.set(0,size());

      // initialize the context of the bottom and top sorts:
      Sort.bottom().setContext(_context);
      Sort.top().setContext(_context);

      // register top and bottom in the named sort array and the code cache:
      _context.namedSorts().put(Sort.top().name,Sort.top());
      _context.codeCache().put(Sort.top().code,Decoded.top());
      _context.namedSorts().put(Sort.bottom().name,Sort.bottom());
      _context.codeCache().put(Sort.bottom().code,Decoded.bottom());
    }

    /**
     * Encodes the sorts between index first and index last (both inclusive)
     * of this sort code array and check for cycles, committing all defined
     * sorts in the specified range.
     *
     * <p>
     *
     * It encodes the taxonomy performing transitive closure using bottom-up
     * encoding, which is much more efficient than the general complete O(n^3)
     * method: it is simply O(n) as it sweeps the sort array just once
     * encoding each sort as the boolean 'or' of its immediate subsorts
     * (children) in a layer starting from bottom. A layer is the union of all
     * the parents of the current layer minus this sorts that do not have all
     * their children encoded (which means that they can be reached later).
     *
     * <p>
     *
     * However, this method is garanteed to compute the transitive closure
     * only for acyclic posets. Indeed, computing a layer may not be done
     * correctly if there are loops in the taxonomy. This means that after
     * proceeding with a bottom-up encoding, if there are sorts that are still
     * unlocked, then this implies that there are cycles.
     *
     * <p>
     *
     * While this may be detected (by a simple check that all codes are
     * locked), it is non trivial to identify and enumerate all the
     * cycles. But cycle identification is much easier if encoding was done
     * with the general transitive closure method in O(n^3).
     *
     * <p>
     *
     * In order to do so, we can restrict the taxonomy only to unlocked codes
     * and re-encode them using the O(n^3) method. This is viable since in
     * general the number of still unlocked codes is usually a relatively
     * small subset of the whole taxonomy.
     */
    public void encodeSorts (int first, int last)
      throws AnomalousSituationException, LockedCodeArrayException, CyclicSortOrderingException
    {
      if (first > last)
	throw new AnomalousSituationException("No sorts have been defined to encode");

      if (_isLocked)
	throw new LockedCodeArrayException("Unable to encode an already encoded sort taxonomy");

      // perform the encoding by transitive closure:
      System.out.println("*** Performing transitive closure...");
      long time = System.currentTimeMillis();
      // _transitiveClosure(first,last);	// this is too expensive - O(n^3)
      _bottomUpClosure();			// this is linear - but see comment below
      time = System.currentTimeMillis() - time;
      System.out.println("*** Transitive closure processing time = "+time+" ms");

      // Verify that all sorts have be encoded correctly:
      System.out.println("*** Performing consistency check of the taxonomy...");
      time = System.currentTimeMillis();
      _checkCodes(first,last);
      time = System.currentTimeMillis() - time;
      System.out.println("*** Code consistency check processing time = "+time+" ms");

      // Commit all defined sorts:
      System.out.println("*** Committing all sorts...");
      time = System.currentTimeMillis();
      _commitAllSorts(first,last);
      time = System.currentTimeMillis() - time;
      System.out.println("*** Sort commitment processing time = "+time+" ms");
    }

    /* ************************************************************************ */
    
    /**
     * This verifies that there are no remaining sorts with unlocked
     * codes.  If this is the case, this means that the taxonomy
     * contains cycles.  In that case, this taxonomy is replaced with
     * the unlocked sorts and re-encoded using the complete O(n^3)
     * transitive closure procedure, re-ordered and swept for cycles.
     * These cycles are reported by throwing
     * <tt>CyclicSortOrderingException</tt> on the identified cycles.
     */
    void _checkCodes (int first, int last) throws CyclicSortOrderingException
    {
      ArrayList badSorts = new ArrayList();
      
      for (int i= first; i<=last; i++)
    	{
    	  Sort sort = getSort(i);
    	  if (!sort.isLocked())
    	    badSorts.add(sort);
    	}

      if (badSorts.isEmpty())
    	return;

      // There are sorts that are still unlocked repertoried in badSorts.

      // DisplayManager dm = _context.displayManager();
      // dm.println("*** "+(badSorts.size()-1)+
      // 		 " sorts have not been properly encoded (cyclic taxonomy): "+
      // 		 badSorts);

      reset();	// clear the taxonomy
      // replace the taxonomy with the "bad" sorts:
      int size = badSorts.size()-1;
      for (int index = 0; index<=size; index++)
    	{
    	  Sort sort = (Sort)badSorts.get(index);
    	  sort.index = index;	// reset the index to the new one in taxonomy
    	  sort.code.clear();	// erases all the bits in the sort's code
    	  sort.code.set(index);	// sets the bit for this sort's index
    	  add(sort);		// add the sort to the "bad sort" taxonomy
    	}
      Sort.setCodeSize(size());

      // Reinitialize the codes' bits from the "is-a" declarations; this
      // is done for a bad sort using only its unlocked parents. This
      // must be done after the loop refilling the taxonomy since we
      // need all the indices for the bad sorts to be all reset first
      // (which is done in the previous loop):
      for (int index = 0; index<=size; index++)
    	{
    	  Sort sort = getSort(index);
    	  for (Iterator it=sort.parents().iterator(); it.hasNext();)
    	    {
    	      Sort parent = (Sort)it.next();
    	      if (!parent.isLocked())
		{
		  // System.out.println(">>> "+sort+" <| "+parent);
		  parent.code.set(sort.index);
		}
    	    }
    	}

      // perform "complete" Warshall transitive closure:
      _transitiveClosure(0,size);
      // reorder the "bad sort" taxonomy:
      _reorder(0,size);
      // perform cycle identification and throw a cyclic-ordering exception
      throw new CyclicSortOrderingException(_identifyCycles(0,size));
    }


    /**
     * This is called when we know that the taxonomy contains cycles
     * (and is therefore inconsistent). It will identify the cycles in
     * the reordered subset of inconsistent sorts closed with the
     * complete transitive closure, all this having been done in the
     * method above (<tt>_checkCodes</tt>).
     */
    private ArrayList _identifyCycles (int first, int last)
    {
      _cycles.clear();
      ArrayList cycle = null;

      Sort sort = null;
      Sort prev = null;

      for (int i=first; i<=last; i++)
	{
	  sort = getSort(i);

	  if (prev != null && sort.code.equals(prev.code))
	    { // this is a cycle
	      if (cycle == null)
		{ // this cycle is new; create a record for it
		  cycle = new ArrayList();
		  // and initialize it with the previous sort
		  cycle.add(prev.name);
		}
	      // record the current sort as part of the cycle
	      cycle.add(sort.name);
	    }
	  else
	    { // this sort is not part of a cycle; make it the previous sort
	      prev = sort;
	      if (cycle != null)
		{ // a complete cycle was detected: record it
		  _cycles.add(cycle);
		  // and reinitialize it for potential new cycles
		  cycle = null;
		}
	    }
	}

      // Sort.setCodeSize(size()+1);	// only for debugging purpose
      // showSortCodes(first,last);	// only for debugging purpose

      return _cycles;
    }

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

    /**
     * This contains the numbers sorts per layers for this
     * taxonomy. Therefore, its length is the height of the taxonomy.
     */
    IntArrayList layers = new IntArrayList();

    /**
     * This performs a transitive closure by assigning codes starting
     * from bottom and proceeding upwards layer after layer until we
     * reach top.
     */
    private void _bottomUpClosure ()
    {
      HashSet layer = (HashSet)Sort.bottom().parents().clone();
      int height = 0;

      do
	{
	  // System.out.println(">>> Encoding layer: "+layer);

	  layers.add(layer.size());	// record the size of this layer
	  if (Context.isTracing())
	    System.out.println("*** Layer "+layers.size()+" has "+layer.size()+" sorts");

	  _encodeLayer(layer);		// encode the layer
	  layer = _nextLayer(layer);	// computes the next layer
	}
      while (!layer.isEmpty());
    }

    /**
     * This encodes all the sorts in the specified layer as the 'or' of
     * its children, then locks it as encoded.
     */
    private void _encodeLayer (HashSet layer)
    {
      for (Iterator it=layer.iterator(); it.hasNext();)
	{
	  Sort sort = (Sort)it.next();
	  for (Iterator i=sort.children().iterator(); i.hasNext();)
	    sort.code.or(((Sort)i.next()).code);
	  sort.lock();
	}	  
    }

    /**
     * The next layer is computed from the specified one as the union of
     * all the parents of its elements from which are removed those
     * elements that do not have all their children already encoded
     * (i.e., which still have at least one unlocked child).
     */
    private HashSet _nextLayer (HashSet layer)
    {
      HashSet nextLayer = new HashSet();

      for (Iterator it=layer.iterator(); it.hasNext();)
	{
	  HashSet parents = ((Sort)it.next()).parents();
	  
	  for (Iterator i=parents.iterator(); i.hasNext();)
	    {
	      Sort parent = (Sort)i.next();
	      boolean skipParent = false;
	      
	      for (Iterator j=parent.children().iterator(); j.hasNext();)
		{
		  Sort child = (Sort)j.next();
		  if (!child.isLocked())
		    {
		      skipParent = true;
		      break;
		    }
		}

	      if (!skipParent)
		nextLayer.add(parent);
	    }
	}

      return nextLayer;      
    }

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

    /**
     * This performs a Warshall transitive closure on the codes of the
     * sorts stored in this taxonomy using the <it>O</it>(n<sup>3</sup>)
     * <a
     * href="http://www.jn.inf.ethz.ch/education/script/P3_C11.pdf">Warshall's
     * algorithm</a>. This assumes that all the elements's codes have
     * been set to their initial values as explained in the <a
     * href="../specs/basic.html#warshall">specification</a>.
     */
    private void _transitiveClosure ()
    {
      _transitiveClosure(0,size()-1);
    }

    /**
     * This performs in-place transitive closure on the codes of the
     * sorts stored in this taxonomy of all the elements between
     * index first and index last (both inclusive).
     */
    private void _transitiveClosure (int first, int last)
    {
      for (int k=first; k<=last; k++)
	for (int i=first; i<=last; i++)
	  for (int j=first; j<=last; j++)
	    {
	      Sort sort_i = getSort(i);
	      if (!sort_i.code.get(j))
		sort_i.code.set(j,sort_i.code.get(k) && (getSort(k)).code.get(j));
	    }
    }

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

    /**
     * This reorders in-place this taxonomy using the "precedes"
     * comparison on Sort objects with (non-recursive) <a
     * href="http://en.wikipedia.org/wiki/Quicksort">QuickSort</a>. This
     * assumes that all the elements' codes have their final values
     * after transitive closure.
     */
    private void _reorder ()
    {
      Misc.sort(this);
    }

    /**
     * This reorders in-place the elements of this taxonomy between
     * index first and index last (both inclusive) using the "precedes"
     * comparison on Sort objects with (non-recursive) <a
     * href="http://en.wikipedia.org/wiki/Quicksort">QuickSort</a>. This
     * assumes that all the elements' codes have their final values
     * after transitive closure.
     */
    private void _reorder (int first, int last)
    {
      Misc.sort(this,first,last);
    }

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

    /**
     * Once the taxonomy reordering has been done, we need to register
     * each sort's name and code in the named sort table and its code in
     * the code cache.
     */
    private void _commitAllSorts (int first, int last)
    {
      for (int i=first; i<=last; i++)
	_commitSort(i);
    }

    /**
     * This returns the sort at the specified index in this taxonomy
     * after registering its name and code in the named sort table and
     * its code in the code cache. This method is used in the
     * <tt>_checkForCycles</tt> method as it visits each taxonomy
     * element exactly once - unless a cycle is detected.  In the latter
     * case, a <tt>CyclicSortOrderingException</tt> is thrown that
     * invalidates the operational context, which should then be reset
     * upon catching this exception.
     */
    private Sort _commitSort (int index)
    {
      Sort sort = getSort(index);

      _context.namedSorts().put(sort.name,sort);
      _context.codeCache().put(sort.code,new Decoded(sort));

      return sort; // locking already done if using _bottomUpClosure()
      // return sort.lock(); // locking needed only if NOT using _bottomUpClosure()
    }
    
    /* ************************************************************************ */

    /**
     * This is used to record and report potential cycles that may be
     * detected in the current taxonomy.
     */
    private ArrayList _cycles = new ArrayList();
    
    /* ************************************************************************ */

    public void reset ()
    {
      reset(0);
    }

    public void reset (int minIndex)
    {
      clear(minIndex);
      // The following two hashset clearings are not fully correct in
      // case there are built-in sorts (all of index less than MinIndex)
      // that need to be kept as children of top and parents of
      // bottom. But since there are no built-ins in this version,
      // that'll do for now ...
      Sort.top().children().clear();
      Sort.bottom().parents().clear();
    }

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

    /**
     * This computes the set of maximum lower bounds of a given bit code
     * as a bit code when the given code was obtained without negation.
     * In that case, every "<tt>1</tt>" in the given bit code is at a
     * position corresponding to the index of a lower bound of its
     * sort. So, it is sufficient to loop through the <tt>1</tt>'s of
     * the given bit code and set the corresponding position in the
     * bitset "<tt>mlbs</tt>" to "<tt>1</tt>" if it is maximal.
     */
    public BitCode noNegMaxLowerBounds (BitCode code) throws LockedCodeArrayException
    {
      if (!_isLocked)
    	throw new LockedCodeArrayException("Attempt to perform an operation requiring prior sort encoding");

      BitCode mlbs = new BitCode();

      Sort s = null;
      Sort t = null;

      for (IntIterator i = code.iterator(); i.hasNext();)
    	{
    	  s = getSort(i.next());

    	  // Skip top because it is not a lower bound:
    	  if (s.isTop())
    	    continue;

    	  // We know by definition that s is a lower bound; but we need
    	  // only the maximal ones. So, unless s has no supersort
    	  // already in mlbs, we must remove any subsort of s from mlbs
    	  // before adding s.

    	  Boolean isMax = true;

    	  for (IntIterator it = mlbs.iterator(); it.hasNext();)
    	    {
    	      t = getSort(it.next());
	      
    	      if (s.code.isStrictlyContainedIn(t.code))
    		{ // t is a supersort of s; so s is not maximal: no need
		  // to proceed further:
    		  isMax = false;
    		  break;
    		}

    	      if (t.code.isStrictlyContainedIn(s.code))
    		// t is a subsort of s - remove it:
    		mlbs.set(t.index,false);
    	    }

    	  if (isMax)
    	    mlbs.set(s.index);
    	}

      return mlbs.lock();
    }


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

    /**
     * <h5>Decoding negated codes</h5>
     *
     * The issue of decoding is critical: it must be as efficient as
     * possible since it is used interactively. While such is possible
     * for a code that has been computed without involving negation (see
     * the <tt>noNegMaxLowerBounds</tt> method above), it is less
     * evident when negation is involved. The reason is that the
     * semantics of a sort's code interprets the presence of a
     * <tt>1</tt> in position <i>i</i> to mean that the sort of index
     * <i>i</i> is a subsort of this code, while a <tt>0</tt> means that
     * it is <i>not a subsort</i>; that is, it must be either a
     * supersort or incomparable. Hence, taking the negation of a binary
     * code is not symmetric. Indeed, negating a code will yield a
     * <tt>1</tt> where there was a <tt>0</tt>.  Therefore, <font
     * color="red">a <tt>1</tt> in position <i>i</i> in the code of a
     * negated sort <tt>!s</tt> means that the corresponding sort
     * <i>i</i> is either a subsort of, or incomparable with,
     * <tt>!s</tt></font>. This invalidates decoding such as the one
     * performed by the <tt>noNegMaxLowerBounds</tt> method above which
     * keeps the maximal subsorts corresponding to position containing a
     * <tt>1</tt> in the code and thus can only be used for codes
     * obtained just using conjunction and disjunction, but no negation.
     *
     * <p>
     *
     * In the case where the code to be decoded was obtained using at
     * least one negation, one alternative is to sweep the whole
     * taxonomy and keep only maximal subsorts of each sorts. However,
     * this is not viable as it can reach quadratic complexity in the
     * size of the taxonomy.
     *
     * <p>
     *
     * Another possibility is to get back to the technique used in the
     * <tt>noNegMaxLowerBounds</tt> method, which involves only a loop
     * through the <tt>1</tt> positions of a code. For this to be
     * correct, it must be ensured that the codes respect the semantics
     * whereby a <tt>1</tt> strictly indicates only a subsort.
     *
     * <p>
     *
     * In order to do that, let us consider the case of negating a sort
     * expression <tt>s</tt>. If we compute the code of <tt>!s</tt> by
     * switching all <tt>1</tt>s to <tt>0</tt>s and vice versa in the
     * code of <tt>s</tt>, this will not work (as explained above).
     * However, if we change a <tt>1</tt> in position <i>i</i> to a
     * <tt>0</tt> in the code of <tt>!s</tt> to a <tt>0</tt> whenever
     * the sort of index <i>i</i> is a supersort of a sort corresponding
     * to a <tt>0</tt> in the code of <tt>!s</tt>, then we will be left
     * with a code having a <tt>1</tt> only in positions of actual
     * subsorts of <tt>!s</tt>. With such a code, the more efficient
     * <tt>noNegMaxLowerBounds</tt> method can then compute the correct
     * set of maximal lower bounds of <tt>!s</tt>.
     *
     * <p>
     *
     * Note that when no negation has been used, the above method
     * coincides with the <tt>noNegMaxLowerBounds</tt> method. Indeed,
     * in that case, there must be a <tt>1</tt> in all positions
     * corresponding to subsorts (by construction, since such a code
     * denotes the set of its subsorts). Hence, whenever there is a
     * <tt>0</tt> in such a code, there is necessarily also a <tt>0</tt>
     * in all the positions of its supersorts.
     *
     * <p>
     *
     * The method <tt>maxLowerBounds(BitCode code)</tt> below implements the
     * above scheme. <b><font color="red">This is now rendered obsolete by the
     * <tt>Decode(BitCode)</tt> method below.</font></b>
     */
    public BitCode maxLowerBounds (BitCode code) throws LockedCodeArrayException
    {
      if (!_isLocked)
    	throw new LockedCodeArrayException("Attempt to perform an operation requiring prior sort encoding");

      // we start by gathering the "undesirable" sorts; i.e., the
      // ancestors of all the sorts corresponding to a 0 in the
      // specified code bitcode - we iterate through the 0's in the
      // code (or equivalently through the 1's in the negated code):

      HashSet undesirableSet = new HashSet(code.size());

      // System.out.println("\t>>> code = "+code);

      System.out.print("\t>>> computing undesirables... ");

      for (IntIterator it = BitCode.not(code).iterator(); it.hasNext();)
	{
	  HashSet ancestors = getSort(it.next()).ancestors();
	  if (ancestors != null)
	    undesirableSet.addAll(ancestors);
	  // NB: note that we collect only strict ancestors - this will
	  // have for effect not to include the sort itself in the end
	  // if it is minimal.
	}

      System.out.println(undesirableSet.size()+" found.");

      // System.out.println("\n>>> undesirables = "+undesirableSet);

      // Define an initial set of lower bounds as a copy of code:
      BitCode mlbs = code.copy();

      System.out.println("\t>>> removing the undesirables... ");

      // Remove the undesirables from mlbs:
      for (Iterator it = undesirableSet.iterator(); it.hasNext();)
	{
	  Sort s = (Sort)it.next();
	  mlbs.clear(s.index);
	}

      System.out.println("\t>>> computing maximal lower bounds...");

      // Next, we iterate through the 1's left in mlbs and remove all
      // their descendants, leaving only its maximal lower bounds:

      for (IntIterator it = mlbs.iterator(); it.hasNext();)
	{
	  int subsortIndex = it.next();
	  mlbs.andNot(getSort(subsortIndex).code);
	  mlbs.set(subsortIndex);
	}

      return mlbs.lock();
    }

    /**
     * This returns a bit code representing the set of sorts whose codes are
     * the minimal upper bounds of the specified bit code. Note that the
     * returned bit code may be empty (if the code is the top sort's code). It
     * iterates through the <tt>0</tt>s of the code in order to identify its
     * supersorts, keeping only the minimals. <b><font color="red">This is now
     * rendered obsolete by the <tt>Decode(BitCode)</tt> method
     * below.</font></b>
     */
    public BitCode minUpperBounds (BitCode code) throws LockedCodeArrayException, LockedBitCodeException
    {
      if (!_isLocked)
    	throw new LockedCodeArrayException("Attempt to perform an operation requiring prior sort encoding");

      BitCode mubs = new BitCode();

      // iterate through the 0-bits of code:
      for (IntIterator it = BitCode.not(code).iterator(); it.hasNext();)
	{
	  int index = it.next();

    	  Sort s = getSort(index);

	  if (!code.isStrictlyContainedIn(s.code))
	    // s is not a supersort - skip it:
	    continue;

	  // s is an uppper bound; however, mubs may contain supersorts
	  // of s; if so, we must remove them before adding this lower
	  // upper bound:

	  boolean isMinimal = true;

	  // proceed with the minimality check:
	  for (IntIterator i = mubs.iterator(); i.hasNext();)
	    {
	      Sort t = getSort(i.next());

	      if (t.code.isStrictlyContainedIn(s.code))
		{ // s is a not a minimal supersort - break out of
		  // the minimality check loop:		      
		  isMinimal = false;
		  break;
		}

	      if (s.code.isStrictlyContainedIn(t.code))
		{
		  System.out.println("\tremoving "+t);
		  mubs.remove(t.index);
		}
	    }

	  if (isMinimal)
	    {
	      System.out.println("\tadding "+s);
	      mubs.add(index);
	    }
    	}

      return mubs.lock();
    }

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

    /**
     * Notice that the two methods <tt>maxLowerBounds(BitCode)</tt> and
     * <tt>minUpperBounds(BitCode)</tt> given above both loop through the
     * <tt>0</tt>s of their <tt>BitCode</tt> argument. Since they are both
     * systematically used for decoding a given code, it is a waste to go
     * through such a loop twice, especially for a code containing a large
     * number of <tt>0</tt>s. So, rather than using the <tt>Decoded</tt>
     * constructor calling each method separately, it makes more sense to
     * merge the two methods into a single one, building both mlbs and mubs
     * simultaneously.  This is what the method <tt>decode(BitCode)</tt> does,
     * returning a <tt>Decoded</tt> object with both sets at once.
     */
    public Decoded decode (BitCode code)
    {
      if (!_isLocked)
    	throw new LockedCodeArrayException("Attempt to perform an operation requiring prior sort encoding");

      // define an initial set of upper bounds as an empty bit code:
      BitCode mubs = new BitCode();
      // Define an initial set of lower bounds as a copy of code:
      BitCode mlbs = code.copy();

      // in order to compute the mlbs, we'll need to gather the "undesirable"
      // sorts - i.e., the ancestors of all the sorts corresponding to a 0 in
      // the specified code bitcode; we define an initial hash set for them:
      HashSet undesirableSet = new HashSet(code.size());

      // next, we iterate through the 0-bits of code (or equivalently through
      // the 1's in the negated code):
      for (IntIterator it = BitCode.not(code).iterator(); it.hasNext();)
	{
	  int index = it.next();

	  // we first take care of computing the undesirables for the mlbs in
	  // the case negation was used (NB: note that we collect only strict
	  // ancestors - this will have for effect not to include the sort
	  // itself in the end if it is minimal):
	  if (Context.negativeQuery)
	    {
	      HashSet ancestors = getSort(index).ancestors();

	      if (ancestors != null)
		undesirableSet.addAll(ancestors);
	    }

	  // we then take care of computing the mubs:
    	  Sort s = getSort(index);

	  if (!code.isStrictlyContainedIn(s.code))
	    // s is not a supersort - skip it:
	    continue;

	  // s is an uppper bound; however, mubs may contain supersorts
	  // of s; if so, we must remove them before adding this lower
	  // upper bound:

	  boolean isMinimal = true;

	  // proceed with the minimality check:
	  for (IntIterator i = mubs.iterator(); i.hasNext();)
	    {
	      Sort t = getSort(i.next());

	      if (t.code.isStrictlyContainedIn(s.code))
		{ // s is a not a minimal supersort - break out of
		  // the minimality check loop:		      
		  isMinimal = false;
		  break;
		}

	      if (s.code.isStrictlyContainedIn(t.code))
		mubs.remove(t.index);
	    }

	  if (isMinimal)
	    mubs.add(index);
	}

      // in case negation was used, we now compute the mlbs using the
      // undesirables we just computed, first removing the undesirables from
      // mlbs:
      if (Context.negativeQuery)
	for (Iterator it = undesirableSet.iterator(); it.hasNext();)
	  {
	    Sort s = (Sort)it.next();
	    mlbs.clear(s.index);
	  }

      // reset the negation detection:
      Context.negativeQuery = false;
      
      // next, we iterate through the 1s left in mlbs and remove all their
      // descendants, leaving only maximal lower bounds:

      for (IntIterator it = mlbs.iterator(); it.hasNext();)
	{
	  int subsortIndex = it.next();
	  mlbs.andNot(getSort(subsortIndex).code);
	  mlbs.set(subsortIndex);
	}

      // finally, we return the decoded object:
      return new Decoded(code,mubs.toHashSet(this),mlbs.toHashSet(this));
    }

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

    /**
     * Returns the height of the specified sort in its taxonomy. (See the
     * <a href="../specs/basic.html#height">specification</a>.)
     */
    public int computeHeight (Sort sort) throws LockedCodeArrayException
    {
      if (!isLocked())
	throw new LockedCodeArrayException("Can't compute sort heights in a non-encoded taxonomy");
      
      int height = 0;

      for (IntIterator it = sort.code.iterator(); it.hasNext();)
	{
	  int index = it.next();

	  if (index >= size())	// is this necessary???
	    break;

	  if (index == sort.index)
	    continue;

	  height = Math.max(height,computeHeight(getSort(index)));
	}

      return 1 + height;
    }

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

    /**
     * Returns the set of descendants of the specified sort as a HashSet.
     */
    public HashSet computeDescendants (Sort sort) throws LockedCodeArrayException
    {
      if (!isLocked())
    	throw new LockedCodeArrayException("Can't compute sort descendantss in a non-encoded taxonomy");

      HashSet lowerBounds = sort.code.toHashSet(this);

      lowerBounds.remove(sort);
      
      return lowerBounds;
    }
    
    /* ************************************************************************ */

    /**
     * Returns the set of ancestors of the specified sort as a HashSet.
     */
    public HashSet computeAncestors (Sort sort) throws LockedCodeArrayException
    {
      if (!isLocked())
	throw new LockedCodeArrayException("Can't compute sort ancestors in a non-encoded taxonomy");

      // If the sort is top, return null:
      if (sort.isTop())
	return null;

      // If the sort is bottom, return the descendants of top:
      if (sort.isBottom())
	return Sort.top().descendants();

      // otherwise, collect the parents and their ancestors:
      HashSet ancestors = (HashSet)sort.parents().clone();

      for (Iterator it=sort.parents().iterator(); it.hasNext();)
	{
	  HashSet newAncestors = ((Sort)it.next()).ancestors();
	  if (newAncestors == null)
	    continue;
	  ancestors.addAll(newAncestors);
	}

      //      System.out.println("\t==> "+ancestors);

      return ancestors;
    }
    
    /* ************************************************************************ */

    /**
     * This displays all the defined sorts in this taxonomy using
     * the specified display manager.
     */
    public void showSortCodes ()
    {
      showSortCodes(0,size()-2);
    }

    /**
     * This displays the elements of this taxonomy between index
     * first and index last (both inclusive) using the specified display
     * manager. It always displays @ at the top (with no index) and {}
     * at the bottom (with no index).
     */
    public void showSortCodes (int first, int last)
    {
      int width = Misc.numWidth(last);
      DisplayManager dm = _context.displayManager();

      dm.println(Misc.repeat(width,' ')+" "+
      		 Sort.top().code+" "+
      		 Sort.top().name);

      for (int index=last; index>=first; index--)
      	{
      	  Sort sort = getSort(index);
      	  dm.println(Misc.numberString(index,width)+" "+
      		     sort.code+" "+
      		     sort.name);
      	}

      dm.println(Misc.repeat(width,' ')+" "+
      		 Sort.bottom().code+" "+
      		 Sort.bottom().name);
   }


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

    /**
     * This saves the current encoded taxonomy into a file on disk. The
     * <tt>String</tt> argument is the name of the file. The format of
     * this file is made out of two parts. The first part is such that
     * the first line is the number of elements in the taxonomy
     * (<i>i.e.</i>, <tt>size()</tt>), and each following line contains
     * information for the sort <tt>TAXONOMY[i]</tt> for <tt>i</tt>
     * ranging from <tt>0</tt> to <tt>size()-1</tt>. Each sort on a line
     * is made of 2 pieces:
     *
     * <p>
     * <tt>name code</tt>
     * <p>
     *
     * The <tt>name</tt> is the symbolic name of the sort. The
     * <tt>code</tt> is the sort's <tt>BitCode</tt> code written as a
     * space-separated sequence of pairs of integers, each number
     * corresponding to the next true index followed by the next false
     * index, going from the lowest to the highest. For example, the
     * bitcode:
     *
     * <pre> 000011111001111000000110000 </pre>
     *
     * corresponds to the string:
     *
     * <pre> "4 6 12 16 18 23" </pre>
     *
     * The second part of the saved file consists of information to
     * reconstruct the "is-a" ordering by saving the parents of each sort,
     * from which "is-a" declarations can be processed at load time. This part
     * consists of as many lines as there are non-maximal sorts, each line
     * containing the index of a sort followed by the indices of the parents
     * of sorts in the order of their indices in the taxonomy. <b>NB:</b>
     * maximal sorts (<i>i.e.</i>, having top as a (necessarily single parent)
     * are skipped. This is because there is no need to declare a subsort of
     * top.
     */
    public void save (String file) throws FileNotFoundException
    {
      PrintStream out = new PrintStream(file);

      int size = size()-1;	// no need to save the top sort
      out.println(size);

      Sort sort = null;

      // Saving the first part (each sort's name and code):
      for (int index=0; index<size; index++)
      	{
      	  sort = getSort(index);

      	  out.print(sort.name);		// save the sort's name
      	  out.print(" ");
      	  out.println(sort.code.toSaveFormatString());	// save the sort's code
      	}

      // Saving the second part (each non-maximal sort's parents' indices):
      for (int index=0; index<size; index++)
	{
	  sort = getSort(index);

	  // skip this sort if it is maximal:
	  if (sort.parents().contains(Sort.top()))
	    continue;

	  // save the sort's incex:
	  out.print(index+" ");

	  // System.out.print("\t>>> saving parents of "+sort+": ");

	  // save the sort's parents' indices:
	  for (Iterator it = sort.parents().iterator(); it.hasNext();)
	    {
	      Sort parent = (Sort)it.next();
	      out.print(parent.index+" ");
	      // System.out.print(parent+" ("+parent.index+") ");
	    }

	  out.println();
	  // System.out.println();
	}

      out.close();
    }

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

    /**
     * This loads an encoded taxonomy that was saved in the specified
     * file in the format explained in the <tt>save</tt> method, and
     * initializes all the loaded sorts into the current context.
     */
    public void load (String file) throws FileNotFoundException, IOException, BadTokenException
    {
      TaxonomyLoader input = new TaxonomyLoader(file);

      input.nextToken();	// read the taxonomy size (not counting top)

      if (input.tokenType() != input.NUMBER)
	input.error();

      // System.out.println(input.intValue());

      int size = input.intValue();

      // size+1 to account for the top sort to be added
      ensureCapacity(size+1);
      Sort.setCodeSize(size+1);

      input.nextToken();	// read the end of line

      Sort sort = null;
      BitCode code = null;
      int startBit = 0;

      for (int index=0; index<size; index++)
	{
	  input.nextToken();	// read the symbol

	  // System.out.print(input.symbolValue()+" ");

	  if (input.tokenType() != input.WORD)
	    input.error();

	  // Create the sort and its code, and store the sort in the taxonomy at this index:
	  code = new BitCode();
	  sort = new Sort(index,input.symbolValue(),code).setContext(_context);
	  set(index,sort);

	  // read in the code and set the bits of the sort's code accordingly:

	  input.nextToken();	// read the 1st "startBit" position
	  
	  while (input.tokenType() != input.EOL)
	    {
	      if (input.tokenType() != input.NUMBER)
		input.error();

	      // System.out.print(input.intValue()+" ");
	      startBit = input.intValue();

	      input.nextToken();	// read the "endBit" position

	      if (input.tokenType() != input.NUMBER)
		input.error();

	      // System.out.print(input.intValue()+" ");
	      code.set(startBit,input.intValue());

	      input.nextToken();	// read either the next "startBit" position or the end of line
	    }

	  // install the sort as a named sort:
	  _commitSort(index);
	}

      // Read each non-maximal sort's parents' indices and process the "is-a" information:
      for (;;)
	{
	  input.nextToken();

	  if (input.eof())
	    break;

	  if (input.tokenType() != input.NUMBER)
	    input.error();

	  int index = input.intValue();

	  sort = getSort(index);

	  // System.out.println(">>> Reading parents of "+sort+" (index = "+index+")");
	  for (;;)
	  // read and declare the parents:
	    {
	      // read the next parent index or end-of-line:
	      input.nextToken();

	      if (input.tokenType() == input.EOL)
		break;

	      if (input.tokenType() != input.NUMBER)
		input.error();

	      // process the is-a declaration:
	      sort.addIsaDeclaration(getSort(input.intValue()));
	      // System.out.println("\t>>> Declaring: "+sort+" <| "+getSort(input.intValue()));
	    }

	  sort.lock();
	}

      input.close();
      _initialize();
    }

    /* ************************************************************************ */
}