diff --git a/src/main/java/inference/EquationAxiom.java b/src/main/java/inference/EquationAxiom.java index 33b79b4..5e08459 100644 --- a/src/main/java/inference/EquationAxiom.java +++ b/src/main/java/inference/EquationAxiom.java @@ -1,15 +1,8 @@ package inference; import java.util.List; -import java.util.Set; -import exceptions.SubstituteFailedException; -import models.formulas.Formula; -import models.formulas.meta.MetaEquationFormula; import models.formulas.meta.MetaFormula; -import models.terms.RDLTerm; -import models.terms.meta.MatchConstraint; -import utils.Permutation; public class EquationAxiom extends InferenceRule{ @@ -30,24 +23,4 @@ super(name, assumptions, repetitionAssumptions, conclusion, constraint, conclusionMaxIndexCalculator, conclusionMaxDepthCalculator, assumptionSizeCalculator); } - public RDLTerm generateRightSideHand(List assumptions, RDLTerm leftSideHand) { - if (! (this.conclusion instanceof MetaEquationFormula)) return null; - if (this.assumptions.size() > assumptions.size()) return null; - MetaEquationFormula metaFormula = (MetaEquationFormula) this.conclusion; - Set constraints = metaFormula.getLeftSideHand().isMatchedBy(leftSideHand); - for (List assumptionList: Permutation.permutation(assumptions, assumptions.size())) { - for (int i = 0; i < getAssumptionSize(); i++) { - constraints = this.assumptions.get(i).isMatchedBy(assumptionList.get(i), constraints); - } - for (MatchConstraint constraint: constraints) { - try { - return metaFormula.getRightSideHand().substitute(constraint.getBinding()); - } catch (SubstituteFailedException e) { - continue; - } - } - } - return null; - } - } diff --git a/src/main/java/inference/In.java b/src/main/java/inference/In.java index b354543..f8bee34 100644 --- a/src/main/java/inference/In.java +++ b/src/main/java/inference/In.java @@ -9,6 +9,7 @@ import lombok.RequiredArgsConstructor; import models.algebra.Constant; import models.algebra.Variable; +import models.formulas.Formula; import models.formulas.meta.MetaEquationFormula; import models.terms.EvaluatableTerm; import models.terms.RDLTerm; @@ -23,7 +24,7 @@ @RequiredArgsConstructor @Getter -public class In { +public class In extends Formula { private final EvaluatableTerm leftSideHand; private final EvaluatableTerm rightSideHand; @@ -173,10 +174,22 @@ return result; } - @Override public String toString() { return leftSideHand.toString() + " in " + rightSideHand.toString(); } + @Override + public boolean equals(Object another) { + if (another instanceof In in) { + return this.leftSideHand.equals(in.getLeftSideHand()) && this.rightSideHand.equals(in.getRightSideHand()); + } + return false; + } + + @Override + public int hashCode() { + return toString().hashCode(); + } + } diff --git a/src/main/java/inference/InferenceRule.java b/src/main/java/inference/InferenceRule.java index 3a65936..d9f553a 100644 --- a/src/main/java/inference/InferenceRule.java +++ b/src/main/java/inference/InferenceRule.java @@ -9,11 +9,12 @@ import exceptions.SubstituteFailedException; import lombok.Getter; +import models.formulas.DependencyFormula; import models.formulas.Formula; -import models.formulas.meta.MetaDependencyFormula; 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; @@ -143,24 +144,37 @@ return subRes; } - private static Set requiredAssumptions(EvaluatableTerm term) { + private static Set requiredAssumptions(EvaluatableTerm term) { if (term instanceof Resource) { return new HashSet<>(); } DependencyTerm depTerm = (DependencyTerm) term; - Set result = new HashSet<>(); + Set result = new HashSet<>(); EvaluatableTerm dependingTerm = depTerm.getDependingTerm(); List dependedTerms = depTerm.getDependedTerms(); List argumentTerms = depTerm.getArgumentTerms(); + for (int i = 0; i < dependedTerms.size(); i++) { + EvaluatableTerm dependedTerm = dependedTerms.get(i); + EvaluatableTerm argTerm = argumentTerms.get(i); + In in = new In(argTerm, dependedTerm); + result.add(in); + } if (dependingTerm instanceof Resource) { - result.add(new MetaDependencyFormula(dependingTerm, dependedTerms)); - for (int i = 0; i < dependedTerms.size(); i++) { - EvaluatableTerm dependedTerm = dependedTerms.get(i); - EvaluatableTerm argTerm = argumentTerms.get(i); - In in = new In(dependedTerm, argTerm); + result.add(new DependencyFormula(dependingTerm, dependedTerms)); + } else if (dependingTerm instanceof DependencyTerm depending) { + for (Formula formula : requiredAssumptions(depending)) { + if (formula instanceof DependencyFormula dependency) { + DependencyTerm newDependingTerm = new DependencyTerm((EvaluatableTerm) dependency.getDependency().getDependingTerm(), dependedTerms, argumentTerms); + List newDependedTerms = new ArrayList<>(); + for (RDLTerm dependedTerm : dependency.getDependency().getDependedTerms()) { + newDependedTerms.add(new DependencyTerm((EvaluatableTerm) dependedTerm, dependedTerms, argumentTerms)); + } + result.add(new DependencyFormula(newDependingTerm, newDependedTerms)); + } else if(formula instanceof In in) { + result.add(new In(new DependencyTerm(in.getLeftSideHand(), dependedTerms, argumentTerms), new DependencyTerm(in.getRightSideHand(), dependedTerms, argumentTerms))); + } } } - return result; } diff --git a/src/main/java/inference/axioms/RightSubstitution.java b/src/main/java/inference/axioms/RightSubstitution.java index 2af7896..0d3edd9 100644 --- a/src/main/java/inference/axioms/RightSubstitution.java +++ b/src/main/java/inference/axioms/RightSubstitution.java @@ -12,7 +12,6 @@ import models.formulas.meta.MetaDependencyFormula; import models.formulas.meta.MetaEquationFormula; import models.formulas.meta.MetaFormula; -import models.terms.RDLTerm; import models.terms.meta.MatchConstraint; import models.terms.meta.MetaDependencyTerm; import models.terms.meta.MetaDynamicDependencyTerm; @@ -117,34 +116,34 @@ 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())); - } +// @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/models/formulas/meta/MetaDependencyFormula.java b/src/main/java/models/formulas/meta/MetaDependencyFormula.java index 9006d47..035a095 100644 --- a/src/main/java/models/formulas/meta/MetaDependencyFormula.java +++ b/src/main/java/models/formulas/meta/MetaDependencyFormula.java @@ -65,7 +65,7 @@ } @Override - public MetaDependencyFormula replace(Map mapping) { + public MetaDependencyFormula replace(Map mapping) { return new MetaDependencyFormula(this.dependency.replace(mapping)); } diff --git a/src/main/java/models/formulas/meta/MetaEquationFormula.java b/src/main/java/models/formulas/meta/MetaEquationFormula.java index b048a56..25ad5f1 100644 --- a/src/main/java/models/formulas/meta/MetaEquationFormula.java +++ b/src/main/java/models/formulas/meta/MetaEquationFormula.java @@ -71,7 +71,7 @@ } @Override - public MetaEquationFormula replace(Map mapping) { + public MetaEquationFormula replace(Map mapping) { RDLTerm left = leftSideHand; RDLTerm right = rightSideHand; if (leftSideHand instanceof MetaRDLTerm metaLeft) { diff --git a/src/main/java/models/formulas/meta/MetaFormula.java b/src/main/java/models/formulas/meta/MetaFormula.java index b004432..36ad2c4 100644 --- a/src/main/java/models/formulas/meta/MetaFormula.java +++ b/src/main/java/models/formulas/meta/MetaFormula.java @@ -11,7 +11,7 @@ import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaVariable; -public abstract class MetaFormula extends Formula{ +public abstract class MetaFormula extends Formula { public Set isMatchedBy(Formula formula) { return isMatchedBy(formula, MatchConstraint.createDefault()); @@ -32,7 +32,7 @@ public abstract Set getSubTerms(Class clazz); - public abstract MetaFormula replace(Map mapping); + public abstract MetaFormula replace(Map mapping); public abstract Set getAllVariables(); } diff --git a/src/main/java/models/terms/meta/MetaDependency.java b/src/main/java/models/terms/meta/MetaDependency.java index ee84213..c749270 100644 --- a/src/main/java/models/terms/meta/MetaDependency.java +++ b/src/main/java/models/terms/meta/MetaDependency.java @@ -128,7 +128,7 @@ } @Override - public MetaRDLTerm replace(Map mapping) { + public MetaRDLTerm replace(Map mapping) { RDLTerm dependingTerm = this.dependingTerm; List dependedTerms = new ArrayList<>(); if (dependingTerm instanceof MetaRDLTerm metaTerm) { diff --git a/src/main/java/models/terms/meta/MetaDependencyTerm.java b/src/main/java/models/terms/meta/MetaDependencyTerm.java index 93519f9..3adedb8 100644 --- a/src/main/java/models/terms/meta/MetaDependencyTerm.java +++ b/src/main/java/models/terms/meta/MetaDependencyTerm.java @@ -153,7 +153,7 @@ } @Override - public MetaRDLTerm replace(Map mapping) { + public MetaRDLTerm replace(Map mapping) { RDLTerm dependingTerm = this.dependingTerm; List termPairs = new ArrayList<>(); if (dependingTerm instanceof MetaRDLTerm metaTerm) { diff --git a/src/main/java/models/terms/meta/MetaRDLTerm.java b/src/main/java/models/terms/meta/MetaRDLTerm.java index 7fd1acb..7167e81 100644 --- a/src/main/java/models/terms/meta/MetaRDLTerm.java +++ b/src/main/java/models/terms/meta/MetaRDLTerm.java @@ -112,7 +112,7 @@ return -1; } - public abstract RDLTerm replace(Map mapping); + public abstract RDLTerm replace(Map mapping); @Override public String toStringWithOrder() { diff --git a/src/main/java/models/terms/meta/MetaVariable.java b/src/main/java/models/terms/meta/MetaVariable.java index 5d2541a..31edbfb 100644 --- a/src/main/java/models/terms/meta/MetaVariable.java +++ b/src/main/java/models/terms/meta/MetaVariable.java @@ -138,7 +138,7 @@ public abstract MetaVariable cloneWithName(String name); @Override - public RDLTerm replace(Map mapping) { + public RDLTerm replace(Map mapping) { RDLTerm v = this; if (mapping.containsKey(v)) { v = mapping.get(v); diff --git a/src/test/java/inferencerule/EqualityAxiomTest.java b/src/test/java/inferencerule/EqualityAxiomTest.java index 3c242a6..effb141 100644 --- a/src/test/java/inferencerule/EqualityAxiomTest.java +++ b/src/test/java/inferencerule/EqualityAxiomTest.java @@ -1,7 +1,6 @@ package inferencerule; import static org.junit.jupiter.api.Assertions.*; -import java.util.List; import java.util.Set; import org.junit.jupiter.api.Test; @@ -66,7 +65,7 @@ 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); +// 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);