// (c) MIT 2003.  All rights reserved.

// -*-Mode: Java-*- 
// $Id: Node.java,v 1.6 2003/03/06 00:40:39 moltmans Exp $
// Node.java -- 
// Author: Michael Oltmans <moltmans@ai.mit.edu> 
// Created: <Wed Apr 26 17:28:01 2000> 
// Time-stamp: <2000-05-13 17:13:09 moltmans> 
package rec.tms;

import java.util.*;
import rec.util.*;

public class Node 
{
  /** keep track of a unique id to assign to new nodes. **/
  private static int m_indexCounter = 0;

  public static final int IN  = 1975;
  public static final int OUT = 2080;

  public static final int ASSUMPTION = 1110;
  public static final int DEFAULT_ASSUMPTION = 1275;
  public static final int NOT_ASSUMPTION = 1165;

  /** the jtms this node is part of. **/
  private JTMS m_jtms;
  /** unique index for this node. **/
  private int m_index;
  
  private Datum m_datum;
  /** IN if believed OUT if not believed **/
  private int m_label;
  /** the current justification. **/
  private Justification m_support;
  /** list of possible justifications. **/
  private LinkedList m_justs;
  /** Justifications in which this is an antecedent **/
  private LinkedList m_consequences;
  /** For use in mark and sweep algs. **/
  private Object m_mark;
  /** true if it is contradictory **/
  private boolean m_isContradictory;
  /** ASSUMPTION, DEFAULT_ASSUMPTION, or NOT_ASSUMPTION **/
  private int m_assumption;
  /** Rules that should be triggered when node goes in. **/
  private LinkedList m_inRules;
  /** Rules that should be triggered when node goes out. **/
  private LinkedList m_outRules;

  public Node( JTMS jtms, Datum datum,
	       boolean isAssumption, boolean isContradictory )
  {
    m_index = m_indexCounter++;
    m_datum = datum;
    if( isAssumption )
      m_assumption = ASSUMPTION;
    else
      m_assumption = NOT_ASSUMPTION;

    m_label = OUT;
    m_support = null;
    m_justs = new LinkedList();
    m_consequences = new LinkedList();
    m_mark = null;
    m_inRules = new LinkedList();
    m_outRules = new LinkedList();
    
    m_isContradictory = isContradictory;
    m_jtms = jtms;
    m_jtms.addNode( this );
  }
  
  public Node( JTMS jtms, Datum datum ) 
  {
    this( jtms, datum, false, false );
  }
  
  ////////////////////////////////////////////////////////////////////
  // Justification handling code:

  /** @return Collection of possible justifications of this node. **/
  public Collection getJustifications() 
  {
    return m_justs;
  }

  /**
   * @return Collection of the justifications that are consequences of
   *         this node.
   **/
  public Collection getConsequences() 
  {
    return m_consequences;
  }

  void addConsequence( Justification conseq ) 
  {
    m_consequences.add( conseq );
  }
  
  public Justification getSupport()
  {
    return m_support;
  }

  public Datum getDatum() 
  {
    return m_datum;
  }

  /**
   * Make ourselves IN, and propagate in-ness to consequences.  Users
   * should not explicitly install supports they should call
   * justify instead.
   * @see justify
   **/
  void installSupport( Justification just )
  {
    makeIn( just );
    propagateInness();
  }

  /**
   * Add justification link between antecedents and this node.
   * @param informant anything that identifies the source of the
   *                  justification, usually a string
   * @param antecedents collection of nodes that are antecedents for
   *                    this node
   **/
  public void justify( Object informant, Collection antecedents ) 
  {
    Justification just = null;
    just = new Justification( informant, this, antecedents );
    m_justs.add( just );
    m_jtms.addJustification( just );

    m_jtms.debugging( "Justifying: " + just.toString() );

    Iterator it = antecedents.iterator();
    while( it.hasNext() ) {
      Node node = (Node)it.next();
      node.addConsequence( just );
    }

    // install new support structure if needed
    if( !antecedents.isEmpty() || isOut() ) {
      if( just.checkJustification() ) {
	installSupport( just );
      }
    }
    else {
      m_support = just;
    }
    
    m_jtms.checkForContradictions();
  }
  

  ////////////////////////////////////////////////////////////////////
  // Truth propagation
  
  /** Progate IN label to consequences that are now supported. **/
  private void propagateInness() 
  {
    LinkedList queue = new LinkedList();
    queue.add( this );

    while( !queue.isEmpty() ) {
      m_jtms.debugging( "   Propagating belief in " + this + "." );
      
      Node node = (Node)queue.removeFirst();
      Iterator it = node.getConsequences().iterator();
      while( it.hasNext() ) {
	Justification just = (Justification)it.next();
	if( just.checkJustification() ) {
	  just.getConsequence().makeIn( just );
	  queue.addLast( just.getConsequence() );
	}
      }
    }
  }

  /** Propagate OUT label to those nodes no longer supported. **/
  private LinkedList propagateOutness()
  {
    LinkedList outQueue = new LinkedList();
    LinkedList justs = new LinkedList( m_consequences );

    m_jtms.debugging( "   Propagating disbelief in " + this + "." );

    // For each justification using this node, check to see if it
    // supports some other node.  If so, queue it up to look for other
    // support
    while( !justs.isEmpty() ) {
      Justification just = (Justification)justs.removeFirst();
      Node conseq = (Node)just.getConsequence();

      // if they are both null or of they are the same make it out
      if( ((conseq.getSupport() != null) &&
	   (just != null)  &&
	   conseq.getSupport().equals( just ) ) ||
	  ((conseq.getSupport() == null) &&
	   (just == null)) )
      {
	conseq.makeOut();
	outQueue.addLast( conseq );
	justs.addAll( conseq.getConsequences() );
      }
    }
    return outQueue;
  }

  ////////////////////////////////////////////////////////////////////
  // Assumption manipulation:

  public boolean isAssumption() 
  {
    return( (m_assumption == ASSUMPTION) ||
	    (m_assumption == DEFAULT_ASSUMPTION) );
  }

  public boolean isDefaultAssumption() 
  {
    return m_assumption == DEFAULT_ASSUMPTION;
  }

  public boolean isEnabledAssumption()
  {
    return m_support == Justification.ENABLED_ASSUMPTION;
  }

  /** Make this node an assumption and enable it. **/
  public void assume()
  {
    if( !isAssumption() ) {
      m_jtms.debugging( "Converting " + this + " into an assumption" );
      m_assumption = ASSUMPTION;
    }
    enableAssumption();
  }

  /** Enable (assume IN) the fact in this node. **/
  void enableAssumption()
  {
    Assert.check( isAssumption(),
		  "Cannot enable non-assumption: " + this );
    m_jtms.debugging( "  Enabling assumption " + this );

    if( isOut() ) {
      makeIn( Justification.ENABLED_ASSUMPTION );
      propagateInness();
    }
    // if it's not supported by an assumption and its support has no
    // antecedent then it is not an assumption so make it one
    else if( ! isEnabledAssumption() &&
	     ! m_support.getAntecedents().isEmpty() )
    {
      m_support = Justification.ENABLED_ASSUMPTION;
    }

    m_jtms.checkForContradictions();
  }
  
  
  /** Retract (assume OUT) this node. **/
  public void retractAssumption()
  {
    if( (m_support != null) && m_support.isEnabledAssumption() ) {
      m_jtms.debugging( "  Retracting assumption " + this + "." );
      makeOut();
      LinkedList outs = propagateOutness();
      outs.addFirst( this );
      m_jtms.findAlternativeSupport( outs );
    }
  }

  /** 
   * Returns the set of enabled assumptions underlying the
   * well-founded support for a node.
   **/
  public Collection getAssumptions() 
  {
    // this is just an object to check equality with
    Object flag = new Object();
    
    LinkedList nodes = new LinkedList();
    LinkedList assumptions = new LinkedList();
    nodes.add( this );

    while( !nodes.isEmpty() ) {
      Node node = (Node)nodes.removeFirst();
      if( (node.m_mark != flag) &&
	  node.isEnabledAssumption() )
      {
	assumptions.add( node );
      }
      else if( node.isIn() ) {
	nodes.addAll( node.getSupport().getAntecedents() );
      }
      node.m_mark = flag;
    }

    return assumptions;
  }

  ////////////////////////////////////////////////////////////////////
  // Contradiction stuff:

  public boolean isContradictory() 
  {
    return m_isContradictory;
  }
  

  /** Mark this node as a contradiction. **/
  public void makeContradiction()
  {
    if( !isContradictory() ) {
      m_isContradictory = true;
      m_jtms.addContradiction( this );
      m_jtms.checkForContradictions();
    }
  }
  
  

  ////////////////////////////////////////////////////////////////////
  // adjustment and query of the inness and outness of this node

  public boolean isOut() 
  {
    return m_label == OUT;
  }
  
  public boolean isIn() 
  {
    return m_label == IN;
  }

  void addInRule( RuleApplication ra ) 
  {
    m_inRules.add( ra );
  }
  
  void addOutRule( RuleApplication ra ) 
  {
    m_outRules.add( ra );
  }

  /** Label this node as IN and set the support to just. **/
  private void makeIn( Justification just ) 
  {
    m_jtms.debugging( "     Making " + this + " in via " + just );
    m_label = IN;
    m_support = just;

    Thunk thunk = m_jtms.getEnqueueProc();
    if( thunk != null ) {
      while( !m_inRules.isEmpty() ) {
	thunk.run( m_inRules.removeFirst() );
      }
    }
  }

  /** Label this node as OUT and set the support to null. **/
  private void makeOut()
  {
    m_jtms.debugging( "     retracting belief in " + this + "." );
    m_label = OUT;
    m_support = null;

    Thunk thunk = m_jtms.getEnqueueProc();
    if( thunk != null ) {
      while( !m_outRules.isEmpty() ) {
	thunk.run( m_outRules.removeFirst() );
      }
    }
  }

  public String toString() 
  {
    return "<Node: " + m_datum + ">";
  }
  
}
