diff --git a/src/main/java/Main.java b/src/main/java/Main.java index b4a2d4b..2da9d3a 100644 --- a/src/main/java/Main.java +++ b/src/main/java/Main.java @@ -104,7 +104,6 @@ Dependency d3 = new Dependency(d2, new Resource("v2", 2)); Dependency d4 = new Dependency(d3, new Resource("v1", 1)); System.out.println(d3); - System.out.println(md1.isMatchedBy(d3, Map.of("maxOrder", 4))); } diff --git a/src/main/java/inference/EquationAxiom.java b/src/main/java/inference/EquationAxiom.java deleted file mode 100644 index 5e08459..0000000 --- a/src/main/java/inference/EquationAxiom.java +++ /dev/null @@ -1,26 +0,0 @@ -package inference; - -import java.util.List; - -import models.formulas.meta.MetaFormula; - -public class EquationAxiom extends InferenceRule{ - - public EquationAxiom(String name) { - super(name); - } - - public EquationAxiom( - String name, - List assumptions, - List repetitionAssumptions, - MetaFormula conclusion, - InferenceOrderConstraint constraint, - ConclusionSizeCalculator conclusionMaxIndexCalculator, - ConclusionSizeCalculator conclusionMaxDepthCalculator, - AssumptionSizeCalculator assumptionSizeCalculator - ) { - super(name, assumptions, repetitionAssumptions, conclusion, constraint, conclusionMaxIndexCalculator, conclusionMaxDepthCalculator, assumptionSizeCalculator); - } - -} diff --git a/src/main/java/inference/InferenceRule.java b/src/main/java/inference/InferenceRule.java index d9f553a..e47a0a6 100644 --- a/src/main/java/inference/InferenceRule.java +++ b/src/main/java/inference/InferenceRule.java @@ -1,25 +1,23 @@ package inference; import java.util.ArrayList; -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.formulas.DependencyFormula; +import models.formulas.EquationFormula; import models.formulas.Formula; +import models.formulas.meta.MetaEquationFormula; import models.formulas.meta.MetaFormula; import models.terms.DependencyTerm; import models.terms.EvaluatableTerm; import models.terms.RDLTerm; import models.terms.Resource; import models.terms.meta.MatchConstraint; -import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaVariable; -import utils.Permutation; +import utils.Product; public class InferenceRule { @@ -32,10 +30,7 @@ protected MetaFormula conclusion; protected InferenceOrderConstraint defaultOrderConstraint; - protected List repetitionAssumptions = new ArrayList<>(); - protected ConclusionSizeCalculator conclusionMaxIndexCalculator; - protected ConclusionSizeCalculator conclusionMaxDepthCalculator; - protected AssumptionSizeCalculator assumptionRepetitionSizeCalculator; + protected List missingVariables; protected InferenceRule(String name) { this.name = name; @@ -46,102 +41,97 @@ this.assumptions = assumptions; this.conclusion = conclusion; this.defaultOrderConstraint = constraint; - } - - public InferenceRule( - String name, - List assumptions, - List repetitionAssumptions, - MetaFormula conclusion, - InferenceOrderConstraint constraint, - ConclusionSizeCalculator conclusionMaxIndexCalculator, - ConclusionSizeCalculator conclusionMaxDepthCalculator, - AssumptionSizeCalculator assumptionSizeCalculator - ) { - this.name = name; - this.assumptions = assumptions; - this.repetitionAssumptions = repetitionAssumptions; - this.conclusion = conclusion; - this.defaultOrderConstraint = constraint; - this.conclusionMaxIndexCalculator = conclusionMaxIndexCalculator; - this.conclusionMaxDepthCalculator = conclusionMaxDepthCalculator; - this.assumptionRepetitionSizeCalculator = assumptionSizeCalculator; - } - - public InferenceRule( List assumptions, MetaFormula conclusion, InferenceOrderConstraint constraint) { - this("undefined", assumptions, conclusion, constraint); + Set missingVariables = conclusion.getAllVariables(); + for (MetaFormula assumption: assumptions) { + missingVariables.removeAll(assumption.getAllVariables()); + } + this.missingVariables = new ArrayList<>(missingVariables); } public InferenceRule(String name, List assumptions, MetaFormula conclusion) { this(name, assumptions, conclusion, null); } - public InferenceRule(List assumptions, MetaFormula conclusion) { - this("undefined", assumptions, conclusion, null); - } - - - public Set apply(Formula ...assumptions) { - return apply(Set.of(assumptions)); - } - - public Set apply(Set assumptions) { - if (assumptions.size() < getAssumptionSize()) { - return new HashSet<>(); - } + public Set apply(Set formulas, Set existTerms) { + List> matchFormulas = new ArrayList<>(); + List> matchTerms = new ArrayList<>(); Set result = new HashSet<>(); - for (List assumptionList : Permutation.permutation(assumptions, assumptions.size())) { - result.addAll(apply(assumptionList)); - } - return result; - } - - protected Set apply(List assumptions) { - return apply(assumptions, MatchConstraint.createDefault()); - } - - protected Set apply(List assumptions, MatchConstraint constraint) { - if (assumptions.size() < getAssumptionSize()) { - 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); - if (result.isEmpty()) { + for (int i = 0; i < assumptions.size(); i++) { + matchFormulas.add(new ArrayList<>()); + for (Formula formula: formulas) { + if (! assumptions.get(i).isMatchedBy(formula).isEmpty()) { + matchFormulas.get(i).add(formula); + } + } + if (matchFormulas.get(i).isEmpty()) { return new HashSet<>(); } } - if (this.repetitionAssumptions.size() != 0 && (assumptions.size() - this.assumptions.size()) % this.repetitionAssumptions.size() != 0) { - return new HashSet<>(); + for (int i = 0; i < missingVariables.size(); i++) { + matchTerms.add(new ArrayList<>()); + for (RDLTerm term : existTerms) { + if (! missingVariables.get(i).isMatchedBy(term).isEmpty()) { + matchTerms.get(i).add(term); + } + } + if (matchTerms.get(i).isEmpty()) { + 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); - if (result.isEmpty()) { - return new HashSet<>(); + if (matchFormulas.size() == 0) { + for (List terms : Product.product(matchTerms)) { + MatchConstraint constraint = MatchConstraint.createDefault(); + for (int i = 0; i < terms.size(); i++) { + MetaVariable variable = missingVariables.get(i); + RDLTerm term = terms.get(i); + constraint.setBinding(variable.getVariableName(), term); + Formula conclusion = this.conclusion.substitution(constraint.getBinding(), constraint.getContext()); + if (conclusionCheck(conclusion, constraint, formulas)) { + result.add(conclusion); } } } } - 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; - con.getContext().put("maxIndex", maxIndex); - con.getContext().put("maxDepth", maxDepth); - subRes.add(conclusion.substitution(con.getBinding(), con.getContext())); - } catch (SubstituteFailedException e) { + for (List assumptions: Product.product(matchFormulas)) { + Set matchResult = matchCheck(assumptions); + if (matchResult.isEmpty()) { continue; } + for (MatchConstraint constraint: matchResult) { + if (missingVariables.size() == 0) { + Formula conclusion = this.conclusion.substitution(constraint.getBinding(), constraint.getContext()); + if (conclusionCheck(conclusion, constraint, formulas)) { + result.add(conclusion); + } + } + for (List terms : Product.product(matchTerms)) { + for (int i = 0; i < terms.size(); i++) { + MetaVariable variable = missingVariables.get(i); + RDLTerm term = terms.get(i); + constraint.setBinding(variable.getVariableName(), term); + Formula conclusion = this.conclusion.substitution(constraint.getBinding(), constraint.getContext()); + if (conclusionCheck(conclusion, constraint, formulas)) { + result.add(conclusion); + } + } + } + } } - return subRes; + return result; + } + + protected Set matchCheck(List assumptions) { + Set matchResult = new HashSet<>(); + matchResult.add(MatchConstraint.createDefault()); + for (int i = 0; i < assumptions.size(); i++) { + Formula assumption = assumptions.get(i); + MetaFormula metaAssumption = this.assumptions.get(i); + matchResult = metaAssumption.isMatchedBy(assumption, matchResult); + if (matchResult.isEmpty()) { + return new HashSet<>(); + } + } + return matchResult; } private static Set requiredAssumptions(EvaluatableTerm term) { @@ -178,26 +168,38 @@ return result; } + private static boolean conclusionCheck(Formula conclusion, MatchConstraint constraint, Set formulas) { + if (conclusion instanceof DependencyFormula) return true; + EquationFormula eq = (EquationFormula) conclusion; + EvaluatableTerm leftSideHand = eq.getLeftSideHand(); + for (Formula formula: requiredAssumptions(leftSideHand)) { + if (formula instanceof DependencyFormula dep) { + if (! formulas.contains(dep)) { + return false; + } + } else if (formula instanceof In in) { + boolean flg = false; + for (MetaEquationFormula metaFormula: in.deriveRule()) { + for (Formula existFormula: formulas) { + if (! metaFormula.isMatchedBy(existFormula, constraint).isEmpty()) { + flg = true; + break; + } + } + if (flg) break; + } + if (!flg) { + return false; + } + } + } + return true; + } public int getAssumptionSize() { return this.assumptions.size(); } - protected List repetitionAssumptionGenerate(int i) { -// if (i == 0) { -// return new ArrayList<>(this.repetitionAssumptions); -// } - List result = new ArrayList<>(); - for (MetaFormula metaFormula : this.repetitionAssumptions) { - Map mapping = new HashMap<>(); - for (MetaVariable variable : metaFormula.getAllVariables()) { - mapping.put(variable, variable.cloneWithName(variable.getVariableName().getName() + i)); - } - result.add(metaFormula.replace(mapping)); - } - return result; - } - public String toString() { StringBuilder sb = new StringBuilder(); diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index 4677ca7..85cda79 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -12,34 +12,14 @@ import java.util.Set; import java.util.stream.Collectors; -import inference.axioms.ArgumentDependencyExtraction; -import inference.axioms.CompositeMapping; -import inference.axioms.Constantness; -import inference.axioms.MapComposition; -import inference.axioms.RedundancyElimination; -import inference.axioms.RightNormalization; -import inference.axioms.RightSubstitution; -import inference.axioms.UncurriedMapping; -import inference.axioms.Uncurrying; -import models.algebra.Constant; 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.MetaDependencyTerm; -import models.terms.meta.MetaDependencyVariable; -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; -import models.terms.meta.OrderConstraint; -import utils.ExpressionUtils; -import utils.Product; public class ProofSystem { @@ -87,191 +67,191 @@ ); - public static final InferenceRule rightSubstitution = new RightSubstitution(); - - public static final InferenceRule leftSubstitution = new EquationAxiom( - "Left Substitution", - List.of( - new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ), - List.of( - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("re")) - ), - new MetaEquationFormula( - new MetaDependencyTerm( - new MetaEvaluatableTermVariable(new Variable("re")), - new MetaEvaluatableTermVariable(new Variable("x")), - new MetaEvaluatableTermVariable(new Variable("y")) - ), - new MetaEvaluatableTermVariable(new Variable("ue")) - ) - ), - new MetaEquationFormula( - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 1; - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("re" + curIndex / 2)); - } - return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); - } - }, - new MetaEvaluatableTermVariable(new Variable("se")) - ), - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 1; - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("re" + curIndex / 2)); - } - return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); - } - }, - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ), - null, - (assumptions) -> (assumptions.size() - 1) / 2 * 2 + 1, - (assumptions) -> 1, - (conclusion) -> (conclusion.getMaxIndex() - 1) / 2 - ); - +// public static final InferenceRule rightSubstitution = new RightSubstitution(); +// +// public static final InferenceRule leftSubstitution = new EquationAxiom( +// "Left Substitution", +// List.of( +// new MetaEquationFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ) +// ), +// List.of( +// new MetaDependencyFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaEvaluatableTermVariable(new Variable("re")) +// ), +// new MetaEquationFormula( +// new MetaDependencyTerm( +// new MetaEvaluatableTermVariable(new Variable("re")), +// new MetaEvaluatableTermVariable(new Variable("x")), +// new MetaEvaluatableTermVariable(new Variable("y")) +// ), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ) +// ), +// new MetaEquationFormula( +// new MetaDynamicDependencyTerm( +// new MetaTermGenerator() { +// @Override +// public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { +// curIndex -= 1; +// if (curIndex % 2 == 0) { +// return new MetaEvaluatableTermVariable(new Variable("re" + curIndex / 2)); +// } +// return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); +// } +// }, +// new MetaEvaluatableTermVariable(new Variable("se")) +// ), +// new MetaDynamicDependencyTerm( +// new MetaTermGenerator() { +// @Override +// public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { +// curIndex -= 1; +// if (curIndex % 2 == 0) { +// return new MetaEvaluatableTermVariable(new Variable("re" + curIndex / 2)); +// } +// return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); +// } +// }, +// new MetaEvaluatableTermVariable(new Variable("te")) +// ) +// ), +// null, +// (assumptions) -> (assumptions.size() - 1) / 2 * 2 + 1, +// (assumptions) -> 1, +// (conclusion) -> (conclusion.getMaxIndex() - 1) / 2 +// ); +// - public static final InferenceRule identity = new EquationAxiom( - "Identity", - List.of(), - List.of( - new MetaEquationFormula( - new MetaDependencyTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("x")), - new MetaEvaluatableTermVariable(new Variable("y")) - ), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ), - new MetaEquationFormula( - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 1; - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("se" + curIndex / 2)); - } - return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2)); - } - - }, - new MetaEvaluatableTermVariable(new Variable("se0")) - ), - new MetaEvaluatableTermVariable(new Variable("te0")) - ), - null, - (assumptions) -> assumptions.size() * 2 + 1, - (assumptions) -> 1, - (conclusion) -> (conclusion.getMaxIndex() - 1) / 2 - ); +// public static final InferenceRule identity = new EquationAxiom( +// "Identity", +// List.of(), +// List.of( +// new MetaEquationFormula( +// new MetaDependencyTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaEvaluatableTermVariable(new Variable("x")), +// new MetaEvaluatableTermVariable(new Variable("y")) +// ), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ) +// ), +// new MetaEquationFormula( +// new MetaDynamicDependencyTerm( +// new MetaTermGenerator() { +// @Override +// public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { +// curIndex -= 1; +// if (curIndex % 2 == 0) { +// return new MetaEvaluatableTermVariable(new Variable("se" + curIndex / 2)); +// } +// return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2)); +// } +// +// }, +// new MetaEvaluatableTermVariable(new Variable("se0")) +// ), +// new MetaEvaluatableTermVariable(new Variable("te0")) +// ), +// null, +// (assumptions) -> assumptions.size() * 2 + 1, +// (assumptions) -> 1, +// (conclusion) -> (conclusion.getMaxIndex() - 1) / 2 +// ); +// +// public static final InferenceRule mapComposition = new MapComposition(); +// +// public static final InferenceRule constantness = new Constantness(); +// +// public static final InferenceRule rightNormalization = new RightNormalization(); +// +// public static final InferenceRule pseudoConstantness = new InferenceRule( +// "Pseudo-Constantness", +// List.of( +// new MetaDependencyFormula( +// new MetaDynamicDependency( +// (ci, cd, mi, md, context) -> new MetaEvaluatableTermVariable(new Variable("re" + (ci - 1)), new Variable("n")), +// new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) +// ) +// ) +// ), +// List.of(), +// new MetaEquationFormula( +// new MetaDynamicDependencyTerm( +// (ci, cd, mi, md, context) -> new MetaEvaluatableTermVariable(new Variable("re" + (ci - 1) / 2), new Variable("n")), +// new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) +// ), +// new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) +// ), +// new InferenceOrderConstraint(new Constant("0"), OrderConstraint.GT, new Variable("n")), +// (assumptions) -> (((DependencyFormula)assumptions.get(0)).getDependency().getMaxIndex() - 1) * 2 + 1, +// (assumptions) -> 1, +// (term) -> (term.getMaxIndex() - 1) / 2 + 1 +// ); - public static final InferenceRule mapComposition = new MapComposition(); - - public static final InferenceRule constantness = new Constantness(); - - public static final InferenceRule rightNormalization = new RightNormalization(); - - public static final InferenceRule pseudoConstantness = new InferenceRule( - "Pseudo-Constantness", - List.of( - new MetaDependencyFormula( - new MetaDynamicDependency( - (ci, cd, mi, md, context) -> new MetaEvaluatableTermVariable(new Variable("re" + (ci - 1)), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) - ) - ) - ), - List.of(), - new MetaEquationFormula( - new MetaDynamicDependencyTerm( - (ci, cd, mi, md, context) -> new MetaEvaluatableTermVariable(new Variable("re" + (ci - 1) / 2), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) - ), - new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) - ), - new InferenceOrderConstraint(new Constant("0"), OrderConstraint.GT, new Variable("n")), - (assumptions) -> (((DependencyFormula)assumptions.get(0)).getDependency().getMaxIndex() - 1) * 2 + 1, - (assumptions) -> 1, - (term) -> (term.getMaxIndex() - 1) / 2 + 1 - ); - - public static final InferenceRule uncurrying = new Uncurrying(); - - public static final InferenceRule argumentDependencyExtraction = new ArgumentDependencyExtraction(); +// public static final InferenceRule uncurrying = new Uncurrying(); +// +// public static final InferenceRule argumentDependencyExtraction = new ArgumentDependencyExtraction(); // // //======================Dependency Axioms============================= // - public static final InferenceRule identityMapping = new InferenceRule( - "Identity Mapping", - List.of( - new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaEvaluatableTermVariable(new Variable("se")) - ) - ), - List.of(), - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaEvaluatableTermVariable(new Variable("se")) - ), - null, - null, - null, - null - ); +// public static final InferenceRule identityMapping = new InferenceRule( +// "Identity Mapping", +// List.of( +// new MetaEquationFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaEvaluatableTermVariable(new Variable("se")) +// ) +// ), +// List.of(), +// new MetaDependencyFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaEvaluatableTermVariable(new Variable("se")) +// ), +// null, +// null, +// null, +// null +// ); - public static final InferenceRule compositeMapping = new CompositeMapping(); +// public static final InferenceRule compositeMapping = new CompositeMapping(); - public static final InferenceRule constantMapping = new InferenceRule( - "Constant Mapping", - List.of(), - List.of(), - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("re"), new Variable("m")) - ), - new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")), - null, - null, - null - ); +// public static final InferenceRule constantMapping = new InferenceRule( +// "Constant Mapping", +// List.of(), +// List.of(), +// new MetaDependencyFormula( +// new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), +// new MetaEvaluatableTermVariable(new Variable("re"), new Variable("m")) +// ), +// new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")), +// null, +// null, +// null +// ); - public static final InferenceRule uncurriedMapping = new UncurriedMapping(); +// 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"), ExpressionUtils.parse("n - 1"))), - null, - null, - null, - null - ); +// 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"), ExpressionUtils.parse("n - 1"))), +// null, +// null, +// null, +// null +// ); - public static final InferenceRule redundancyElimination = new RedundancyElimination(); +// public static final InferenceRule redundancyElimination = new RedundancyElimination(); /* * new InferenceRule( @@ -410,29 +390,29 @@ private static Set applyAxiom(InferenceRule axiom, Set formulas, Set> appliedFormulas, Set existTerms, Map proofGraph) { Set result = new HashSet<>(); - List> matchedFormulas = new ArrayList<>(); - for (int i = 0; i < axiom.getAssumptionSize(); i++) { - matchedFormulas.add(new ArrayList<>()); - for (Formula formula : formulas) { - if (! axiom.getAssumptions().get(i).isMatchedBy(formula).isEmpty()) { - matchedFormulas.get(i).add(formula); - } - } - } - for(List applyFormulas : Product.product(matchedFormulas)) { - if (appliedFormulas.contains(applyFormulas)) continue; - Set applied = axiom.apply(applyFormulas); - if (applied != null) { - for (Formula formula : applied) { - if (! formulas.contains(formula)) { - addExistTerms(formula, existTerms); - proofGraph.put(formula, new AxiomResult(axiom, applyFormulas)); - } - } - result.addAll(applied); - appliedFormulas.add(applyFormulas); - } - } +// List> matchedFormulas = new ArrayList<>(); +// for (int i = 0; i < axiom.getAssumptionSize(); i++) { +// matchedFormulas.add(new ArrayList<>()); +// for (Formula formula : formulas) { +// if (! axiom.getAssumptions().get(i).isMatchedBy(formula).isEmpty()) { +// matchedFormulas.get(i).add(formula); +// } +// } +// } +// for(List applyFormulas : Product.product(matchedFormulas)) { +// if (appliedFormulas.contains(applyFormulas)) continue; +// Set applied = axiom.apply(applyFormulas); +// if (applied != null) { +// for (Formula formula : applied) { +// if (! formulas.contains(formula)) { +// addExistTerms(formula, existTerms); +// proofGraph.put(formula, new AxiomResult(axiom, applyFormulas)); +// } +// } +// result.addAll(applied); +// appliedFormulas.add(applyFormulas); +// } +// } return result; } diff --git a/src/main/java/inference/axioms/ArgumentDependencyExtraction.java b/src/main/java/inference/axioms/ArgumentDependencyExtraction.java deleted file mode 100644 index f160716..0000000 --- a/src/main/java/inference/axioms/ArgumentDependencyExtraction.java +++ /dev/null @@ -1,93 +0,0 @@ -package inference.axioms; -import java.util.Map; - -import inference.EquationAxiom; -import models.algebra.Variable; -import models.formulas.EquationFormula; -import models.formulas.meta.MetaDependencyFormula; -import models.formulas.meta.MetaEquationFormula; -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 ArgumentDependencyExtraction extends EquationAxiom { - - public ArgumentDependencyExtraction() { - super("Argument Dependency Extraction"); - 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 + 2); - return new MetaEvaluatableTermVariable(new Variable("t" + curIndex)); - } - }, - new MetaEvaluatableTermVariable(new Variable("t")) - ) - ) - ); - assumptions.add( - new MetaDependencyFormula( - new MetaDynamicDependency( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 2; - return new MetaEvaluatableTermVariable(new Variable("t" + curIndex)); - } - }, - new MetaEvaluatableTermVariable(new Variable("s")), - new MetaEvaluatableTermVariable(new Variable("t")) - ) - ) - ); - assumptions.add( - new MetaEquationFormula( - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 3; - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("t" + curIndex / 2)); - } - return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2)); - } - }, - new MetaEvaluatableTermVariable(new Variable("s")), - new MetaEvaluatableTermVariable(new Variable("t")), - new MetaEvaluatableTermVariable(new Variable("x")) - ), - new MetaEvaluatableTermVariable(new Variable("c")) - ) - ); - - conclusion = new MetaEquationFormula( - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - int firstAssumptionIndex = (Integer) context.get("firstAssumptionIndex"); - curIndex -= 1; - if (curIndex >= firstAssumptionIndex) { - return null; - } - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("t" + curIndex / 2)); - } - return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2)); - } - }, - new MetaEvaluatableTermVariable(new Variable("t")) - ), - new MetaEvaluatableTermVariable(new Variable("x")) - ); - conclusionMaxIndexCalculator = (assumptions) -> ((EquationFormula) assumptions.get(2)).getLeftSideHand().getMaxIndex() - 3 + 1; - } - -} diff --git a/src/main/java/inference/axioms/CompositeMapping.java b/src/main/java/inference/axioms/CompositeMapping.java deleted file mode 100644 index 035272d..0000000 --- a/src/main/java/inference/axioms/CompositeMapping.java +++ /dev/null @@ -1,105 +0,0 @@ -package inference.axioms; - -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.MetaTermGenerator; - -public class CompositeMapping extends InferenceRule { - - public CompositeMapping() { - super("Compsite Mapping"); - this.assumptions.add( - new MetaDependencyFormula( - new MetaDynamicDependency( - (ci, cd, mi, md, context) -> new MetaEvaluatableTermVariable(new Variable("te" + (ci - 2))), - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ) - ); - this.assumptions.add( - new MetaDependencyFormula( - new MetaDynamicDependency( - (ci, cd, mi, md, context) -> new MetaEvaluatableTermVariable(new Variable("ue" + (ci - 1))), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ) - ); - this.conclusion = new MetaDependencyFormula( - new MetaDynamicDependency( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth,Map context) { - curIndex -= 1; - int firstAssumptionSize = (Integer) context.get("firstAssumptionSize") - 2; - if (curIndex < firstAssumptionSize) { - return new MetaEvaluatableTermVariable(new Variable("te" + (curIndex))); - } - return new MetaEvaluatableTermVariable(new Variable("ue" + (curIndex - firstAssumptionSize))); - } - - }, - new MetaEvaluatableTermVariable(new Variable("se")) - ) - ); - conclusionMaxIndexCalculator = (assumptions) -> ((DependencyFormula) assumptions.get(0)).getDependency().getMaxIndex() - 2 + ((DependencyFormula) assumptions.get(1)).getDependency().getMaxIndex() - 1 + 1; - } - - protected Set apply(List assumptions, MatchConstraint constraint) { - if (assumptions.size() < getAssumptionSize()) { - 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); - 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); - 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; - int firstAssumptionSize = ((DependencyFormula) assumptions.get(0)).getDependency().getMaxIndex(); - subRes.add(conclusion.substitution(con.getBinding(), Map.of("maxIndex", maxIndex, "maxDepth", maxDepth, "firstAssumptionSize", firstAssumptionSize))); - } catch (SubstituteFailedException e) { - continue; - } - } - return subRes; - } - -} diff --git a/src/main/java/inference/axioms/Constantness.java b/src/main/java/inference/axioms/Constantness.java deleted file mode 100644 index 47a3c0d..0000000 --- a/src/main/java/inference/axioms/Constantness.java +++ /dev/null @@ -1,135 +0,0 @@ -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.EquationAxiom; -import models.algebra.Constant; -import models.algebra.Variable; -import models.formulas.EquationFormula; -import models.formulas.Formula; -import models.formulas.meta.MetaEquationFormula; -import models.terms.DependencyTerm; -import models.terms.meta.MatchConstraint; -import models.terms.meta.MetaDependencyTerm; -import models.terms.meta.MetaDynamicDependencyTerm; -import models.terms.meta.MetaEvaluatableTermVariable; -import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaTermGenerator; - -public class Constantness extends EquationAxiom { - - public Constantness() { - super("Constantness"); - } - - @Override - protected Set apply(List assumptions, MatchConstraint constraint) { - Set result = new HashSet<>(); - Map context = new HashMap<>(); - result.add(constraint); - int prevOrder = 0; - int m = 0; - int n = 1; - if (assumptions.get(0) instanceof EquationFormula eq) { - if (eq.getLeftSideHand() instanceof DependencyTerm dt) { - prevOrder = dt.getDependingTerm().getOrder(); - m = prevOrder; - } else { - return new HashSet<>(); - } - } else { - return new HashSet<>(); - } - - for (int i = 1; i < assumptions.size(); i++) { - if (assumptions.get(i) instanceof EquationFormula eq2) { - if (eq2.getLeftSideHand() instanceof DependencyTerm dt) { - int order = dt.getDependingTerm().getOrder(); - n = order; - if (prevOrder - order != 1) { - return new HashSet<>(); - } - prevOrder = order; - } else { - return new HashSet<>(); - } - } else { - return new HashSet<>(); - } - } - - if (n >= m) { - return new HashSet<>(); - } - - if (m - n != assumptions.size()) { - return new HashSet<>(); - } - - for (int i = 0; i < assumptions.size(); i++) { - Formula assumption = assumptions.get(i); - MetaDependencyTerm mdt = new MetaDependencyTerm( - new MetaEvaluatableTermVariable(new Variable("r" + i), new Constant("" + (m + i))), - new MetaEvaluatableTermVariable(new Variable("xxx" + i)), - new MetaEvaluatableTermVariable(new Variable("yyy" + i)) - ); - MetaEquationFormula mef = new MetaEquationFormula(mdt, new MetaEvaluatableTermVariable(new Variable("t" + i))); - result = mef.isMatchedBy(assumption, result); - if (result.isEmpty()) { - return new HashSet<>(); - } - } - - MetaEquationFormula conclusion = new MetaEquationFormula( - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - int n = (Integer) context.get("n"); - int m = (Integer) context.get("m"); - int i = maxDepth - curDepth - 1; - if (curDepth == maxDepth - 1) { - return new MetaDependencyTerm( - new MetaEvaluatableTermVariable(new Variable("se"), new Constant("" + n)), - new MetaEvaluatableTermVariable(new Variable("r" + i), new Constant("" + (m + i))), - new MetaEvaluatableTermVariable(new Variable("t" + i)) - ); - } - if (curIndex == 0) { - return new MetaDynamicDependencyTerm(this); - } else if (curIndex == 1) { - return new MetaEvaluatableTermVariable(new Variable("r" + i), new Constant("" + (m + i))); - } - return new MetaEvaluatableTermVariable(new Variable("t" + i)); - } - } - ), - new MetaEvaluatableTermVariable(new Variable("se"), new Constant("" + n)) - ); - - Set subRes = new HashSet<>(); - for (MatchConstraint con: result) { - try { - int maxIndex = 3; - int maxDepth = m - n; - context.put("maxIndex", maxIndex); - context.put("maxDepth", maxDepth); - context.put("n", n); - context.put("m", m); - subRes.add(conclusion.substitution(con.getBinding(), context)); - } catch (SubstituteFailedException e) { - continue; - } - } - - return super.apply(assumptions, constraint); - } - - - - -} diff --git a/src/main/java/inference/axioms/MapComposition.java b/src/main/java/inference/axioms/MapComposition.java deleted file mode 100644 index e15b026..0000000 --- a/src/main/java/inference/axioms/MapComposition.java +++ /dev/null @@ -1,182 +0,0 @@ -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.EquationAxiom; -import models.algebra.Variable; -import models.formulas.Formula; -import models.formulas.meta.MetaDependencyFormula; -import models.formulas.meta.MetaEquationFormula; -import models.terms.meta.MatchConstraint; -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( - 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("t")) - ) - ) - ); - assumptions.add( - new MetaDependencyFormula( - new MetaDynamicDependency( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 2; - context.put("secondAssumptionIndex", curIndex + 1); - return new MetaEvaluatableTermVariable(new Variable("u" + curIndex)); - } - - }, - new MetaEvaluatableTermVariable(new Variable("s")), - new MetaEvaluatableTermVariable(new Variable("t")) - ) - ) - ); - this.conclusion = new MetaEquationFormula( - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 3; - int secondAssumptionIndex = (Integer)context.get("secondAssumptionIndex"); - if (curIndex >= secondAssumptionIndex * 2) { - return null; - } - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("u" + curIndex / 2)); - } - return new MetaEvaluatableTermVariable(new Variable("y" + curIndex / 2)); - } - }, - 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) { - curIndex -= 1; - int firstAssumptionIndex = (Integer)context.get("firstAssumptionIndex"); - if (curIndex >= firstAssumptionIndex * 2) { - return null; - } - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("v" + curIndex / 2)); - } - return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2)); - }}, - new MetaEvaluatableTermVariable(new Variable("t")) - ) - ), - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 1; - int firstAssumptionIndex = (Integer)context.get("firstAssumptionIndex"); - int secondAssumptionIndex = (Integer)context.get("secondAssumptionIndex"); - if (curIndex >= firstAssumptionIndex * 2 + secondAssumptionIndex * 2) { - return null; - } - if (curIndex < firstAssumptionIndex * 2) { - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("v" + curIndex / 2)); - } - return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2)); - } - curIndex -= firstAssumptionIndex * 2; - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("u" + curIndex / 2)); - } - return new MetaEvaluatableTermVariable(new Variable("y" + curIndex / 2)); - }}, - new MetaEvaluatableTermVariable(new Variable("s")) - ) - ); - } - - @Override - protected Set apply(List assumptions, MatchConstraint constraint) { - Map context = new HashMap<>(); - Set matchResult = new HashSet<>(); - matchResult.add(constraint); - if (assumptions.size() < 2) { - return new HashSet<>(); - } - for (int i = 0; i < 2; i++) { - matchResult = this.assumptions.get(i).isMatchedBy(assumptions.get(i), matchResult); - if (matchResult.isEmpty()) { - return new HashSet<>(); - } - } - int firstAssumptionIndex = (Integer)context.get("firstAssumptionIndex"); - int secondAssumptionIndex = (Integer)context.get("secondAssumptionIndex"); - if (assumptions.size() < 2 + firstAssumptionIndex + secondAssumptionIndex) { - return new HashSet<>(); - } - for (int i = 0; i < firstAssumptionIndex; i++) { - Formula assumption = assumptions.get(i + 2); - MetaDependencyTerm mdt = new MetaDependencyTerm( - new MetaEvaluatableTermVariable(new Variable("v" + i)), - new MetaEvaluatableTermVariable(new Variable("xxx" + i)), - new MetaEvaluatableTermVariable(new Variable("yyy" + i)) - ); - MetaEquationFormula mef = new MetaEquationFormula(mdt, new MetaEvaluatableTermVariable(new Variable("x" + i))); - matchResult = mef.isMatchedBy(assumption, matchResult); - if (matchResult.isEmpty()) { - return new HashSet<>(); - } - } - for (int i = 0; i < secondAssumptionIndex; i++) { - Formula assumption = assumptions.get(i + 2 + firstAssumptionIndex); - MetaDependencyTerm mdt = new MetaDependencyTerm( - new MetaEvaluatableTermVariable(new Variable("u" + i)), - new MetaEvaluatableTermVariable(new Variable("xxxx" + i)), - new MetaEvaluatableTermVariable(new Variable("yyyy" + i)) - ); - MetaEquationFormula mef = new MetaEquationFormula(mdt, new MetaEvaluatableTermVariable(new Variable("y" + i))); - matchResult = mef.isMatchedBy(assumption, matchResult); - if (matchResult.isEmpty()) { - return new HashSet<>(); - } - } - Set subRes = new HashSet<>(); - for (MatchConstraint con: matchResult) { - try { - int maxIndex = 10000; - int maxDepth = 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/main/java/inference/axioms/RedundancyElimination.java b/src/main/java/inference/axioms/RedundancyElimination.java deleted file mode 100644 index e30ff40..0000000 --- a/src/main/java/inference/axioms/RedundancyElimination.java +++ /dev/null @@ -1,114 +0,0 @@ -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); - 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); - 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/main/java/inference/axioms/RightNormalization.java b/src/main/java/inference/axioms/RightNormalization.java deleted file mode 100644 index c214870..0000000 --- a/src/main/java/inference/axioms/RightNormalization.java +++ /dev/null @@ -1,218 +0,0 @@ -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.EquationAxiom; -import models.algebra.Expression; -import models.algebra.Variable; -import models.formulas.Formula; -import models.formulas.meta.MetaDependencyFormula; -import models.formulas.meta.MetaEquationFormula; -import models.terms.meta.MatchConstraint; -import models.terms.meta.MetaDependency; -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; -import utils.ExpressionUtils; - -public class RightNormalization extends EquationAxiom { - - private final Expression n1 = ExpressionUtils.parse("n-1"); - - public RightNormalization() { - super("RIght Normalization"); - 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), n1); - } - }, - new MetaDependency( - new MetaEvaluatableTermVariable(new Variable("s"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")) - ) - ) - ) - ); - 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("secondAssumptionIndex", curIndex + 1); - return new MetaEvaluatableTermVariable(new Variable("w" + curIndex), n1); - } - }, - new MetaEvaluatableTermVariable(new Variable("u"), n1) - ) - ) - ); - - assumptions.add( - new MetaEquationFormula( - new MetaDependencyTerm( - new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("xxx")), - new MetaEvaluatableTermVariable(new Variable("yyy")) - ), - new MetaEvaluatableTermVariable(new Variable("u"), n1) - ) - ); - - conclusion = new MetaEquationFormula( - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 1; - int firstAssumptionIndex = (Integer) context.get("firstAssumptionIndex"); - int secondAssumptionIndex = (Integer) context.get("secondAssumptionIndex"); - if (curIndex >= (firstAssumptionIndex + secondAssumptionIndex) * 2) { - return null; - } - if (curIndex < firstAssumptionIndex * 2) { - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("v" + curIndex / 2), n1); - } - return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2)); - } - curIndex -= firstAssumptionIndex * 2; - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("w" + curIndex / 2), n1); - } - return new MetaEvaluatableTermVariable(new Variable("y" + curIndex / 2)); - } - }, - new MetaDependencyTerm( - new MetaEvaluatableTermVariable(new Variable("s"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("u"), n1) - ) - ), - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 1; - int firstAssumptionIndex = (Integer) context.get("firstAssumptionIndex"); - if (curIndex >= firstAssumptionIndex * 2) { - return null; - } - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("v" + curIndex / 2), n1); - } - return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2)); - } - - }, - new MetaDependencyTerm( - new MetaEvaluatableTermVariable(new Variable("s"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")), - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 1; - int secondAssumptionIndex = (Integer) context.get("secondAssumptionIndex"); - if (curIndex >= secondAssumptionIndex * 2) { - return null; - } - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("w" + curIndex / 2), n1); - } - return new MetaEvaluatableTermVariable(new Variable("y" + curIndex / 2)); - } - - }, - new MetaEvaluatableTermVariable(new Variable("u"), n1) - ) - ) - ) - ); - - } - - @Override - protected Set apply(List assumptions, MatchConstraint constraint) { - if (assumptions.size() < 3) { - return new HashSet<>(); - } - Set result = new HashSet<>(); - result.add(constraint); - Map context = new HashMap<>(); - for (int i = 0; i < 3; i++) { - result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result); - if (result.isEmpty()) { - return new HashSet<>(); - } - } - - int firstAssumptionIndex = (Integer) context.get("firstAssumptionIndex"); - int secondAssumptionIndex = (Integer) context.get("secondAssumptionIndex"); - if (assumptions.size() < 3 + firstAssumptionIndex + secondAssumptionIndex) { - return new HashSet<>(); - } - for (int i = 0; i < firstAssumptionIndex; i++) { - Formula assumption = assumptions.get(i + 3); - MetaEquationFormula mef = new MetaEquationFormula( - new MetaDependencyTerm( - new MetaEvaluatableTermVariable(new Variable("v" + i), n1), - new MetaEvaluatableTermVariable(new Variable("xxxx" + i)), - new MetaEvaluatableTermVariable(new Variable("yyyy" + i)) - ), - new MetaEvaluatableTermVariable(new Variable("x" + i)) - ); - result = mef.isMatchedBy(assumption, result); - if (result.isEmpty()) { - return new HashSet<>(); - } - } - - for(int i = 0; i < secondAssumptionIndex; i++) { - Formula assumption = assumptions.get(i + 3 + firstAssumptionIndex); - MetaEquationFormula mef = new MetaEquationFormula( - new MetaDependencyTerm( - new MetaEvaluatableTermVariable(new Variable("w" + i), n1), - new MetaEvaluatableTermVariable(new Variable("xxyy" + i)), - new MetaEvaluatableTermVariable(new Variable("yyxx" + i)) - ), - new MetaEvaluatableTermVariable(new Variable("y" + i)) - ); - result = mef.isMatchedBy(assumption, result); - if (result.isEmpty()) { - return new HashSet<>(); - } - } - - Set subRes = new HashSet<>(); - for (MatchConstraint con: result) { - try { - int maxIndex = 10000; - int maxDepth = 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/main/java/inference/axioms/RightSubstitution.java b/src/main/java/inference/axioms/RightSubstitution.java deleted file mode 100644 index 0d3edd9..0000000 --- a/src/main/java/inference/axioms/RightSubstitution.java +++ /dev/null @@ -1,149 +0,0 @@ -package inference.axioms; -import java.util.ArrayList; -import java.util.HashSet; -import java.util.List; -import java.util.Map; -import java.util.Set; - -import exceptions.SubstituteFailedException; -import inference.EquationAxiom; -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.meta.MatchConstraint; -import models.terms.meta.MetaDependencyTerm; -import models.terms.meta.MetaDynamicDependencyTerm; -import models.terms.meta.MetaEvaluatableTermVariable; -import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaTermGenerator; - -public class RightSubstitution extends EquationAxiom { - - public RightSubstitution() { - super("Right Substitution"); - this.assumptions = new ArrayList<>(); - this.repetitionAssumptions = new ArrayList<>(); - assumptions.add(new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("te0")), - new MetaEvaluatableTermVariable(new Variable("ue0")) - )); - repetitionAssumptions.add(new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("re")) - )); - repetitionAssumptions.add(new MetaEquationFormula( - new MetaDependencyTerm( - new MetaEvaluatableTermVariable(new Variable("re")), - new MetaEvaluatableTermVariable(new Variable("x")), - new MetaEvaluatableTermVariable(new Variable("y")) - ), - new MetaEvaluatableTermVariable(new Variable("te")) - )); - conclusion = new MetaEquationFormula( - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 1; - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("re" + curIndex / 2)); - } - return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2)); - } - }, - new MetaEvaluatableTermVariable(new Variable("se0")) - ), - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - curIndex -= 1; - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("re" + curIndex / 2)); - } - if (curIndex == 1) { - return new MetaEvaluatableTermVariable(new Variable("ue0")); - } - return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2)); - } - }, - new MetaEvaluatableTermVariable(new Variable("se0")) - ) - ); - conclusionMaxIndexCalculator = (assumptions) -> (assumptions.size() - 1) / 2 * 2 + 1; - conclusionMaxDepthCalculator = (assumptions) -> 1; - assumptionRepetitionSizeCalculator = (conclusion) -> (conclusion.getMaxIndex() - 1) / 2; - } - - @Override - protected Set apply(List assumptions, MatchConstraint constraint) { - Set result = new HashSet<>(); - result.add(constraint); - for (int i = 0; i < this.assumptions.size(); i++) { - MetaFormula metaAssumption = this.assumptions.get(i); - Formula assumption = assumptions.get(i); - result = metaAssumption.isMatchedBy(assumption, result); - if (result.isEmpty()) { - return new HashSet<>(); - } - } - if (this.repetitionAssumptions.size() != 0 && (assumptions.size() - this.assumptions.size()) % this.repetitionAssumptions.size() != 0) { - return new HashSet<>(); - } - 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); - 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) : 0; - subRes.add(conclusion.substitution(con.getBinding(), Map.of("maxIndex", maxIndex, "maxDepth", maxDepth))); - } catch (SubstituteFailedException e) { - continue; - } - } - return subRes; - } - -// @Override -// public RDLTerm generateRightSideHand(List assumptions, RDLTerm leftSideHand) { -// MetaRDLTerm metaLeftSideHand = ((MetaEquationFormula) conclusion).getLeftSideHand(); -// Set result = metaLeftSideHand.isMatchedBy(leftSideHand); -// int assumptionsSize = assumptionRepetitionSizeCalculator.calculate(leftSideHand); -// for (int i = 0; i < this.assumptions.size(); i++) { -// Formula assumption = assumptions.get(i); -// MetaFormula metaAssumption = this.assumptions.get(i); -// result = metaAssumption.isMatchedBy(assumption, result); -// if (result.isEmpty()) { -// return null; -// } -// } -// if (this.repetitionAssumptions.size() != 0 && (assumptions.size() - this.assumptions.size()) % this.repetitionAssumptions.size() != 0) { -// return null; -// } -// for (int i = 0; i < assumptionsSize; i++) { -// List metaAssumptions = repetitionAssumptionGenerate(i); -// for (int j = 0; j < metaAssumptions.size(); j++) { -// Formula assumption = assumptions.get(this.assumptions.size() + i * this.repetitionAssumptions.size() + j); -// MetaFormula metaAssumption = metaAssumptions.get(j); -// result = metaAssumption.isMatchedBy(assumption, result); -// if (result.isEmpty()) { -// return null; -// } -// } -// } -// return ((MetaEquationFormula) conclusion).getRightSideHand().substitute(result.iterator().next().getBinding(), Map.of("maxIndex", leftSideHand.getMaxIndex(), "maxDepth", leftSideHand.getMaxDepth())); -// } - -} diff --git a/src/main/java/inference/axioms/UncurriedMapping.java b/src/main/java/inference/axioms/UncurriedMapping.java deleted file mode 100644 index 2c168c7..0000000 --- a/src/main/java/inference/axioms/UncurriedMapping.java +++ /dev/null @@ -1,166 +0,0 @@ -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.Constant; -import models.algebra.Variable; -import models.formulas.DependencyFormula; -import models.formulas.Formula; -import models.formulas.meta.MetaDependencyFormula; -import models.formulas.meta.MetaEquationFormula; -import models.formulas.meta.MetaFormula; -import models.terms.Dependency; -import models.terms.RDLTerm; -import models.terms.Resource; -import models.terms.meta.MatchConstraint; -import models.terms.meta.MetaDependency; -import models.terms.meta.MetaDependencyTerm; -import models.terms.meta.MetaDynamicDependency; -import models.terms.meta.MetaEvaluatableTermVariable; -import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaTermGenerator; - -public class UncurriedMapping extends InferenceRule { - - public UncurriedMapping() { - super("Uncurried Mapping"); - this.assumptions.add( - new MetaDependencyFormula( - new MetaDynamicDependency(new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - int maxOrder = (Integer) context.get("maxOrder"); - context.put("" + curDepth, curIndex + 1); - context.put("maxDepth", Math.max((Integer) context.getOrDefault("maxDepth", 0), curDepth + 1)); - if (curIndex == 0 && curDepth == maxDepth - 1) { - return new MetaDependency( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")) - ); - } - if (curDepth < maxDepth && curIndex == 0) { - return new MetaDynamicDependency(this); - } - return new MetaEvaluatableTermVariable(new Variable("v" + curDepth), new Constant("" + (maxOrder - (maxDepth - curDepth)))); - } - }) - ) - ); - this.assumptions.add(new MetaEquationFormula( - new MetaDependencyTerm( - new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("xxx")), - new MetaEvaluatableTermVariable(new Variable("yyy")) - ), - new MetaEvaluatableTermVariable(new Variable("ue"), new Variable("m")) - )); - this.conclusion = new MetaDependencyFormula( - new MetaDynamicDependency(new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - int maxOrder = (Integer) context.get("maxOrder"); - int uOrder = (Integer) context.get("uOrder"); - int maxIdx = (Integer) context.get("" + curDepth); - if (curIndex >= maxIdx) { - return null; - } - if (curIndex == 0 && curDepth == maxDepth - 1) { - return new MetaDependencyTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("ue"), new Variable("m")) - ); - } - if (curDepth < maxDepth - 1 && curIndex == 0) { - return new MetaDynamicDependency(this); - } - if (curDepth == uOrder && curIndex == 1) { - return new MetaEvaluatableTermVariable(new Variable("ue"), new Variable("m")); - } - return new MetaEvaluatableTermVariable(new Variable("v" + curDepth), new Constant("" + (maxOrder - (maxDepth - curDepth)))); - } - }) - ); - } - - - protected Set apply(List assumptions, MatchConstraint constraint) { - Map context = new HashMap<>(); - if (assumptions.size() < getAssumptionSize()) { - return new HashSet<>(); - } - - Set result = new HashSet<>(); - result.add(constraint); - if (! (assumptions.get(0) instanceof DependencyFormula)) { - return new HashSet<>(); - } - Dependency dep = ((DependencyFormula)assumptions.get(0)).getDependency(); - int maxOrder = 0; - while (true) { - RDLTerm d2 = dep.getDependingTerm(); - if (d2 instanceof Resource) { - maxOrder = dep.getDependedTerms().iterator().next().getOrder(); - break; - } - dep = (Dependency) d2; - } - - for (int i = 0; i < getAssumptionSize(); i++) { - context.put("maxOrder", maxOrder); - result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result); - if (result.isEmpty()) { - return new HashSet<>(); - } - } - - Set ng = new HashSet<>(); - int m = 0; - for (MatchConstraint matchConstraint : result) { - int n = matchConstraint.getOrderConstraint().get(new Variable("n")).getOrder(); - m = matchConstraint.getOrderConstraint().get(new Variable("m")).getOrder(); - if (n != maxOrder) { - ng.add(matchConstraint); - continue; - } - } - context.put("" + m, (Integer) context.get("" + m) + 1); - - 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); - if (result.isEmpty()) { - return new HashSet<>(); - } - } - } - } - Set subRes = new HashSet<>(); - for (MatchConstraint con: result) { - try { - int maxIndex = conclusionMaxIndexCalculator != null ? conclusionMaxIndexCalculator.calculate(assumptions) : 10000; - int uOrder = con.getBinding().get(new Variable("ue")).getOrder(); - context.put("maxIndex", maxIndex); - context.put("uOrder", uOrder); - subRes.add(conclusion.substitution(con.getBinding(), context)); - } catch (SubstituteFailedException e) { - continue; - } - } - return subRes; - } - -} diff --git a/src/main/java/inference/axioms/Uncurrying.java b/src/main/java/inference/axioms/Uncurrying.java deleted file mode 100644 index 93f0dc0..0000000 --- a/src/main/java/inference/axioms/Uncurrying.java +++ /dev/null @@ -1,244 +0,0 @@ -package inference.axioms; -import java.util.HashSet; -import java.util.List; -import java.util.Map; -import java.util.Set; - -import exceptions.SubstituteFailedException; -import inference.EquationAxiom; -import models.algebra.Variable; -import models.formulas.Formula; -import models.formulas.meta.MetaDependencyFormula; -import models.formulas.meta.MetaEquationFormula; -import models.terms.meta.MatchConstraint; -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; -import utils.ExpressionUtils; - -public class Uncurrying extends EquationAxiom { - - public Uncurrying() { - super("Uncurrying"); - - assumptions.add( - new MetaDependencyFormula( - new MetaDynamicDependency( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - int i = maxDepth - curDepth; - context.put("" + curDepth, curIndex); - context.put("depth", curDepth + 1); - if (curDepth == maxDepth - 1 && curIndex == 0) { - return new MetaDynamicDependency( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex2, int curDepth2, int maxIndex2, int maxDepth2, Map context2) { - curIndex2 -= 2; - context2.put("" + curDepth2, curIndex2 + 1); - context2.put("depth", curDepth2); - return new MetaEvaluatableTermVariable(new Variable("v" + curDepth2 + "_" + curIndex2), new Variable("n")); - } - }, - new MetaEvaluatableTermVariable(new Variable("s"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")) - ); - } else if (curIndex == 0) { - return new MetaDynamicDependency(this); - } - curIndex -= 1; - return new MetaEvaluatableTermVariable(new Variable("v" + curDepth + "_" + curIndex), ExpressionUtils.parse("n - " + i)); - } - } - ) - ) - ); - - assumptions.add( - new MetaEquationFormula( - new MetaDependencyTerm( - new MetaEvaluatableTermVariable(new Variable("q"), new Variable("m")), - new MetaEvaluatableTermVariable(new Variable("xxx")), - new MetaEvaluatableTermVariable(new Variable("yyy")) - ), - new MetaEvaluatableTermVariable(new Variable("u"), new Variable("m")) - ) - ); - - assumptions.add( - new MetaEquationFormula( - new MetaDependencyTerm( - new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("xxxx")), - new MetaEvaluatableTermVariable(new Variable("yyyy")) - ), - new MetaEvaluatableTermVariable(new Variable("q"), new Variable("m")) - ) - ); - - conclusion = new MetaEquationFormula( - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - int i = maxDepth - curDepth; - maxIndex = (Integer) context.get("" + curDepth); - if (curDepth == maxDepth - 1 && curIndex == 0) { - return new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex2, int curDepth2, int maxIndex2, int maxDepth2, Map context2) { - curIndex2 -= 3; - maxIndex2 = (Integer) context.getOrDefault("" + curDepth2, 0); - if (curIndex2 >= maxIndex2 * 2) { - return null; - } - if (curIndex2 % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("v" + curDepth2 + "_" + curIndex2 / 2), new Variable("n")); - } - return new MetaEvaluatableTermVariable(new Variable("x" + curDepth2 + "_" + curIndex2 / 2), new Variable("n")); - } - }, - new MetaEvaluatableTermVariable(new Variable("s"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("u"), new Variable("m")) - ); - } - if (curIndex == 0) { - return new MetaDynamicDependency(this); - } - curIndex -= 1; - if (curIndex >= maxIndex * 2) { - return null; - } - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("v" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n - " + i)); - } - return new MetaEvaluatableTermVariable(new Variable("x" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n - " + i)); - } - } - ), - new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - int m = (Integer) context.get("m"); - int n = (Integer) context.get("n"); - int i = maxDepth - curDepth; - maxIndex = (Integer) context.get("" + curDepth); - if (curDepth == maxDepth - 1 && curIndex == 0) { - return new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex2, int curDepth2, int maxIndex2, int maxDepth2, Map context2) { - curIndex2 -= 3; - maxIndex2 = (Integer) context.getOrDefault("" + curDepth2, 0); - if (curIndex2 >= maxIndex2 * 2) { - return null; - } - if (curIndex2 % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("v" + curDepth2 + "_" + curIndex2 / 2), new Variable("n")); - } - return new MetaEvaluatableTermVariable(new Variable("x" + curDepth2 + "_" + curIndex2 / 2), new Variable("n")); - } - }, - new MetaEvaluatableTermVariable(new Variable("s"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("q"), new Variable("m")) - ); - } - if (curIndex == 0) { - return new MetaDynamicDependency(this); - } - curIndex -= 1; - if (n - i == m) { - if (curIndex == 0) { - return new MetaEvaluatableTermVariable(new Variable("q"), new Variable("m")); - } - if (curIndex == 1) { - return new MetaEvaluatableTermVariable(new Variable("u"), new Variable("m")); - } - curIndex -= 2; - if (curIndex >= maxIndex * 2) { - return null; - } - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("v" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n - " + i)); - } - return new MetaEvaluatableTermVariable(new Variable("x" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n - " + i)); - } - if (curIndex >= maxIndex * 2) { - return null; - } - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("v" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n - " + i)); - } - return new MetaEvaluatableTermVariable(new Variable("x" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n - " + i)); - } - } - ) - ); - - } - - - @Override - protected Set apply(List assumptions, MatchConstraint constraint) { - - Set result = new HashSet<>(); - result.add(constraint); - if (assumptions.size() < 2) { - return new HashSet<>(); - } - - for (int i = 0; i < 3; i++) { - result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result); - if (result.isEmpty()) { - return new HashSet<>(); - } - } - - int count = 3; - int depth = (Integer) context.get("depth"); - for (int d = 1; d < depth + 1; d++) { - if (! context.containsKey("" + d)) break; - for (int i = 0; i < (Integer) context.getOrDefault("" + d, 0); i++) { - Formula assumption = assumptions.get(count); - MetaEquationFormula mef = new MetaEquationFormula( - new MetaDependencyTerm( - new MetaEvaluatableTermVariable(new Variable("v" + d + "_" + i), ExpressionUtils.parse("n-" + (depth - d))), - new MetaEvaluatableTermVariable(new Variable("xxx" + d + "_" + i)), - new MetaEvaluatableTermVariable(new Variable("yyy" + d + "_" + i)) - ), - new MetaEvaluatableTermVariable(new Variable("x" + d + "_" + i), ExpressionUtils.parse("n-" + (depth - d))) - ); - result = mef.isMatchedBy(assumption, result); - if (result.isEmpty()) { - return new HashSet<>(); - } - count++; - } - } - - Set subRes = new HashSet<>(); - for (MatchConstraint con: result) { - try { - int maxIndex = 10000; - int maxDepth = depth; - con.getContext().put("maxIndex", maxIndex); - con.getContext().put("maxDepth", maxDepth); - con.getContext().put("m", con.getOrderConstraint().get(new Variable("m")).getOrder()); - con.getContext().put("n", con.getOrderConstraint().get(new Variable("n")).getOrder()); - subRes.add(conclusion.substitution(con.getBinding(), con.getContext())); - } catch (SubstituteFailedException e) { - continue; - } - } - return subRes; - } - -} diff --git a/src/test/java/inferencerule/EqualityAxiomTest.java b/src/test/java/inferencerule/EqualityAxiomTest.java index effb141..21af142 100644 --- a/src/test/java/inferencerule/EqualityAxiomTest.java +++ b/src/test/java/inferencerule/EqualityAxiomTest.java @@ -1,20 +1,17 @@ package inferencerule; import static org.junit.jupiter.api.Assertions.*; +import java.util.HashSet; import java.util.Set; import org.junit.jupiter.api.Test; import inference.ProofSystem; -import inference.axioms.RightSubstitution; -import models.formulas.DependencyFormula; import models.formulas.EquationFormula; import models.formulas.Formula; -import models.terms.Dependency; import models.terms.DependencyTerm; +import models.terms.RDLTerm; import models.terms.Resource; -import models.terms.ResourceConstant; -import utils.Utils; public class EqualityAxiomTest { @@ -35,81 +32,43 @@ @Test void ReflexivityTest() { + Set terms = new HashSet<>(); + terms.add(a); + terms.add(b); + Set formulas = ProofSystem.reflexivity.apply(new HashSet<>(), terms); + assertTrue(formulas.contains(new EquationFormula(a, a))); + assertTrue(formulas.contains(new EquationFormula(b, b))); } @Test void SymmetryTest() { - EquationFormula eq1 = new EquationFormula(a, b); - Set result = ProofSystem.symmetry.apply(eq1); - assertTrue(result.contains(new EquationFormula(b, a))); + Set formulas = ProofSystem.symmetry.apply(Set.of(new EquationFormula(a, b), new EquationFormula(new DependencyTerm(a, b, c), d)), Set.of()); + assertTrue(formulas.contains(new EquationFormula(b, a))); + assertTrue(formulas.contains(new EquationFormula(d, new DependencyTerm(a, b, c)))); } @Test void TransitivityTest() { - EquationFormula eq1 = new EquationFormula(a, b); - EquationFormula eq2 = new EquationFormula(b, c); - EquationFormula eq3 = new EquationFormula(a, c); - Set result = ProofSystem.transitivity.apply(eq1, eq2); - assertTrue(result.contains(eq3)); - + Set formulas = ProofSystem.transitivity.apply(Set.of(new EquationFormula(a, b), new EquationFormula(b, c), new EquationFormula(c, d)), Set.of()); + assertTrue(formulas.contains(new EquationFormula(a, c))); + assertTrue(formulas.contains(new EquationFormula(b, d))); + assertFalse(formulas.contains(new EquationFormula(a, d))); } @Test void RightSubTest() { - RightSubstitution rs = new RightSubstitution(); - EquationFormula eq = new EquationFormula(a, b); - DependencyFormula dep = new DependencyFormula(c, d); - DependencyTerm t1 = new DependencyTerm(c, d, a); - DependencyTerm t2 = new DependencyTerm(c, d, b); - EquationFormula eq2 = new EquationFormula(new DependencyTerm(d, e, f), a); - Set result = rs.apply(Set.of(eq, dep, eq2)); - assertTrue(result.contains(new EquationFormula(t1, t2))); - -// assertEquals(rs.generateRightSideHand(List.of(eq, dep, eq2), t1), t2); - DependencyFormula dep2 = new DependencyFormula(c, g); - EquationFormula eq3 = new EquationFormula(new DependencyTerm(g, h, i), j); - DependencyTerm t3 = new DependencyTerm(c, d, a, g, j); - DependencyTerm t4 = new DependencyTerm(c, d, b, g, j); - result = rs.apply(Set.of(eq, eq2, eq3, dep, dep2)); - assertTrue(result.contains(new EquationFormula(t3, t4))); } @Test void LeftSubTest() { - EquationFormula eq1 = new EquationFormula(a, b); - DependencyFormula d1 = new DependencyFormula(a, c); - EquationFormula eq2 = new EquationFormula(new DependencyTerm(c, d, e), f); - Set result = ProofSystem.leftSubstitution.apply(eq1, d1, eq2); - assertTrue(result.contains(new EquationFormula(new DependencyTerm(a, c, f), new DependencyTerm(b, c, f)))); } @Test void IdentityTest() { - EquationFormula eq1 = new EquationFormula(new DependencyTerm(a, b, c), d); - Set result = ProofSystem.identity.apply(eq1); - assertTrue(result.contains(new EquationFormula(new DependencyTerm(a, a, d), d))); - - EquationFormula eq2 = new EquationFormula(new DependencyTerm(a, b, c), d); - EquationFormula eq3 = new EquationFormula(new DependencyTerm(e, f, g), h); - result = ProofSystem.identity.apply(eq2, eq3); - assertTrue(result.contains(new EquationFormula(new DependencyTerm(a, a, d, e, h), d))); } @Test void MapCompositionTest() { - DependencyFormula df1 = new DependencyFormula(a, b, c); - DependencyFormula df2 = new DependencyFormula(b, d, e); - EquationFormula eq1 = Utils.in(f, c); - EquationFormula eq2 = Utils.in(g, d); - EquationFormula eq3 = Utils.in(h, e); - Set result = ProofSystem.mapComposition.apply(df2, df1, eq2, eq3, eq1); - EquationFormula conc1 = new EquationFormula( - new DependencyTerm( - a, b, new DependencyTerm(b, d, g, e, h), c, f - ), - new DependencyTerm(a, d, g, e, h, c, f) - ); - assertTrue(result.contains(conc1)); } @Test @@ -119,63 +78,18 @@ @Test void RightNormalizationTest() { - DependencyFormula d1 = new DependencyFormula(new Dependency(m, n), a, b); - DependencyFormula d2 = new DependencyFormula(c, d, e); - EquationFormula eq1 = Utils.in(c, n); - EquationFormula eq2 = Utils.in(f, a); - EquationFormula eq3 = Utils.in(g, b); - EquationFormula eq4 = Utils.in(h, d); - EquationFormula eq5 = Utils.in(j, e); - Set result = ProofSystem.rightNormalization.apply(d1, d2, eq1, eq2, eq3, eq4, eq5); - EquationFormula conc1 = new EquationFormula( - new DependencyTerm( - new DependencyTerm( - m, n, c - ), - a, f, b, g, d, h, e, j - ), - new DependencyTerm( - new DependencyTerm( - m ,n, new DependencyTerm( - c, d, h, e, j - ) - ), - a, f, b, g - ) - ); - assertTrue(result.contains(conc1)); } @Test void PseudoConstantnessTest() { - Set result = ProofSystem.pseudoConstantness.apply(new DependencyFormula(a, b)); - assertTrue(result.contains(new EquationFormula(new DependencyTerm(a, b, b), a))); - - result = ProofSystem.pseudoConstantness.apply(new DependencyFormula(a, b, c, d)); - assertTrue(result.contains(new EquationFormula(new DependencyTerm(a, b, b, c, c, d, d), a))); } @Test void UncurryingTest() { - DependencyFormula d1 = new DependencyFormula(new Dependency(m, n), a); - EquationFormula eq1 = Utils.in(c, n); - EquationFormula eq2 = Utils.in(b, c); - EquationFormula eq3 = Utils.in(d, a); - Set result = ProofSystem.uncurrying.apply(d1, eq1, eq2, eq3); - EquationFormula eq4 = new EquationFormula( - new DependencyTerm(new DependencyTerm(m, n, b), a, d), - new DependencyTerm(new DependencyTerm(m, n, c), a, d, c, b) - ); - assertTrue(result.contains(eq4)); } @Test void ArgumentDependencyExtractionTest() { - Set result = ProofSystem.argumentDependencyExtraction.apply( - new DependencyFormula(a, b, c), - new DependencyFormula(b, c), - new EquationFormula(new DependencyTerm(a, b, d, c, e), new ResourceConstant("ccc"))); - assertTrue(result.contains(new EquationFormula(new DependencyTerm(b, c, e), d))); } } diff --git a/src/test/java/terms/meta/MetaDynamicDependencyTest.java b/src/test/java/terms/meta/MetaDynamicDependencyTest.java index ba8c937..ed8ce54 100644 --- a/src/test/java/terms/meta/MetaDynamicDependencyTest.java +++ b/src/test/java/terms/meta/MetaDynamicDependencyTest.java @@ -111,7 +111,6 @@ Dependency d3 = new Dependency(d2, b); assertFalse(md1.isMatchedBy(d2).isEmpty()); assertFalse(md1.isMatchedBy(d3).isEmpty()); - System.out.println(md1.isMatchedBy(d3)); } }