diff --git a/src/inference/equivalence/MetaSemanticEquivalenceRelation.java b/src/inference/equivalence/MetaSemanticEquivalenceRelation.java index f1c9342..05941ee 100644 --- a/src/inference/equivalence/MetaSemanticEquivalenceRelation.java +++ b/src/inference/equivalence/MetaSemanticEquivalenceRelation.java @@ -8,7 +8,9 @@ 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; @@ -16,6 +18,7 @@ import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaVariable; import models.terms.meta.OrderVariableConstraint; +import utils.ExpressionUitls; import utils.Permutation; @Getter @@ -24,11 +27,27 @@ 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) { @@ -42,6 +61,47 @@ && rightSideHand.isMatchedBy(relation.getRightSideHand(), binding, orderConstraint); } + public Set substitute(Map binding, Map orderConstraint, Collection existedTerms) { + Set result = new HashSet<>(); + Set allVariables = new HashSet<>(); + for(MetaVariable variable : leftSideHand.getAllVariables()) { + allVariables.add(variable.getVariableName()); + } + for(MetaVariable variable : rightSideHand.getAllVariables()) { + allVariables.add(variable.getVariableName()); + } + allVariables.removeAll(binding.keySet()); + List leftVariables = new ArrayList<>(allVariables); + for(List useTerms: 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), useTerms.get(i)); + } + RDLTerm leftTerm = leftSideHand.substitute(tempBinding); + RDLTerm rightTerm = 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); @@ -63,13 +123,14 @@ if (! leftSideHand.isMatchedBy(term, binding, orderConstraint)) { return null; } - if (! orderConstraint.containsKey(order)) { + if (! orderConstraint.containsKey(orderVariable)) { return null; } - int order = orderConstraint.get(this.order).getOrder(); + 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()); @@ -102,13 +163,14 @@ if (! rightSideHand.isMatchedBy(term, binding, orderConstraint)) { return null; }; - if (! orderConstraint.containsKey(order)) { + if (! orderConstraint.containsKey(orderVariable)) { return null; } - int order = orderConstraint.get(this.order).getOrder(); + int order = orderConstraint.get(this.orderVariable).getOrder(); if (order == -1) { return null; } + order += orderConstant; Set allVariables = new HashSet<>(); for (MetaVariable vari : leftSideHand.getAllVariables()) { diff --git a/src/inference/equivalence/SemanticEquivalenceProofSystem.java b/src/inference/equivalence/SemanticEquivalenceProofSystem.java index 7bccd5d..7c1d04a 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.HashMap; import java.util.HashSet; import java.util.List; import java.util.Map; @@ -16,6 +17,8 @@ import models.terms.meta.MetaEvaluatableTermVariable; import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaResourceVariable; +import models.terms.meta.OrderConstraint; +import models.terms.meta.OrderVariableConstraint; public class SemanticEquivalenceProofSystem { @@ -39,6 +42,20 @@ 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 MetaResourceVariable(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 MetaResourceVariable(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, SemanticEquivalenceRelation conclusion) { for(SemanticEquivalenceRelation assumption : assumptions) { maxOrder = Math.max(maxOrder, assumption.getOrder()); @@ -60,9 +77,35 @@ } } for (int i = maxOrder; i > 0; i--) { - + for (SemanticEquivalenceRelation relation : assumptions.get(i)) { + applyRule4(relation, existTerms); + } } + System.out.println(assumptions); return false; } + private void applyRule1() { + + } + + private void applyRule4(SemanticEquivalenceRelation relation, Set existTerms) { + Map binding = new HashMap<>(); + Map orderConstraint = new HashMap<>(); + 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.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()); + } + } + + } + } diff --git a/src/models/terms/meta/MetaVariable.java b/src/models/terms/meta/MetaVariable.java index e3c9595..ed96b12 100644 --- a/src/models/terms/meta/MetaVariable.java +++ b/src/models/terms/meta/MetaVariable.java @@ -4,18 +4,15 @@ import java.util.Map; import exceptions.CoefficientNotOneException; -import exceptions.NonLinearExpressionException; import exceptions.SubstituteFailedException; import exceptions.TooManyVariablesException; import lombok.Getter; -import models.algebra.Constant; import models.algebra.Expression; import models.algebra.Symbol; -import models.algebra.Term; import models.algebra.Variable; -import models.dataConstraintModel.DataConstraintModel; import models.terms.LinearRightNormalizedType; import models.terms.RDLTerm; +import utils.ExpressionUitls; @Getter public abstract class MetaVariable extends MetaRDLTerm { @@ -32,7 +29,7 @@ this.constraint = constraint; this.orderExpression = order; Map coefficients = new HashMap<>(); - int constant = getCoefficientAndConstantsFromExpression(order, coefficients, 1); + int constant = ExpressionUitls.getCoefficientAndConstantsFromExpression(order, coefficients, 1); if (coefficients.size() > 1) { // todo: create exception throw new TooManyVariablesException("Too many variables"); @@ -54,7 +51,7 @@ this.constraint = constraint; this.orderExpression = order; Map coefficients = new HashMap<>(); - int constant = getCoefficientAndConstantsFromExpression(order, coefficients, 1); + int constant = ExpressionUitls.getCoefficientAndConstantsFromExpression(order, coefficients, 1); if (coefficients.size() > 1) { // todo: create exception throw new TooManyVariablesException("Too many variables"); @@ -132,60 +129,7 @@ return false; } - private int getCoefficientAndConstantsFromExpression(Expression expression, Map coefficients, int curWeight) { - int res = 0; - if(expression instanceof Constant) { - return getConstantValue((Constant) expression) * curWeight; - } else if(expression instanceof Variable) { - coefficients.put((Variable) expression, coefficients.getOrDefault((Variable) expression, 0) + curWeight); - return 0; - } - Term term = (Term) expression; - Symbol symbol = term.getSymbol(); - if(symbol.equals(DataConstraintModel.add)) { - Expression c1 = term.getChild(0); - Expression c2 = term.getChild(1); - res += getCoefficientAndConstantsFromExpression(c1, coefficients, curWeight); - res += getCoefficientAndConstantsFromExpression(c2, coefficients, curWeight); - } else if(symbol.equals(DataConstraintModel.sub)) { - Expression c1 = term.getChild(0); - Expression c2 = term.getChild(1); - res += getCoefficientAndConstantsFromExpression(c1, coefficients, curWeight); - res += getCoefficientAndConstantsFromExpression(c2, coefficients, -curWeight); - } else if(symbol.equals(DataConstraintModel.mul)) { - Expression c1 = term.getChild(0); - Expression c2 = term.getChild(1); - if(c1.getVariables().size() == 0 && c2.getVariables().size() == 0) { - res += getCoefficientAndConstantsFromExpression(c1, coefficients, curWeight) * - getCoefficientAndConstantsFromExpression(c2, coefficients, curWeight); - } else if(c1.getVariables().size() == 0) { - res += getCoefficientAndConstantsFromExpression( - c2, - coefficients, - getCoefficientAndConstantsFromExpression(c1, coefficients, curWeight) - ); - } else if(c2.getVariables().size() == 0){ - res += getCoefficientAndConstantsFromExpression( - c1, - coefficients, - getCoefficientAndConstantsFromExpression(c2, coefficients, curWeight) - ); - } else { - throw new NonLinearExpressionException("Order expression must be linear expression."); - } - } else if(symbol.equals(DataConstraintModel.minus)) { - Expression c1 = term.getChild(0); - res += getCoefficientAndConstantsFromExpression(c1, coefficients, -curWeight); - } else { - throw new NonLinearExpressionException("Order expression must be linear expression."); - } - return res; - - } - private int getConstantValue(Constant constant) { - return Integer.parseInt((String) constant.getValue()); - } @Override diff --git a/src/models/terms/meta/OrderVariableConstraint.java b/src/models/terms/meta/OrderVariableConstraint.java index 00ab2cd..7a80c79 100644 --- a/src/models/terms/meta/OrderVariableConstraint.java +++ b/src/models/terms/meta/OrderVariableConstraint.java @@ -5,7 +5,7 @@ @NoArgsConstructor @Getter -public class OrderVariableConstraint { +public class OrderVariableConstraint implements Cloneable{ // lower <= x <= upper private int upper = 100000000; @@ -59,4 +59,13 @@ return false; } + @Override + public Object clone() { + OrderVariableConstraint constraint = new OrderVariableConstraint(); + constraint.isOk = isOk; + constraint.lower = lower; + constraint.upper = upper; + return constraint; + } + } diff --git a/src/tests/equivalence/SubstituteTest.java b/src/tests/equivalence/SubstituteTest.java index 27eed7e..2eac027 100644 --- a/src/tests/equivalence/SubstituteTest.java +++ b/src/tests/equivalence/SubstituteTest.java @@ -1,17 +1,23 @@ package tests.equivalence; +import java.util.HashMap; import java.util.List; +import java.util.Map; import org.junit.jupiter.api.Test; import inference.equivalence.MetaSemanticEquivalenceRelation; +import inference.equivalence.SemanticEquivalenceRelation; import models.algebra.Variable; import models.terms.DependencyTerm; import models.terms.LinearRightNormalizedType; +import models.terms.RDLTerm; import models.terms.ResourceVariable; import models.terms.meta.MetaEvaluatableTermVariable; import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaResourceVariable; +import models.terms.meta.OrderConstraint; +import models.terms.meta.OrderVariableConstraint; import tests.Utils; public class SubstituteTest { @@ -40,4 +46,33 @@ } } + @Test + void SubstituteTest2() { + MetaEvaluatableTermVariable t = new MetaEvaluatableTermVariable(new Variable("t"), Utils.parse("n + 1")); + t.setLinearRightNormalizedType(LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED); + MetaEvaluatableTermVariable tp = new MetaEvaluatableTermVariable(new Variable("t'"), Utils.parse("n + 1")); + tp.setLinearRightNormalizedType(LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED); + MetaSemanticEquivalenceRelation r1 = new MetaSemanticEquivalenceRelation(t, tp, Utils.parse("n + 1")); + DependencyTerm t1 = new DependencyTerm(A, B, C); + DependencyTerm t2 = new DependencyTerm(Ap, Bp, Cp); + SemanticEquivalenceRelation r2 = new SemanticEquivalenceRelation(t1, t2, 2); + MetaResourceVariable v = new MetaResourceVariable(new Variable("v"), Utils.parse("n + 1")); + MetaEvaluatableTermVariable s = new MetaEvaluatableTermVariable(new Variable("s"), OrderConstraint.LT, Utils.parse("n + 1")); + MetaSemanticEquivalenceRelation r3 = new MetaSemanticEquivalenceRelation( + new MetaRDLTerm(t, v, s), + new MetaRDLTerm(tp, v, s), + Utils.parse("n") + ); + + Map binding = new HashMap<>(); + Map orderConstraint = new HashMap<>(); + r1.isMatchedBy(r2, binding, orderConstraint); + var tmp = r3.substitute(binding, orderConstraint, List.of(D, E, F, G)); + System.out.println(); + System.out.println(binding); + for(var a : tmp) { + System.out.println(a); + } + } + } diff --git a/src/utils/ExpressionUitls.java b/src/utils/ExpressionUitls.java new file mode 100644 index 0000000..7981932 --- /dev/null +++ b/src/utils/ExpressionUitls.java @@ -0,0 +1,71 @@ +package utils; + +import java.util.Map; + +import exceptions.NonLinearExpressionException; +import models.algebra.Constant; +import models.algebra.Expression; +import models.algebra.Symbol; +import models.algebra.Term; +import models.algebra.Variable; +import models.dataConstraintModel.DataConstraintModel; + +public class ExpressionUitls { + + + public static int getCoefficientAndConstantsFromExpression(Expression expression, Map coefficients, int curWeight) { + int res = 0; + if(expression instanceof Constant) { + return getConstantValue((Constant) expression) * curWeight; + } else if(expression instanceof Variable) { + coefficients.put((Variable) expression, coefficients.getOrDefault((Variable) expression, 0) + curWeight); + return 0; + } + Term term = (Term) expression; + Symbol symbol = term.getSymbol(); + if(symbol.equals(DataConstraintModel.add)) { + Expression c1 = term.getChild(0); + Expression c2 = term.getChild(1); + res += getCoefficientAndConstantsFromExpression(c1, coefficients, curWeight); + res += getCoefficientAndConstantsFromExpression(c2, coefficients, curWeight); + } else if(symbol.equals(DataConstraintModel.sub)) { + Expression c1 = term.getChild(0); + Expression c2 = term.getChild(1); + res += getCoefficientAndConstantsFromExpression(c1, coefficients, curWeight); + res += getCoefficientAndConstantsFromExpression(c2, coefficients, -curWeight); + } else if(symbol.equals(DataConstraintModel.mul)) { + Expression c1 = term.getChild(0); + Expression c2 = term.getChild(1); + if(c1.getVariables().size() == 0 && c2.getVariables().size() == 0) { + res += getCoefficientAndConstantsFromExpression(c1, coefficients, curWeight) * + getCoefficientAndConstantsFromExpression(c2, coefficients, curWeight); + } else if(c1.getVariables().size() == 0) { + res += getCoefficientAndConstantsFromExpression( + c2, + coefficients, + getCoefficientAndConstantsFromExpression(c1, coefficients, curWeight) + ); + } else if(c2.getVariables().size() == 0){ + res += getCoefficientAndConstantsFromExpression( + c1, + coefficients, + getCoefficientAndConstantsFromExpression(c2, coefficients, curWeight) + ); + } else { + throw new NonLinearExpressionException("Order expression must be linear expression."); + } + } else if(symbol.equals(DataConstraintModel.minus)) { + Expression c1 = term.getChild(0); + res += getCoefficientAndConstantsFromExpression(c1, coefficients, -curWeight); + } else { + throw new NonLinearExpressionException("Order expression must be linear expression."); + } + return res; + + } + + public static int getConstantValue(Constant constant) { + return Integer.parseInt((String) constant.getValue()); + } + +}