|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectorg.semanticweb.HermiT.tableau.Tableau
public final class Tableau
This class coordinates the main tableau expansion for a given DLOntology (a normalized and clausified ontology). It represents the state of a run on a set of clauses and coordinates the extension of the ABox and also the retraction of facts when backtracking. Before starting the expansion, the given clauses are (for better performance) preprocessed via the HyperresolutionManager into a compiled and executable form.
Constructor Summary | |
---|---|
Tableau(InterruptFlag interruptFlag,
TableauMonitor tableauMonitor,
ExistentialExpansionStrategy existentialsExpansionStrategy,
boolean useDisjunctionLearning,
DLOntology permanentDLOntology,
DLOntology additionalDLOntology,
java.util.Map<java.lang.String,java.lang.Object> parameters)
|
Method Summary | |
---|---|
void |
addGroundDisjunction(GroundDisjunction groundDisjunction)
|
protected void |
backtrackLastMergedOrPrunedNode()
|
protected void |
backtrackTo(int newCurrentBrancingPoint)
Backtrack to a certain branching point in the list of branching points that have been set during the run. |
void |
checkTableauList()
|
void |
clear()
|
void |
clearAdditionalDLOntology()
|
Node |
createNewConcreteNode(DependencySet dependencySet,
Node parent)
Create a new concrete node for datatypes. |
Node |
createNewGraphNode(Node parent,
DependencySet dependencySet)
Create a new node graph node for description graphs |
Node |
createNewNamedNode(DependencySet dependencySet)
Create a new node that represents an individual named in the input ontology (thus, keys have to be applied to it) |
Node |
createNewNINode(DependencySet dependencySet)
Create a new node that represents a nominal, but one that is not named in the input ontology (thus, keys are not applicable) |
protected Node |
createNewNodeRaw(DependencySet dependencySet,
Node parent,
NodeType nodeType,
int treeDepth)
|
Node |
createNewRootConstantNode(DependencySet dependencySet)
Create a new root constant node for datatypes. |
Node |
createNewTreeNode(DependencySet dependencySet,
Node parent)
Create a new tree node. |
protected void |
destroyLastTableauNode()
|
protected boolean |
doIteration()
|
DLOntology |
getAdditionalDLOntology()
|
HyperresolutionManager |
getAdditionalHyperresolutionManager()
|
BranchingPoint |
getCurrentBranchingPoint()
|
int |
getCurrentBranchingPointLevel()
|
DependencySetFactory |
getDependencySetFactory()
|
DescriptionGraphManager |
getDescriptionGraphManager()
|
protected java.util.List<ExistentialConcept> |
getExistentialConceptsBuffer()
|
ExistentialExpansionManager |
getExistentialExpansionManager()
|
ExistentialExpansionStrategy |
getExistentialsExpansionStrategy()
|
ExtensionManager |
getExtensionManager()
|
Node |
getFirstTableauNode()
|
GroundDisjunction |
getFirstUnprocessedGroundDisjunction()
|
InterruptFlag |
getInterruptFlag()
|
Node |
getLastTableauNode()
|
MergingManager |
getMergingManager()
|
Node |
getNode(int nodeID)
|
protected Node |
getNodeForTerm(java.util.Map<Term,Node> termsToNodes,
Term term,
DependencySet dependencySet)
|
NominalIntroductionManager |
getNominalIntroductionManager()
|
int |
getNumberOfAllocatedNodes()
|
int |
getNumberOfMergedOrPrunedNodes()
|
int |
getNumberOfNodeCreations()
|
int |
getNumberOfNodesInTableau()
|
java.util.Map<java.lang.String,java.lang.Object> |
getParameters()
|
DLOntology |
getPermanentDLOntology()
|
HyperresolutionManager |
getPermanentHyperresolutionManager()
|
TableauMonitor |
getTableauMonitor()
|
boolean |
isCurrentModelDeterministic()
|
boolean |
isDeterministic()
|
boolean |
isSatisfiable(boolean loadPermanentABox,
boolean loadAdditionalABox,
java.util.Set<Atom> perTestPositiveFactsNoDependency,
java.util.Set<Atom> perTestNegativeFactsNoDependency,
java.util.Set<Atom> perTestPositiveFactsDummyDependency,
java.util.Set<Atom> perTestNegativeFactsDummyDependency,
java.util.Map<Individual,Node> nodesForIndividuals,
ReasoningTaskDescription reasoningTaskDescription)
|
boolean |
isSatisfiable(boolean loadAdditionalABox,
java.util.Set<Atom> perTestPositiveFactsNoDependency,
java.util.Set<Atom> perTestNegativeFactsNoDependency,
java.util.Set<Atom> perTestPositiveFactsDummyDependency,
java.util.Set<Atom> perTestNegativeFactsDummyDependency,
java.util.Map<Individual,Node> nodesForIndividuals,
ReasoningTaskDescription reasoningTaskDescription)
|
protected void |
loadNegativeFact(java.util.Map<Term,Node> termsToNodes,
Atom atom,
DependencySet dependencySet)
|
protected void |
loadPositiveFact(java.util.Map<Term,Node> termsToNodes,
Atom atom,
DependencySet dependencySet)
|
void |
mergeNode(Node node,
Node mergeInto,
DependencySet dependencySet)
Merges node into mergeInto. |
void |
pruneNode(Node node)
|
void |
pushBranchingPoint(BranchingPoint branchingPoint)
Add a branching point in case we need to backtrack to this state. |
void |
putExistentialConceptsBuffer(java.util.List<ExistentialConcept> buffer)
|
protected boolean |
runCalculus()
|
void |
setAdditionalDLOntology(DLOntology additionalDLOntology)
|
boolean |
supportsAdditionalDLOntology(DLOntology additionalDLOntology)
|
protected void |
updateFlagsDependentOnAdditionalOntology()
|
Methods inherited from class java.lang.Object |
---|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
---|
protected final InterruptFlag m_interruptFlag
protected final java.util.Map<java.lang.String,java.lang.Object> m_parameters
protected final TableauMonitor m_tableauMonitor
protected final ExistentialExpansionStrategy m_existentialExpansionStrategy
protected final DLOntology m_permanentDLOntology
protected DLOntology m_additionalDLOntology
protected final DependencySetFactory m_dependencySetFactory
protected final ExtensionManager m_extensionManager
protected final ClashManager m_clashManager
protected final HyperresolutionManager m_permanentHyperresolutionManager
protected HyperresolutionManager m_additionalHyperresolutionManager
protected final MergingManager m_mergingManager
protected final ExistentialExpansionManager m_existentialExpasionManager
protected final NominalIntroductionManager m_nominalIntroductionManager
protected final DescriptionGraphManager m_descriptionGraphManager
protected final DatatypeManager m_datatypeManager
protected final java.util.List<java.util.List<ExistentialConcept>> m_existentialConceptsBuffers
protected final boolean m_useDisjunctionLearning
protected final boolean m_hasDescriptionGraphs
protected BranchingPoint[] m_branchingPoints
protected int m_currentBranchingPoint
protected int m_nonbacktrackableBranchingPoint
protected boolean m_isCurrentModelDeterministic
protected boolean m_needsThingExtension
protected boolean m_needsNamedExtension
protected boolean m_needsRDFSLiteralExtension
protected boolean m_checkDatatypes
protected boolean m_checkUnknownDatatypeRestrictions
protected int m_allocatedNodes
protected int m_numberOfNodesInTableau
protected int m_numberOfMergedOrPrunedNodes
protected int m_numberOfNodeCreations
protected Node m_firstFreeNode
protected Node m_firstTableauNode
protected Node m_lastTableauNode
protected Node m_lastMergedOrPrunedNode
protected GroundDisjunction m_firstGroundDisjunction
protected GroundDisjunction m_firstUnprocessedGroundDisjunction
Constructor Detail |
---|
public Tableau(InterruptFlag interruptFlag, TableauMonitor tableauMonitor, ExistentialExpansionStrategy existentialsExpansionStrategy, boolean useDisjunctionLearning, DLOntology permanentDLOntology, DLOntology additionalDLOntology, java.util.Map<java.lang.String,java.lang.Object> parameters)
Method Detail |
---|
public InterruptFlag getInterruptFlag()
public DLOntology getPermanentDLOntology()
public DLOntology getAdditionalDLOntology()
public java.util.Map<java.lang.String,java.lang.Object> getParameters()
public TableauMonitor getTableauMonitor()
public ExistentialExpansionStrategy getExistentialsExpansionStrategy()
public boolean isDeterministic()
public DependencySetFactory getDependencySetFactory()
public ExtensionManager getExtensionManager()
public HyperresolutionManager getPermanentHyperresolutionManager()
public HyperresolutionManager getAdditionalHyperresolutionManager()
public MergingManager getMergingManager()
public ExistentialExpansionManager getExistentialExpansionManager()
public NominalIntroductionManager getNominalIntroductionManager()
public DescriptionGraphManager getDescriptionGraphManager()
public void clear()
public boolean supportsAdditionalDLOntology(DLOntology additionalDLOntology)
public void setAdditionalDLOntology(DLOntology additionalDLOntology)
public void clearAdditionalDLOntology()
protected void updateFlagsDependentOnAdditionalOntology()
public boolean isSatisfiable(boolean loadAdditionalABox, java.util.Set<Atom> perTestPositiveFactsNoDependency, java.util.Set<Atom> perTestNegativeFactsNoDependency, java.util.Set<Atom> perTestPositiveFactsDummyDependency, java.util.Set<Atom> perTestNegativeFactsDummyDependency, java.util.Map<Individual,Node> nodesForIndividuals, ReasoningTaskDescription reasoningTaskDescription)
public boolean isSatisfiable(boolean loadPermanentABox, boolean loadAdditionalABox, java.util.Set<Atom> perTestPositiveFactsNoDependency, java.util.Set<Atom> perTestNegativeFactsNoDependency, java.util.Set<Atom> perTestPositiveFactsDummyDependency, java.util.Set<Atom> perTestNegativeFactsDummyDependency, java.util.Map<Individual,Node> nodesForIndividuals, ReasoningTaskDescription reasoningTaskDescription)
protected void loadPositiveFact(java.util.Map<Term,Node> termsToNodes, Atom atom, DependencySet dependencySet)
protected void loadNegativeFact(java.util.Map<Term,Node> termsToNodes, Atom atom, DependencySet dependencySet)
protected Node getNodeForTerm(java.util.Map<Term,Node> termsToNodes, Term term, DependencySet dependencySet)
protected boolean runCalculus()
protected boolean doIteration()
public boolean isCurrentModelDeterministic()
public int getCurrentBranchingPointLevel()
public BranchingPoint getCurrentBranchingPoint()
public void addGroundDisjunction(GroundDisjunction groundDisjunction)
public GroundDisjunction getFirstUnprocessedGroundDisjunction()
public void pushBranchingPoint(BranchingPoint branchingPoint)
branchingPoint
- protected void backtrackTo(int newCurrentBrancingPoint)
newCurrentBrancingPoint
- public Node createNewNamedNode(DependencySet dependencySet)
dependencySet
- the dependency set for the node
public Node createNewNINode(DependencySet dependencySet)
dependencySet
- the dependency set for the node
public Node createNewTreeNode(DependencySet dependencySet, Node parent)
dependencySet
- the dependency set for the nodeparent
- the parent of the node that is to be created
public Node createNewConcreteNode(DependencySet dependencySet, Node parent)
dependencySet
- the dependency set for the nodeparent
- the parent of the node that is to be created
public Node createNewRootConstantNode(DependencySet dependencySet)
dependencySet
- the dependency set for the node
public Node createNewGraphNode(Node parent, DependencySet dependencySet)
parent
- the parent of the node that is to be created (may be null)dependencySet
- the dependency set for the node
protected Node createNewNodeRaw(DependencySet dependencySet, Node parent, NodeType nodeType, int treeDepth)
public void mergeNode(Node node, Node mergeInto, DependencySet dependencySet)
node
- the node that is to be mergedmergeInto
- the node we merge intodependencySet
- public void pruneNode(Node node)
protected void backtrackLastMergedOrPrunedNode()
protected void destroyLastTableauNode()
public int getNumberOfNodeCreations()
public Node getFirstTableauNode()
public Node getLastTableauNode()
public int getNumberOfAllocatedNodes()
public int getNumberOfNodesInTableau()
public int getNumberOfMergedOrPrunedNodes()
public Node getNode(int nodeID)
protected java.util.List<ExistentialConcept> getExistentialConceptsBuffer()
public void putExistentialConceptsBuffer(java.util.List<ExistentialConcept> buffer)
public void checkTableauList()
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |