diff --git a/src/main/java/inference/equivalence/MetaSemanticEquivalenceRelation.java b/src/main/java/inference/equivalence/MetaSemanticEquivalenceRelation.java index 6c73c1d..961716d 100644 --- a/src/main/java/inference/equivalence/MetaSemanticEquivalenceRelation.java +++ b/src/main/java/inference/equivalence/MetaSemanticEquivalenceRelation.java @@ -1,237 +1,217 @@ package inference.equivalence; -import java.util.ArrayList; -import java.util.Collection; -import java.util.HashMap; -import java.util.HashSet; -import java.util.List; -import java.util.Map; -import java.util.Set; - -import exceptions.CoefficientNotOneException; -import exceptions.SubstituteFailedException; -import exceptions.TooManyVariablesException; 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; -import models.terms.meta.OrderVariableConstraint; -import utils.ExpressionUitls; -import utils.Permutation; @Getter public class MetaSemanticEquivalenceRelation { - private MetaRDLTerm leftSideHand; - private MetaRDLTerm rightSideHand; - private Expression order; - private Variable orderVariable; - private int orderConstant = 0; - - public MetaSemanticEquivalenceRelation(MetaRDLTerm lsh, MetaRDLTerm rsh, Expression order) { - leftSideHand = lsh; - rightSideHand = rsh; - this.order = order; - Map coefficients = new HashMap<>(); - orderConstant = ExpressionUitls.getCoefficientAndConstantsFromExpression(order, coefficients, 1); - if (coefficients.size() > 1) { - // todo: create exception - throw new TooManyVariablesException("Too many variables"); - } - if (coefficients.size() == 1) { - orderVariable = coefficients.keySet().iterator().next(); - if (coefficients.get(orderVariable) != 1) { - throw new CoefficientNotOneException(); - } - } else { - orderVariable = null; - } - } - - public boolean isMatchedBy(SemanticEquivalenceRelation relation) { - Map binding = new HashMap<>(); - Map orderConstraint = new HashMap<>(); - return isMatchedBy(relation, binding, orderConstraint); - } - - public boolean isMatchedBy(SemanticEquivalenceRelation relation, Map binding, Map orderConstraint) { - return leftSideHand.isMatchedBy(relation.getLeftSideHand(), binding, orderConstraint) - && rightSideHand.isMatchedBy(relation.getRightSideHand(), binding, orderConstraint); - } - - public Set substitute(Map binding, Map orderConstraint, Collection existedTerms) { - Set result = new HashSet<>(); - Map allVariables = new HashMap<>(); - for(MetaVariable variable : leftSideHand.getAllVariables()) { - allVariables.put(variable.getVariableName(), variable); - } - for(MetaVariable variable : rightSideHand.getAllVariables()) { - allVariables.put(variable.getVariableName(), variable); - } - for (Variable variable : binding.keySet()) { - allVariables.remove(variable); - } - List leftVariables = new ArrayList<>(allVariables.keySet()); - for(List useTerms: Permutation.permutation(existedTerms, leftVariables.size())) { - Map tempBinding = new HashMap<>(); - tempBinding.putAll(binding); - boolean flg = false; - for (int i = 0; i < leftVariables.size(); i++) { - if (!allVariables.get(leftVariables.get(i)).isMatchedBy(useTerms.get(i))) { - flg = true; - break; - } - tempBinding.put(leftVariables.get(i), useTerms.get(i)); - } - if (flg) { - continue; - } - 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()); - } - if (leftSideHand.isMatchedBy(leftTerm, binding, tempOrderConstraint) && rightSideHand.isMatchedBy(rightTerm, binding, tempOrderConstraint)) { - if (! tempOrderConstraint.containsKey(orderVariable)) { - continue; - } - int order = tempOrderConstraint.get(this.orderVariable).getOrder(); - if (order == -1) { - continue; - } - order += orderConstant; - result.add(new SemanticEquivalenceRelation(leftTerm, rightTerm, order)); - } - for(Variable variable: leftVariables) { - binding.remove(variable); - } - } - return result; - } - - public Set substitute(RDLTerm term, Collection existedTerms) { - Set result = new HashSet<>(); - Set leftSub = leftSubstitute(term, existedTerms); - if (leftSub != null) { - result.addAll(leftSub); - } - - Set rightSub = rightSubstitute(term, existedTerms); - if (rightSub != null) { - result.addAll(rightSub); - } - return result; - } - - private Set leftSubstitute(RDLTerm term, Collection existedTerms) { - Set result = new HashSet<>(); - Map binding = new HashMap<>(); - Map orderConstraint = new HashMap<>(); - if (! leftSideHand.isMatchedBy(term, binding, orderConstraint)) { - return null; - } - if (! orderConstraint.containsKey(orderVariable)) { - return null; - } - int order = orderConstraint.get(this.orderVariable).getOrder(); - if (order == -1) { - return null; - } - order += orderConstant; - - Set allVariables = new HashSet<>(rightSideHand.getVariables().values()); - allVariables.removeAll(binding.keySet()); - List leftVariables = new ArrayList<>(allVariables); - for (List useVariables: Permutation.permutation(existedTerms, leftVariables.size())) { - Map tempBinding = new HashMap<>(); - tempBinding.putAll(binding); - for (int i = 0; i < leftVariables.size(); i++) { - tempBinding.put(leftVariables.get(i), useVariables.get(i)); - } - RDLTerm tempTerm = rightSideHand.substitute(tempBinding); - if (! rightSideHand.isMatchedBy(tempTerm, binding, orderConstraint)) { - continue; - } - 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((EvaluatableTerm)leftSideHand.substitute(binding), (EvaluatableTerm)rightSideHand.substitute(binding), order)); - } catch (SubstituteFailedException e){} - return result; - } - - private Set rightSubstitute(RDLTerm term, Collection existedTerms) { - Set result = new HashSet<>(); - Map binding = new HashMap<>(); - Map orderConstraint = new HashMap<>(); - if (! rightSideHand.isMatchedBy(term, binding, orderConstraint)) { - return null; - }; - if (! orderConstraint.containsKey(orderVariable)) { - return null; - } - int order = orderConstraint.get(this.orderVariable).getOrder(); - if (order == -1) { - return null; - } - order += orderConstant; - - Set allVariables = new HashSet<>(); - for (MetaVariable vari : leftSideHand.getAllVariables()) { - allVariables.add(vari.getVariableName()); - } - allVariables.removeAll(binding.keySet()); - List leftVariables = new ArrayList<>(allVariables); - for (List useVariables: Permutation.permutation(existedTerms, leftVariables.size())) { - Map tempBinding = new HashMap<>(); - tempBinding.putAll(binding); - for (int i = 0; i < leftVariables.size(); i++) { - tempBinding.put(leftVariables.get(i), useVariables.get(i)); - } - RDLTerm tempTerm = leftSideHand.substitute(tempBinding); - if (! leftSideHand.isMatchedBy(tempTerm, binding, orderConstraint)) { - for (int i = 0; i < leftVariables.size(); i++) { - binding.remove(leftVariables.get(i)); - } - continue; - } - 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((EvaluatableTerm)leftSideHand.substitute(binding), (EvaluatableTerm)rightSideHand.substitute(binding), order)); - } catch (SubstituteFailedException e){} - return result; - - } - - - @Override - public String toString() { - return leftSideHand.toString() + " ===(" + order + ") " + rightSideHand.toString(); - } - - @Override - public boolean equals(Object another) { - if (! (another instanceof SemanticEquivalenceRelation)) { - return false; - } - SemanticEquivalenceRelation relation = (SemanticEquivalenceRelation) another; - return leftSideHand.equals(relation.getLeftSideHand()) && rightSideHand.equals(relation.getRightSideHand()); - } - - @Override - public int hashCode() { - return toString().hashCode(); - } +// private MetaRDLTerm leftSideHand; +// private MetaRDLTerm rightSideHand; +// private Expression order; +// private Variable orderVariable; +// private int orderConstant = 0; +// +// public MetaSemanticEquivalenceRelation(MetaRDLTerm lsh, MetaRDLTerm rsh, Expression order) { +// leftSideHand = lsh; +// rightSideHand = rsh; +// this.order = order; +// Map coefficients = new HashMap<>(); +// orderConstant = ExpressionUitls.getCoefficientAndConstantsFromExpression(order, coefficients, 1); +// if (coefficients.size() > 1) { +// // todo: create exception +// throw new TooManyVariablesException("Too many variables"); +// } +// if (coefficients.size() == 1) { +// orderVariable = coefficients.keySet().iterator().next(); +// if (coefficients.get(orderVariable) != 1) { +// throw new CoefficientNotOneException(); +// } +// } else { +// orderVariable = null; +// } +// } +// +// public boolean isMatchedBy(SemanticEquivalenceRelation relation) { +// Map binding = new HashMap<>(); +// Map orderConstraint = new HashMap<>(); +// return isMatchedBy(relation, binding, orderConstraint); +// } +// +// public boolean isMatchedBy(SemanticEquivalenceRelation relation, Map binding, Map orderConstraint) { +// return leftSideHand.isMatchedBy(relation.getLeftSideHand(), binding, orderConstraint) +// && rightSideHand.isMatchedBy(relation.getRightSideHand(), binding, orderConstraint); +// } +// +// public Set substitute(Map binding, Map orderConstraint, Collection existedTerms) { +// Set result = new HashSet<>(); +// Map allVariables = new HashMap<>(); +// for(MetaVariable variable : leftSideHand.getAllVariables()) { +// allVariables.put(variable.getVariableName(), variable); +// } +// for(MetaVariable variable : rightSideHand.getAllVariables()) { +// allVariables.put(variable.getVariableName(), variable); +// } +// for (Variable variable : binding.keySet()) { +// allVariables.remove(variable); +// } +// List leftVariables = new ArrayList<>(allVariables.keySet()); +// for(List useTerms: Permutation.permutation(existedTerms, leftVariables.size())) { +// Map tempBinding = new HashMap<>(); +// tempBinding.putAll(binding); +// boolean flg = false; +// for (int i = 0; i < leftVariables.size(); i++) { +// if (!allVariables.get(leftVariables.get(i)).isMatchedBy(useTerms.get(i))) { +// flg = true; +// break; +// } +// tempBinding.put(leftVariables.get(i), useTerms.get(i)); +// } +// if (flg) { +// continue; +// } +// 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()); +// } +// if (leftSideHand.isMatchedBy(leftTerm, binding, tempOrderConstraint) && rightSideHand.isMatchedBy(rightTerm, binding, tempOrderConstraint)) { +// if (! tempOrderConstraint.containsKey(orderVariable)) { +// continue; +// } +// int order = tempOrderConstraint.get(this.orderVariable).getOrder(); +// if (order == -1) { +// continue; +// } +// order += orderConstant; +// result.add(new SemanticEquivalenceRelation(leftTerm, rightTerm, order)); +// } +// for(Variable variable: leftVariables) { +// binding.remove(variable); +// } +// } +// return result; +// } +// +// public Set substitute(RDLTerm term, Collection existedTerms) { +// Set result = new HashSet<>(); +// Set leftSub = leftSubstitute(term, existedTerms); +// if (leftSub != null) { +// result.addAll(leftSub); +// } +// +// Set rightSub = rightSubstitute(term, existedTerms); +// if (rightSub != null) { +// result.addAll(rightSub); +// } +// return result; +// } +// +// private Set leftSubstitute(RDLTerm term, Collection existedTerms) { +// Set result = new HashSet<>(); +// Map binding = new HashMap<>(); +// Map orderConstraint = new HashMap<>(); +// if (! leftSideHand.isMatchedBy(term, binding, orderConstraint)) { +// return null; +// } +// if (! orderConstraint.containsKey(orderVariable)) { +// return null; +// } +// int order = orderConstraint.get(this.orderVariable).getOrder(); +// if (order == -1) { +// return null; +// } +// order += orderConstant; +// +// Set allVariables = new HashSet<>(rightSideHand.getVariables().values()); +// allVariables.removeAll(binding.keySet()); +// List leftVariables = new ArrayList<>(allVariables); +// for (List useVariables: Permutation.permutation(existedTerms, leftVariables.size())) { +// Map tempBinding = new HashMap<>(); +// tempBinding.putAll(binding); +// for (int i = 0; i < leftVariables.size(); i++) { +// tempBinding.put(leftVariables.get(i), useVariables.get(i)); +// } +// RDLTerm tempTerm = rightSideHand.substitute(tempBinding); +// if (! rightSideHand.isMatchedBy(tempTerm, binding, orderConstraint)) { +// continue; +// } +// 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((EvaluatableTerm)leftSideHand.substitute(binding), (EvaluatableTerm)rightSideHand.substitute(binding), order)); +// } catch (SubstituteFailedException e){} +// return result; +// } +// +// private Set rightSubstitute(RDLTerm term, Collection existedTerms) { +// Set result = new HashSet<>(); +// Map binding = new HashMap<>(); +// Map orderConstraint = new HashMap<>(); +// if (! rightSideHand.isMatchedBy(term, binding, orderConstraint)) { +// return null; +// }; +// if (! orderConstraint.containsKey(orderVariable)) { +// return null; +// } +// int order = orderConstraint.get(this.orderVariable).getOrder(); +// if (order == -1) { +// return null; +// } +// order += orderConstant; +// +// Set allVariables = new HashSet<>(); +// for (MetaVariable vari : leftSideHand.getAllVariables()) { +// allVariables.add(vari.getVariableName()); +// } +// allVariables.removeAll(binding.keySet()); +// List leftVariables = new ArrayList<>(allVariables); +// for (List useVariables: Permutation.permutation(existedTerms, leftVariables.size())) { +// Map tempBinding = new HashMap<>(); +// tempBinding.putAll(binding); +// for (int i = 0; i < leftVariables.size(); i++) { +// tempBinding.put(leftVariables.get(i), useVariables.get(i)); +// } +// RDLTerm tempTerm = leftSideHand.substitute(tempBinding); +// if (! leftSideHand.isMatchedBy(tempTerm, binding, orderConstraint)) { +// for (int i = 0; i < leftVariables.size(); i++) { +// binding.remove(leftVariables.get(i)); +// } +// continue; +// } +// 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((EvaluatableTerm)leftSideHand.substitute(binding), (EvaluatableTerm)rightSideHand.substitute(binding), order)); +// } catch (SubstituteFailedException e){} +// return result; +// +// } +// +// +// @Override +// public String toString() { +// return leftSideHand.toString() + " ===(" + order + ") " + rightSideHand.toString(); +// } +// +// @Override +// public boolean equals(Object another) { +// if (! (another instanceof SemanticEquivalenceRelation)) { +// return false; +// } +// SemanticEquivalenceRelation relation = (SemanticEquivalenceRelation) another; +// return leftSideHand.equals(relation.getLeftSideHand()) && rightSideHand.equals(relation.getRightSideHand()); +// } +// +// @Override +// public int hashCode() { +// return toString().hashCode(); +// } } diff --git a/src/main/java/inference/equivalence/SemanticEquivalenceProofSystem.java b/src/main/java/inference/equivalence/SemanticEquivalenceProofSystem.java index 876aad4..a44057d 100644 --- a/src/main/java/inference/equivalence/SemanticEquivalenceProofSystem.java +++ b/src/main/java/inference/equivalence/SemanticEquivalenceProofSystem.java @@ -1,153 +1,130 @@ package inference.equivalence; -import java.util.ArrayList; -import java.util.Collection; -import java.util.Collections; -import java.util.HashMap; -import java.util.HashSet; -import java.util.List; -import java.util.Map; -import java.util.Set; - -import models.algebra.Constant; -import models.algebra.Term; -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; -import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaResource; -import models.terms.meta.OrderConstraint; -import models.terms.meta.OrderVariableConstraint; - public class SemanticEquivalenceProofSystem { - private Map> assumptions; - private EquationFormula conclusion; - private Map proofGraph = new HashMap<>(); - int maxOrder = -1; - - private static MetaSemanticEquivalenceRelation rule1 = new MetaSemanticEquivalenceRelation( - new MetaRDLTerm( - new MetaResource(new Variable("v"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))), - new MetaResource(new Variable("v"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))), - new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n"), LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED) - ), - new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n"), LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED), - new Variable("n") - ); - - private static MetaSemanticEquivalenceRelation rule4_1 = new MetaSemanticEquivalenceRelation( - new MetaEvaluatableTermVariable(new Variable("t"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1"))), LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED), - new MetaEvaluatableTermVariable(new Variable("t'"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1"))), LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED), - new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1"))) - ); - - private static MetaSemanticEquivalenceRelation rule4_2 = new MetaSemanticEquivalenceRelation( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("t"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))), - new MetaResource(new Variable("v"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))), - new MetaEvaluatableTermVariable(new Variable("s"), OrderConstraint.LT, new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))) - ), - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("t'"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))), - new MetaResource(new Variable("v"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))), - new MetaEvaluatableTermVariable(new Variable("s"), OrderConstraint.LT, new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))) - ), - new Variable("n") - ); - - public SemanticEquivalenceProofSystem(Collection assumptions, EquationFormula conclusion) { - this.assumptions = new HashMap<>(); - for(SemanticEquivalenceRelation assumption : assumptions) { - maxOrder = Math.max(maxOrder, assumption.getOrder()); - if (! this.assumptions.containsKey(assumption.getOrder())) { - this.assumptions.put(assumption.getOrder(), new HashSet<>()); - } - this.assumptions.get(assumption.getOrder()).add(assumption.linearRightNormalized()); - this.conclusion = conclusion; - } - } - - public boolean proof() { - Set existTerms = new HashSet<>(); - 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(EvaluatableTerm.class).values()); - existTerms.add(relation.getLeftSideHand()); - existTerms.addAll(relation.getRightSideHand().getSubTerms(EvaluatableTerm.class).values()); - existTerms.add(relation.getRightSideHand()); - } - } - - - for (int i = maxOrder; i > linearRightNormalizedConclusion.getLeftSideHand().getOrder(); i--) { - Set apperTerms = new HashSet<>(); - for (SemanticEquivalenceRelation relation : assumptions.get(i)) { - apperTerms.addAll(applyRule4(relation, existTerms)); - } - existTerms.addAll(apperTerms); - } - - - List proofResult = new ArrayList<>(); - SemanticEquivalenceRelation currentRelation = conclusionRelation; - while(proofGraph.containsKey(currentRelation)) { - proofResult.add(currentRelation); - currentRelation = proofGraph.get(currentRelation); - } - 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() { - - } - - public static void debug() { - System.out.println(rule4_1); - System.out.println(rule4_2); - } - - private Set applyRule4(SemanticEquivalenceRelation relation, Set existTerms) { - Map binding = new HashMap<>(); - Map orderConstraint = new HashMap<>(); - Set appearTerms = 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 HashSet<>()); - } - proofGraph.put(result, relation); - SemanticEquivalenceRelation linear = result.linearRightNormalized(); - assumptions.get(linear.getOrder()).add(linear); - if (!linear.equals(result)) { - proofGraph.put(linear, result); - } - appearTerms.addAll(linear.getLeftSideHand().getSubTerms(EvaluatableTerm.class).values()); - appearTerms.add(linear.getLeftSideHand()); - appearTerms.addAll(linear.getRightSideHand().getSubTerms(EvaluatableTerm.class).values()); - appearTerms.add(linear.getRightSideHand()); - } - } - return appearTerms; - } +// private Map> assumptions; +// private EquationFormula conclusion; +// private Map proofGraph = new HashMap<>(); +// int maxOrder = -1; +// +// private static MetaSemanticEquivalenceRelation rule1 = new MetaSemanticEquivalenceRelation( +// new MetaRDLTerm( +// new MetaResource(new Variable("v"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))), +// new MetaResource(new Variable("v"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))), +// new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n"), LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED) +// ), +// new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n"), LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED), +// new Variable("n") +// ); +// +// private static MetaSemanticEquivalenceRelation rule4_1 = new MetaSemanticEquivalenceRelation( +// new MetaEvaluatableTermVariable(new Variable("t"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1"))), LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED), +// new MetaEvaluatableTermVariable(new Variable("t'"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1"))), LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED), +// new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1"))) +// ); +// +// private static MetaSemanticEquivalenceRelation rule4_2 = new MetaSemanticEquivalenceRelation( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("t"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))), +// new MetaResource(new Variable("v"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))), +// new MetaEvaluatableTermVariable(new Variable("s"), OrderConstraint.LT, new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))) +// ), +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("t'"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))), +// new MetaResource(new Variable("v"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))), +// new MetaEvaluatableTermVariable(new Variable("s"), OrderConstraint.LT, new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))) +// ), +// new Variable("n") +// ); +// +// public SemanticEquivalenceProofSystem(Collection assumptions, EquationFormula conclusion) { +// this.assumptions = new HashMap<>(); +// for(SemanticEquivalenceRelation assumption : assumptions) { +// maxOrder = Math.max(maxOrder, assumption.getOrder()); +// if (! this.assumptions.containsKey(assumption.getOrder())) { +// this.assumptions.put(assumption.getOrder(), new HashSet<>()); +// } +// this.assumptions.get(assumption.getOrder()).add(assumption.linearRightNormalized()); +// this.conclusion = conclusion; +// } +// } +// +// public boolean proof() { +// Set existTerms = new HashSet<>(); +// 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(EvaluatableTerm.class).values()); +// existTerms.add(relation.getLeftSideHand()); +// existTerms.addAll(relation.getRightSideHand().getSubTerms(EvaluatableTerm.class).values()); +// existTerms.add(relation.getRightSideHand()); +// } +// } +// +// +// for (int i = maxOrder; i > linearRightNormalizedConclusion.getLeftSideHand().getOrder(); i--) { +// Set apperTerms = new HashSet<>(); +// for (SemanticEquivalenceRelation relation : assumptions.get(i)) { +// apperTerms.addAll(applyRule4(relation, existTerms)); +// } +// existTerms.addAll(apperTerms); +// } +// +// +// List proofResult = new ArrayList<>(); +// SemanticEquivalenceRelation currentRelation = conclusionRelation; +// while(proofGraph.containsKey(currentRelation)) { +// proofResult.add(currentRelation); +// currentRelation = proofGraph.get(currentRelation); +// } +// 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() { +// +// } +// +// public static void debug() { +// System.out.println(rule4_1); +// System.out.println(rule4_2); +// } +// +// private Set applyRule4(SemanticEquivalenceRelation relation, Set existTerms) { +// Map binding = new HashMap<>(); +// Map orderConstraint = new HashMap<>(); +// Set appearTerms = 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 HashSet<>()); +// } +// proofGraph.put(result, relation); +// SemanticEquivalenceRelation linear = result.linearRightNormalized(); +// assumptions.get(linear.getOrder()).add(linear); +// if (!linear.equals(result)) { +// proofGraph.put(linear, result); +// } +// appearTerms.addAll(linear.getLeftSideHand().getSubTerms(EvaluatableTerm.class).values()); +// appearTerms.add(linear.getLeftSideHand()); +// appearTerms.addAll(linear.getRightSideHand().getSubTerms(EvaluatableTerm.class).values()); +// appearTerms.add(linear.getRightSideHand()); +// } +// } +// return appearTerms; +// } }