diff --git a/src/main/java/Main.java b/src/main/java/Main.java index 18049d3..2bbb7a3 100644 --- a/src/main/java/Main.java +++ b/src/main/java/Main.java @@ -1,4 +1,5 @@ import java.util.HashMap; +import java.util.List; import java.util.Map; import java.util.Set; @@ -24,7 +25,7 @@ public static void main(String[] args) { // - sandbox4(); + sandbox5(); } static void sandbox() { @@ -75,6 +76,22 @@ System.out.println(ps.getState().getHistory().getHistoryString(d3)); } + static void sandbox5() { + Resource a = new Resource("a", 1); + Resource b = new Resource("b", 1); + Resource c = new Resource("c", 1); + Resource d = new Resource("d", 1); + Resource e = new Resource("e", 1); + Resource f = new Resource("f", 2); + Resource g = new Resource("g", 2); + Resource h = new Resource("h", 3); + Resource i = new Resource("i", 3); + Dependency d1 = new Dependency(new DependencyTerm(f, g, b), b); + var tmp = ProofSystem.argumentExtension.getAssumptions().get(0).isMatchedBy(new DependencyFormula(d1)); + var tmp1 = ProofSystem.argumentExtension.derive(List.of(new DependencyFormula(d1)), Set.of(a)); + System.out.println(tmp1); + } + static void sandBox8() { MetaDynamicDependency md = new MetaDynamicDependency( new MetaTermGenerator() { diff --git a/src/main/java/inference/DependencyAxiom.java b/src/main/java/inference/DependencyAxiom.java index ecfff8e..34c04a2 100644 --- a/src/main/java/inference/DependencyAxiom.java +++ b/src/main/java/inference/DependencyAxiom.java @@ -7,6 +7,7 @@ import java.util.List; import java.util.Set; +import exceptions.SyntaxException; import models.Position; import models.formulas.DependencyFormula; import models.formulas.Formula; @@ -47,15 +48,17 @@ while (! q.isEmpty()) { Position curPos = q.pollFirst(); RDLTerm curTerm = baseTerm; - for (int i = 1; i < curPos.getPath(i); i++) { + for (int i = 1; i < curPos.size(); i++) { curTerm = (RDLTerm) curTerm.getChild(curPos.getPath(i)); } if (curTerm instanceof Dependency d) { List assumptionsCopy = new ArrayList(assumptions); assumptionsCopy.set(targetAssumptionIndex, new DependencyFormula(d)); - for (Formula derived: super.derive(assumptionsCopy, constraint.clone())) { + for (Formula derived: derive(assumptionsCopy, constraint.clone())) { if (derived instanceof DependencyFormula df) { - result.add(new DependencyFormula(baseTerm.replace(curPos, df.getDependency()))); + try { + result.add(new DependencyFormula((Dependency) baseTerm.replace(curPos, df.getDependency()))); + } catch (SyntaxException e) {} } } } diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index cbb0d97..333725a 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -225,7 +225,7 @@ Set result = dependencyInferenceStep(); Set sizeConstraintOk = new HashSet<>(); for (DependencyFormula df: result) { - if (dep.getMaxIndex() >= df.getMaxIndex()) { + if (dep.getDependency().getSize() >= df.getDependency().getSize()) { if (! state.getFormulas().contains(df)) { sizeConstraintOk.add(df); } @@ -263,7 +263,7 @@ Set result = new HashSet<>(); for (Formula res: rule.derive(assumptions, state.getExistTerms())) { if (state.formulaExist(res)) continue; - state.addHistory(List.of(), rule, res); + state.addHistory(assumptions, rule, res); if (res instanceof DependencyFormula df) { result.add(df); } diff --git a/src/main/java/inference/axioms/ArgumentExtension.java b/src/main/java/inference/axioms/ArgumentExtension.java index 15d88d1..9a89d16 100644 --- a/src/main/java/inference/axioms/ArgumentExtension.java +++ b/src/main/java/inference/axioms/ArgumentExtension.java @@ -5,7 +5,7 @@ import java.util.Set; import exceptions.SubstituteFailedException; -import inference.InferenceRule; +import inference.DependencyAxiom; import models.Position; import models.algebra.Variable; import models.formulas.Formula; @@ -14,9 +14,10 @@ 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 ArgumentExtension extends InferenceRule { +public class ArgumentExtension extends DependencyAxiom { public ArgumentExtension() { super("Argument Extension"); @@ -29,7 +30,7 @@ return new MetaEvaluatableTermVariable(new Variable("te" + curIndex)); } }, - new MetaEvaluatableTermVariable(new Variable("se")) + new MetaRDLTermVariable(new Variable("se")) ) )); @@ -42,7 +43,7 @@ return new MetaEvaluatableTermVariable(new Variable("te" + curIndex)); } }, - new MetaEvaluatableTermVariable(new Variable("se")), + new MetaRDLTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("ue")) ) ); diff --git a/src/main/java/inference/axioms/ArgumentReduction.java b/src/main/java/inference/axioms/ArgumentReduction.java index 13d89be..55a090d 100644 --- a/src/main/java/inference/axioms/ArgumentReduction.java +++ b/src/main/java/inference/axioms/ArgumentReduction.java @@ -16,6 +16,7 @@ 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 ArgumentReduction extends InferenceRule { @@ -46,7 +47,7 @@ return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex)); } }, - new MetaEvaluatableTermVariable(new Variable("se")), + new MetaRDLTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("te")) ) )); @@ -60,7 +61,7 @@ return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex)); } }, - new MetaEvaluatableTermVariable(new Variable("se")) + new MetaRDLTermVariable(new Variable("se")) ) ); diff --git a/src/main/java/inference/axioms/CompositeMapping.java b/src/main/java/inference/axioms/CompositeMapping.java index 6263d1d..51bd77a 100644 --- a/src/main/java/inference/axioms/CompositeMapping.java +++ b/src/main/java/inference/axioms/CompositeMapping.java @@ -15,6 +15,7 @@ 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 CompositeMapping extends InferenceRule { @@ -49,7 +50,7 @@ return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex)); } }, - new MetaEvaluatableTermVariable(new Variable("se")), + new MetaRDLTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("te")) ) ) @@ -69,7 +70,7 @@ return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex)); } }, - new MetaEvaluatableTermVariable(new Variable("se")) + new MetaRDLTermVariable(new Variable("se")) ) ); } diff --git a/src/main/java/inference/axioms/ConstantMapping.java b/src/main/java/inference/axioms/ConstantMapping.java index 633a497..ec6aa6f 100644 --- a/src/main/java/inference/axioms/ConstantMapping.java +++ b/src/main/java/inference/axioms/ConstantMapping.java @@ -9,6 +9,7 @@ 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; import models.terms.meta.OrderConstraint; @@ -26,7 +27,7 @@ return new MetaEvaluatableTermVariable(new Variable("te" + curIndex), new Variable("m")); } }, - new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) + new MetaRDLTermVariable(new Variable("se"), new Variable("n")) ) ); } diff --git a/src/main/java/inference/axioms/DependencyExtension.java b/src/main/java/inference/axioms/DependencyExtension.java index 8e403e4..cf63345 100644 --- a/src/main/java/inference/axioms/DependencyExtension.java +++ b/src/main/java/inference/axioms/DependencyExtension.java @@ -12,6 +12,7 @@ import models.formulas.Formula; import models.formulas.meta.MetaDependencyFormula; import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDependency; import models.terms.meta.MetaDynamicDependency; import models.terms.meta.MetaEvaluatableTermVariable; import models.terms.meta.MetaRDLTerm; @@ -37,14 +38,7 @@ )); conclusion = new MetaDependencyFormula( - new MetaDynamicDependency( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 1; - return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex), ExpressionUtils.parse("n-1")); - } - }, + new MetaDependency( new MetaDynamicDependency( new MetaTermGenerator() { @Override @@ -54,9 +48,11 @@ } }, new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) - ) + ), + new MetaEvaluatableTermVariable(new Variable("ue"), ExpressionUtils.parse("n-1")) ) ); + missingVariables.add(new MetaEvaluatableTermVariable(new Variable("ue"))); } @Override diff --git a/src/main/java/inference/axioms/MapComposition.java b/src/main/java/inference/axioms/MapComposition.java index 5276f81..41c9e81 100644 --- a/src/main/java/inference/axioms/MapComposition.java +++ b/src/main/java/inference/axioms/MapComposition.java @@ -77,6 +77,9 @@ @Override public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { curIndex -= 1; + if (! context.containsKey("uIndex")) { + throw new MissingContextException(); + } int uIndex = (Integer) context.get("uIndex"); if (curIndex >= uIndex * 2) { return null; diff --git a/src/main/java/inference/axioms/UncurriedMapping.java b/src/main/java/inference/axioms/UncurriedMapping.java index 3a33527..ee174da 100644 --- a/src/main/java/inference/axioms/UncurriedMapping.java +++ b/src/main/java/inference/axioms/UncurriedMapping.java @@ -16,6 +16,7 @@ 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; import utils.ExpressionUtils; @@ -32,7 +33,7 @@ context.put("i", Math.max(i, (Integer) context.getOrDefault("i", 0))); if (curDepth == maxDepth) { if (curIndex == 0) { - return new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")); + return new MetaRDLTermVariable(new Variable("se"), new Variable("n")); } else if (curIndex == 1) { return new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")); } @@ -55,7 +56,7 @@ int i = (Integer) context.get("i"); if (curDepth == maxDepth - 1 && curIndex == 0) { return new MetaDependencyTerm( - new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), + new MetaRDLTermVariable(new Variable("se"), new Variable("n")), new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), new MetaEvaluatableTermVariable(new Variable("ve"), ExpressionUtils.parse("n-" + i)) ); diff --git a/src/main/java/models/terms/meta/MetaDynamicDependency.java b/src/main/java/models/terms/meta/MetaDynamicDependency.java index 947b244..c9e342c 100644 --- a/src/main/java/models/terms/meta/MetaDynamicDependency.java +++ b/src/main/java/models/terms/meta/MetaDynamicDependency.java @@ -38,6 +38,9 @@ @Override public Set isMatchedBy(RDLTerm another, MatchConstraint constraint, Position position) { int maxIndex = another.getMaxIndex(); + if (! another.isDependency()) { + return new HashSet<>(); + } Set result = new HashSet<>(); constraint.getContext().put(position, maxIndex); if (! (Boolean) constraint.getContext().getOrDefault("isDynamicStarted", false)) { diff --git a/src/test/java/inference/DependencyInferenceTest.java b/src/test/java/inference/DependencyInferenceTest.java index f4b03a3..5746f39 100644 --- a/src/test/java/inference/DependencyInferenceTest.java +++ b/src/test/java/inference/DependencyInferenceTest.java @@ -67,6 +67,12 @@ DependencyFormula d3 = new DependencyFormula(a, c, d); ProofSystem ps = new ProofSystem(Set.of(d1, d2), d3); assertTrue(ps.dependencyInference()); + + DependencyFormula d4 = new DependencyFormula(new Dependency(a, b), c); + DependencyFormula d5 = new DependencyFormula(b, d); + ProofSystem ps2 = new ProofSystem(Set.of(d4, d5), new DependencyFormula(new Dependency(a, d), c)); + assertTrue(ps2.dependencyInference()); + } @Test @@ -98,4 +104,14 @@ assertTrue(ps3.dependencyInference()); } + @Test + void DependencyExtensionInferenceTest() { + DependencyFormula d1 = new DependencyFormula(f, g); + ProofSystem ps1 = new ProofSystem(Set.of(d1), new DependencyFormula(new Dependency(f, g), a), Set.of(a)); + assertTrue(ps1.dependencyInference()); + + ProofSystem ps2 = new ProofSystem(Set.of(d1), new DependencyFormula(new Dependency(f, g), a, b, c), Set.of(a, b, c, d)); + assertTrue(ps2.dependencyInference()); + } + }