org.semanticweb.HermiT.tableau
Class NominalIntroductionManager

java.lang.Object
  extended by org.semanticweb.HermiT.tableau.NominalIntroductionManager
All Implemented Interfaces:
java.io.Serializable

public final class NominalIntroductionManager
extends java.lang.Object
implements java.io.Serializable

Implements the nominal introduction rule.

See Also:
Serialized Form

Nested Class Summary
protected  class NominalIntroductionManager.NominalIntroductionBranchingPoint
           
 
Field Summary
protected  TupleTable m_annotatedEqualities
           
protected  java.lang.Object[] m_bufferForAnnotatedEquality
           
protected  java.lang.Object[] m_bufferForRootNodes
           
protected  DependencySetFactory m_dependencySetFactory
           
protected  int m_firstUnprocessedAnnotatedEquality
           
protected  int[] m_indicesByBranchingPoint
           
protected  InterruptFlag m_interruptFlag
           
protected  MergingManager m_mergingManager
           
protected  TupleTableFullIndex m_newRootNodesIndex
           
protected  TupleTable m_newRootNodesTable
           
protected  Tableau m_tableau
           
 
Constructor Summary
NominalIntroductionManager(Tableau tableau)
           
 
Method Summary
 boolean addAnnotatedEquality(AnnotatedEquality annotatedEquality, Node node0, Node node1, Node node2, DependencySet dependencySet)
           
protected  boolean applyNIRule(AnnotatedEquality annotatedEquality, Node node0, Node node1, Node node2, DependencySet dependencySet)
           
 void backtrack()
           
 void branchingPointPushed()
           
 boolean canForgetAnnotation(AnnotatedEquality annotatedEquality, Node node0, Node node1, Node node2)
           
 void clear()
           
protected  Node getNIRootFor(DependencySet dependencySet, Node rootNode, AnnotatedEquality annotatedEquality, int number)
           
 boolean processAnnotatedEqualities()
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

m_tableau

protected final Tableau m_tableau

m_dependencySetFactory

protected final DependencySetFactory m_dependencySetFactory

m_interruptFlag

protected final InterruptFlag m_interruptFlag

m_mergingManager

protected final MergingManager m_mergingManager

m_annotatedEqualities

protected final TupleTable m_annotatedEqualities

m_bufferForAnnotatedEquality

protected final java.lang.Object[] m_bufferForAnnotatedEquality

m_newRootNodesTable

protected final TupleTable m_newRootNodesTable

m_newRootNodesIndex

protected final TupleTableFullIndex m_newRootNodesIndex

m_bufferForRootNodes

protected final java.lang.Object[] m_bufferForRootNodes

m_indicesByBranchingPoint

protected int[] m_indicesByBranchingPoint

m_firstUnprocessedAnnotatedEquality

protected int m_firstUnprocessedAnnotatedEquality
Constructor Detail

NominalIntroductionManager

public NominalIntroductionManager(Tableau tableau)
Method Detail

clear

public void clear()

branchingPointPushed

public void branchingPointPushed()

backtrack

public void backtrack()

processAnnotatedEqualities

public boolean processAnnotatedEqualities()

canForgetAnnotation

public boolean canForgetAnnotation(AnnotatedEquality annotatedEquality,
                                   Node node0,
                                   Node node1,
                                   Node node2)

addAnnotatedEquality

public boolean addAnnotatedEquality(AnnotatedEquality annotatedEquality,
                                    Node node0,
                                    Node node1,
                                    Node node2,
                                    DependencySet dependencySet)

applyNIRule

protected boolean applyNIRule(AnnotatedEquality annotatedEquality,
                              Node node0,
                              Node node1,
                              Node node2,
                              DependencySet dependencySet)

getNIRootFor

protected Node getNIRootFor(DependencySet dependencySet,
                            Node rootNode,
                            AnnotatedEquality annotatedEquality,
                            int number)