diff --git a/src/main/java/inference/InferenceRule.java b/src/main/java/inference/InferenceRule.java index f8e16ff..5f76eca 100644 --- a/src/main/java/inference/InferenceRule.java +++ b/src/main/java/inference/InferenceRule.java @@ -96,6 +96,7 @@ } protected Set apply(List assumptions, MatchConstraint constraint) { + Map context = new HashMap<>(); if (assumptions.size() < getAssumptionSize()) { return new HashSet<>(); } @@ -103,7 +104,7 @@ Set result = new HashSet<>(); result.add(constraint); for (int i = 0; i < getAssumptionSize(); i++) { - result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result); + result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result, context); if (result.isEmpty()) { return new HashSet<>(); } @@ -117,7 +118,7 @@ for (int j = 0; j < this.repetitionAssumptions.size(); j++) { Formula assumption = assumptions.get(this.assumptions.size() + i * this.repetitionAssumptions.size() + j); MetaFormula metaAssumption = metaAssumptions.get(j); - result = metaAssumption.isMatchedBy(assumption, result); + result = metaAssumption.isMatchedBy(assumption, result, context); if (result.isEmpty()) { return new HashSet<>(); } @@ -129,7 +130,9 @@ try { int maxIndex = conclusionMaxIndexCalculator != null ? conclusionMaxIndexCalculator.calculate(assumptions) : 0; int maxDepth = conclusionMaxDepthCalculator != null ? conclusionMaxDepthCalculator.calculate(assumptions) : 1; - subRes.add(conclusion.substitution(con.getBinding(), Map.of("maxIndex", maxIndex, "maxDepth", maxDepth))); + context.put("maxIndex", maxIndex); + context.put("maxDepth", maxDepth); + subRes.add(conclusion.substitution(con.getBinding(), context)); } catch (SubstituteFailedException e) { continue; } @@ -137,7 +140,6 @@ return subRes; } - public int getAssumptionSize() { return this.assumptions.size(); } diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index 624f162..566c628 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -13,6 +13,7 @@ import java.util.stream.Collectors; import inference.axioms.CompositeMapping; +import inference.axioms.RedundancyElimination; import inference.axioms.RightSubstitution; import inference.axioms.UncurriedMapping; import models.algebra.Variable; @@ -24,11 +25,13 @@ import models.terms.EvaluatableTerm; import models.terms.RDLTerm; import models.terms.meta.MetaDependencyTerm; +import models.terms.meta.MetaDependencyVariable; import models.terms.meta.MetaDynamicDependencyTerm; import models.terms.meta.MetaEvaluatableTermVariable; import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaTermGenerator; import models.terms.meta.OrderConstraint; +import utils.ExpressionUitls; import utils.Product; public class ProofSystem { @@ -202,6 +205,8 @@ ); + + // // //======================Dependency Axioms============================= // @@ -243,6 +248,21 @@ public static final InferenceRule uncurriedMapping = new UncurriedMapping(); + public static final InferenceRule redundantDependency = new InferenceRule( + "Redundant Dependency", + List.of( + new MetaDependencyFormula(new MetaDependencyVariable(new Variable("d"), new Variable("n"))) + ), + List.of(), + new MetaDependencyFormula(new MetaDependencyVariable(new Variable("d"), new Variable("n")), new MetaEvaluatableTermVariable(new Variable("p"), ExpressionUitls.parse("n - 1"))), + null, + null, + null, + null + ); + + public static final InferenceRule redundancyElimination = new RedundancyElimination(); + /* * new InferenceRule( "", diff --git a/src/main/java/inference/axioms/MapComposition.java b/src/main/java/inference/axioms/MapComposition.java new file mode 100644 index 0000000..42186f9 --- /dev/null +++ b/src/main/java/inference/axioms/MapComposition.java @@ -0,0 +1,72 @@ +package inference.axioms; +import java.util.Map; + +import inference.EquationAxiom; +import models.algebra.Variable; +import models.formulas.meta.MetaDependencyFormula; +import models.formulas.meta.MetaEquationFormula; +import models.terms.meta.MetaDependencyTerm; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaDynamicDependencyTerm; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; + +public class MapComposition extends EquationAxiom { + + public MapComposition() { + super("Map Composition"); + assumptions.add( + new MetaDependencyFormula( + new MetaDynamicDependency( + (ci, cd, mi, md, context) -> ci - 2 == 0 ? new MetaEvaluatableTermVariable(new Variable("u")) : new MetaEvaluatableTermVariable(new Variable("u" + (ci - 2))), + new MetaEvaluatableTermVariable(new Variable("s")), + new MetaEvaluatableTermVariable(new Variable("t")) + ) + ) + ); + assumptions.add( + new MetaDependencyFormula( + new MetaDynamicDependency( + (ci, cd, mi, md, context) -> ci - 1 == 0 ? new MetaEvaluatableTermVariable(new Variable("v")) : new MetaEvaluatableTermVariable(new Variable("v" + (ci - 1))), + new MetaEvaluatableTermVariable(new Variable("t")) + ) + ) + ); + repetitionAssumptions.add( + new MetaEquationFormula( + new MetaDependencyTerm( + new MetaEvaluatableTermVariable(new Variable("v")), + new MetaEvaluatableTermVariable(new Variable("xxx")), + new MetaEvaluatableTermVariable(new Variable("yyy")) + ), + new MetaEvaluatableTermVariable(new Variable("x")) + ) + ); + + conclusion = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + + return null; + }}, + new MetaEvaluatableTermVariable(new Variable("s")), + new MetaEvaluatableTermVariable(new Variable("t")) + ), + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + return null; + } + }, + new MetaEvaluatableTermVariable(new Variable("s")) + ) + ); + + } + +} diff --git a/src/main/java/inference/axioms/RedundancyElimination.java b/src/main/java/inference/axioms/RedundancyElimination.java new file mode 100644 index 0000000..3d28f79 --- /dev/null +++ b/src/main/java/inference/axioms/RedundancyElimination.java @@ -0,0 +1,114 @@ +package inference.axioms; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import exceptions.SubstituteFailedException; +import inference.InferenceRule; +import models.algebra.Variable; +import models.formulas.DependencyFormula; +import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.formulas.meta.MetaFormula; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaRDLTermVariable; +import models.terms.meta.MetaTermGenerator; + +public class RedundancyElimination extends InferenceRule { + + public RedundancyElimination() { + super("Redundancy Elimination"); + assumptions.add( + new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + context.put("firstAssumptionIndex", curIndex + 1); + return new MetaEvaluatableTermVariable(new Variable("v" + curIndex)); + } + }, + new MetaEvaluatableTermVariable(new Variable("u")) + ) + ) + ); + assumptions.add( + new MetaDependencyFormula( + new MetaDynamicDependency( + (ci, cd, mi, md, context) -> new MetaEvaluatableTermVariable(new Variable("v" + (ci - 2))), + new MetaRDLTermVariable(new Variable("s")), + new MetaEvaluatableTermVariable(new Variable("u")) + ) + ) + ); + conclusion = new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 2; + int firstAssumptionIndex = (Integer) context.get("firstAssumptionIndex"); + return new MetaEvaluatableTermVariable(new Variable("v" + (curIndex + firstAssumptionIndex))); + }}, + new MetaRDLTermVariable(new Variable("s")), + new MetaEvaluatableTermVariable(new Variable("u")) + ) + ); + this.conclusionMaxIndexCalculator = (assumptions) -> ((DependencyFormula) assumptions.get(1)).getDependency().getMaxIndex() - ((DependencyFormula) assumptions.get(0)).getDependency().getMaxIndex() + 1; + } + + protected Set apply(List assumptions, MatchConstraint constraint) { + Map context = new HashMap<>(); + if (assumptions.size() < getAssumptionSize()) { + return new HashSet<>(); + } + if (((DependencyFormula) assumptions.get(0)).getDependency().getMaxIndex() >= ((DependencyFormula) assumptions.get(1)).getDependency().getMaxIndex()) { + return new HashSet<>(); + } + + Set result = new HashSet<>(); + result.add(constraint); + for (int i = 0; i < getAssumptionSize(); i++) { + result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result, context); + if (result.isEmpty()) { + return new HashSet<>(); + } + } + if (this.repetitionAssumptions.size() != 0 && (assumptions.size() - this.assumptions.size()) % this.repetitionAssumptions.size() != 0) { + return new HashSet<>(); + } + if (this.repetitionAssumptions.size() != 0) { + for (int i = 0; i < (assumptions.size() - this.assumptions.size()) / this.repetitionAssumptions.size(); i++) { + List metaAssumptions = repetitionAssumptionGenerate(i); + for (int j = 0; j < this.repetitionAssumptions.size(); j++) { + Formula assumption = assumptions.get(this.assumptions.size() + i * this.repetitionAssumptions.size() + j); + MetaFormula metaAssumption = metaAssumptions.get(j); + result = metaAssumption.isMatchedBy(assumption, result, context); + if (result.isEmpty()) { + return new HashSet<>(); + } + } + } + } + Set subRes = new HashSet<>(); + for (MatchConstraint con: result) { + try { + int maxIndex = conclusionMaxIndexCalculator != null ? conclusionMaxIndexCalculator.calculate(assumptions) : 0; + int maxDepth = conclusionMaxDepthCalculator != null ? conclusionMaxDepthCalculator.calculate(assumptions) : 1; + context.put("maxIndex", maxIndex); + context.put("maxDepth", maxDepth); + subRes.add(conclusion.substitution(con.getBinding(), context)); + } catch (SubstituteFailedException e) { + continue; + } + } + return subRes; + } + +} diff --git a/src/test/java/inferencerule/DependencyAxiomTest.java b/src/test/java/inferencerule/DependencyAxiomTest.java index f84dd16..19b756c 100644 --- a/src/test/java/inferencerule/DependencyAxiomTest.java +++ b/src/test/java/inferencerule/DependencyAxiomTest.java @@ -1,10 +1,10 @@ package inferencerule; import static org.junit.jupiter.api.Assertions.*; -import java.util.Set; - import org.junit.jupiter.api.Test; +import java.util.Set; + import inference.ProofSystem; import models.formulas.DependencyFormula; import models.formulas.EquationFormula; @@ -80,4 +80,18 @@ assertTrue(res.contains(new DependencyFormula(d11))); } + @Test + void RedundantDependencyTest() { + //todo + } + + @Test + void RedundancyEliminationTest() { + Set result = ProofSystem.redundancyElimination.apply(new DependencyFormula(a, b), new DependencyFormula(c, a, b, d)); + assertTrue(result.contains(new DependencyFormula(c, a, d))); + + result = ProofSystem.redundancyElimination.apply(new DependencyFormula(a, b, c, d), new DependencyFormula(c, a, b, c, d, e, f, g)); + assertTrue(result.contains(new DependencyFormula(c, a, e, f, g))); + } + } diff --git a/src/test/java/terms/meta/MetaDependencyTest.java b/src/test/java/terms/meta/MetaDependencyTest.java index 5ddf185..08173dd 100644 --- a/src/test/java/terms/meta/MetaDependencyTest.java +++ b/src/test/java/terms/meta/MetaDependencyTest.java @@ -19,6 +19,7 @@ import models.terms.meta.MetaDependency; import models.terms.meta.MetaDependencyTerm; import models.terms.meta.MetaDependencyTermVariable; +import models.terms.meta.MetaDependencyVariable; import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaResource; import models.terms.meta.OrderVariableConstraint; @@ -152,6 +153,14 @@ } @Test + void MatchTest2() { + MetaDependencyVariable md1 = new MetaDependencyVariable(new Variable("md1"), new Variable("n")); + Dependency d = new Dependency(new Resource("a", 2), new Resource("b", 2), new Resource("c", 2)); + Set result = md1.isMatchedBy(d); + assertEquals(2, result.iterator().next().getOrderConstraint().get(new Variable("n")).getOrder()); + } + + @Test void MetaDependencyReplaceTest() { MetaResource x = new MetaResource(new Variable("x")); MetaResource y = new MetaResource(new Variable("y"));