diff --git a/src/main/java/inference/InferenceRule.java b/src/main/java/inference/InferenceRule.java index 5c86b88..4c2305f 100644 --- a/src/main/java/inference/InferenceRule.java +++ b/src/main/java/inference/InferenceRule.java @@ -206,7 +206,14 @@ } } } - Formula subRes = conclusion.substitution(result.iterator().next().getBinding()); + Formula subRes = null; + for (MatchConstraint con: result) { + try { + subRes = conclusion.substitution(con.getBinding()); + } catch (SubstituteFailedException e) { + continue; + } + } return subRes; } diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index 9283825..51c6254 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -364,32 +364,27 @@ "Composite Mapping", List.of( new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("se")), new MetaTermGenerator() { @Override public MetaRDLTerm generate(int i, int depth, boolean isLast) { - if (i == 0) { - return new MetaResource(new Variable("r")); - } else { - return new MetaResource(new Variable("r" + i)); - } + return new MetaEvaluatableTermVariable(new Variable("te" + i)); }} ), new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("r")), - new MetaResource(new Variable("q")) + new MetaEvaluatableTermVariable(new Variable("te0")), + new MetaEvaluatableTermVariable(new Variable("ue0")) ) ), new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("se")), new MetaTermGenerator() { @Override public MetaRDLTerm generate(int i, int depth, boolean isLast) { if (i == 0) { - return new MetaResource(new Variable("q")); - } else { - return new MetaResource(new Variable("r" + i)); + return new MetaResource(new Variable("ue0")); } + return new MetaResource(new Variable("te" + i)); }} ) ); diff --git a/src/main/java/models/formulas/meta/MetaDependencyFormula.java b/src/main/java/models/formulas/meta/MetaDependencyFormula.java index 10df361..5dee6c4 100644 --- a/src/main/java/models/formulas/meta/MetaDependencyFormula.java +++ b/src/main/java/models/formulas/meta/MetaDependencyFormula.java @@ -13,9 +13,10 @@ import models.terms.Dependency; import models.terms.RDLTerm; import models.terms.meta.MatchConstraint; -import models.terms.meta.MetaTermGenerator; import models.terms.meta.MetaDependencyVariable; +import models.terms.meta.MetaDynamicTerm; import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; @Getter public class MetaDependencyFormula extends MetaFormula { @@ -42,7 +43,7 @@ } public MetaDependencyFormula(MetaRDLTerm dependingTerm, MetaTermGenerator generator) { - this.dependency = new MetaRDLTerm(dependingTerm, generator); + this.dependency = new MetaDynamicTerm(dependingTerm, generator); } @Override diff --git a/src/main/java/models/terms/DependencyTerm.java b/src/main/java/models/terms/DependencyTerm.java index 981bd56..484b040 100644 --- a/src/main/java/models/terms/DependencyTerm.java +++ b/src/main/java/models/terms/DependencyTerm.java @@ -83,7 +83,6 @@ return new ArrayList<>(termPairs.values()); } - @Override public String toString() { StringBuilder sb = new StringBuilder(); diff --git a/src/main/java/models/terms/meta/MetaDynamicTerm.java b/src/main/java/models/terms/meta/MetaDynamicTerm.java index 6e1e54c..e3e78a4 100644 --- a/src/main/java/models/terms/meta/MetaDynamicTerm.java +++ b/src/main/java/models/terms/meta/MetaDynamicTerm.java @@ -16,6 +16,7 @@ import models.terms.Resource; import models.terms.ResourceConstant; import models.terms.meta.MetaTermPairGenerator.TermPair; +import utils.Permutation; public class MetaDynamicTerm extends MetaRDLTerm { @@ -86,49 +87,73 @@ private Set dependencyMatch(Dependency another, MatchConstraint constraint, int depth) { Set result = new HashSet<>(); + Set tmpRes = new HashSet<>(); RDLTerm anotherDependingTerm = another.getDependingTerm(); TreeSet anotherDependedTerms = another.getDependedTerms(); boolean isLast = anotherDependingTerm instanceof Resource || anotherDependingTerm instanceof ResourceConstant; MetaRDLTerm metaDependingTerm = dependingTermGenerator.generate(0, depth, isLast); - result = metaDependingTerm.isMatchedBy(anotherDependingTerm, constraint, depth + 1); - if (result.isEmpty()) { + tmpRes = metaDependingTerm.isMatchedBy(anotherDependingTerm, constraint, depth + 1); + if (tmpRes.isEmpty()) { return result; } - int i = 0; - for (EvaluatableTerm anotherDependedTerm : anotherDependedTerms) { - isLast = anotherDependedTerm instanceof Resource || anotherDependedTerm instanceof ResourceConstant; - MetaRDLTerm metaDependedTerm = dependedTermGenerator.generate(i, depth, isLast); - result = metaDependedTerm.isMatchedBy(anotherDependedTerm, result, depth + 1); - if (result.isEmpty()) { - return result; + for (List perm: Permutation.permutation(anotherDependedTerms.size())) { + Set localResult = new HashSet<>(tmpRes); + boolean flg = true; + for (int metaTermIndex = 0; metaTermIndex < perm.size(); metaTermIndex++) { + int anotherTermIndex = perm.get(metaTermIndex); + EvaluatableTerm anotherDependedTerm = anotherDependedTerms.stream().skip(anotherTermIndex).findFirst().orElse(null); + isLast = anotherDependedTerm instanceof Resource || anotherDependedTerm instanceof ResourceConstant; + MetaRDLTerm metaDependedTerm = dependedTermGenerator.generate(metaTermIndex, depth, isLast); + localResult = metaDependedTerm.isMatchedBy(anotherDependedTerm, localResult, depth + 1); + if (localResult.isEmpty()) { + flg = false; + break; + } } - i++; + if (flg) { + result.addAll(localResult); + } } return result; } private Set dependencyTermMatch(DependencyTerm another, MatchConstraint constraint, int depth) { Set result = new HashSet<>(); + Set tmpRes = new HashSet<>(); RDLTerm anotherDependingTerm = another.getDependingTerm(); List anotherDependedTerms = another.getDependedTerms(); List anotherArgumentTerms = another.getArgumentTerms(); boolean isLast = anotherDependingTerm instanceof Resource || anotherDependingTerm instanceof ResourceConstant; MetaRDLTerm metaDependingTerm = dependingTermGenerator.generate(0, depth, isLast); - result = metaDependingTerm.isMatchedBy(anotherDependingTerm, constraint, depth + 1); - if (result.isEmpty()) { - return result; + tmpRes = metaDependingTerm.isMatchedBy(anotherDependingTerm, constraint, depth + 1); + if (tmpRes.isEmpty()) { + return tmpRes; } - int i = 0; - for (EvaluatableTerm anotherDependedTerm : anotherDependedTerms) { - isLast = anotherDependedTerm instanceof Resource || anotherDependedTerm instanceof ResourceConstant; - TermPair termPair = termPairGenerator.generate(i, depth, isLast); - result = termPair.dependedTerm().isMatchedBy(anotherDependedTerm, result, depth + 1); - isLast = anotherDependedTerm instanceof Resource || anotherDependedTerm instanceof ResourceConstant; - result = termPair.argTerm().isMatchedBy(anotherArgumentTerms.get(i), result, depth + 1); - if (result.isEmpty()) { - return result; + for (List perm: Permutation.permutation(anotherDependedTerms.size())) { + Set localResult = new HashSet<>(tmpRes); + boolean flg = true; + for (int metaTermIndex = 0; metaTermIndex < perm.size(); metaTermIndex++) { + int anotherTermIndex = perm.get(metaTermIndex); + EvaluatableTerm anotherDependedTerm = anotherDependedTerms.get(anotherTermIndex); + EvaluatableTerm anotherArgTerm = anotherArgumentTerms.get(anotherTermIndex); + TermPair metaTermPair = termPairGenerator.generate(metaTermIndex, depth, isLast); + isLast = anotherDependedTerm instanceof Resource || anotherDependedTerm instanceof ResourceConstant; + localResult = metaTermPair.dependedTerm().isMatchedBy(anotherDependedTerm, localResult, depth + 1); + if (localResult.isEmpty()) { + flg = false; + break; + } + + isLast = anotherArgTerm instanceof Resource || anotherArgTerm instanceof ResourceConstant; + localResult = metaTermPair.argTerm().isMatchedBy(anotherArgTerm, localResult, depth + 1); + if (localResult.isEmpty()) { + flg = false; + break; + } } - i++; + if (flg) { + result.addAll(localResult); + } } return result; } @@ -249,11 +274,15 @@ } public MetaRDLTerm dependencyGenerate(Map binding) { - int ok = -1; + int ok = 0; int ng = 100; while (Math.abs(ok - ng) > 1) { int mid = (ok + ng) / 2; MetaRDLTerm generatedTerm = dependencyRecursionGenerate(mid, 0); + if (generatedTerm == null) { + ng = mid; + continue; + } Set variables = new HashSet<>(generatedTerm.getAllVariables().stream().map(v -> v.getVariableName()).toList()); variables.removeAll(binding.keySet()); if (variables.isEmpty()) { diff --git a/src/main/java/models/terms/meta/MetaRDLTerm.java b/src/main/java/models/terms/meta/MetaRDLTerm.java index e86b1e5..c981362 100644 --- a/src/main/java/models/terms/meta/MetaRDLTerm.java +++ b/src/main/java/models/terms/meta/MetaRDLTerm.java @@ -106,7 +106,7 @@ } if (isDependency()) { List dependedTerms = new ArrayList<>(); - for (int i = 0; i < getChildren().size() - 1; i++) { + for (int i = 1; i < getChildren().size(); i++) { RDLTerm dependedTerm = (RDLTerm) getChild(i); if (dependedTerm instanceof MetaRDLTerm metaTerm) { dependedTerm = metaTerm.substitute(binding, depth + 1); @@ -126,8 +126,8 @@ else if (isDependencyTerm()) { List termPairs = new ArrayList<>(); for (int i = 0; i < (getChildren().size() - 1) / 2; i++) { - RDLTerm dependedTerm = (RDLTerm) getChild(i * 2); - RDLTerm argTerm = (RDLTerm) getChild(i * 2 + 1); + RDLTerm dependedTerm = (RDLTerm) getChild(i * 2 + 1); + RDLTerm argTerm = (RDLTerm) getChild(i * 2 + 2); if (dependedTerm instanceof MetaRDLTerm metaTerm) { dependedTerm = metaTerm.substitute(binding, depth + 1); } @@ -183,128 +183,90 @@ Set res = new HashSet<>(); if (dependingChild instanceof MetaRDLTerm) { MetaRDLTerm metaChild = (MetaRDLTerm) dependingChild; - res = metaChild.isMatchedBy(anotherDependingChild, constraint, depth + 1); + result = metaChild.isMatchedBy(anotherDependingChild, constraint, depth + 1); } else { if (!(dependingChild.equals(anotherDependingChild))) { return result; } } if (isDependencyTerm()) { -// for (List perm : Permutation.permutation((another.getChildren().size() - 1) / 2)) { -// Set res2 = new HashSet<>(res); -// boolean flg = true; -// for (int metaTermIndex = 0; metaTermIndex < perm.size(); metaTermIndex++) { -// int anotherTermIndex = perm.get(metaTermIndex); -// RDLTerm metaDependedTerm = (RDLTerm) getChild(metaTermIndex * 2 + 1); -// RDLTerm metaArgTerm = (RDLTerm) getChild(metaTermIndex * 2 + 2); -// RDLTerm anotherDependedChild = (RDLTerm) another.getChild(anotherTermIndex * 2 + 1); -// RDLTerm anotherArgChild = (RDLTerm) another.getChild(anotherTermIndex * 2 + 2); -// if (metaDependedTerm instanceof MetaRDLTerm metaTerm) { -// res2 = metaTerm.isMatchedBy(anotherDependedChild, res2, depth + 1); -// if (res2.isEmpty()) { -// flg = false; -// break; -// } -// } else { -// if (!(metaDependedTerm.equals(anotherDependedChild))) { -// flg = false; -// break; -// } -// } -// if (metaArgTerm instanceof MetaRDLTerm metaTerm) { -// res2 = metaTerm.isMatchedBy(anotherArgChild, res2, depth + 1); -// if (res2.isEmpty()) { -// flg = false; -// break; -// } -// } else { -// if (!(metaArgTerm.equals(anotherArgChild))) { -// flg = false; -// break; -// } -// } -// } -// if (flg) { -// result.addAll(res2); -// break; -// } -// } -// return result; - result.addAll(dependencyTermMatch(another, result, depth)); + return dependencyTermMatch(another, result, depth); } else if (isDependency()) { -// for (List perm : Permutation.permutation(another.getChildren().size() - 1)) { -// Set res2 = new HashSet<>(res); -// boolean flg = true; -// for (int metaTermIndex = 0; metaTermIndex < perm.size(); metaTermIndex++) { -// int anotherTermIndex = perm.get(metaTermIndex); -// RDLTerm metaDependedTerm = (RDLTerm) getChild(metaTermIndex + 1); -// RDLTerm anotherDependedTerm = (RDLTerm) another.getChild(anotherTermIndex + 1); -// if (metaDependedTerm instanceof MetaRDLTerm metaTerm) { -// res2 = metaTerm.isMatchedBy(anotherDependedTerm, res2, depth + 1); -// if (res2.isEmpty()) { -// flg = false; -// break; -// } -// } else { -// if (!(metaDependedTerm.equals(anotherDependedTerm))) { -// flg = false; -// break; -// } -// } -// } -// if (flg) { -// result.addAll(res2); -// break; -// } - result.addAll(dependencyMatch(another, result, depth)); + return dependencyMatch(another, result, depth); } return result; } private Set dependencyMatch(RDLTerm another, Set constraint, int depth) { + Set result = new HashSet<>(); for (List perm : Permutation.permutation(another.getChildren().size() - 1)) { - Set result = new HashSet<>(constraint); + Set localResult = new HashSet<>(constraint); + boolean flg = true; for (int metaTermIndex = 0; metaTermIndex < perm.size(); metaTermIndex++) { int anotherTermIndex = perm.get(metaTermIndex); RDLTerm metaDependedTerm = (RDLTerm) getChild(metaTermIndex + 1); RDLTerm anotherDependedTerm = (RDLTerm) another.getChild(anotherTermIndex + 1); if (metaDependedTerm instanceof MetaRDLTerm metaTerm) { - result = metaTerm.isMatchedBy(anotherDependedTerm, result, depth + 1); - if (result.isEmpty()) { + localResult = metaTerm.isMatchedBy(anotherDependedTerm, localResult, depth + 1); + if (localResult.isEmpty()) { + flg = false; break; } } else { if (!(metaDependedTerm.equals(anotherDependedTerm))) { + flg = false; break; } } } - return result; + if (flg) { + result.addAll(localResult); + } } - return new HashSet<>(); + return result; } private Set dependencyTermMatch(RDLTerm another, Set constraint, int depth) { - for (List perm : Permutation.permutation(another.getChildren().size() - 1)) { - Set result = new HashSet<>(constraint); + Set result = new HashSet<>(); + for (List perm : Permutation.permutation((another.getChildren().size() - 1) / 2)) { + Set localResult = new HashSet<>(constraint); + boolean flg = true;; for (int metaTermIndex = 0; metaTermIndex < perm.size(); metaTermIndex++) { int anotherTermIndex = perm.get(metaTermIndex); - RDLTerm metaDependedTerm = (RDLTerm) getChild(metaTermIndex + 1); - RDLTerm anotherDependedTerm = (RDLTerm) another.getChild(anotherTermIndex + 1); + RDLTerm metaDependedTerm = (RDLTerm) getChild(2 * metaTermIndex + 1); + RDLTerm anotherDependedTerm = (RDLTerm) another.getChild(2 * anotherTermIndex + 1); + RDLTerm metaArgTerm = (RDLTerm) getChild(2 * metaTermIndex + 2); + RDLTerm anotherArgTerm = (RDLTerm) another.getChild(2 * anotherTermIndex + 2); if (metaDependedTerm instanceof MetaRDLTerm metaTerm) { - result = metaTerm.isMatchedBy(anotherDependedTerm, result, depth + 1); - if (result.isEmpty()) { + localResult = metaTerm.isMatchedBy(anotherDependedTerm, localResult, depth + 1); + if (localResult.isEmpty()) { + flg = false; break; } } else { if (!(metaDependedTerm.equals(anotherDependedTerm))) { + flg = false; + break; + } + } + if (metaArgTerm instanceof MetaRDLTerm metaTerm) { + localResult = metaTerm.isMatchedBy(anotherArgTerm, localResult, depth + 1); + if (localResult.isEmpty()) { + flg = false; + break; + } + } else { + if (!(metaArgTerm.equals(anotherArgTerm))) { + flg = false; break; } } } - return result; + if (flg) { + result.addAll(localResult); + } } - return new HashSet<>(); + return result; } public boolean checkTermType(Class clazz) { diff --git a/src/test/java/terms/DependencyTermTest.java b/src/test/java/terms/DependencyTermTest.java index eaa726d..e3542e6 100644 --- a/src/test/java/terms/DependencyTermTest.java +++ b/src/test/java/terms/DependencyTermTest.java @@ -147,7 +147,6 @@ ) ); Set tmp = mt1.isMatchedBy(t1); - System.out.println(tmp); assertTrue(! tmp.isEmpty()); }