From d0c209780ac209ba20de1ef2ba68551dd3321b3c Mon Sep 17 00:00:00 2001
From: RncLsn <rnc.lsn@gmail.com>
Date: Wed, 13 May 2015 16:04:41 +0100
Subject: Implemented SkolemTermsManager.

---
 src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java')

diff --git a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java
index 331ad12..b169053 100644
--- a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java
+++ b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java
@@ -4,7 +4,7 @@ import org.semanticweb.HermiT.model.*;
 import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
 import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine;
 import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram;
-import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
+import uk.ac.ox.cs.pagoda.rules.approximators.SkolemTermsManager;
 import uk.ac.ox.cs.pagoda.util.Namespace;
 
 import java.util.*;
@@ -22,8 +22,9 @@ public abstract class TrackingRuleEncoderDisj extends TrackingRuleEncoderWithGap
 	 */
 	protected void processDisjunctiveRules() {
 		Map<Atom, Collection<DLClause>> auxiliaryAtoms = new HashMap<Atom, Collection<DLClause>>(); 
-		Map<Individual, Collection<DLClause>> skolemisedAtoms = new HashMap<Individual, Collection<DLClause>>(); 
-		
+		Map<Individual, Collection<DLClause>> skolemisedAtoms = new HashMap<Individual, Collection<DLClause>>();
+		SkolemTermsManager termsManager = SkolemTermsManager.getInstance();
+
 		for (Map.Entry<DLClause, Collection<DLClause>> entry: disjunctiveRules.entrySet()) {
 			DLClause original = entry.getKey();
 			Collection<DLClause> overClauses = entry.getValue(); 
@@ -33,7 +34,7 @@ public abstract class TrackingRuleEncoderDisj extends TrackingRuleEncoderWithGap
 				DLClause subClause = iter.next(); 
 				if (DLClauseHelper.hasSubsetBodyAtoms(subClause, original)) {
 					Atom headAtom = subClause.getHeadAtom(0);
-					if ((index = OverApproxExist.indexOfSkolemisedIndividual(headAtom)) != -1) {
+					if ((index = SkolemTermsManager.indexOfSkolemisedIndividual(headAtom)) != -1) {
 						Individual i = (Individual) headAtom.getArgument(index);
 						Collection<DLClause> clauses = skolemisedAtoms.get(i);
 						if (clauses == null) {
@@ -55,7 +56,7 @@ public abstract class TrackingRuleEncoderDisj extends TrackingRuleEncoderWithGap
 					Collection<DLClause> clauses = new HashSet<DLClause>();
 					Individual[] individuals = new Individual[alc.getNumber()]; 
 					for (int i = 0; i < alc.getNumber(); ++i) {
-						individuals[i] = OverApproxExist.getNewIndividual(original, i);
+						individuals[i] = termsManager.getFreshIndividual(original, i);
 						clauses.addAll(skolemisedAtoms.get(individuals[i])); 
 					}
 					auxiliaryAtoms.put(getAuxiliaryAtom(original, headAtom, individuals), clauses);
-- 
cgit v1.2.3