diff --git a/src/Main.java b/src/Main.java index 4156845..85f114c 100644 --- a/src/Main.java +++ b/src/Main.java @@ -38,17 +38,38 @@ DependencyTerm t2 = new DependencyTerm(Ap, Bp, Cp); EquationFormula assumptionFormula = new EquationFormula(t1, t2); EquationFormula conclusionFormula = new EquationFormula( - new DependencyTerm(new DependencyTerm(A, B, new DependencyTerm(C, D, E)),F, G), - new DependencyTerm(new DependencyTerm(Ap, Bp, new DependencyTerm(Cp, D, E)),F, G) + new DependencyTerm(new DependencyTerm(new DependencyTerm(A, B, C), D, E), F, G), + new DependencyTerm(new DependencyTerm(new DependencyTerm(Ap, Bp, Cp), D, E), F, G) ); SemanticEquivalenceProofSystem proofSystem = new SemanticEquivalenceProofSystem( List.of(new SemanticEquivalenceRelation(assumptionFormula, 2)), conclusionFormula ); - proofSystem.proof(); + +// System.out.println(conclusionFormula.linearRightNormalized()); + System.out.println(proofSystem.proof()); +// sandbox2(); } + static void sandbox2() { + ResourceVariable A = new ResourceVariable("A", Utils.INT, 2); + ResourceVariable Ap = new ResourceVariable("A'", Utils.INT, 2); + ResourceVariable B = new ResourceVariable("B", Utils.INT, 2); + ResourceVariable Bp = new ResourceVariable("B'", Utils.INT, 2); + ResourceVariable C = new ResourceVariable("C", Utils.INT, 2); + ResourceVariable Cp = new ResourceVariable("C'", Utils.INT, 2); + ResourceVariable D = new ResourceVariable("D", Utils.INT, 2); + ResourceVariable E = new ResourceVariable("E", Utils.INT, 1); + ResourceVariable F = new ResourceVariable("F", Utils.INT, 1); + ResourceVariable G = new ResourceVariable("G", Utils.INT, 0); + DependencyTerm t1 = new DependencyTerm(A, B, C); + DependencyTerm t2 = new DependencyTerm(t1, B, E); + System.out.println(t2); + System.out.println(t2.isLinearRightNormalized()); + t2.selfLinearRightNormalize(); + System.out.println(t2); + } diff --git a/src/inference/equivalence/MetaSemanticEquivalenceRelation.java b/src/inference/equivalence/MetaSemanticEquivalenceRelation.java index 3e0c395..6c73c1d 100644 --- a/src/inference/equivalence/MetaSemanticEquivalenceRelation.java +++ b/src/inference/equivalence/MetaSemanticEquivalenceRelation.java @@ -14,6 +14,7 @@ import lombok.Getter; import models.algebra.Expression; import models.algebra.Variable; +import models.terms.EvaluatableTerm; import models.terms.RDLTerm; import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaVariable; @@ -88,8 +89,8 @@ if (flg) { continue; } - RDLTerm leftTerm = leftSideHand.substitute(tempBinding); - RDLTerm rightTerm = rightSideHand.substitute(tempBinding); + EvaluatableTerm leftTerm = (EvaluatableTerm) leftSideHand.substitute(tempBinding); + EvaluatableTerm rightTerm = (EvaluatableTerm) rightSideHand.substitute(tempBinding); Map tempOrderConstraint = new HashMap<>(); for(Variable key : orderConstraint.keySet()) { tempOrderConstraint.put(key, (OrderVariableConstraint)orderConstraint.get(key).clone()); @@ -155,13 +156,13 @@ if (! rightSideHand.isMatchedBy(tempTerm, binding, orderConstraint)) { continue; } - result.add(new SemanticEquivalenceRelation(leftSideHand.substitute(binding), rightSideHand.substitute(binding), order)); + result.add(new SemanticEquivalenceRelation((EvaluatableTerm)leftSideHand.substitute(binding), (EvaluatableTerm) rightSideHand.substitute(binding), order)); for (int i = 0; i < leftVariables.size(); i++) { binding.remove(leftVariables.get(i)); } } try { - result.add(new SemanticEquivalenceRelation(leftSideHand.substitute(binding), rightSideHand.substitute(binding), order)); + result.add(new SemanticEquivalenceRelation((EvaluatableTerm)leftSideHand.substitute(binding), (EvaluatableTerm)rightSideHand.substitute(binding), order)); } catch (SubstituteFailedException e){} return result; } @@ -201,13 +202,13 @@ } continue; } - result.add(new SemanticEquivalenceRelation(leftSideHand.substitute(binding), rightSideHand.substitute(binding), order)); + result.add(new SemanticEquivalenceRelation((EvaluatableTerm)leftSideHand.substitute(binding), (EvaluatableTerm)rightSideHand.substitute(binding), order)); for (int i = 0; i < leftVariables.size(); i++) { binding.remove(leftVariables.get(i)); } } try { - result.add(new SemanticEquivalenceRelation(leftSideHand.substitute(binding), rightSideHand.substitute(binding), order)); + result.add(new SemanticEquivalenceRelation((EvaluatableTerm)leftSideHand.substitute(binding), (EvaluatableTerm)rightSideHand.substitute(binding), order)); } catch (SubstituteFailedException e){} return result; diff --git a/src/inference/equivalence/SemanticEquivalenceProofSystem.java b/src/inference/equivalence/SemanticEquivalenceProofSystem.java index a865300..a2e8aa6 100644 --- a/src/inference/equivalence/SemanticEquivalenceProofSystem.java +++ b/src/inference/equivalence/SemanticEquivalenceProofSystem.java @@ -2,6 +2,7 @@ import java.util.ArrayList; import java.util.Collection; +import java.util.Collections; import java.util.HashMap; import java.util.HashSet; import java.util.List; @@ -13,6 +14,7 @@ import models.algebra.Variable; import models.dataConstraintModel.DataConstraintModel; import models.formulas.EquationFormula; +import models.terms.EvaluatableTerm; import models.terms.LinearRightNormalizedType; import models.terms.RDLTerm; import models.terms.meta.MetaEvaluatableTermVariable; @@ -23,8 +25,9 @@ public class SemanticEquivalenceProofSystem { - private Map> assumptions; + private Map> assumptions; private EquationFormula conclusion; + private Map proofGraph = new HashMap<>(); int maxOrder = -1; private static MetaSemanticEquivalenceRelation rule1 = new MetaSemanticEquivalenceRelation( @@ -62,64 +65,84 @@ for(SemanticEquivalenceRelation assumption : assumptions) { maxOrder = Math.max(maxOrder, assumption.getOrder()); if (! this.assumptions.containsKey(assumption.getOrder())) { - this.assumptions.put(assumption.getOrder(), new ArrayList<>()); + this.assumptions.put(assumption.getOrder(), new HashSet<>()); } - this.assumptions.get(assumption.getOrder()).add(assumption); + this.assumptions.get(assumption.getOrder()).add(assumption.linearRightNormalized()); + this.conclusion = conclusion; } - this.conclusion = conclusion; } public boolean proof() { Set existTerms = new HashSet<>(); - existTerms.addAll(conclusion.getLeftSideHand().getSubTerms(RDLTerm.class).values()); - existTerms.addAll(conclusion.getRightSideHand().getSubTerms(RDLTerm.class).values()); + EquationFormula linearRightNormalizedConclusion = conclusion.linearRightNormalized(); + existTerms.addAll(linearRightNormalizedConclusion.getLeftSideHand().getSubTerms(EvaluatableTerm.class).values()); + existTerms.addAll(linearRightNormalizedConclusion.getRightSideHand().getSubTerms(EvaluatableTerm.class).values()); + SemanticEquivalenceRelation conclusionRelation = new SemanticEquivalenceRelation(conclusion.getLeftSideHand(), conclusion.getRightSideHand(), conclusion.getLeftSideHand().getOrder()); + SemanticEquivalenceRelation linearConclusionRelation = new SemanticEquivalenceRelation(linearRightNormalizedConclusion.getLeftSideHand(), linearRightNormalizedConclusion.getRightSideHand(), linearRightNormalizedConclusion.getLeftSideHand().getOrder()); + if (! linearRightNormalizedConclusion.equals(conclusion)) { + proofGraph.put(conclusionRelation, linearConclusionRelation); + } for(int key : assumptions.keySet()) { for(SemanticEquivalenceRelation relation : assumptions.get(key)) { - existTerms.addAll(relation.getLeftSideHand().getSubTerms(RDLTerm.class).values()); + existTerms.addAll(relation.getLeftSideHand().getSubTerms(EvaluatableTerm.class).values()); existTerms.add(relation.getLeftSideHand()); - existTerms.addAll(relation.getRightSideHand().getSubTerms(RDLTerm.class).values()); + existTerms.addAll(relation.getRightSideHand().getSubTerms(EvaluatableTerm.class).values()); existTerms.add(relation.getRightSideHand()); } } - for (int i = maxOrder; i > 0; i--) { - if (i == 1) { - System.out.println("aaa"); - } + + + for (int i = maxOrder; i > linearRightNormalizedConclusion.getLeftSideHand().getOrder(); i--) { + Set apperTerms = new HashSet<>(); for (SemanticEquivalenceRelation relation : assumptions.get(i)) { - applyRule4(relation, existTerms); + apperTerms.addAll(applyRule4(relation, existTerms)); } + existTerms.addAll(apperTerms); } - for(int order : assumptions.keySet()) { - System.out.println(order); - for(SemanticEquivalenceRelation relation : assumptions.get(order)) { - System.out.println(relation); - } - System.out.println("============================"); + + + List proofResult = new ArrayList<>(); + SemanticEquivalenceRelation currentRelation = conclusionRelation; + while(proofGraph.containsKey(currentRelation)) { + proofResult.add(currentRelation); + currentRelation = proofGraph.get(currentRelation); } - return false; + proofResult.add(currentRelation); + Collections.reverse(proofResult); + for (int i = 0; i < proofResult.size(); i++) { + SemanticEquivalenceRelation relation = proofResult.get(i); + System.out.println(relation); + if (i < proofResult.size() - 1) System.out.println("=============================================================="); + } + return assumptions.get(0).contains(linearConclusionRelation); } private void applyRule1() { } - private void applyRule4(SemanticEquivalenceRelation relation, Set existTerms) { + private Set applyRule4(SemanticEquivalenceRelation relation, Set existTerms) { Map binding = new HashMap<>(); Map orderConstraint = new HashMap<>(); + Set apperTerms = new HashSet<>(); if (rule4_1.isMatchedBy(relation, binding, orderConstraint)) { Set results = rule4_2.substitute(binding, orderConstraint, existTerms); for (SemanticEquivalenceRelation result : results) { if (! assumptions.containsKey(result.getOrder())) { - assumptions.put(result.getOrder(), new ArrayList<>()); + assumptions.put(result.getOrder(), new HashSet<>()); } - assumptions.get(result.getOrder()).add(result); - existTerms.addAll(result.getLeftSideHand().getSubTerms(RDLTerm.class).values()); - existTerms.add(result.getLeftSideHand()); - existTerms.addAll(result.getRightSideHand().getSubTerms(RDLTerm.class).values()); - existTerms.add(result.getRightSideHand()); + proofGraph.put(result, relation); + SemanticEquivalenceRelation linear = result.linearRightNormalized(); + assumptions.get(linear.getOrder()).add(linear); + if (!linear.equals(result)) { + proofGraph.put(linear, result); + } + apperTerms.addAll(linear.getLeftSideHand().getSubTerms(EvaluatableTerm.class).values()); + apperTerms.add(linear.getLeftSideHand()); + apperTerms.addAll(linear.getRightSideHand().getSubTerms(EvaluatableTerm.class).values()); + apperTerms.add(linear.getRightSideHand()); } } - + return apperTerms; } - } diff --git a/src/inference/equivalence/SemanticEquivalenceRelation.java b/src/inference/equivalence/SemanticEquivalenceRelation.java index 2a15bf9..3dcc5d0 100644 --- a/src/inference/equivalence/SemanticEquivalenceRelation.java +++ b/src/inference/equivalence/SemanticEquivalenceRelation.java @@ -2,16 +2,16 @@ import lombok.Getter; import models.formulas.EquationFormula; -import models.terms.RDLTerm; +import models.terms.EvaluatableTerm; @Getter public class SemanticEquivalenceRelation { - private RDLTerm leftSideHand; - private RDLTerm rightSideHand; + private EvaluatableTerm leftSideHand; + private EvaluatableTerm rightSideHand; private int order; - public SemanticEquivalenceRelation(RDLTerm lsh, RDLTerm rsh, int order) { + public SemanticEquivalenceRelation(EvaluatableTerm lsh, EvaluatableTerm rsh, int order) { leftSideHand = lsh; rightSideHand = rsh; this.order = order; @@ -22,7 +22,11 @@ rightSideHand = formula.getRightSideHand(); this.order = order; } - + + public SemanticEquivalenceRelation linearRightNormalized() { + return new SemanticEquivalenceRelation(leftSideHand.linearRightNormalize(), rightSideHand.linearRightNormalize(), order); + } + @Override public String toString() { diff --git a/src/models/formulas/EquationFormula.java b/src/models/formulas/EquationFormula.java index e12dc46..4ed83f6 100644 --- a/src/models/formulas/EquationFormula.java +++ b/src/models/formulas/EquationFormula.java @@ -14,6 +14,10 @@ this.rightSideHand = rightTerm; } + public EquationFormula linearRightNormalized() { + return new EquationFormula(leftSideHand.linearRightNormalize(), rightSideHand.linearRightNormalize()); + } + @Override public String toString() {