diff --git a/src/main/java/inference/InferenceRule.java b/src/main/java/inference/InferenceRule.java index ca3b6e7..7c87363 100644 --- a/src/main/java/inference/InferenceRule.java +++ b/src/main/java/inference/InferenceRule.java @@ -1,18 +1,21 @@ package inference; +import java.util.ArrayList; import java.util.Collection; +import java.util.HashMap; import java.util.HashSet; import java.util.List; +import java.util.Map; import java.util.Set; import exceptions.SubstituteFailedException; import lombok.Getter; +import models.algebra.Variable; import models.formulas.Formula; -import models.formulas.meta.MetaDependencyFormula; -import models.formulas.meta.MetaEquationFormula; import models.formulas.meta.MetaFormula; import models.terms.RDLTerm; import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaVariable; import utils.Permutation; public class InferenceRule { @@ -60,41 +63,12 @@ return false; } - Set matchResult = this.conclusion.isMatchedBy(conclusion); - Set givenAssumptions = new HashSet<>(assumptions); - - for (MetaFormula assumption : this.assumptions) { - boolean flg = false; - for (Formula given : givenAssumptions) { - matchResult = assumption.isMatchedBy(given, matchResult); - if (! matchResult.isEmpty()) { - flg = true; - givenAssumptions.remove(given); - break; - } - } - if (!flg) { - return false; + for(List assumption : Permutation.permutation(assumptions, this.assumptions.size())) { + if (check(assumption, conclusion)) { + return true; } } - - if (this.defaultOrderConstraint != null) { - for (MatchConstraint constraint: matchResult) { - if (defaultOrderConstraint.check(constraint.getOrderConstraint())) { - return true; - } - } - return false; - } - - return true; - -// for(List assumption : permutation(assumptions, this.assumptions.size())) { -// if (check(assumption, conclusion)) { -// return true; -// } -// } -// return false; + return false; } private boolean check(List assumptions, Formula conclusion) { @@ -121,12 +95,70 @@ } - public Formula apply(List assumptions) { + public Set apply(List assumptions, Set existTerms) { + Set result = new HashSet<>(); + Set assumptionVariables = new HashSet<>(); + Set conclusionVariables = new HashSet<>(); + for (MetaFormula assumption: this.assumptions) { + assumptionVariables.addAll(assumption.getSubTerms(MetaVariable.class)); + } + conclusionVariables.addAll(conclusion.getSubTerms(MetaVariable.class)); + + conclusionVariables.removeAll(assumptionVariables); + List leftVariables = new ArrayList<>(conclusionVariables); + + if (! conclusionVariables.isEmpty()) { + for (List variables: Permutation.permutation(existTerms, leftVariables.size())) { + Map binding = new HashMap<>(); + for (int i = 0; i < variables.size(); i++) { + binding.put(leftVariables.get(i).getVariableName(), variables.get(i)); + } + try { + Formula res = apply(assumptions, new MatchConstraint(binding, new HashMap<>())); + if (res != null) { + Set constraints = conclusion.isMatchedBy(res); + boolean flg = true; + for (MatchConstraint constraint : constraints) { + if (! defaultOrderConstraint.check(constraint.getOrderConstraint())) { + flg = false; + break; + } + } + if (flg) { + result.add(res); + } + } + } catch (SubstituteFailedException e) { + continue; + } + } + } + return result; + } + + public Formula apply(Formula ...assumptions) { + return apply(Set.of(assumptions)); + } + + public Formula apply(Collection assumptions) { + if (assumptions.size() != getAssumptionSize()) { + return null; + } + for (List assumptionList : Permutation.permutation(assumptions, assumptions.size())) { + Formula result = apply(assumptionList); + if (result != null) { + return result; + } + } + return null; + } + + private Formula apply(List assumptions) { if (assumptions.size() != getAssumptionSize()) { return null; } Set result = this.assumptions.get(0).isMatchedBy(assumptions.get(0)); - for (int i = 0; i < getAssumptionSize(); i++) { + for (int i = 1; i < getAssumptionSize(); i++) { result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result); if (result.isEmpty()) { return null; @@ -135,70 +167,23 @@ return conclusion.substitution(result.iterator().next().getBinding()); } - public Set apply(List assumptions, Set existTerms) { - Set result = new HashSet<>(); + private Formula apply(List assumptions, MatchConstraint constraint) { if (assumptions.size() != getAssumptionSize()) { return null; } - Set res = this.assumptions.get(0).isMatchedBy(assumptions.get(0)); + + Set result = new HashSet<>(); + result.add(constraint); for (int i = 0; i < getAssumptionSize(); i++) { - res = this.assumptions.get(i).isMatchedBy(assumptions.get(i), res); - if (res.isEmpty()) { - return result; + result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result); + if (result.isEmpty()) { + return null; } } - for (MatchConstraint constraint : res) { - try { - result.add(conclusion.substitution(constraint.getBinding())); - } catch (SubstituteFailedException e) {} - } - for (RDLTerm term : existTerms) { - Set localConstraints = new HashSet<>(res.stream().map(v -> new MatchConstraint(v)).toList()); - if (conclusion instanceof MetaEquationFormula equation) { - localConstraints= equation.getLeftSideHand().isMatchedBy(term, localConstraints); - } - else if (conclusion instanceof MetaDependencyFormula dependency) { - localConstraints = dependency.getDependency().isMatchedBy(term, localConstraints); - } - for (MatchConstraint constraint : localConstraints) { - result.add(conclusion.substitution(constraint.getBinding())); - } - } - for (RDLTerm term : existTerms) { - Set localConstraints = new HashSet<>(res.stream().map(v -> new MatchConstraint(v)).toList()); - if (conclusion instanceof MetaEquationFormula equation) { - localConstraints= equation.getRightSideHand().isMatchedBy(term, localConstraints); - } - for (MatchConstraint constraint : localConstraints) { - result.add(conclusion.substitution(constraint.getBinding())); - } - } - return result; + Formula subRes = conclusion.substitution(result.iterator().next().getBinding()); + return subRes; } - public Formula apply(Collection assumptions) { - if (assumptions.size() != getAssumptionSize()) { - return null; - } - for (List assumptionList : Permutation.permutation(assumptions, assumptions.size())) { - boolean matchFailed = false; - for (int i = 0; i < getAssumptionSize(); i++) { - Set result = this.assumptions.get(i).isMatchedBy(assumptionList.get(i)); - if (result.isEmpty()) { - matchFailed = true; - break; - } - } - if (matchFailed) { - continue; - } else { - return apply(assumptionList); - } - } - return null; - } - - public int getAssumptionSize() { return this.assumptions.size(); } diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index 1c48625..03126a7 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -12,11 +12,19 @@ import java.util.Set; import java.util.stream.Collectors; +import models.algebra.Variable; import models.formulas.DependencyFormula; import models.formulas.EquationFormula; import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.formulas.meta.MetaEquationFormula; import models.terms.EvaluatableTerm; import models.terms.RDLTerm; +import models.terms.meta.MetaDependencyGenerator; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaResource; +import models.terms.meta.OrderConstraint; import utils.Product; public class ProofSystem { @@ -257,72 +265,88 @@ // // //======================Dependency Axioms============================= // -// private static final InferenceRule identityMapping = new InferenceRule( -// "Identity Mapping", -// List.of( -// new MetaEquationFormula( -// new MetaEvaluatableTermVariable(new Variable("te")), -// new MetaResource(new Variable("r")) -// ) -// ), -// new MetaDependencyFormula( -// new MetaEvaluatableTermVariable(new Variable("te")), -// new MetaResource(new Variable("r")) -// ) -// ); -// -// private static final InferenceRule compositeMapping = new InferenceRule( -// "Composite Mapping", -// List.of( -// new MetaDependencyFormula( -// new MetaEvaluatableTermVariable(new Variable("te")), -// new MetaResource(new Variable("r")) -// ), -// new MetaDependencyFormula( -// new MetaEvaluatableTermVariable(new Variable("r")), -// new MetaResource(new Variable("q")) -// ) -// ), -// new MetaDependencyFormula( -// new MetaEvaluatableTermVariable(new Variable("te")), -// new MetaResource(new Variable("q")) -// ) -// ); -// -// private static final InferenceRule constantMapping = new InferenceRule( -// "Constant Mapping", -// List.of(), -// new MetaDependencyFormula( -// new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), -// new MetaResource(new Variable("r"), new Variable("m")) -// ), -// new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")) -// ); -// -// private static final InferenceRule slicedMapping = new InferenceRule( -// "Sliced Mapping", -// List.of( -// new MetaDependencyFormula( -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaResource(new Variable("r")) -// ), -// new MetaResource(new Variable("p")) -// ), -// new MetaDependencyFormula( -// new MetaEvaluatableTermVariable(new Variable("te")), -// new MetaResource(new Variable("p")) -// ) -// ), -// new MetaDependencyFormula( -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaResource(new Variable("r")), -// new MetaEvaluatableTermVariable(new Variable("te")) -// ), -// new MetaResource(new Variable("p")) -// ) -// ); + public static final InferenceRule identityMapping = new InferenceRule( + "Identity Mapping", + List.of( + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaResource(new Variable("r")) + ) + ), + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaResource(new Variable("r")) + ) + ); + + public static final InferenceRule compositeMapping = new InferenceRule( + "Composite Mapping", + List.of( + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaDependencyGenerator() { + @Override + public RDLTerm generate(int i) { + if (i == 0) { + return new MetaResource(new Variable("r")); + } else { + return new MetaResource(new Variable("r" + i)); + } + }} + ), + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("r")), + new MetaResource(new Variable("q")) + ) + ), + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaDependencyGenerator() { + @Override + public RDLTerm generate(int i) { + if (i == 0) { + return new MetaResource(new Variable("q")); + } else { + return new MetaResource(new Variable("r" + i)); + } + }} + ) + ); + + public static final InferenceRule constantMapping = new InferenceRule( + "Constant Mapping", + List.of(), + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), + new MetaResource(new Variable("r"), new Variable("m")) + ), + new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")) + ); + + public static final InferenceRule slicedMapping = new InferenceRule( + "Sliced Mapping", + List.of( + new MetaDependencyFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResource(new Variable("r")) + ), + new MetaResource(new Variable("p")) + ), + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaResource(new Variable("p")) + ) + ), + new MetaDependencyFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResource(new Variable("r")), + new MetaEvaluatableTermVariable(new Variable("te")) + ), + new MetaResource(new Variable("p")) + ) + ); // // //======================Set-Theoretic Axioms============================= // diff --git a/src/main/java/models/formulas/DependencyFormula.java b/src/main/java/models/formulas/DependencyFormula.java index 2d0d5b6..6918696 100644 --- a/src/main/java/models/formulas/DependencyFormula.java +++ b/src/main/java/models/formulas/DependencyFormula.java @@ -17,10 +17,13 @@ this.dependency = dependency; } - public DependencyFormula(RDLTerm dependingTerm, Set dependedResources) { - this.dependency = new Dependency(dependingTerm, new TreeSet<>(dependedResources)); + public DependencyFormula(RDLTerm dependingTerm, Set dependedTerms) { + this.dependency = new Dependency(dependingTerm, new TreeSet<>(dependedTerms)); } - + + public DependencyFormula(RDLTerm dependingTerm, EvaluatableTerm ...dependedTerms) { + this.dependency = new Dependency(dependingTerm, dependedTerms); + } @Override public String toString() { diff --git a/src/main/java/models/formulas/meta/MetaDependencyFormula.java b/src/main/java/models/formulas/meta/MetaDependencyFormula.java index d6757bb..871deee 100644 --- a/src/main/java/models/formulas/meta/MetaDependencyFormula.java +++ b/src/main/java/models/formulas/meta/MetaDependencyFormula.java @@ -13,6 +13,7 @@ import models.terms.Dependency; import models.terms.RDLTerm; import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDependencyGenerator; import models.terms.meta.MetaDependencyVariable; import models.terms.meta.MetaRDLTerm; @@ -40,6 +41,10 @@ this(dependingTerm, new HashSet<>(Arrays.asList(dependedTerms))); } + public MetaDependencyFormula(MetaRDLTerm dependingTerm, MetaDependencyGenerator generator) { + this.dependency = new MetaRDLTerm(dependingTerm, generator); + } + @Override public Set isMatchedBy(Formula formula, MatchConstraint constraint) { if (! (formula instanceof DependencyFormula)) { @@ -72,5 +77,10 @@ public int hashCode() { return ("MDF" + toString()).hashCode(); } + + @Override + public Set getSubTerms(Class clazz) { + return new HashSet<>(dependency.getSubTerms(clazz).values()); + } } diff --git a/src/main/java/models/formulas/meta/MetaEquationFormula.java b/src/main/java/models/formulas/meta/MetaEquationFormula.java index 8c07b25..e061866 100644 --- a/src/main/java/models/formulas/meta/MetaEquationFormula.java +++ b/src/main/java/models/formulas/meta/MetaEquationFormula.java @@ -63,5 +63,13 @@ public int hashCode() { return ("MEF" + toString()).hashCode(); } + + @Override + public Set getSubTerms(Class clazz) { + Set result = new HashSet<>(); + result.addAll(leftSideHand.getSubTerms(clazz).values()); + result.addAll(rightSideHand.getSubTerms(clazz).values()); + return result; + } } diff --git a/src/main/java/models/formulas/meta/MetaFormula.java b/src/main/java/models/formulas/meta/MetaFormula.java index 0340d09..4087d45 100644 --- a/src/main/java/models/formulas/meta/MetaFormula.java +++ b/src/main/java/models/formulas/meta/MetaFormula.java @@ -29,6 +29,8 @@ public abstract Formula substitution(Map binding); + public abstract Set getSubTerms(Class clazz); + public abstract String toString(); public abstract boolean equals(Object another); public abstract int hashCode(); diff --git a/src/main/java/models/terms/Dependency.java b/src/main/java/models/terms/Dependency.java index d382318..e4d031f 100644 --- a/src/main/java/models/terms/Dependency.java +++ b/src/main/java/models/terms/Dependency.java @@ -1,6 +1,7 @@ package models.terms; import java.util.Arrays; +import java.util.List; import java.util.Set; import java.util.TreeSet; import java.util.stream.Collectors; @@ -35,6 +36,10 @@ this(dependingTerm, new TreeSet<>(Arrays.asList(dependedTerms))); } + public Dependency(RDLTerm dependingTerm, ListdependedTerms) { + this(dependingTerm, new TreeSet<>(dependedTerms)); + } + @Override public int getTermOrder() { return getOrder() - 1; diff --git a/src/main/java/models/terms/meta/MetaDependencyGenerator.java b/src/main/java/models/terms/meta/MetaDependencyGenerator.java index 191ecf1..d90f8e0 100644 --- a/src/main/java/models/terms/meta/MetaDependencyGenerator.java +++ b/src/main/java/models/terms/meta/MetaDependencyGenerator.java @@ -5,6 +5,6 @@ @FunctionalInterface public interface MetaDependencyGenerator { - RDLTerm generate(int i, int size); + RDLTerm generate(int i); } diff --git a/src/main/java/models/terms/meta/MetaDependencyTermGenerator.java b/src/main/java/models/terms/meta/MetaDependencyTermGenerator.java index 2974988..07c1ef8 100644 --- a/src/main/java/models/terms/meta/MetaDependencyTermGenerator.java +++ b/src/main/java/models/terms/meta/MetaDependencyTermGenerator.java @@ -7,6 +7,6 @@ record TermPair(RDLTerm dependedTerm, RDLTerm argTerm) {}; - TermPair generate(int i, int size); + TermPair generate(int i); } diff --git a/src/main/java/models/terms/meta/MetaRDLTerm.java b/src/main/java/models/terms/meta/MetaRDLTerm.java index 1993240..0253723 100644 --- a/src/main/java/models/terms/meta/MetaRDLTerm.java +++ b/src/main/java/models/terms/meta/MetaRDLTerm.java @@ -59,7 +59,7 @@ } this.size = size; this.termType = TermType.META_DEPENDENCY; - this.metaDependencyGenerator = (i, j) -> (RDLTerm) this.getChild(i + 1); + this.metaDependencyGenerator = (i) -> (RDLTerm) this.getChild(i + 1); } public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaRDLTerm dependedTerm) { @@ -106,7 +106,7 @@ addChild(argTerm); } this.termType = TermType.META_DEPENDENCY_TERM; - this.metaDependencyTermGenerator = (i, j) -> new TermPair((RDLTerm) this.getChild(i * 2 + 1), (RDLTerm) this.getChild(i * 2 + 2)); + this.metaDependencyTermGenerator = (i) -> new TermPair((RDLTerm) this.getChild(i * 2 + 1), (RDLTerm) this.getChild(i * 2 + 2)); } public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaRDLTerm ...terms) { @@ -122,33 +122,57 @@ } public RDLTerm substitute(Map binding) { + RDLTerm dependingTerm = (RDLTerm) getChild(0); + List dependedTerms = new ArrayList<>(); + if (dependingTerm instanceof MetaRDLTerm) { + dependingTerm = ((MetaRDLTerm) dependingTerm).substitute(binding); + } if (isDependency()) { - RDLTerm dependingTerm = (RDLTerm) getChild(0); - RDLTerm dependedVariable = (RDLTerm) getChild(1); - if (dependingTerm instanceof MetaRDLTerm) { - dependingTerm = ((MetaRDLTerm) dependingTerm).substitute(binding); + for (int i = 0; i < binding.size(); i++) { + if ((! isDynamic) && (i >= getChildren().size() - 1)) break; + RDLTerm term = metaDependencyGenerator.generate(i); + try { + if (term instanceof MetaRDLTerm metaTerm) { + term = metaTerm.substitute(binding); + } + } catch(SubstituteFailedException e) { + continue; + } + if (term instanceof EvaluatableTerm te) { + dependedTerms.add(te); + } } - if (dependedVariable instanceof MetaRDLTerm) { - dependedVariable = ((MetaRDLTerm) dependedVariable).substitute(binding); - } - if (dependedVariable instanceof Resource) { - return new Dependency(dependingTerm, (Resource) dependedVariable); + try { + return new Dependency(dependingTerm, dependedTerms); + } catch (SyntaxException e) { + throw new SubstituteFailedException(e.getMessage()); } } else if (isDependencyTerm()) { - RDLTerm dependingTerm = (RDLTerm) getChild(0); - if (dependingTerm instanceof MetaRDLTerm metaDependingTerm) { - dependingTerm = metaDependingTerm.substitute(binding); - } List terms = new ArrayList<>(); - for (int i = 1; i < getArity(); i++) { - RDLTerm term = (RDLTerm) getChild(i); - if (term instanceof MetaRDLTerm metaTerm) { - term = metaTerm.substitute(binding); + for (int i = 0; i < binding.size(); i++) { + if ((! isDynamic) && (i >= getChildren().size() - 1)) break; + TermPair termPair = metaDependencyTermGenerator.generate(i); + RDLTerm dependedTerm = termPair.dependedTerm(); + RDLTerm argTerm = termPair.argTerm(); + try { + if (dependedTerm instanceof MetaRDLTerm metaTerm) { + dependedTerm = metaTerm.substitute(binding); + } + if (argTerm instanceof MetaRDLTerm metaTerm) { + argTerm = metaTerm.substitute(binding); + } + terms.add((EvaluatableTerm) dependedTerm); + terms.add((EvaluatableTerm) argTerm); + } catch (SubstituteFailedException e) { + continue; } - terms.add((EvaluatableTerm) term); } - return new DependencyTerm((EvaluatableTerm) dependingTerm, terms); + try { + return new DependencyTerm((EvaluatableTerm) dependingTerm, terms); + } catch (SyntaxException e) { + throw new SubstituteFailedException(e.getMessage()); + } } throw new SubstituteFailedException(); } @@ -197,7 +221,7 @@ boolean flg = true; for (int i = 0; i < perm.size(); i++) { int j = perm.get(i); - TermPair termPair = this.metaDependencyTermGenerator.generate(j, perm.size()); + TermPair termPair = this.metaDependencyTermGenerator.generate(j); RDLTerm dependedChild = termPair.dependedTerm(); RDLTerm argChild = termPair.argTerm(); RDLTerm anotherDependedChild = (RDLTerm) another.getChild(i * 2 + 1); @@ -240,7 +264,7 @@ boolean flg = true; for (int i = 0; i < perm.size(); i++) { int j = perm.get(i); - RDLTerm dependedChild = this.metaDependencyGenerator.generate(j, perm.size()); + RDLTerm dependedChild = this.metaDependencyGenerator.generate(j); RDLTerm anotherDependedChild = (RDLTerm) another.getChild(i + 1); if (dependedChild instanceof MetaRDLTerm) { MetaRDLTerm metaChild = (MetaRDLTerm) dependedChild; @@ -312,6 +336,7 @@ return true; } + @Override public String toString() { switch(termType) { diff --git a/src/test/java/inferencerule/DependencyAxiomTest.java b/src/test/java/inferencerule/DependencyAxiomTest.java new file mode 100644 index 0000000..834cfe0 --- /dev/null +++ b/src/test/java/inferencerule/DependencyAxiomTest.java @@ -0,0 +1,68 @@ +package inferencerule; +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.jupiter.api.Test; + +import java.util.List; +import java.util.Set; + +import inference.ProofSystem; +import models.formulas.DependencyFormula; +import models.formulas.EquationFormula; +import models.formulas.Formula; +import models.terms.DependencyTerm; +import models.terms.Resource; +import utils.Utils; + +public class DependencyAxiomTest { + + Resource a = new Resource("a", Utils.INT, 1); + Resource b = new Resource("b", Utils.INT, 1); + Resource c = new Resource("c", Utils.INT, 1); + Resource d = new Resource("d", Utils.INT, 1); + Resource e = new Resource("e", Utils.INT, 1); + + @Test + void IdentityMappingTest() { + EquationFormula ef1 = new EquationFormula(a, b); + DependencyFormula df1 = new DependencyFormula(a, b); + boolean tmp = ProofSystem.identityMapping.check(List.of(ef1), df1); + assertTrue(tmp); + Formula conclusion = ProofSystem.identityMapping.apply(List.of(ef1)); + assertEquals(df1, conclusion); + + DependencyTerm t1 = new DependencyTerm(a, b, c); + EquationFormula ef2 = new EquationFormula(t1, d); + DependencyFormula df2 = new DependencyFormula(t1, d); + assertTrue(ProofSystem.identityMapping.check(List.of(ef2), df2)); + assertEquals(df2, ProofSystem.identityMapping.apply(ef2)); + } + + @Test + void CompositeMappingTest() { + DependencyFormula df1 = new DependencyFormula(a, b, c); + DependencyFormula df2 = new DependencyFormula(c, d); + DependencyFormula df3 = new DependencyFormula(a, d, b); + assertTrue(ProofSystem.compositeMapping.check(List.of(df1, df2), df3)); + assertEquals(df3, ProofSystem.compositeMapping.apply(List.of(df1, df2))); + + DependencyFormula df4 = new DependencyFormula(a, b); + DependencyFormula df5 = new DependencyFormula(b, c); + DependencyFormula df6 = new DependencyFormula(a, c); + assertTrue(ProofSystem.compositeMapping.check(List.of(df4, df5), df6)); + assertEquals(df6, ProofSystem.compositeMapping.apply(List.of(df4, df5))); + } + + @Test + void ConstantMapping() { + Resource aa = new Resource("aa", Utils.INT, 1); + Resource bb = new Resource("bb", Utils.INT, 2); + Resource cc = new Resource("cc", Utils.INT, 1); + DependencyFormula d1 = new DependencyFormula(aa, bb); + DependencyFormula d3 = new DependencyFormula(aa, cc); + Set result = ProofSystem.constantMapping.apply(List.of(), Set.of(aa, bb, cc)); + assertTrue(result.contains(d1)); + assertFalse(result.contains(d3)); + } + +} diff --git a/src/test/java/terms/DependencyTermTest.java b/src/test/java/terms/DependencyTermTest.java index 39835cf..8fedc28 100644 --- a/src/test/java/terms/DependencyTermTest.java +++ b/src/test/java/terms/DependencyTermTest.java @@ -139,7 +139,7 @@ DependencyTerm t1 = new DependencyTerm(a1, a2, a3, a4, a5); MetaResource x = new MetaResource(new Variable("x"), new Variable("n")); MetaRDLTerm mt1 = new MetaRDLTerm(x, - (MetaDependencyTermGenerator) (i, j) -> + (MetaDependencyTermGenerator) (i) -> new TermPair( new MetaResource(new Variable("x" + (2*i + 1)), Utils.parse("n-1-" + i)), new MetaResource(new Variable("x" + (2*i + 2)), Utils.parse("n+1")) @@ -154,7 +154,7 @@ @Test void DynamicMatchTest2() { MetaResource x = new MetaResource(new Variable("x")); - MetaRDLTerm mt1 = new MetaRDLTerm(x, (MetaDependencyTermGenerator) (i, j) -> new TermPair(new MetaResource(new Variable("x" + i)), new MetaResource(new Variable("y"+i)))); + MetaRDLTerm mt1 = new MetaRDLTerm(x, (MetaDependencyTermGenerator) (i) -> new TermPair(new MetaResource(new Variable("x" + i)), new MetaResource(new Variable("y"+i)))); DependencyTerm d1 = new DependencyTerm(a, b, c); DependencyTerm d2 = new DependencyTerm(a, b, c, d, e); assertTrue(! mt1.isMatchedBy(d1).isEmpty()); diff --git a/src/test/java/terms/DependencyTest.java b/src/test/java/terms/DependencyTest.java index f31a5ff..13c885b 100644 --- a/src/test/java/terms/DependencyTest.java +++ b/src/test/java/terms/DependencyTest.java @@ -124,8 +124,8 @@ MetaResource x = new MetaResource(new Variable("x")); MetaRDLTerm md1 = new MetaRDLTerm(x, new MetaDependencyGenerator() { @Override - public RDLTerm generate(int i, int size) { - if (i != size) { + public RDLTerm generate(int i) { + if (i != 0) { return new MetaResource(new Variable("r" + i)); } else { return new MetaResource(new Variable("y")); @@ -142,12 +142,4 @@ assertTrue(! md2.isMatchedBy(d3, tmp).isEmpty()); } -// { -// if (i != size) { -// return new MetaResource(new Variable("r" + i)) -// } else { -// return new MetaResource(new Variable("y")) -// } -// } - }