Implementing Limited Skolemisation, in particular SkolemTermsDispenser.

7 files changed, 595 insertions, 0 deletions

diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/Approximator.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/Approximator.java
new file mode 100644
index 0000000..f910c64
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/Approximator.java
@@ -0,0 +1,42 @@
+package uk.ac.ox.cs.pagoda.rules.approximators;
+
+import org.semanticweb.HermiT.model.DLClause;
+
+import java.util.Collection;
+
+public interface Approximator {
+
+    Collection<DLClause> convert(DLClause clause, DLClause originalClause);
+
+}
+
+// TODO remove
+//class IgnoreExist implements Approximator {
+//
+//      @Override
+//      public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
+//              Collection<DLClause> ret = new LinkedList<DLClause>();
+//              DLPredicate p;
+//              for (Atom headAtom: clause.getHeadAtoms()) {
+//                      p = headAtom.getDLPredicate();
+//                      if (p instanceof AtLeast) return ret;
+//              }
+//
+//              ret.add(clause);
+//              return ret;
+//      }
+//
+//}
+//
+//
+//
+//class IgnoreDisj implements Approximator {
+//
+//      @Override
+//      public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
+//              Collection<DLClause> ret = new LinkedList<DLClause>();
+//              if (clause.getHeadLength() > 1) return ret;
+//              ret.add(clause);
+//              return ret;
+//      }
+//}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
new file mode 100644
index 0000000..8fc6b77
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
@@ -0,0 +1,74 @@
+package uk.ac.ox.cs.pagoda.rules.approximators;
+
+import org.semanticweb.HermiT.model.DLClause;
+import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID;
+import uk.ac.ox.cs.pagoda.rules.ExistConstantApproximator;
+
+import java.util.*;
+
+/**
+ * Approximates existential rules by a limited form of Skolemisation.
+ * <p>
+ * Given a rule and a grounding substitution,
+ * it Skolemises the rule if
+ * all the terms in the substitution have depth less than a given depth,
+ * otherwise it approximates using an alternative <tt>TupleDependentApproximator</tt>.
+ *
+ * */
+public class LimitedSkolemisationApproximator implements TupleDependentApproximator {
+
+    private final int maxTermDepth;
+    private final TupleDependentApproximator alternativeApproximator;
+
+    private Map<AnswerTupleID, Integer> mapIndividualsToDepth;
+
+    public LimitedSkolemisationApproximator(int maxTermDepth) {
+        this(maxTermDepth, new ExistConstantApproximator());
+    }
+
+    public LimitedSkolemisationApproximator(int maxTermDepth, TupleDependentApproximator alternativeApproximator) {
+        this.maxTermDepth = maxTermDepth;
+        this.alternativeApproximator = alternativeApproximator;
+        this.mapIndividualsToDepth = new HashMap<>();
+    }
+
+    @Override
+    public Collection<DLClause> convert(DLClause clause, DLClause originalClause, Collection<AnswerTupleID> violationTuples) {
+        switch (clause.getHeadLength()) {
+            case 1:
+                return overApprox(clause, originalClause, violationTuples);
+            case 0:
+                return Arrays.asList(clause);
+            default:
+                ArrayList<DLClause> result = new ArrayList<>();
+                // TODO implement
+                return result;
+        }
+
+
+    }
+
+    private Collection<DLClause> overApprox(DLClause clause, DLClause originalClause, Collection<AnswerTupleID> violationTuples) {
+        ArrayList<DLClause> result = new ArrayList<>();
+
+        for (AnswerTupleID violationTuple : violationTuples)
+            if (getDepth(violationTuple) > maxTermDepth)
+                result.addAll(alternativeApproximator.convert(clause, originalClause, null));
+            else
+                result.add(getInstantiatedSkolemisation(clause, originalClause, violationTuple));
+
+        return result;
+    }
+
+
+    private DLClause getInstantiatedSkolemisation(DLClause clause, DLClause originalClause, AnswerTupleID violationTuple) {
+        // TODO implement
+        // filter the violation tuples appearing on both the sides of the rule
+        return null;
+    }
+
+    private int getDepth(AnswerTupleID violationTuple) {
+        if (!mapIndividualsToDepth.containsKey(violationTuple)) return 0;
+        return mapIndividualsToDepth.get(violationTuple);
+    }
+}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxBoth.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxBoth.java
new file mode 100644
index 0000000..ae2a2cf
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxBoth.java
@@ -0,0 +1,24 @@
+package uk.ac.ox.cs.pagoda.rules.approximators;
+
+import org.semanticweb.HermiT.model.AtLeastDataRange;
+import org.semanticweb.HermiT.model.DLClause;
+
+import java.util.Collection;
+import java.util.LinkedList;
+
+public class OverApproxBoth implements Approximator {
+        
+        Approximator approxDist = new OverApproxDisj(), approxExist = new OverApproxExist();
+                
+        @Override
+        public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
+                Collection<DLClause> ret = new LinkedList<DLClause>(); 
+                for (DLClause tClause: approxDist.convert(clause, originalClause)) {
+                        if (tClause.getHeadLength() > 0 && tClause.getHeadAtom(0).getDLPredicate() instanceof AtLeastDataRange) 
+                                continue; 
+                        ret.addAll(approxExist.convert(tClause, originalClause)); 
+                }
+                return ret; 
+        }
+                
+}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxDisj.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxDisj.java
new file mode 100644
index 0000000..05d9442
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxDisj.java
@@ -0,0 +1,100 @@
+package uk.ac.ox.cs.pagoda.rules.approximators;
+
+import org.semanticweb.HermiT.model.*;
+import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
+
+import java.util.*;
+
+public class OverApproxDisj implements Approximator {
+
+        /**
+         * Splits a disjunctive rule into a bunch of rules.
+         * <p>
+         * It returns a collection containing a rule for each atom in the head of the input rule.
+         * Each rule has the same body of the input rule,
+         * and the relative head atom as head.
+         * */
+        @Override
+        public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
+                LinkedList<DLClause> distincts = new LinkedList<DLClause>();
+                Atom[] headAtoms = clause.getHeadAtoms(), bodyAtoms = clause.getBodyAtoms();
+                LinkedList<DLClause> newClauses = new LinkedList<DLClause>();
+                DLClause newClause;
+                if (headAtoms.length > 1) {
+                        for (Atom headAtom: headAtoms) {
+                                newClause = DLClause.create(new Atom[] {headAtom}, bodyAtoms);
+                                newClauses.add(newClause);
+//                              distincts.add(newClause); 
+                        }
+                        
+                        for (DLClause cls: newClauses) {
+                                newClause = DLClauseHelper.simplified(cls);
+                                if (!isSubsumedBy(newClause, distincts)) 
+                                        distincts.add(newClause);
+                        }
+                }
+                else distincts.add(clause);
+                
+                return distincts;
+        }
+
+        public static boolean isSubsumedBy(DLClause newClause, Collection<DLClause> distinctClauses) {
+                Map<Variable, Term> unifier;
+                Set<Atom> bodyAtoms = new HashSet<Atom>();
+                for (DLClause clause: distinctClauses) { 
+                        if (newClause.getHeadLength() > 0 && clause.getHeadLength() > 0 && 
+                                        (unifier = isSubsumedBy(newClause.getHeadAtom(0), clause.getHeadAtom(0))) == null)
+                                continue;
+                        else 
+                                unifier = new HashMap<Variable, Term>();
+                        
+                        for (Atom atom: clause.getBodyAtoms())
+                                bodyAtoms.add(rename(atom, unifier));
+                        unifier.clear();
+                        
+                        for (Atom atom: newClause.getBodyAtoms()) 
+                                if (!bodyAtoms.contains(atom)) 
+                                        continue;
+                        
+                        return true;
+                }
+                
+                return false;
+        }
+        
+        public static Map<Variable, Term> isSubsumedBy(Atom atom1, Atom atom2) {
+                DLPredicate predicate = atom1.getDLPredicate();
+                if (!predicate.equals(atom2.getDLPredicate()))
+                        return null;
+
+                Map<Variable, Term> unifier = new HashMap<Variable, Term>();
+                Term term1, term2;
+                for (int index = 0; index < predicate.getArity(); ++index) {
+                        term1 = rename(atom1.getArgument(index), unifier);
+                        term2 = rename(atom2.getArgument(index), unifier);
+                        
+                        if (term1.equals(term2));
+                        else if (term1 instanceof Variable)
+                                        unifier.put((Variable) term1, term2);
+                        else
+                                return null;
+                }
+                return unifier;
+        }
+        
+        public static Atom rename(Atom atom, Map<Variable, Term> unifier) {
+                Term[] arguments = new Term[atom.getArity()];
+                for (int i = 0; i < atom.getArity(); ++i)
+                        arguments[i] = rename(atom.getArgument(i), unifier);
+                return Atom.create(atom.getDLPredicate(), arguments);
+        }
+
+        public static Term rename(Term argument, Map<Variable, Term> unifier) {
+                Term newArg;
+                while ((newArg = unifier.get(argument)) != null) 
+                        return newArg;
+                return argument;
+        }
+
+
+}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java
new file mode 100644
index 0000000..e0bafe0
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java
@@ -0,0 +1,265 @@
+package uk.ac.ox.cs.pagoda.rules.approximators;
+
+import org.semanticweb.HermiT.model.*;
+import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
+import uk.ac.ox.cs.pagoda.util.Namespace;
+
+import java.util.*;
+
+public class OverApproxExist implements Approximator {
+
+        public static final String negativeSuffix = "_neg";
+        public static final String skolemisedIndividualPrefix = Namespace.PAGODA_ANONY + "individual";
+        private static final Variable X = Variable.create("X");
+        //DEBUG
+        public static Collection<String> createdIndividualIRIs = new HashSet<>();
+        private static int individualCounter = 0;
+        private static Map<DLClause, Integer> individualNumber = new HashMap<DLClause, Integer>();
+
+        private static int noOfExistential(DLClause originalClause) {
+                int no = 0;
+                for (Atom atom: originalClause.getHeadAtoms())
+                        if (atom.getDLPredicate() instanceof AtLeast)
+                                no += ((AtLeast) atom.getDLPredicate()).getNumber();
+                return no;
+        }
+
+        private static int indexOfExistential(Atom headAtom, DLClause originalClause) {
+                if (!(headAtom.getDLPredicate() instanceof AtLeast)) return -1;
+                AtLeastConcept alc = (AtLeastConcept) headAtom.getDLPredicate();
+                if (alc.getToConcept() instanceof AtomicConcept) {
+                        AtomicConcept ac = (AtomicConcept) alc.getToConcept();
+                        if (ac.getIRI().endsWith(negativeSuffix)) {
+                                alc = AtLeastConcept.create(alc.getNumber(), alc.getOnRole(), AtomicNegationConcept.create(getNegationConcept(ac)));
+                                headAtom = Atom.create(alc, headAtom.getArgument(0));
+                        }
+                }
+
+                int index = 0;
+                for (Atom atom: originalClause.getHeadAtoms()) {
+                        if (atom.equals(headAtom))
+                                return index;
+                        if (atom.getDLPredicate() instanceof AtLeast)
+                                index += ((AtLeast) atom.getDLPredicate()).getNumber();
+                }
+                return -1;
+        }
+
+        public static AtomicConcept getNegationConcept(DLPredicate p) {
+                if (p.equals(AtomicConcept.THING)) return AtomicConcept.NOTHING;
+                if (p.equals(AtomicConcept.NOTHING)) return AtomicConcept.THING;
+
+                if (p instanceof AtomicConcept) {
+                        String iri = ((AtomicConcept) p).getIRI();
+                        if (iri.endsWith(negativeSuffix))
+                                iri = iri.substring(0, iri.length() - 4);
+                        else
+                                iri += negativeSuffix;
+
+                        return AtomicConcept.create(iri);
+                }
+                if (p instanceof AtLeastConcept) {
+                        // FIXME !!! here
+                        return null;
+                }
+                return null;
+        }
+
+        public static int getNumberOfSkolemisedIndividual() {
+                return individualCounter;
+        }
+        //DEBUG
+
+        public static Individual getNewIndividual(DLClause originalClause, int offset) {
+                Individual ret;
+                int individualID;
+                if (individualNumber.containsKey(originalClause)) {
+                        individualID = individualNumber.get(originalClause) + offset;
+                        ret = Individual.create(skolemisedIndividualPrefix + individualID);
+                }
+                else {
+                        individualNumber.put(originalClause, individualCounter);
+                        individualID = individualCounter + offset;
+                        ret = Individual.create(skolemisedIndividualPrefix + individualID);
+                        individualCounter += noOfExistential(originalClause);
+                }
+                return ret;
+        }
+        
+        public static int indexOfSkolemisedIndividual(Atom atom) {
+                Term t;
+                for (int index = 0; index < atom.getArity(); ++index) {
+                        t = atom.getArgument(index);
+                        if (t instanceof Individual && ((Individual) t).getIRI().contains(skolemisedIndividualPrefix)) return index;
+                }
+                return -1;
+        }
+
+        @Override
+        public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
+                Collection<DLClause> ret;
+                switch (clause.getHeadLength()) {
+                        case 1:
+                                return overApprox(clause.getHeadAtom(0), clause.getBodyAtoms(), originalClause);
+                        case 0:
+                                ret = new LinkedList<DLClause>();
+                                ret.add(clause);
+                                return ret;
+                        default:
+                                ret = new LinkedList<DLClause>();
+                                for (Iterator<DLClause> iter = new DisjunctiveHeads(clause, originalClause); iter.hasNext(); )
+                                        ret.add(iter.next());
+                                return ret;
+                }
+        }
+        
+        public Collection<DLClause> overApprox(Atom headAtom, Atom[] bodyAtoms, DLClause originalClause) {
+                return overApprox(headAtom, bodyAtoms, originalClause, indexOfExistential(headAtom, originalClause)); 
+        }
+        
+        public Collection<DLClause> overApprox(Atom headAtom, Atom[] bodyAtoms, DLClause originalClause, int offset) {
+                Collection<DLClause> ret = new LinkedList<DLClause>(); 
+                DLPredicate predicate = headAtom.getDLPredicate();
+                if (predicate instanceof AtLeastConcept) {
+                        AtLeastConcept atLeastConcept = (AtLeastConcept) predicate;
+                        LiteralConcept concept = atLeastConcept.getToConcept();
+                        Role role = atLeastConcept.getOnRole();
+                        AtomicConcept atomicConcept = null;
+                        
+                        if (concept instanceof AtomicNegationConcept) {
+                                // TODO CHECK: is this already in MultiStageUpperProgram?
+                                Atom atom1 = Atom.create(atomicConcept = ((AtomicNegationConcept) concept).getNegatedAtomicConcept(), X);
+                                Atom atom2 = Atom.create(atomicConcept = getNegationConcept(atomicConcept), X);
+                                ret.add(DLClause.create(new Atom[0], new Atom[] {atom1, atom2})); 
+                        }
+                        else {
+                                atomicConcept = (AtomicConcept) concept;
+                                if (atomicConcept.equals(AtomicConcept.THING))
+                                        atomicConcept = null;
+                        }
+
+                        int card = atLeastConcept.getNumber(); 
+                        Individual[] individuals = new Individual[card];
+                        for (int i = 0; i < card; ++i) individuals[i] = getNewIndividual(originalClause, offset + i);
+                        
+                        for (int i = 0; i < card; ++i) {
+                                if (atomicConcept != null)
+                                        ret.add(DLClause.create(new Atom[] {Atom.create(atomicConcept, individuals[i])}, bodyAtoms)); 
+
+                                Atom atom = role instanceof AtomicRole ?
+                                                Atom.create((AtomicRole) role, X, individuals[i]) : 
+                                                Atom.create(((InverseRole) role).getInverseOf(), individuals[i], X);
+
+                                ret.add(DLClause.create(new Atom[] {atom}, bodyAtoms)); 
+                        }
+                        
+                        for (int i = 0; i < card; ++i)
+                                for (int j = i + 1; j < card; ++j)
+                                        // TODO to be checked ... different as 
+                                        ret.add(DLClause.create(new Atom[] {Atom.create(Inequality.INSTANCE, individuals[i], individuals[j])}, bodyAtoms)); 
+                                                        //DLClauseHelper.contructor_differentAs(individuals[i], individuals[j]));  
+                                                                                
+                }
+                else if (predicate instanceof AtLeastDataRange) {
+                        // TODO to be implemented ... 
+                }
+                else
+                        ret.add(DLClause.create(new Atom[] {headAtom}, bodyAtoms)); 
+                
+                return ret; 
+        }
+
+        class DisjunctiveHeads implements Iterator<DLClause> {
+
+                Atom[] bodyAtoms; 
+                Atom[][] disjunctHeadAtoms; 
+                int[] pointer;
+                int length, l; 
+                LinkedList<DLClause> auxiliaryClauses = new LinkedList<DLClause>();  
+
+                public DisjunctiveHeads(DLClause clause, DLClause originalClause) {
+                        length = clause.getHeadLength();
+                        
+                        bodyAtoms = clause.getBodyAtoms(); 
+                        disjunctHeadAtoms = new Atom[length][];
+                        pointer = new int[length];
+                        if (length > 0) l = length - 1;
+                        else length = 0; 
+                        
+                        int index = 0, offset = 0;
+                        Collection<DLClause> datalogRules;
+                        DLClause newClause; 
+                        for (Atom headAtom: clause.getHeadAtoms()) {
+                                pointer[index] = 0;
+                                
+                                datalogRules = overApprox(headAtom, bodyAtoms, originalClause, offset);
+                                
+                                if (datalogRules.isEmpty()) {
+                                        l = -1; 
+                                        auxiliaryClauses.clear(); 
+                                        return ; 
+                                }
+                                
+                                for (Iterator<DLClause> iter = datalogRules.iterator(); iter.hasNext(); ) {
+                                        newClause = iter.next(); 
+                                        if (!DLClauseHelper.hasSubsetBodyAtoms(newClause, clause)) {
+                                                auxiliaryClauses.add(newClause); 
+                                                iter.remove();
+                                        }
+                                }
+                                
+                                disjunctHeadAtoms[index] = new Atom[datalogRules.size()];
+                                
+                                int j = 0; 
+                                for (DLClause disjunct: datalogRules) {
+                                        disjunctHeadAtoms[index][j++] = disjunct.getHeadAtom(0); 
+                                }
+                                
+                                ++index; 
+                                if (headAtom.getDLPredicate() instanceof AtLeast) 
+                                        offset += ((AtLeast) headAtom.getDLPredicate()).getNumber();
+                                
+                        }
+                                
+                }
+
+                @Override
+                public boolean hasNext() {
+                        return l != -1 || !auxiliaryClauses.isEmpty(); 
+                }
+
+                @Override
+                public DLClause next() {
+                        if (l == -1) 
+                                return auxiliaryClauses.removeFirst(); 
+                        
+                        if (length > 0) {
+                                Atom[] headAtoms = new Atom[length]; 
+                                for (int i = 0; i < length; ++i)
+                                        headAtoms[i] = disjunctHeadAtoms[i][pointer[i]];
+                                
+                                ++pointer[l];
+                                while (l >= 0 && pointer[l] >= disjunctHeadAtoms[l].length) {
+                                        pointer[l] = 0; 
+                                        --l; 
+                                        if (l >= 0) 
+                                                ++pointer[l];
+                                }
+                                
+                                if (l >= 0) l = length - 1; 
+                                
+                                return DLClauseHelper.simplified(DLClause.create(headAtoms, bodyAtoms));  
+//                              return DLClause.create(headAtoms, bodyAtoms);  
+                        }
+                        else {
+                                --l; 
+                                return DLClauseHelper.simplified(DLClause.create(new Atom[0], bodyAtoms));
+//                              return DLClause.create(new Atom[0], bodyAtoms);
+                        }
+                }
+
+                @Override
+                public void remove() { }
+                
+        }
+}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsDispenser.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsDispenser.java
new file mode 100644
index 0000000..a920ec5
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsDispenser.java
@@ -0,0 +1,74 @@
+package uk.ac.ox.cs.pagoda.rules.approximators;
+
+import org.semanticweb.HermiT.model.AtLeast;
+import org.semanticweb.HermiT.model.Atom;
+import org.semanticweb.HermiT.model.DLClause;
+import org.semanticweb.HermiT.model.Individual;
+import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID;
+import uk.ac.ox.cs.pagoda.util.Namespace;
+
+import java.util.HashMap;
+import java.util.Map;
+
+/**
+ * If you need a Skolem term (i.e. fresh individual), ask this class.
+ */
+public class SkolemTermsDispenser {
+
+    public static final String skolemisedIndividualPrefix = Namespace.PAGODA_ANONY + "individual";
+    private static SkolemTermsDispenser skolemTermsDispenser;
+    private int individualCounter = 0;
+    private Map<DLClause, Integer> termNumber = new HashMap<>();
+    private Map<SkolemTermId, Integer> mapTermToDepth = new HashMap<>();
+    private int dependenciesCounter = 0;
+    private Map<AnswerTupleID, Integer> mapDependencyToId = new HashMap<>();
+
+    private SkolemTermsDispenser() {
+    }
+
+    public static SkolemTermsDispenser getInstance() {
+        if (skolemTermsDispenser == null) skolemTermsDispenser = new SkolemTermsDispenser();
+        return skolemTermsDispenser;
+    }
+
+    private int getDependencyId(AnswerTupleID answerTupleID) {
+        if (mapDependencyToId.containsKey(answerTupleID)) return mapDependencyToId.get(answerTupleID);
+        else return mapDependencyToId.put(answerTupleID, dependenciesCounter++);
+    }
+
+    public Individual getNewIndividual(DLClause originalClause, int offset, AnswerTupleID dependency) {
+        if (!termNumber.containsKey(originalClause)) {
+            termNumber.put(originalClause, individualCounter);
+            individualCounter += noOfExistential(originalClause);
+        }
+        if (!mapDependencyToId.containsKey(dependency)) {
+            mapDependencyToId.put(dependency, dependenciesCounter++);
+        }
+
+        SkolemTermId termId = new SkolemTermId(termNumber.get(originalClause) + offset, getDependencyId(dependency));
+        return Individual.create(skolemisedIndividualPrefix + termId);
+    }
+
+    private int noOfExistential(DLClause originalClause) {
+        int no = 0;
+        for (Atom atom : originalClause.getHeadAtoms())
+            if (atom.getDLPredicate() instanceof AtLeast)
+                no += ((AtLeast) atom.getDLPredicate()).getNumber();
+        return no;
+    }
+
+    private class SkolemTermId {
+        private final int idBase;
+        private final int idOffset;
+
+        private SkolemTermId(int idBase, int idOffset) {
+            this.idBase = idBase;
+            this.idOffset = idOffset;
+        }
+
+        @Override
+        public String toString() {
+            return idBase + "_" + idOffset;
+        }
+    }
+}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java
new file mode 100644
index 0000000..1a729e5
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java
@@ -0,0 +1,16 @@
+package uk.ac.ox.cs.pagoda.rules.approximators;
+
+import org.semanticweb.HermiT.model.DLClause;
+import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID;
+
+import java.util.Collection;
+
+/**
+ * It approximates rules according to a specific instantiation of the body.
+ */
+public interface TupleDependentApproximator {
+
+    Collection<DLClause> convert(DLClause clause,
+                                 DLClause originalClause,
+                                 Collection<AnswerTupleID> violationTuples);
+}