[DL-Learner SVN] SF.net SVN: dl-learner:[3171] trunk/components-core/src

[<jen...@us...>]

Revision: 3171
          http://dl-learner.svn.sourceforge.net/dl-learner/?rev=3171&view=rev
Author:   jenslehmann
Date:     2011-08-30 15:17:02 +0000 (Tue, 30 Aug 2011)
Log Message:
-----------
moved fuzzy CELOE to new architecture

Modified Paths:
--------------
    trunk/components-core/src/main/java/org/dllearner/algorithms/fuzzydll/FuzzyCELOE.java
    trunk/components-core/src/main/java/org/dllearner/algorithms/fuzzydll/FuzzyOEHeuristicRuntime.java
    trunk/components-core/src/test/java/org/dllearner/test/FuzzyDLLTest.java
    trunk/components-core/src/test/java/org/dllearner/test/FuzzyDLLTest_Trains.java
    trunk/components-core/src/test/java/org/dllearner/test/FuzzyDLLTest_Trains_noFuzzyIndividuals.java

Added Paths:
-----------
    trunk/components-core/src/main/java/org/dllearner/refinementoperators/FuzzyRhoDRDown.java

Removed Paths:
-------------
    trunk/components-core/src/main/java/org/dllearner/refinementoperators/fuzzydll/

Modified: trunk/components-core/src/main/java/org/dllearner/algorithms/fuzzydll/FuzzyCELOE.java
===================================================================
--- trunk/components-core/src/main/java/org/dllearner/algorithms/fuzzydll/FuzzyCELOE.java	2011-08-30 12:13:54 UTC (rev 3170)
+++ trunk/components-core/src/main/java/org/dllearner/algorithms/fuzzydll/FuzzyCELOE.java	2011-08-30 15:17:02 UTC (rev 3171)
@@ -35,6 +35,7 @@
 import java.util.TreeSet;
 
 import org.apache.log4j.Logger;
+import org.dllearner.algorithms.celoe.OEHeuristicRuntime;
 import org.dllearner.core.AbstractCELA;
 import org.dllearner.core.ComponentInitException;
 import org.dllearner.core.EvaluatedDescription;
@@ -60,10 +61,10 @@
 import org.dllearner.learningproblems.PosOnlyLP;
 import org.dllearner.learningproblems.fuzzydll.FuzzyPosNegLP;
 import org.dllearner.learningproblems.fuzzydll.FuzzyPosNegLPStandard;
+import org.dllearner.refinementoperators.FuzzyRhoDRDown;
 import org.dllearner.refinementoperators.OperatorInverter;
 import org.dllearner.refinementoperators.RefinementOperator;
 import org.dllearner.refinementoperators.RhoDRDown;
-import org.dllearner.refinementoperators.fuzzydll.FuzzyRhoDRDown;
 import org.dllearner.utilities.Files;
 import org.dllearner.utilities.Helper;
 import org.dllearner.utilities.owl.ConceptComparator;
@@ -71,6 +72,7 @@
 import org.dllearner.utilities.owl.DescriptionMinimizer;
 import org.dllearner.utilities.owl.EvaluatedDescriptionSet;
 import org.dllearner.utilities.owl.PropertyContext;
+import org.springframework.beans.factory.annotation.Autowired;
 
 import com.jamonapi.Monitor;
 import com.jamonapi.MonitorFactory;
@@ -86,7 +88,7 @@
 public class FuzzyCELOE extends AbstractCELA implements FuzzyClassExpressionLearningAlgorithm {
 
 	private static Logger logger = Logger.getLogger(FuzzyCELOE.class);
-	private FuzzyCELOEConfigurator configurator;
+//	private FuzzyCELOEConfigurator configurator;
 	
 	private boolean isRunning = false;
 	private boolean stop = false;	
@@ -130,7 +132,6 @@
 	
 	// important parameters
 	private double noise;
-	private double maxDepth;
 	private boolean filterFollowsFromKB;	
 	
 	// less important parameters
@@ -154,13 +155,47 @@
 //	private PrintWriter out;
 //	private long start = 0;
 	
-	public FuzzyCELOEConfigurator getConfigurator() {
-		return configurator;
+	// TODO: turn those into config options
+	
+	// important: do not initialise those with empty sets
+	// null = no settings for allowance / ignorance
+	// empty set = allow / ignore nothing (it is often not desired to allow no class!)
+	Set<NamedClass> allowedConcepts = null;
+	Set<NamedClass> ignoredConcepts = null;
+
+	private boolean writeSearchTree = false;
+
+	private String searchTreeFile = "log/searchTree.txt";
+
+	private int maxNrOfResults = 10;
+
+	private double noisePercentage = 0.0;
+
+	private boolean filterDescriptionsFollowingFromKB = false;
+
+	private boolean reuseExistingDescription = false;
+
+	private boolean replaceSearchTree = false;
+
+	private int maxClassDescriptionTests = 0;
+
+	private int maxExecutionTimeInSeconds = 100;
+
+	private boolean terminateOnNoiseReached = false;
+	
+	private double maxDepth = 7;	
+	
+	public FuzzyCELOE() {
+		
 	}
 	
+//	public FuzzyCELOEConfigurator getConfigurator() {
+//		return configurator;
+//	}
+	
 	public FuzzyCELOE(AbstractLearningProblem problem, AbstractReasonerComponent reasoner) {
 		super(problem, reasoner);
-		configurator = new FuzzyCELOEConfigurator(this);
+//		configurator = new FuzzyCELOEConfigurator(this);
 	}
 
 	public static Collection<Class<? extends AbstractLearningProblem>> supportedLearningProblems() {
@@ -206,68 +241,72 @@
 	@Override
 	public void init() throws ComponentInitException {
 		
-		// TODO: remove, just for testing purposes
-//		FileWriter fstream;
-//		try {			
-//			fstream = new FileWriter("../examples/fuzzydll/kk.log");
-//			out = new PrintWriter(fstream);
-//		} catch (IOException e) {
-//			// TODO Auto-generated catch block
-//			e.printStackTrace();
-//		}
+		// compute used concepts/roles from allowed/ignored
+		// concepts/roles
+		Set<NamedClass> usedConcepts;
+//		Set<NamedClass> allowedConcepts = configurator.getAllowedConcepts()==null ? null : CommonConfigMappings.getAtomicConceptSet(configurator.getAllowedConcepts());
+//		Set<NamedClass> ignoredConcepts = configurator.getIgnoredConcepts()==null ? null : CommonConfigMappings.getAtomicConceptSet(configurator.getIgnoredConcepts());
+		if(allowedConcepts != null) {
+			// sanity check to control if no non-existing concepts are in the list
+			Helper.checkConcepts(reasoner, allowedConcepts);
+			usedConcepts = allowedConcepts;
+		} else if(ignoredConcepts != null) {
+			usedConcepts = Helper.computeConceptsUsingIgnoreList(reasoner, ignoredConcepts);
+		} else {
+			usedConcepts = Helper.computeConcepts(reasoner);
+		}
 		
 		// copy class hierarchy and modify it such that each class is only
 		// reachable via a single path
-		ClassHierarchy classHierarchy = reasoner.getClassHierarchy().clone();
+//		ClassHierarchy classHierarchy = reasoner.getClassHierarchy().clone();
+		ClassHierarchy classHierarchy = reasoner.getClassHierarchy().cloneAndRestrict(usedConcepts);
 		classHierarchy.thinOutSubsumptionHierarchy();
+
+		// if no one injected a heuristic, we use a default one
+		if(heuristic == null) {
+			heuristic = new FuzzyOEHeuristicRuntime();
+		}
 		
-		heuristic = new FuzzyOEHeuristicRuntime(configurator);
-		
 		minimizer = new DescriptionMinimizer(reasoner);
 		
 		startClass = Thing.instance;
 		
-		singleSuggestionMode = configurator.getSingleSuggestionMode();
+//		singleSuggestionMode = configurator.getSingleSuggestionMode();
 		
-		// TODO: 1. turn those into instance variables / fields 2. provide getters/setters; 
-		// 3. annotate them with @ConfigOption => this all needs to be done in FuzzyRhoDRDown,
-		// not in this class
-		boolean useExistsConstructor = true;
-		int valueFrequencyThreshold = 2;
-		boolean useCardinalityRestrictions = false;
-		int cardinalityLimit = 1;
-		boolean useHasValueConstructor = false;
-		boolean useNegation = true;
-		boolean useStringDatatypes = false;
-		boolean useBooleanDatatypes = false;
-		boolean useDoubleDatatypes = false;
-		boolean instanceBasedDisjoints = true;
-		boolean applyAllFilter = true;
-		boolean applyExistsFilter = true;
-		boolean useAllConstructor = true;
-
 		// create refinement operator
-		operator = new FuzzyRhoDRDown(reasoner, classHierarchy, cardinalityLimit, useHasValueConstructor, useStringDatatypes, instanceBasedDisjoints, applyAllFilter, applyExistsFilter, useAllConstructor,
-				useExistsConstructor, valueFrequencyThreshold, useCardinalityRestrictions, useNegation, useBooleanDatatypes, useDoubleDatatypes, (NamedClass) startClass);
+		if(operator == null) {
+			operator = new RhoDRDown();
+			((RhoDRDown)operator).setStartClass(startClass);
+			((RhoDRDown)operator).setSubHierarchy(classHierarchy);
+			((RhoDRDown)operator).setReasoner(reasoner);
+			((RhoDRDown)operator).init();
+		}
+//		operator = new RhoDRDown(reasoner, classHierarchy, startClass, configurator);
 		baseURI = reasoner.getBaseURI();
 		prefixes = reasoner.getPrefixes();		
-		if(configurator.getWriteSearchTree()) {
-			Files.clearFile(new File(configurator.getSearchTreeFile()));
+		if(writeSearchTree) {
+			File f = new File(searchTreeFile );
+			Files.clearFile(f);
 		}
 		
-		bestEvaluatedDescriptions = new EvaluatedDescriptionSet(configurator.getMaxNrOfResults());
+		bestEvaluatedDescriptions = new EvaluatedDescriptionSet(maxNrOfResults);
 		
 		isClassLearningProblem = (learningProblem instanceof ClassLearningProblem);
 		
 		// we put important parameters in class variables
-		noise = configurator.getNoisePercentage()/100d;
+		noise = noisePercentage/100d;
 //		System.out.println("noise " + noise);
-		maxDepth = configurator.getMaxDepth();
+//		maxDepth = configurator.getMaxDepth();
 		// (filterFollowsFromKB is automatically set to false if the problem
 		// is not a class learning problem
-		filterFollowsFromKB = configurator.getFilterDescriptionsFollowingFromKB()
-		  && isClassLearningProblem;
+		filterFollowsFromKB = filterDescriptionsFollowingFromKB && isClassLearningProblem;
 		
+//		Set<Description> concepts = operator.refine(Thing.instance, 5);
+//		for(Description concept : concepts) {
+//			System.out.println(concept);
+//		}
+//		System.out.println("refinements of thing: " + concepts.size());
+		
 		// actions specific to ontology engineering
 		if(isClassLearningProblem) {
 			ClassLearningProblem problem = (ClassLearningProblem) learningProblem;
@@ -281,7 +320,7 @@
 			// superfluous to add super classes in this case)
 			if(isEquivalenceProblem) {
 				Set<Description> existingDefinitions = reasoner.getAssertedDefinitions(classToDescribe);
-				if(configurator.getReuseExistingDescription() && (existingDefinitions.size() > 0)) {
+				if(reuseExistingDescription && (existingDefinitions.size() > 0)) {
 					// the existing definition is reused, which in the simplest case means to
 					// use it as a start class or, if it is already too specific, generalise it
 					
@@ -344,7 +383,7 @@
 								"sensible to learn a description in this case.");
 					}					
 				}
-			}				
+			}					
 		} else if(learningProblem instanceof PosOnlyLP) {
 			examples = ((PosOnlyLP)learningProblem).getPositiveExamples();
 		// changed by Josue
@@ -457,7 +496,7 @@
 			updateMinMaxHorizExp(nextNode);
 			
 			// writing the search tree (if configured)
-			if (configurator.getWriteSearchTree()) {
+			if (writeSearchTree) {
 				String treeString = "best node: " + bestEvaluatedDescriptions.getBest() + "\n";
 				if (refinements.size() > 1) {
 					treeString += "all expanded nodes:\n";
@@ -468,10 +507,10 @@
 				treeString += startNode.toTreeString(baseURI);
 				treeString += "\n";
 
-				if (configurator.getReplaceSearchTree())
-					Files.createFile(new File(configurator.getSearchTreeFile()), treeString);
+				if (replaceSearchTree)
+					Files.createFile(new File(searchTreeFile), treeString);
 				else
-					Files.appendFile(new File(configurator.getSearchTreeFile()), treeString);
+					Files.appendFile(new File(searchTreeFile), treeString);
 			}
 			
 //			System.out.println(loop);
@@ -758,9 +797,9 @@
 	private boolean terminationCriteriaSatisfied() {
 		return 
 		stop || 
-		(configurator.getMaxClassDescriptionTests() != 0 && (expressionTests >= configurator.getMaxClassDescriptionTests())) ||
-		(configurator.getMaxExecutionTimeInSeconds() != 0 && ((System.nanoTime() - nanoStartTime) >= (configurator.getMaxExecutionTimeInSeconds()*1000000000l))) ||
-		(configurator.getTerminateOnNoiseReached() && (100*getCurrentlyBestAccuracy()>100-configurator.getNoisePercentage()));
+		(maxClassDescriptionTests != 0 && (expressionTests >= maxClassDescriptionTests)) ||
+		(maxExecutionTimeInSeconds != 0 && ((System.nanoTime() - nanoStartTime) >= (maxExecutionTimeInSeconds*1000000000l))) ||
+		(terminateOnNoiseReached && (100*getCurrentlyBestAccuracy()>=100-noisePercentage));
 	}
 	
 	private void reset() {
@@ -860,13 +899,6 @@
 	public int getMinimumHorizontalExpansion() {
 		return minHorizExp;
 	}
-	
-	/**
-	 * @return the expressionTests
-	 */
-	public int getClassExpressionTests() {
-		return expressionTests;
-	}
 
 	// added by Josue (when implementing FuzzyClassExpressionLearningAlgorithm)
 
@@ -881,5 +913,128 @@
 			int nrOfDescriptions) {
 		// TODO Auto-generated method stub
 		return null;
+	}
+	
+
+	/**
+	 * @return the expressionTests
+	 */
+	public int getClassExpressionTests() {
+		return expressionTests;
+	}
+
+	public RefinementOperator getOperator() {
+		return operator;
+	}
+
+	@Autowired(required=false)
+	public void setOperator(RefinementOperator operator) {
+		this.operator = operator;
+	}
+
+	public Description getStartClass() {
+		return startClass;
+	}
+
+	public void setStartClass(Description startClass) {
+		this.startClass = startClass;
+	}
+
+	public Set<NamedClass> getAllowedConcepts() {
+		return allowedConcepts;
+	}
+
+	public void setAllowedConcepts(Set<NamedClass> allowedConcepts) {
+		this.allowedConcepts = allowedConcepts;
+	}
+
+	public Set<NamedClass> getIgnoredConcepts() {
+		return ignoredConcepts;
+	}
+
+	public void setIgnoredConcepts(Set<NamedClass> ignoredConcepts) {
+		this.ignoredConcepts = ignoredConcepts;
+	}
+
+	public boolean isWriteSearchTree() {
+		return writeSearchTree;
+	}
+
+	public void setWriteSearchTree(boolean writeSearchTree) {
+		this.writeSearchTree = writeSearchTree;
+	}
+
+	public String getSearchTreeFile() {
+		return searchTreeFile;
+	}
+
+	public void setSearchTreeFile(String searchTreeFile) {
+		this.searchTreeFile = searchTreeFile;
+	}
+
+	public int getMaxNrOfResults() {
+		return maxNrOfResults;
+	}
+
+	public void setMaxNrOfResults(int maxNrOfResults) {
+		this.maxNrOfResults = maxNrOfResults;
+	}
+
+	public double getNoisePercentage() {
+		return noisePercentage;
+	}
+
+	public void setNoisePercentage(double noisePercentage) {
+		this.noisePercentage = noisePercentage;
+	}
+
+	public boolean isFilterDescriptionsFollowingFromKB() {
+		return filterDescriptionsFollowingFromKB;
+	}
+
+	public void setFilterDescriptionsFollowingFromKB(boolean filterDescriptionsFollowingFromKB) {
+		this.filterDescriptionsFollowingFromKB = filterDescriptionsFollowingFromKB;
+	}
+
+	public boolean isReplaceSearchTree() {
+		return replaceSearchTree;
+	}
+
+	public void setReplaceSearchTree(boolean replaceSearchTree) {
+		this.replaceSearchTree = replaceSearchTree;
+	}
+
+	public int getMaxClassDescriptionTests() {
+		return maxClassDescriptionTests;
+	}
+
+	public void setMaxClassDescriptionTests(int maxClassDescriptionTests) {
+		this.maxClassDescriptionTests = maxClassDescriptionTests;
+	}
+
+	public int getMaxExecutionTimeInSeconds() {
+		return maxExecutionTimeInSeconds;
+	}
+
+	public void setMaxExecutionTimeInSeconds(int maxExecutionTimeInSeconds) {
+		this.maxExecutionTimeInSeconds = maxExecutionTimeInSeconds;
+	}
+
+	public boolean isTerminateOnNoiseReached() {
+		return terminateOnNoiseReached;
+	}
+
+	public void setTerminateOnNoiseReached(boolean terminateOnNoiseReached) {
+		this.terminateOnNoiseReached = terminateOnNoiseReached;
+	}
+
+	public boolean isReuseExistingDescription() {
+		return reuseExistingDescription;
+	}
+
+	public void setReuseExistingDescription(boolean reuseExistingDescription) {
+		this.reuseExistingDescription = reuseExistingDescription;
 	}	
+		
+	
 }

Modified: trunk/components-core/src/main/java/org/dllearner/algorithms/fuzzydll/FuzzyOEHeuristicRuntime.java
===================================================================
--- trunk/components-core/src/main/java/org/dllearner/algorithms/fuzzydll/FuzzyOEHeuristicRuntime.java	2011-08-30 12:13:54 UTC (rev 3170)
+++ trunk/components-core/src/main/java/org/dllearner/algorithms/fuzzydll/FuzzyOEHeuristicRuntime.java	2011-08-30 15:17:02 UTC (rev 3171)
@@ -44,8 +44,8 @@
 	// syntactic comparison as final comparison criterion
 	private ConceptComparator conceptComparator = new ConceptComparator();
 	
-	public FuzzyOEHeuristicRuntime(FuzzyCELOEConfigurator configurator) {
-		expansionPenaltyFactor = configurator.getExpansionPenaltyFactor();
+	public FuzzyOEHeuristicRuntime() {
+//		expansionPenaltyFactor = configurator.getExpansionPenaltyFactor();
 	}
 	
 	@Override
@@ -81,7 +81,29 @@
 		return score;
 	}
 
+
 	public double getExpansionPenaltyFactor() {
 		return expansionPenaltyFactor;
+	}
+
+	public double getGainBonusFactor() {
+		return gainBonusFactor;
+	}
+
+	public void setGainBonusFactor(double gainBonusFactor) {
+		this.gainBonusFactor = gainBonusFactor;
+	}
+
+	public double getNodeRefinementPenalty() {
+		return nodeRefinementPenalty;
+	}
+
+	public void setNodeRefinementPenalty(double nodeRefinementPenalty) {
+		this.nodeRefinementPenalty = nodeRefinementPenalty;
+	}
+
+	public void setExpansionPenaltyFactor(double expansionPenaltyFactor) {
+		this.expansionPenaltyFactor = expansionPenaltyFactor;
 	}	
+		
 }

Copied: trunk/components-core/src/main/java/org/dllearner/refinementoperators/FuzzyRhoDRDown.java (from rev 3167, trunk/components-core/src/main/java/org/dllearner/refinementoperators/fuzzydll/FuzzyRhoDRDown.java)
===================================================================
--- trunk/components-core/src/main/java/org/dllearner/refinementoperators/FuzzyRhoDRDown.java	                        (rev 0)
+++ trunk/components-core/src/main/java/org/dllearner/refinementoperators/FuzzyRhoDRDown.java	2011-08-30 15:17:02 UTC (rev 3171)
@@ -0,0 +1,1673 @@
+/**
+ * Copyright (C) 2007-2011, Jens Lehmann
+ *
+ * This file is part of DL-Learner.
+ *
+ * DL-Learner is free software; you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation; either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * DL-Learner is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+package org.dllearner.refinementoperators;
+
+import java.util.Collection;
+import java.util.Collections;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Iterator;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.Map;
+import java.util.Map.Entry;
+import java.util.Set;
+import java.util.SortedSet;
+import java.util.TreeMap;
+import java.util.TreeSet;
+
+import org.apache.log4j.Logger;
+import org.dllearner.core.AbstractReasonerComponent;
+import org.dllearner.core.config.BooleanEditor;
+import org.dllearner.core.config.ConfigOption;
+import org.dllearner.core.options.CommonConfigOptions;
+import org.dllearner.core.owl.BooleanValueRestriction;
+import org.dllearner.core.owl.ClassHierarchy;
+import org.dllearner.core.owl.Constant;
+import org.dllearner.core.owl.DataRange;
+import org.dllearner.core.owl.DatatypeProperty;
+import org.dllearner.core.owl.DatatypeSomeRestriction;
+import org.dllearner.core.owl.Description;
+import org.dllearner.core.owl.DoubleMaxValue;
+import org.dllearner.core.owl.DoubleMinValue;
+import org.dllearner.core.owl.Individual;
+import org.dllearner.core.owl.Intersection;
+import org.dllearner.core.owl.NamedClass;
+import org.dllearner.core.owl.Negation;
+import org.dllearner.core.owl.Nothing;
+import org.dllearner.core.owl.ObjectAllRestriction;
+import org.dllearner.core.owl.ObjectCardinalityRestriction;
+import org.dllearner.core.owl.ObjectMaxCardinalityRestriction;
+import org.dllearner.core.owl.ObjectMinCardinalityRestriction;
+import org.dllearner.core.owl.ObjectProperty;
+import org.dllearner.core.owl.ObjectPropertyExpression;
+import org.dllearner.core.owl.ObjectQuantorRestriction;
+import org.dllearner.core.owl.ObjectSomeRestriction;
+import org.dllearner.core.owl.ObjectValueRestriction;
+import org.dllearner.core.owl.StringValueRestriction;
+import org.dllearner.core.owl.Thing;
+import org.dllearner.core.owl.Union;
+import org.dllearner.core.owl.fuzzydll.FuzzyIndividual;
+import org.dllearner.utilities.Helper;
+import org.dllearner.utilities.owl.ConceptComparator;
+import org.dllearner.utilities.owl.ConceptTransformation;
+import org.springframework.beans.factory.annotation.Autowired;
+
+/**
+ * A downward refinement operator, which makes use of domains
+ * and ranges of properties. The operator is currently under
+ * development. Its aim is to span a much "cleaner" and smaller search
+ * tree compared to RhoDown by omitting many class descriptions,
+ * which are obviously too weak, because they violate 
+ * domain/range restrictions. Furthermore, it makes use of disjoint
+ * classes in the knowledge base.
+ * 
+ * TODO Some of the code has moved to {@link Utility} in a modified
+ * form to make it accessible for implementations of other refinement
+ * operators. These utility methods may be completed and carefully
+ * integrated back later. 
+ * 
+ * @author Jens Lehmann
+ *
+ */
+public class FuzzyRhoDRDown extends RefinementOperatorAdapter {
+
+	private static Logger logger = Logger
+	.getLogger(FuzzyRhoDRDown.class);	
+	
+	private AbstractReasonerComponent reasoner;
+	
+	// hierarchies
+	private ClassHierarchy subHierarchy;
+	
+	// domains and ranges
+	private Map<ObjectProperty,Description> opDomains = new TreeMap<ObjectProperty,Description>();
+	private Map<DatatypeProperty,Description> dpDomains = new TreeMap<DatatypeProperty,Description>();
+	private Map<ObjectProperty,Description> opRanges = new TreeMap<ObjectProperty,Description>();
+	
+	// maximum number of fillers for eeach role
+	private Map<ObjectProperty,Integer> maxNrOfFillers = new TreeMap<ObjectProperty,Integer>();
+	// limit for cardinality restrictions (this makes sense if we e.g. have compounds with up to
+	// more than 200 atoms but we are only interested in atoms with certain characteristics and do
+	// not want something like e.g. >= 204 hasAtom.NOT Carbon-87; which blows up the search space
+	private int cardinalityLimit = 5;
+	
+	// start concept (can be used to start from an arbitrary concept, needs
+	// to be Thing or NamedClass), note that when you use e.g. Compound as 
+	// start class, then the algorithm should start the search with class
+	// Compound (and not with Thing), because otherwise concepts like
+	// NOT Carbon-87 will be returned which itself is not a subclass of Compound
+	private Description startClass = new Thing();
+	
+	// the length of concepts of top refinements, the first values is
+	// for refinements of \rho_\top(\top), the second one for \rho_A(\top)
+	private int topRefinementsLength = 0;
+	private Map<NamedClass, Integer> topARefinementsLength = new TreeMap<NamedClass, Integer>();
+	// M is finite and this value is the maximum length of any value in M
+	private static int mMaxLength = 4;
+	
+	// the sets M_\top and M_A
+	private Map<Integer,SortedSet<Description>> m = new TreeMap<Integer,SortedSet<Description>>();
+	private Map<NamedClass,Map<Integer,SortedSet<Description>>> mA = new TreeMap<NamedClass,Map<Integer,SortedSet<Description>>>();
+	
+	// @see MathOperations.getCombos
+	private Map<Integer, List<List<Integer>>> combos = new HashMap<Integer, List<List<Integer>>>();
+
+	// refinements of the top concept ordered by length
+	private Map<Integer, SortedSet<Description>> topRefinements = new TreeMap<Integer, SortedSet<Description>>();
+	private Map<NamedClass,Map<Integer, SortedSet<Description>>> topARefinements = new TreeMap<NamedClass,Map<Integer, SortedSet<Description>>>();
+	
+	// cumulated refinements of top (all from length one to the specified length)
+	private Map<Integer, TreeSet<Description>> topRefinementsCumulative = new HashMap<Integer, TreeSet<Description>>();
+	private Map<NamedClass,Map<Integer, TreeSet<Description>>> topARefinementsCumulative = new TreeMap<NamedClass,Map<Integer, TreeSet<Description>>>();
+	
+	// app_A set of applicable properties for a given class (separate for
+	// object properties, boolean datatypes, and double datatypes)
+	private Map<NamedClass, Set<ObjectProperty>> appOP = new TreeMap<NamedClass, Set<ObjectProperty>>();
+	private Map<NamedClass, Set<DatatypeProperty>> appBD = new TreeMap<NamedClass, Set<DatatypeProperty>>();
+	private Map<NamedClass, Set<DatatypeProperty>> appDD = new TreeMap<NamedClass, Set<DatatypeProperty>>();
+	
+	// most general applicable properties
+	private Map<NamedClass,Set<ObjectProperty>> mgr = new TreeMap<NamedClass,Set<ObjectProperty>>();
+	private Map<NamedClass,Set<DatatypeProperty>> mgbd = new TreeMap<NamedClass,Set<DatatypeProperty>>();
+	private Map<NamedClass,Set<DatatypeProperty>> mgdd = new TreeMap<NamedClass,Set<DatatypeProperty>>();
+	private Map<NamedClass,Set<DatatypeProperty>> mgsd = new TreeMap<NamedClass,Set<DatatypeProperty>>();
+	
+	// concept comparator
+	private ConceptComparator conceptComparator = new ConceptComparator();
+	
+	// splits for double datatype properties in ascening order
+	private Map<DatatypeProperty,List<Double>> splits = new TreeMap<DatatypeProperty,List<Double>>();
+	private int maxNrOfSplits = 10;
+	
+	// data structure for a simple frequent pattern matching preprocessing phase
+	private int frequencyThreshold = CommonConfigOptions.valueFrequencyThresholdDefault;
+	private Map<ObjectProperty, Map<Individual, Integer>> valueFrequency = new HashMap<ObjectProperty, Map<Individual, Integer>>();
+	// data structure with identified frequent values
+	private Map<ObjectProperty, Set<Individual>> frequentValues = new HashMap<ObjectProperty, Set<Individual>>();	
+	// frequent data values
+	private Map<DatatypeProperty, Set<Constant>> frequentDataValues = new HashMap<DatatypeProperty, Set<Constant>>();	
+	private Map<DatatypeProperty, Map<Constant, Integer>> dataValueFrequency = new HashMap<DatatypeProperty, Map<Constant, Integer>>();		
+	private boolean useDataHasValueConstructor = false;
+	
+	// staistics
+	public long mComputationTimeNs = 0;
+	public long topComputationTimeNs = 0;
+
+	@ConfigOption(name = "applyAllFilter", defaultValue="true", propertyEditorClass = BooleanEditor.class)
+	private boolean applyAllFilter = true;
+	
+	@ConfigOption(name = "applyExistsFilter", defaultValue="true", propertyEditorClass = BooleanEditor.class)
+	private boolean applyExistsFilter = true;
+	
+	@ConfigOption(name = "useAllConstructor", defaultValue="true", propertyEditorClass = BooleanEditor.class)
+	private boolean useAllConstructor = true;
+	
+	@ConfigOption(name = "useExistsConstructor", defaultValue="true", propertyEditorClass = BooleanEditor.class)
+	private boolean useExistsConstructor = true;
+	
+	@ConfigOption(name = "useHasValueConstructor", defaultValue="false", propertyEditorClass = BooleanEditor.class)
+	private boolean useHasValueConstructor = false;
+	
+	@ConfigOption(name = "useCardinalityRestrictions", defaultValue="true", propertyEditorClass = BooleanEditor.class)
+	private boolean useCardinalityRestrictions = true;
+	
+	@ConfigOption(name = "useNegation", defaultValue="true", propertyEditorClass = BooleanEditor.class)
+	private boolean useNegation = true;
+	
+	@ConfigOption(name = "useBooleanDatatypes", defaultValue="true", propertyEditorClass = BooleanEditor.class)
+	private boolean useBooleanDatatypes = true;
+	
+	@ConfigOption(name = "useDoubleDatatypes", defaultValue="true", propertyEditorClass = BooleanEditor.class)
+	private boolean useDoubleDatatypes = true;
+	
+	@ConfigOption(name = "useStringDatatypes", defaultValue="false", propertyEditorClass = BooleanEditor.class)
+	private boolean useStringDatatypes = false;
+	
+	@ConfigOption(name = "disjointChecks", defaultValue="true", propertyEditorClass = BooleanEditor.class)
+	private boolean disjointChecks = true;
+	
+	@ConfigOption(name = "instanceBasedDisjoints", defaultValue="true", propertyEditorClass = BooleanEditor.class)
+	private boolean instanceBasedDisjoints = true;
+	
+	@ConfigOption(name = "dropDisjuncts", defaultValue="false", propertyEditorClass = BooleanEditor.class)
+	private boolean dropDisjuncts = false;	
+	
+	// caches for reasoner queries
+	private Map<Description,Map<Description,Boolean>> cachedDisjoints = new TreeMap<Description,Map<Description,Boolean>>(conceptComparator);
+
+//	private Map<NamedClass,Map<NamedClass,Boolean>> abDisjoint = new TreeMap<NamedClass,Map<NamedClass,Boolean>>();
+//	private Map<NamedClass,Map<NamedClass,Boolean>> notABDisjoint = new TreeMap<NamedClass,Map<NamedClass,Boolean>>();
+//	private Map<NamedClass,Map<NamedClass,Boolean>> notABMeaningful = new TreeMap<NamedClass,Map<NamedClass,Boolean>>();
+	
+	public FuzzyRhoDRDown(AbstractReasonerComponent reasoningService) {
+//		this(reasoningService, reasoningService.getClassHierarchy(), null, true, true, true, true, true, 3, true, true, true, true, null);
+		this.reasoner = reasoningService;
+		this.subHierarchy = reasoner.getClassHierarchy();
+		init();
+	}
+	
+//	public FuzzyRhoDRDown(AbstractReasonerComponent reasoner, ClassHierarchy subHierarchy, Description startClass, RefinementOperatorConfigurator configurator) {
+//		this.rs = reasoner;
+//		this.subHierarchy = subHierarchy;
+//		this.startClass = startClass;
+//		useAllConstructor = configurator.getUseAllConstructor();
+//		useExistsConstructor = configurator.getUseExistsConstructor();
+//		useHasValueConstructor = configurator.getUseHasValueConstructor();
+//		setUseDataHasValueConstructor(configurator.getUseDataHasValueConstructor());
+//		frequencyThreshold = configurator.getValueFrequencyThreshold();
+//		useCardinalityRestrictions = configurator.getUseCardinalityRestrictions();
+//		cardinalityLimit = configurator.getCardinalityLimit();
+//		useNegation = configurator.getUseNegation();
+//		useBooleanDatatypes = configurator.getUseBooleanDatatypes();
+//		useDoubleDatatypes = configurator.getUseDoubleDatatypes();
+//		useStringDatatypes = configurator.getUseStringDatatypes();
+//		init();
+//	}
+//	
+
+	// the goal is to use the configurator system while still being flexible enough to
+	// use one refinement operator in several learning algorithms
+	public FuzzyRhoDRDown(AbstractReasonerComponent reasoningService, ClassHierarchy subHierarchy, int cardinalityLimit, boolean useHasValueConstructor, boolean useStringDatatypes, boolean instanceBasedDisjoints, boolean applyAllFilter, boolean applyExistsFilter, boolean useAllConstructor,
+			boolean useExistsConstructor, int valueFrequencyThreshold, boolean useCardinalityRestrictions,boolean useNegation, boolean useBooleanDatatypes, boolean useDoubleDatatypes, NamedClass startClass) {
+		this.reasoner = reasoningService;
+		this.subHierarchy = subHierarchy;
+		this.applyAllFilter = applyAllFilter;
+		this.applyExistsFilter = applyExistsFilter;
+		this.useAllConstructor = useAllConstructor;
+		this.useExistsConstructor = useExistsConstructor;
+		this.useHasValueConstructor = useHasValueConstructor;
+		this.frequencyThreshold = valueFrequencyThreshold;
+		this.useCardinalityRestrictions = useCardinalityRestrictions;
+		this.cardinalityLimit = cardinalityLimit;
+		this.useNegation = useNegation;
+		this.useBooleanDatatypes = useBooleanDatatypes;
+		this.useDoubleDatatypes = useDoubleDatatypes;
+		this.useStringDatatypes = useStringDatatypes;
+		this.instanceBasedDisjoints = instanceBasedDisjoints;
+		if(startClass != null) {
+			this.startClass = startClass;
+		}
+		init();
+	}
+		
+//		subHierarchy = rs.getClassHierarchy();
+	public void init() {	
+		// query reasoner for domains and ranges
+		// (because they are used often in the operator)
+		for(ObjectProperty op : reasoner.getObjectProperties()) {
+			opDomains.put(op, reasoner.getDomain(op));
+			opRanges.put(op, reasoner.getRange(op));
+			
+			if(useHasValueConstructor) {
+				// init
+				Map<Individual, Integer> opMap = new TreeMap<Individual, Integer>();
+				valueFrequency.put(op, opMap);
+				
+				// sets ordered by corresponding individual (which we ignore)
+				Collection<SortedSet<Individual>> fillerSets = reasoner.getPropertyMembers(op).values();
+				for(SortedSet<Individual> fillerSet : fillerSets) {
+					for(Individual i : fillerSet) {
+//						System.out.println("op " + op + " i " + i);
+						Integer value = opMap.get(i);
+						
+						if(value != null) {
+							opMap.put(i, value+1);
+						} else {
+							opMap.put(i, 1);
+						}
+					}
+				}
+				
+				// keep only frequent patterns
+				Set<Individual> frequentInds = new TreeSet<Individual>();
+				for(Individual i : opMap.keySet()) {
+					if(opMap.get(i) >= frequencyThreshold) {
+						frequentInds.add(i);
+//						break;
+					}
+				}
+				frequentValues.put(op, frequentInds);
+				
+			}
+			
+		}
+		
+		for(DatatypeProperty dp : reasoner.getDatatypeProperties()) {
+			dpDomains.put(dp, reasoner.getDomain(dp));
+			
+			if(useDataHasValueConstructor) {
+				Map<Constant, Integer> dpMap = new TreeMap<Constant, Integer>();
+				dataValueFrequency.put(dp, dpMap);
+				
+				// sets ordered by corresponding individual (which we ignore)
+				Collection<SortedSet<Constant>> fillerSets = reasoner.getDatatypeMembers(dp).values();
+				for(SortedSet<Constant> fillerSet : fillerSets) {
+					for(Constant i : fillerSet) {
+//						System.out.println("op " + op + " i " + i);
+						Integer value = dpMap.get(i);
+						
+						if(value != null) {
+							dpMap.put(i, value+1);
+						} else {
+							dpMap.put(i, 1);
+						}
+					}
+				}
+				
+				// keep only frequent patterns
+				Set<Constant> frequentInds = new TreeSet<Constant>();
+				for(Constant i : dpMap.keySet()) {
+					if(dpMap.get(i) >= frequencyThreshold) {
+						logger.trace("adding value "+i+", because "+dpMap.get(i) +">="+frequencyThreshold);
+						frequentInds.add(i);
+					}
+				}
+				frequentDataValues.put(dp, frequentInds);				
+			}
+		}
+		
+		// we do not need the temporary set anymore and let the
+		// garbage collector take care of it
+		valueFrequency = null;
+		dataValueFrequency = null;
+		
+		// compute splits for double datatype properties
+		for(DatatypeProperty dp : reasoner.getDoubleDatatypeProperties()) {
+			computeSplits(dp);
+		}
+		
+		// determine the maximum number of fillers for each role
+		// (up to a specified cardinality maximum)
+		if(useCardinalityRestrictions) {
+		for(ObjectProperty op : reasoner.getObjectProperties()) {
+			int maxFillers = 0;
+			Map<Individual,SortedSet<Individual>> opMembers = reasoner.getPropertyMembers(op);
+			for(SortedSet<Individual> inds : opMembers.values()) {
+				if(inds.size()>maxFillers)
+					maxFillers = inds.size();
+				if(maxFillers >= cardinalityLimit) {
+					maxFillers = cardinalityLimit;
+					break;
+				}	
+			}
+			maxNrOfFillers.put(op, maxFillers);
+		}
+		}
+		
+		/*
+		String conceptStr = "(\"http://dl-learner.org/carcinogenesis#Compound\" AND (>= 2 \"http://dl-learner.org/carcinogenesis#hasStructure\".\"http://dl-learner.org/carcinogenesis#Ar_halide\" OR ((\"http://dl-learner.org/carcinogenesis#amesTestPositive\" IS TRUE) AND >= 5 \"http://dl-learner.org/carcinogenesis#hasBond\". TOP)))";
+		try {
+			NamedClass struc = new NamedClass("http://dl-learner.org/carcinogenesis#Compound");
+			Description d = KBParser.parseConcept(conceptStr);
+			SortedSet<Description> ds = (SortedSet<Description>) refine(d,15,null,struc);
+			System.out.println(ds);
+			
+			Individual i = new Individual("http://dl-learner.org/carcinogenesis#d101");
+			rs.instanceCheck(ds.first(), i);
+			
+		} catch (ParseException e) {
+			// TODO Auto-generated catch block
+			e.printStackTrace();
+		}
+		System.exit(0);
+		*/
+		
+		/*
+		NamedClass struc = new NamedClass("http://dl-learner.org/carcinogenesis#Atom");
+		ObjectProperty op = new ObjectProperty("http://dl-learner.org/carcinogenesis#hasAtom");
+		ObjectSomeRestriction oar = new ObjectSomeRestriction(op,Thing.instance);
+
+		Set<Description> ds = refine(Thing.instance,3,null,struc);
+//		Set<Description> improper = new HashSet<Description>();
+		for(Description d : ds) {
+//			if(rs.subsumes(d, struc)) {
+//				improper.add(d);
+				System.out.println(d);
+//			}
+		}
+		System.out.println(ds.size());
+//		System.out.println(improper.size());
+		System.exit(0);
+		*/
+		 
+	}
+	
+	/* (non-Javadoc)
+	 * @see org.dllearner.algorithms.refinement.RefinementOperator#refine(org.dllearner.core.owl.Description)
+	 */
+	@Override
+	public Set<Description> refine(Description concept) {
+		throw new RuntimeException();
+	}
+
+	@Override
+	public Set<Description> refine(Description description, int maxLength) {
+		// check that maxLength is valid
+		if(maxLength < description.getLength()) {
+			throw new Error("length has to be at least description length (description: " + description + ", max length: " + maxLength + ")");
+		}
+		return refine(description, maxLength, null, startClass);
+	}
+	
+	/* (non-Javadoc)
+	 * @see org.dllearner.algorithms.refinement.RefinementOperator#refine(org.dllearner.core.owl.Description, int, java.util.List)
+	 */
+	@Override
+	public Set<Description> refine(Description description, int maxLength,
+			List<Description> knownRefinements) {
+		return refine(description, maxLength, knownRefinements, startClass);
+	}
+
+	@SuppressWarnings({"unchecked"})
+	public Set<Description> refine(Description description, int maxLength,
+			List<Description> knownRefinements, Description currDomain) {
+		
+//		System.out.println("|- " + description + " " + currDomain + " " + maxLength);
+		
+		// actions needing to be performed if this is the first time the
+		// current domain is used
+		if(!(currDomain instanceof Thing) && !topARefinementsLength.containsKey(currDomain))
+			topARefinementsLength.put((NamedClass)currDomain, 0);
+		
+		// check whether using list or set makes more sense 
+		// here; and whether HashSet or TreeSet should be used
+		// => TreeSet because duplicates are possible
+		Set<Description> refinements = new TreeSet<Description>(conceptComparator);
+		
+		// used as temporary variable
+		Set<Description> tmp = new HashSet<Description>();
+		
+		if(description instanceof Thing) {
+			// extends top refinements if necessary
+			if(currDomain instanceof Thing) {
+				if(maxLength>topRefinementsLength)
+					computeTopRefinements(maxLength);
+				refinements = (TreeSet<Description>) topRefinementsCumulative.get(maxLength).clone();
+			} else {
+				if(maxLength>topARefinementsLength.get(currDomain)) {
+					computeTopRefinements(maxLength, (NamedClass) currDomain);
+				}
+				refinements = (TreeSet<Description>) topARefinementsCumulative.get(currDomain).get(maxLength).clone();
+			}
+//			refinements.addAll(subHierarchy.getMoreSpecialConcepts(description));
+		} else if(description instanceof Nothing) {
+			// cannot be further refined
+		} else if(description instanceof NamedClass) {
+			refinements.addAll(subHierarchy.getSubClasses(description));
+			refinements.remove(new Nothing());
+		} else if (description instanceof Negation && description.getChild(0) instanceof NamedClass) {
+		
+			tmp = subHierarchy.getSuperClasses(description.getChild(0));
+				
+			for(Description c : tmp) {
+				if(!(c instanceof Thing))
+					refinements.add(new Negation(c));
+			}
+		
+		} else if (description instanceof Intersection) {
+				
+			// refine one of the elements
+			for(Description child : description.getChildren()) {
+				
+				// refine the child; the new max length is the current max length minus
+				// the currently considered concept plus the length of the child
+				// TODO: add better explanation
+				tmp = refine(child, maxLength - description.getLength()+child.getLength(),null,currDomain);
+				
+				// create new intersection
+				for(Description c : tmp) {
+					List<Description> newChildren = (List<Description>)((LinkedList<Description>)description.getChildren()).clone();
+					newChildren.add(c);
+					newChildren.remove(child);
+					Intersection mc = new Intersection(newChildren);
+					
+					// clean concept and transform it to ordered negation normal form
+					// (non-recursive variant because only depth 1 was modified)
+					ConceptTransformation.cleanConceptNonRecursive(mc);
+					ConceptTransformation.transformToOrderedNegationNormalFormNonRecursive(mc, conceptComparator);
+					
+					// check whether the intersection is OK (sanity checks), then add it
+					if(checkIntersection(mc))
+						refinements.add(mc);
+				}
+				
+			}
+				
+		} else if (description instanceof Union) {
+			// refine one of the elements
+			for(Description child : description.getChildren()) {
+				
+//				System.out.println("union child: " + child + " " + maxLength + " " + description.getLength() + " " + child.getLength());
+				
+				// refine child
+				tmp = refine(child, maxLength - description.getLength()+child.getLength(),null,currDomain);
+				
+				// construct intersection (see above)
+				for(Description c : tmp) {
+					List<Description> newChildren = new LinkedList<Description>(description.getChildren());
+					newChildren.remove(child);						
+					newChildren.add(c);
+					Union md = new Union(newChildren);
+						
+					// transform to ordered negation normal form
+					ConceptTransformation.transformToOrderedNegationNormalFormNonRecursive(md, conceptComparator);
+					// note that we do not have to call clean here because a disjunction will
+					// never be nested in another disjunction in this operator
+					
+					refinements.add(md);	
+				}
+				
+			}
+			
+			// if enabled, we can remove elements of the disjunction
+			if(dropDisjuncts) {
+				// A1 OR A2 => {A1,A2}
+				if(description.getChildren().size() == 2) {
+					refinements.add(description.getChild(0));
+					refinements.add(description.getChild(1));
+				} else {
+					// copy children list and remove a different element in each turn
+					for(int i=0; i<description.getChildren().size(); i++) {
+						List<Description> newChildren = new LinkedList<Description>(description.getChildren());
+						newChildren.remove(i);						
+						Union md = new Union(newChildren);
+						refinements.add(md);
+					}
+				}
+			}
+			
+		} else if (description instanceof ObjectSomeRestriction) {
+			ObjectPropertyExpression role = ((ObjectQuantorRestriction)description).getRole();
+			Description range = opRanges.get(role);
+			
+			// rule 1: EXISTS r.D => EXISTS r.E
+			tmp = refine(description.getChild(0), maxLength-2, null, range);
+
+			for(Description c : tmp)
+				refinements.add(new ObjectSomeRestriction(((ObjectQuantorRestriction)description).getRole(),c));
+			
+			// rule 2: EXISTS r.D => EXISTS s.D or EXISTS r^-1.D => EXISTS s^-1.D
+			// currently inverse roles are not supported
+			ObjectProperty ar = (ObjectProperty) role;
+			Set<ObjectProperty> moreSpecialRoles = reasoner.getSubProperties(ar);
+			for(ObjectProperty moreSpecialRole : moreSpecialRoles)
+				refinements.add(new ObjectSomeRestriction(moreSpecialRole, description.getChild(0)));
+
+			// rule 3: EXISTS r.D => >= 2 r.D
+			// (length increases by 1 so we have to check whether max length is sufficient)
+			if(useCardinalityRestrictions) {
+				if(maxLength > description.getLength() && maxNrOfFillers.get(ar)>1) {
+					ObjectMinCardinalityRestriction min = new ObjectMinCardinalityRestriction(2,role,description.getChild(0));
+					refinements.add(min);
+				}
+			}
+			
+			// rule 4: EXISTS r.TOP => EXISTS r.{value}
+			if(useHasValueConstructor && description.getChild(0) instanceof Thing) {
+				// watch out for frequent patterns
+				Set<Individual> frequentInds = frequentValues.get(role);
+				if(frequentInds != null) {
+					for(Individual ind : frequentInds) {
+						ObjectValueRestriction ovr = new ObjectValueRestriction((ObjectProperty)role, ind);
+						refinements.add(ovr);
+					}			
+				}
+			}
+			
+		} else if (description instanceof ObjectAllRestriction) {
+			ObjectPropertyExpression role = ((ObjectQuantorRestriction)description).getRole();
+			Description range = opRanges.get(role);
+			
+			// rule 1: ALL r.D => ALL r.E
+			tmp = refine(description.getChild(0), maxLength-2, null, range);
+
+			for(Description c : tmp) {
+				refinements.add(new ObjectAllRestriction(((ObjectQuantorRestriction)description).getRole(),c));
+			}		
+			
+			// rule 2: ALL r.D => ALL r.BOTTOM if D is a most specific atomic concept
+			if(description.getChild(0) instanceof NamedClass && tmp.size()==0) {
+				refinements.add(new ObjectAllRestriction(((ObjectQuantorRestriction)description).getRole(),new Nothing()));
+			}
+			
+			// rule 3: ALL r.D => ALL s.D or ALL r^-1.D => ALL s^-1.D
+			// currently inverse roles are not supported
+			ObjectProperty ar = (ObjectProperty) role;
+			Set<ObjectProperty> moreSpecialRoles = reasoner.getSubProperties(ar);
+			for(ObjectProperty moreSpecialRole : moreSpecialRoles) {
+				refinements.add(new ObjectAllRestriction(moreSpecialRole, description.getChild(0)));
+			}
+			
+			// rule 4: ALL r.D => <= (maxFillers-1) r.D
+			// (length increases by 1 so we have to check whether max length is sufficient)
+			// => commented out because this is acutally not a downward refinement
+//			if(useCardinalityRestrictions) {
+//				if(maxLength > description.getLength() && maxNrOfFillers.get(ar)>1) {
+//					ObjectMaxCardinalityRestriction max = new ObjectMaxCardinalityRestriction(maxNrOfFillers.get(ar)-1,role,description.getChild(0));
+//					refinements.add(max);
+//				}
+//			}
+		} else if (description instanceof ObjectCardinalityRestriction) {
+			ObjectPropertyExpression role = ((ObjectCardinalityRestriction)description).getRole();
+			Description range = opRanges.get(role);	
+			int number = ((ObjectCardinalityRestriction)description).getCardinality();
+			if(description instanceof ObjectMaxCardinalityRestriction) {
+				// rule 1: <= x r.C =>  <= x r.D
+				tmp = refine(description.getChild(0), maxLength-3, null, range);
+
+				for(Description d : tmp) {
+					refinements.add(new ObjectMaxCardinalityRestriction(number,role,d));
+				}				
+				
+				// rule 2: <= x r.C  =>  <= (x-1) r.C
+				ObjectMaxCardinalityRestriction max = (ObjectMaxCardinalityRestriction) description;
+//				int number = max.getNumber();
+				if(number > 1)
+					refinements.add(new ObjectMaxCardinalityRestriction(number-1,max.getRole(),max.getChild(0)));
+				
+			} else if(description instanceof ObjectMinCardinalityRestriction) {
+				tmp = refine(description.getChild(0), maxLength-3, null, range);
+
+				for(Description d : tmp) {
+					refinements.add(new ObjectMinCardinalityRestriction(number,role,d));
+				}
+				
+				// >= x r.C  =>  >= (x+1) r.C
+				ObjectMinCardinalityRestriction min = (ObjectMinCardinalityRestriction) description;
+//				int number = min.getNumber();
+				if(number < maxNrOfFillers.get(min.getRole()))
+					refinements.add(new ObjectMinCardinalityRestriction(number+1,min.getRole(),min.getChild(0)));				
+			}
+		} else if (description instanceof DatatypeSomeRestriction) {
+			
+			DatatypeSomeRestriction dsr = (DatatypeSomeRestriction) description;
+			DatatypeProperty dp = (DatatypeProperty) dsr.getRestrictedPropertyExpression();
+			DataRange dr = dsr.getDataRange();
+			if(dr instanceof DoubleMaxValue) {
+				double value = ((DoubleMaxValue)dr).getValue();
+				// find out which split value was used
+				int splitIndex = splits.get(dp).lastIndexOf(value);
+				if(splitIndex == -1)
+					throw new Error("split error");
+				int newSplitIndex = splitIndex - 1;
+				if(newSplitIndex >= 0) {
+					DoubleMaxValue max = new DoubleMaxValue(splits.get(dp).get(newSplitIndex));
+					DatatypeSomeRestriction newDSR = new DatatypeSomeRestriction(dp,max);
+					refinements.add(newDSR);
+//					System.out.println(description + " => " + newDSR);
+				}
+			} else if(dr instanceof DoubleMinValue) {
+				double value = ((DoubleMinValue)dr).getValue();
+				// find out which split value was used
+				int splitIndex = splits.get(dp).lastIndexOf(value);
+				if(splitIndex == -1)
+					throw new Error("split error");
+				int newSplitIndex = splitIndex + 1;
+				if(newSplitIndex < splits.get(dp).size()) {
+					DoubleMinValue min = new DoubleMinValue(splits.get(dp).get(newSplitIndex));
+					DatatypeSomeRestriction newDSR = new DatatypeSomeRestriction(dp,min);
+					refinements.add(newDSR);
+				}
+			}
+		} else if (description instanceof StringValueRestriction) {
+			StringValueRestriction svr = (StringValueRestriction) description;
+			DatatypeProperty dp = svr.getRestrictedPropertyExpression();
+			Set<DatatypeProperty> subDPs = reasoner.getSubProperties(dp);
+			for(DatatypeProperty subDP : subDPs) {
+				refinements.add(new StringValueRestriction(subDP, svr.getStringValue()));
+			}
+		}
+		
+		// if a refinement is not Bottom, Top, ALL r.Bottom a refinement of top can be appended
+		if(!(description instanceof Thing) && !(description instanceof Nothing) 
+				&& !(description instanceof ObjectAllRestriction && description.getChild(0) instanceof Nothing)) {
+			// -1 because of the AND symbol which is appended
+			int topRefLength = maxLength - description.getLength() - 1; 
+			
+			// maybe we have to compute new top refinements here
+			if(currDomain instanceof Thing) {
+				if(topRefLength > topRefinementsLength)
+					computeTopRefinements(topRefLength);
+			} else if(topRefLength > topARefinementsLength.get(currDomain))
+				computeTopRefinements(topRefLength,(NamedClass)currDomain);
+			
+			if(topRefLength>0) {
+				Set<Description> topRefs;
+				if(currDomain instanceof Thing)
+					topRefs = topRefinementsCumulative.get(topRefLength);
+				else
+					topRefs = topARefinementsCumulative.get(currDomain).get(topRefLength);
+				
+				for(Description c : topRefs) {
+					// true if refinement should be skipped due to filters,
+					// false otherwise
+					boolean skip = false;
+					
+					// if a refinement of of the form ALL r, we check whether ALL r
+					// does not occur already
+					if(applyAllFilter) {
+						if(c instanceof ObjectAllRestriction) {
+							for(Description child : description.getChildren()) {
+								if(child instanceof ObjectAllRestriction) {
+									ObjectPropertyExpression r1 = ((ObjectAllRestriction)c).getRole();
+									ObjectPropertyExpression r2 = ((ObjectAllRestriction)child).getRole();
+									if(r1.toString().equals(r2.toString()))
+										skip = true;
+								}
+							}
+						}
+					}
+					
+					// check for double datatype properties
+					/*
+					if(c instanceof DatatypeSomeRestriction && 
+							description instanceof DatatypeSomeRestriction) {
+						DataRange dr = ((DatatypeSomeRestriction)c).getDataRange();
+						DataRange dr2 = ((DatatypeSomeRestriction)description).getDataRange();
+						// it does not make sense to have statements like height >= 1.8 AND height >= 1.7
+						if((dr instanceof DoubleMaxValue && dr2 instanceof DoubleMaxValue)
+							||(dr instanceof DoubleMinValue && dr2 instanceof DoubleMinValue))
+							skip = true;
+					}*/
+					
+					// perform a disjointness check when named classes are added;
+					// this can avoid a lot of superfluous computation in the algorithm e.g.
+					// when A1 looks good, so many refinements of the form (A1 OR (A2 AND A3))
+					// are generated which are all equal to A1 due to disjointness of A2 and A3
+					if(disjointChecks && c instanceof NamedClass && description instanceof NamedClass && isDisjoint(description, c)) {
+						skip = true;
+//						System.out.println(c + " ignored when refining " + description);
+					}	
+					
+					if(!skip) {
+						Intersection mc = new Intersection();
+						mc.addChild(description);
+						mc.addChild(c);				
+						
+						// clean and transform to ordered negation normal form
+						ConceptTransformation.cleanConceptNonRecursive(mc);
+						ConceptTransformation.transformToOrderedNegationNormalFormNonRecursive(mc, conceptComparator);
+						
+						// last check before intersection is added
+						if(checkIntersection(mc))
+							refinements.add(mc);
+					}
+				}
+			}
+		}
+		
+//		for(Description refinement : refinements) {
+//			if((refinement instanceof Intersection || refinement instanceof Union) && refinement.getChildren().size()<2) {
+//				System.out.println(description + " " + refinement + " " + currDomain + " " + maxLength);
+//				System.exit(0);
+//			}
+//		}
+		
+		return refinements;		
+	}
+	
+	// when a child of an intersection is refined and reintegrated into the
+	// intersection, we can perform some sanity checks;
+	// method returns true if everything is OK and false otherwise
+	// TODO: can be implemented more efficiently if the newly added child
+	// is given as parameter
+	public static boolean checkIntersection(Intersection intersection) {
+		// rule 1: max. restrictions at most once
+		boolean maxDoubleOccurence = false;
+		// rule 2: min restrictions at most once
+		boolean minDoubleOccurence = false;
+		// rule 3: no double occurences of boolean datatypes
+		TreeSet<DatatypeProperty> occuredDP = new TreeSet<DatatypeProperty>();
+		// rule 4: no double occurences of hasValue restrictions
+		TreeSet<ObjectProperty> occuredVR = new TreeSet<ObjectProperty>();
+		
+		for(Description child : intersection.getChildren()) {
+			if(child instanceof DatatypeSomeRestriction) {
+				DataRange dr = ((DatatypeSomeRestriction)child).getDataRange();
+				if(dr instanceof DoubleMaxValue) {
+					if(maxDoubleOccurence)
+						return false;
+					else
+						maxDoubleOccurence = true;
+				} else if(dr instanceof DoubleMinValue) {
+					if(minDoubleOccurence)
+						return false;
+					else
+						minDoubleOccurence = true;
+				}		
+			} else if(child instanceof BooleanValueRestriction) {
+				DatatypeProperty dp = (DatatypeProperty) ((BooleanValueRestriction)child).getRestrictedPropertyExpression();
+//				System.out.println("dp: " + dp);
+				// return false if the boolean property exists already
+				if(!occuredDP.add(dp))
+					return false;
+			} else if(child instanceof ObjectValueRestriction) {
+				ObjectProperty op = (ObjectProperty) ((ObjectValueRestriction)child).getRestrictedPropertyExpression();
+				if(!occuredVR.add(op))
+					return false;
+			}
+//			System.out.println(child.getClass());
+		}
+		return true;
+	}
+	
+	/**
+	 * By default, the operator does not specialize e.g. (A or B) to A, because
+	 * it only guarantees weak completeness. Under certain circumstances, e.g.
+	 * refinement of a fixed given concept, it can be useful to allow such
+	 * refinements, which can be done by passing the parameter true to this method. 
+	 * @param dropDisjuncts Whether to remove disjuncts in refinement process.
+	 */
+	public void setDropDisjuncts(boolean dropDisjuncts) {
+		this.dropDisjuncts = dropDisjuncts;
+	}	
+	
+	private void computeTopRefinements(int maxLength) {
+		computeTopRefinements(maxLength, null);
+	}
+	
+	private void computeTopRefinements(int maxLength, NamedClass domain) {
+		long topComputationTimeStartNs = System.nanoTime();
+		
+		if(domain == null && m.size() == 0)
+			computeM();
+		
+		if(domain != null && !mA.containsKey(domain))
+			computeM(domain);
+		
+		int refinementsLength;
+		
+		if(domain == null) {
+			refinementsLength = topRefinementsLength;
+		} else {
+			if(!topARefinementsLength.containsKey(domain))
+				topARefinementsLength.put(domain,0);
+
+			refinementsLength = topARefinementsLength.get(domain);
+		}
+
+		// compute all possible combinations of the disjunction
+		for(int i = refinementsLength+1; i <= maxLength; i++) {
+			combos.put(i,MathOperations.getCombos(i, mMaxLength));
+
+			// initialise the refinements with empty sets
+			if(domain == null) {
+				topRefinements.put(i, new TreeSet<Description>(conceptComparator));
+			} else {
+				if(!topARefinements.containsKey(domain))
+					topARefinements.put(domain, new TreeMap<Integer,SortedSet<Description>>());
+				topARefinements.get(domain).put(i, new TreeSet<Description>(conceptComparator));
+			}
+				
+			for(List<Integer> combo : combos.get(i)) {
+				
+				// combination is a single number => try to use M
+				if(combo.size()==1) {
+					// note we cannot use "put" instead of "addAll" because there
+					// can be several combos for one length
+					if(domain == null)
+						topRefinements.get(i).addAll(m.get(i));
+					else
+						topARefinements.get(domain).get(i).addAll(mA.get(domain).get(i));
+				// combinations has several numbers => generate disjunct
+				} else {
+					
+					// check whether the combination makes sense, i.e. whether
+					// all lengths mentioned in it have corresponding elements
+					// e.g. when negation is deactivated there won't be elements of
+					// length 2 in M
+					boolean validCombo = true;
+					for(Integer j : combo) {
+						if((domain == null && m.get(j).size()==0) || 
+								(domain != null && mA.get(domain).get(j).size()==0))
+							validCombo = false;
+					}
+					
+					if(validCombo) {
+						
+						SortedSet<Union> baseSet = new TreeSet<Union>(conceptComparator);
+						for(Integer j : combo) {
+							if(domain == null)
+								baseSet = MathOperations.incCrossProduct(baseSet, m.get(j));
+							else
+								baseSet = MathOperations.incCrossProduct(baseSet, mA.get(domain).get(j));
+						}
+						
+						// convert all concepts in ordered negation normal form
+						for(Description concept : baseSet) {
+							ConceptTransformation.transformToOrderedForm(concept, conceptComparator);
+						}
+						
+						// apply the exists filter (throwing out all refinements with
+						// double \exists r for any r)
+						// TODO: similar filtering can be done for boolean datatype
+						// properties
+						if(applyExistsFilter) {
+							Iterator<Union> it = baseSet.iterator();
+							while(it.hasNext()) {
+								if(MathOperations.containsDoubleObjectSomeRestriction(it.next()))
+									it.remove();							
+							}
+						}
+							
+						// add computed refinements
+						if(domain == null)
+							topRefinements.get(i).addAll(baseSet);
+						else
+							topARefinements.get(domain).get(i).addAll(baseSet);
+						
+					}
+				}
+			}
+			
+			// create cumulative versions of refinements such that they can
+			// be accessed easily
+			TreeSet<Description> cumulativeRefinements = new TreeSet<Description>(conceptComparator);
+			for(int j=1; j<=i; j++) {
+				if(domain == null) {
+					cumulativeRefinements.addAll(topRefinements.get(j));
+				} else {
+					cumulativeRefinements.addAll(topARefinements.get(domain).get(j));
+				}
+			}			
+			
+			if(domain == null) {
+				topRefinementsCumulative.put(i, cumulativeRefinements);
+			} else {
+				if(!topARefinementsCumulative.containsKey(domain))
+					topARefinementsCumulative.put(domain, new TreeMap<Integer, TreeSet<Description>>());
+				topARefinementsCumulative.get(domain).put(i, cumulativeRefinements);
+			}
+		}
+		
+		// register new top refinements length
+		if(domain == null)
+			topRefinementsLength = maxLength;
+		else
+			topARefinementsLength.put(domain,maxLength);
+		
+		topComputationTimeNs += System.nanoTime() - topComputationTimeStartNs;
+	}
+	
+	// compute M_\top
+	private void computeM() {
+		long mComputationTimeStartNs = System.nanoTime();
+
+		// initialise all possible lengths (1 to 3)
+		for(int i=1; i<=mMaxLength; i++) {
+			m.put(i, new TreeSet<Description>(conceptComparator));
+		}
+		
+		SortedSet<Description> m1 = subHierarchy.getSubClasses(new Thing()); 
+		m.put(1,m1);		
+		
+		SortedSet<Description> m2 = new TreeSet<Description>(conceptComparator);
+		if(useNegation) {
+			Set<Description> m2tmp = subHierarchy.getSuperClasses(new Nothing());
+			for(Description c : m2tmp) {
+				if(!(c instanceof Thing)) {
+					m2.add(new Negation(c));	
+				}
+			}
+		}
+		
+		// boolean datatypes, e.g. testPositive = true
+		if(useBooleanDatatypes) {
+			Set<DatatypeProperty> booleanDPs = reasoner.getBooleanDatatypeProperties();
+			for(DatatypeProperty dp : booleanDPs) {
+				m2.add(new BooleanValueRestriction(dp,true));
+				m2.add(new BooleanValueRestriction(dp,false));
+			}
+		}		
+		m.put(2,m2);
+			
+		SortedSet<Description> m3 = new TreeSet<Description>(conceptComparator);
+		if(useExistsConstructor) {
+			// only uses most general roles
+			for(ObjectProperty r : reasoner.getMostGeneralProperties()) {
+				m3.add(new ObjectSomeRestriction(r, new Thing()));
+			}				
+		}
+		
+		if(useAllConstructor) {
+			// we allow \forall r.\top here because otherwise the operator
+			// becomes too difficult to manage due to dependencies between
+			// M_A and M_A' where A'=ran(r)
+			for(ObjectProperty r : reasoner.getMostGeneralProperties()) {
+				m...
 
[truncated message content]