content: /* 
   * Kodkod -- Copyright (c) 2005-present, Emina Torlak
   *
   * Permission is hereby granted, free of charge, to any person obtaining a copy
   * of this software and associated documentation files (the "Software"), to deal
   * in the Software without restriction, including without limitation the rights
   * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
   * copies of the Software, and to permit persons to whom the Software is
   * furnished to do so, subject to the following conditions:
   *
   * The above copyright notice and this permission notice shall be included in
   * all copies or substantial portions of the Software.
   *
   * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
   * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
   * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
   * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
   * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
   * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
   * THE SOFTWARE.
   */
  package kodkod.util.ints;
  
  /**
   * A tree with integer keys.  
   * 
   * @specfield root: lone N
   * @specfield nodes: root.*(left + right)
   * @author Emina Torlak
   */
  final class IntTree<N extends IntTree.Node<N>> implements Cloneable {
  	private static final boolean BLACK = true, RED = false;
  
  	private N root;
  
  	/**
  	 * Creates an empty IntTree.
  	 * @ensures no this.root'
  	 */
  	IntTree() {
  		root = null;
  	}
  
  	/**
  	 * Discards all elements from this tree.
  	 * @ensures  no this.root' 
  	 **/
  	final void clear() {
  		root = null;
  	}
  
  	/**
  	 * Returns the node with the given key, or null no such node exists.
  	 * @return this.nodes & key.index 
  	 */
  	final N search(int k) {	
  		N node = root;
  		while(node != null) {
  			if (node.key==k) break;
  			else if (node.key>k) node = node.left;
  			else node = node.right;
  		}
  		return node;
  	}
  
  	/**
  	 * Returns the node whose key is the ceiling of <tt>k</tt> in this tree, or 
  	 * null if no such node exists.
  	 * @return {n: this.nodes | n.key >= k &&
  	 *           no n': this.nodes - n | n'.key >= k && n'.key < n.key }
  	 */
  	final N searchGTE(int k) {
  		if (root==null) return null;
  		N c = root;
  		while (true) {
  			if (c.key==k) {
  				return c;
  			} else if (c.key>k) {
  				if (c.left != null)
  					c = c.left;
  				else
  					return c;
  			} else {
  				if (c.right != null) 
  					c = c.right;
  				else 
  					return successor(c);
  			}
  		}
  	}
  
  	/**
  	 * Returns the node whose key is the floor of <tt>k</tt> in this tree, or 
  	 * null if no such node exists.
  	 * @return {n: this.nodes | n.key <= k &&
  	 *           no n': this.nodes - n | n'.key <= k && n'.key > n.key }
  	 */
  	final N searchLTE(int k) {
  		if (root==null) return null;
  		N f = root;
  		while(true) {
  			if (f.key==k)
  				return f;
  			else if (f.key>k) {
  				if (f.left != null)
  					f = f.left;
  				else 
  					return predecessor(f);
  			} else {
  				if (f.right != null) 
  					f = f.right;
  				else 
  					return f;
  			}
  		}
  	}
  
  	/**
  	 * Implementation of the tree-predecessor algorithm from CLR.
  	 * Returns the given node's predecessor, if it exists.  
  	 * Otherwise returns null.  
  	 * @return the given node's predecessor
  	 * @throws NullPointerException  node = null
  	 */
  	final N predecessor(N node) {
  		if (node.left != null) {
  			return max(node.left);
  		} else {
  			N n = node;
  			N ancestor = n.parent;
  			while (ancestor != null && n == ancestor.left) {
  				n = ancestor;
  				ancestor = ancestor.parent;
  			}
  			return ancestor;
  		}
  	}	
  
  	/**
  	 * Implementation of the tree-successor algorithm from CLR.
  	 * Returns the given node's successor, if it exists.  
  	 * Otherwise returns null.
  	 * @return the given node's successor
  	 * @throws NullPointerException  node = null
  	 */
  	final N successor(N node) {
  		if (node.right != null) {
  			return min(node.right);
  		} else {
  			N n = node;
  			N ancestor = n.parent;
  			while (ancestor != null && n == ancestor.right) {
  				n = ancestor;
  				ancestor = ancestor.parent;
  			}
  			return ancestor;
  		}
  	}
  
  	/**
  	 * Returns the node with the smallest key.
  	 * @return key.(min(this.nodes.key))
  	 */
  	final N min() {
  		return min(root);
  	}
  
  	/**
  	 * Returns the node with the largest key.
  	 * @return key.(max(this.nodes.key))
  	 */
  	final N max() {
  		return max(root);
  	}
  
  	/**
  	 * Returns the leftmost node in the subtree rooted at start.
  	 * The behavior of this method is unspecified if the given node
  	 * is not in this tree.
  	 * @requires node in this.nodes
  	 * @return {n: start.*left | no n.left }
  	 */
  	private final N min(N start) {
  		if (start != null) {
  			while(start.left != null) {
  				start = start.left;
  			}
  		}
  		return start;
  	}
  
  	/**
  	 * Returns the rightmost in the subtree rooted at start.
  	 * The behavior of this method is unspecified if the given node
  	 * is not in this tree.
  	 * @requires node in this.nodes
  	 * @return {n: start.*left | no n.right }
  	 */
  	private final N max(N start) {
  		if (start != null) {
  			while(start.right != null) {
  				start = start.right;
  			}
  		}
  		return start;
  	}
  
  	/**
  	 * Replaces the old node, o, with the given new node, n, in this tree.
  	 * @requires no n.(left + right + parent)
  	 * @requires o = o.parent.left => n.key < o.parent.key
  	 * @requires o = o.parent.right => n.key > o.parent.key
  	 * @requires some o.left => n.key > o.left.key
  	 * @requires some o.right => n.key < o.right.key
  	 * @ensures this.nodes' = this.nodes - o + n
  	 * @ensures o.parent' = o.left' = o.right' = null
  	 */
  	final void replace(N o, N n) {
  		n.color = o.color;
  		n.parent = o.parent;
  		n.left = o.left;
  		n.right = o.right;
  		if (o.left != null) 			{ o.left.parent = n; }
  		if (o.right != null)			{ o.right.parent = n;	 }	 
  		if (o.parent == null)			{ root = n; }
  		else if (o == o.parent.left) 	{ o.parent.left = n; }
  		else 							{ o.parent.right = n; }
  		o.parent = o.left = o.right = null;
  	}
  
  	private final N parentOf(N n) 					{ return n==null ? null : n.parent; }
  	private final N leftOf(N n) 					{ return n==null ? null : n.left; }
  	private final N rightOf(N n) 					{ return n==null ? null : n.right; }
  	private final boolean colorOf(N n) 				{ return n==null ? BLACK : n.color; }
  	private final void setColor(N n, boolean color)	{ if (n!=null) n.color = color; }
  
  	/**
  	 * Implementation of the CLR insertion algorithm.
  	 * @requires no z.key & this.nodes.key
  	 * @ensures this.nodes' = this.nodes + z
  	 */
  	final void insert(N z) {
  		N y = null;
  		for (N x = root; x != null;) {
  			y = x;
  			if (x.key>z.key) 
  				x = x.left; 
  			else 
  				x = x.right; 
  		}
  
  		z.parent = y;
  		z.left = z.right = null;
  		if (y==null) {	
  			root = z;
  		} else {
  			z.color = RED;
  			if (y.key>z.key)	{ y.left = z; }
  			else 				{ y.right = z; }
  
  			insertFixUp(z);
  		}
  	}
  
  	/**
  	 * A slightly modified implementation of the CLR deletion algorithm.
  	 * @requires z in this.nodes
  	 * @ensures this.nodes' = this.nodes - z
  	 */
  	final void delete(N z) {
  		N y = (z.left==null || z.right==null ? z : successor(z));
  		N x = (y.left != null ? y.left : y.right);
  		
  		N yparent = y.parent;
  		final boolean yleft = (y==leftOf(y.parent));
  		final boolean ycolor = y.color;
  		
  		if (x!=null)						{ x.parent = yparent; }
  		
  		if (yparent == null)				{ root = x; }
  		else if (yleft)						{ yparent.left = x; }
  		else								{ yparent.right = x; }
  		
  		if (y != z) { replace(z, y); }
  		
  		if (ycolor==BLACK) {
  			if (x!=null) { 
  				deleteFixUp(x); 
  			} else if (yparent!=null) { 	// z is not the only node
  
  				if (z==yparent) yparent = y; // y, z's successor, is z's right child
  				z.color = BLACK;
  				z.left = z.right = null;
  				z.parent = yparent;
  				if (yleft)				{ yparent.left = z; }
  				else 					{ yparent.right = z; }
  		
  				deleteFixUp(z);
  				if (z==z.parent.left)	{ z.parent.left = null; }
  				else 					{ z.parent.right = null; }				
  			}
  		}
  		
  		z.left = z.right = z.parent = null; // cut z out of the tree by nulling out its pointers
  	}
  
  	/**
  	 * {@inheritDoc}
  	 * @see java.lang.Object#clone()
  	 * @throws CloneNotSupportedException  nodes contained in this tree are not cloneable
  	 */
  	@SuppressWarnings("unchecked")
  	protected IntTree<N> clone() throws CloneNotSupportedException {
  		final IntTree<N> ret = (IntTree<N>) super.clone();
  		ret.root = clone(root, null);
  		return ret;
  	}
  
  	/**
  	 * Recursively clones the given node.
  	 */
  	@SuppressWarnings("unchecked")
  	private N clone(N n, N parent) throws CloneNotSupportedException {
  		if (n==null) return null;
  		N clone = (N) n.clone();
  		clone.parent = parent;
  		clone.left = clone(n.left, clone);
  		clone.right = clone(n.right, clone);
  		return clone;
  	}
  
  	/*---------balancing operations (CLR, pp.278-289)---------*/
  	/**
  	 * From CLR.
  	 */
  	private void insertFixUp(N z) {
  		while (z != null && z != root && z.parent.color == RED) {
  			if (parentOf(z) == leftOf(parentOf(parentOf(z)))) {
  				N y = rightOf(parentOf(parentOf(z)));
  				if (colorOf(y) == RED) {
  					setColor(parentOf(z), BLACK);
  					setColor(y, BLACK);
  					setColor(parentOf(parentOf(z)), RED);
  					z = parentOf(parentOf(z));
  				} else {
  					if (z == rightOf(parentOf(z))) {
  						z = parentOf(z);
  						rotateLeft(z);
  					}
  					setColor(parentOf(z), BLACK);
  					setColor(parentOf(parentOf(z)), RED);
  					if (parentOf(parentOf(z)) != null)
  						rotateRight(parentOf(parentOf(z)));
  				}
  			} else {
  				N y = leftOf(parentOf(parentOf(z)));
  				if (colorOf(y) == RED) {
  					setColor(parentOf(z), BLACK);
  					setColor(y, BLACK);
  					setColor(parentOf(parentOf(z)), RED);
  					z = parentOf(parentOf(z));
  				} else {
  					if (z == leftOf(parentOf(z))) {
  						z = parentOf(z);
  						rotateRight(z);
  					}
  					setColor(parentOf(z),  BLACK);
  					setColor(parentOf(parentOf(z)), RED);
  					if (parentOf(parentOf(z)) != null)
  						rotateLeft(parentOf(parentOf(z)));
  				}
  			}
  		}
  		root.color = BLACK;
  	}
  
  	/**
  	 * From CLR.
  	 */
  	private void deleteFixUp(N x) {
  		while (x != root && colorOf(x) == BLACK) {
  			if (x == leftOf(parentOf(x))) {
  				N sib = rightOf(parentOf(x));
  
  				if (colorOf(sib) == RED) {
  					setColor(sib, BLACK);
  					setColor(parentOf(x), RED);
  					rotateLeft(parentOf(x));
  					sib = rightOf(parentOf(x));
  				}
  
  				if (colorOf(leftOf(sib))  == BLACK &&
  						colorOf(rightOf(sib)) == BLACK) {
  					setColor(sib,  RED);
  					x = parentOf(x);
  				} else {
  					if (colorOf(rightOf(sib)) == BLACK) {
  						setColor(leftOf(sib), BLACK);
  						setColor(sib, RED);
  						rotateRight(sib);
  						sib = rightOf(parentOf(x));
  					}
  					setColor(sib, colorOf(parentOf(x)));
  					setColor(parentOf(x), BLACK);
  					setColor(rightOf(sib), BLACK);
  					rotateLeft(parentOf(x));
  					x = root;
  				}
  			} else { // symmetric
  				N sib = leftOf(parentOf(x));
  
  				if (colorOf(sib) == RED) {
  					setColor(sib, BLACK);
  					setColor(parentOf(x), RED);
  					rotateRight(parentOf(x));
  					sib = leftOf(parentOf(x));
  				}
  
  				if (colorOf(rightOf(sib)) == BLACK &&
  						colorOf(leftOf(sib)) == BLACK) {
  					setColor(sib,  RED);
  					x = parentOf(x);
  				} else {
  					if (colorOf(leftOf(sib)) == BLACK) {
  						setColor(rightOf(sib), BLACK);
  						setColor(sib, RED);
  						rotateLeft(sib);
  						sib = leftOf(parentOf(x));
  					}
  					setColor(sib, colorOf(parentOf(x)));
  					setColor(parentOf(x), BLACK);
  					setColor(leftOf(sib), BLACK);
  					rotateRight(parentOf(x));
  					x = root;
  				}
  			}
  		}
  
  		setColor(x, BLACK);
  
  	}
  
  	/**
  	 * From CLR.
  	 */
  	private void rotateLeft(N x) {
  		N y = x.right;
  		x.right = y.left;
  		if (y.left != null) 
  			y.left.parent = x;
  		y.parent = x.parent;
  		if (x.parent == null)
  			root = y;
  		else if (x.parent.left == x)
  			x.parent.left = y;
  		else
  			x.parent.right = y;
  		y.left = x;
  		x.parent = y;
  	}
  
  	/**
  	 * From CLR.
  	 */
  	private void rotateRight(N x) {
  		N y = x.left;
  		x.left = y.right;  
  		if (y.right != null) 
  			y.right.parent = x;
  		y.parent = x.parent;
  		if (x.parent == null)
  			root = y;
  		else if (x.parent.right == x)
  			x.parent.right = y;
  		else 
  			x.parent.left = y;
  		y.right = x;
  		x.parent = y;
  	}
  
  	/**
  	 * @see java.lang.Object#toString()
  	 */
  	public String toString() {
  		return root.toString();
  	}
  
  	/**
  	 * A node  in an int tree.  Subclasses need to 
  	 * implement the clone method iff IntTree.clone will
  	 * be called on the tree containing the nodes.
  	 * @specfield key: int
  	 * @specfield parent: lone N
  	 * @specfield left: lone N
  	 * @specfield right: lone N
  	 * @author Emina Torlak
  	 */
  	abstract static class Node<N extends Node<N>> implements Cloneable {
  		N parent, left, right;
  		boolean color;
  		/**
  		 * Subclasses are required to maintain the following invariant:
  		 * @invariant 	this = this.parent.left => this.key < this.parent.key &&
  		 *  			this = this.parent.right => this.key > this.parent.key &&
  		 *  			some this.left => this.key > this.left.key &&
  		 *  			some this.right => this.key < this.right.key
  		 */
  		protected int key;
  
  		/**
  		 * Constructs an empty node with the given key.
  		 * @ensures no this.(parent' + left' + right') && this.key' = key 
  		 */
  		Node(int key) {
  			this.parent = this.left = this.right = null;
  			this.color = BLACK;
  			this.key = key;
  		}
  
  		/**
  		 * Returns the left child of this node.
  		 * @return this.left
  		 */
  		final N left() { return left; }
  
  		/**
  		 * Returns the right child of this node.
  		 * @return this.right
  		 */
  		final N right() { return right; }
  
  		/**
  		 * Return the parent of this node.
  		 * @return this.parent
  		 */
  		final N parent() { return parent; }
  
  		/**
  		 * Clones this node.  Subclasses must override
  		 * this method (and call super.clone()) in order
  		 * for IntTree.clone() to function properly.
  		 * @throws CloneNotSupportedException 
  		 * @see java.lang.Object#clone()
  		 */
  		@SuppressWarnings("unchecked")
  		protected Node<N> clone() throws CloneNotSupportedException {
  			Node<N> ret = (Node<N>) super.clone();
  			ret.parent = ret.left = ret.right = null;
  			return ret;
  		}
  
  		/**
  		 * @see java.lang.Object#toString()
  		 */
  		public String toString() {
  			return "[" + key + " " + (color ? "b" : "r") + " " + (left==this ? key : left) + " "+ 
  			(right==this ? key : right)  + "]";
  
  		}
  	}
  
  }
  