diff options
Diffstat (limited to 'src/uk/ac/ox/cs/pagoda/rules')
| -rw-r--r-- | src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java index 4444c00..ba58e23 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java | |||
| @@ -79,9 +79,11 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima | |||
| 79 | TupleBuilder<Individual> commonIndividualsBuilder = new TupleBuilder<>(); | 79 | TupleBuilder<Individual> commonIndividualsBuilder = new TupleBuilder<>(); |
| 80 | for (int i = 0; i < commonVars.length; i++) | 80 | for (int i = 0; i < commonVars.length; i++) |
| 81 | commonIndividualsBuilder.add(violationTuple.get(i)); | 81 | commonIndividualsBuilder.add(violationTuple.get(i)); |
| 82 | Tuple<Individual> commonIndividuals = commonIndividualsBuilder.create(); | ||
| 82 | 83 | ||
| 83 | Atom headAtom = clause.getHeadAtom(0); | 84 | Atom headAtom = clause.getHeadAtom(0); |
| 84 | Atom[] bodyAtoms = clause.getBodyAtoms(); | 85 | |
| 86 | // Atom[] bodyAtoms = clause.getBodyAtoms(); | ||
| 85 | int offset = OverApproxExist.indexOfExistential(headAtom, originalClause); | 87 | int offset = OverApproxExist.indexOfExistential(headAtom, originalClause); |
| 86 | 88 | ||
| 87 | // BEGIN: copy and paste | 89 | // BEGIN: copy and paste |
| @@ -111,15 +113,15 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima | |||
| 111 | for (int i = 0; i < card; ++i) | 113 | for (int i = 0; i < card; ++i) |
| 112 | individuals[i] = termsManager.getFreshIndividual(originalClause, | 114 | individuals[i] = termsManager.getFreshIndividual(originalClause, |
| 113 | offset + i, | 115 | offset + i, |
| 114 | commonIndividualsBuilder.create()); | 116 | commonIndividuals); |
| 115 | 117 | ||
| 116 | for (int i = 0; i < card; ++i) { | 118 | for (int i = 0; i < card; ++i) { |
| 117 | if (atomicConcept != null) | 119 | if (atomicConcept != null) |
| 118 | ret.add(DLClause.create(new Atom[] {Atom.create(atomicConcept, individuals[i])}, EMPTY_BODY)); | 120 | ret.add(DLClause.create(new Atom[] {Atom.create(atomicConcept, individuals[i])}, EMPTY_BODY)); |
| 119 | 121 | ||
| 120 | Atom atom = role instanceof AtomicRole ? | 122 | Atom atom = role instanceof AtomicRole ? |
| 121 | Atom.create((AtomicRole) role, X, individuals[i]) : | 123 | Atom.create((AtomicRole) role, commonIndividuals.get(0), individuals[i]) : |
| 122 | Atom.create(((InverseRole) role).getInverseOf(), individuals[i], X); | 124 | Atom.create(((InverseRole) role).getInverseOf(), individuals[i], commonIndividuals.get(0)); |
| 123 | 125 | ||
| 124 | ret.add(DLClause.create(new Atom[] {atom}, EMPTY_BODY)); | 126 | ret.add(DLClause.create(new Atom[] {atom}, EMPTY_BODY)); |
| 125 | } | 127 | } |
