diff --git a/src/Main.java b/src/Main.java index 053d306..85f114c 100644 --- a/src/Main.java +++ b/src/Main.java @@ -1,21 +1,18 @@ -import java.util.ArrayList; import java.util.List; -import inference.ProofSystem; +import inference.equivalence.SemanticEquivalenceProofSystem; +import inference.equivalence.SemanticEquivalenceRelation; import lombok.SneakyThrows; import models.algebra.Expression; import models.algebra.Type; import models.dataConstraintModel.DataConstraintModel; import models.dataFlowModel.DataTransferModel; -import models.formulas.DependencyFormula; import models.formulas.EquationFormula; -import models.formulas.Formula; -import models.terms.Dependency; import models.terms.DependencyTerm; -import models.terms.EvaluatableTerm; import models.terms.ResourceVariable; import parser.Parser; import parser.Parser.TokenStream; +import tests.Utils; public class Main { @@ -27,45 +24,55 @@ public static void main(String[] args) { - List initialConditions = new ArrayList<>(); - ResourceVariable A = new ResourceVariable("A", INT, 2); - ResourceVariable B = new ResourceVariable("B", INT, 2); - ResourceVariable C = new ResourceVariable("C", INT, 2); - ResourceVariable D = new ResourceVariable("D", INT, 2); - ResourceVariable E = new ResourceVariable("E", INT, 1); - ResourceVariable F = new ResourceVariable("F", INT, 1); - ResourceVariable G = new ResourceVariable("G", INT, 0); - - ResourceVariable Ap = new ResourceVariable("A'", INT, 2); - ResourceVariable Bp = new ResourceVariable("B'", INT, 2); - ResourceVariable Cp = new ResourceVariable("C'", INT, 2); - ResourceVariable Dp = new ResourceVariable("D'", INT, 2); - ResourceVariable Fp = new ResourceVariable("F'", INT, 1); - - initialConditions.add(new DependencyFormula(new Dependency(new Dependency(A, B), D), F)); - initialConditions.add(new DependencyFormula(new Dependency(new Dependency(Ap, Bp), Dp), Fp)); - initialConditions.add(new EquationFormula(new DependencyTerm(A, B, C), new DependencyTerm(Ap, Bp, Cp))); - EquationFormula conclusion = new EquationFormula( - 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) + 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(Ap, Bp, Cp); + EquationFormula assumptionFormula = new EquationFormula(t1, t2); + EquationFormula conclusionFormula = new EquationFormula( + 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) ); - for(var cond : initialConditions) { - System.out.println(cond.toString()); - } - System.out.println(conclusion.toString()); - ProofSystem.check(initialConditions, conclusion); - System.out.println("======================="); - EvaluatableTerm lrn = conclusion.getLeftSideHand().linearRightNormalize(); - var subTerms = lrn.getSubTerms(EvaluatableTerm.class); - System.out.println(conclusion.getLeftSideHand().linearRightNormalize().toString()); - for(var sub: subTerms.keySet()) { - System.out.println(sub.getOrders().toString()); - System.out.println(subTerms.get(sub).toString()); - } - System.out.println("=================="); - System.out.println(conclusion.getRightSideHand().linearRightNormalize().toString()); + + SemanticEquivalenceProofSystem proofSystem = new SemanticEquivalenceProofSystem( + List.of(new SemanticEquivalenceRelation(assumptionFormula, 2)), + conclusionFormula + ); + +// 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); + } + + + @SneakyThrows static Expression parse(String expr) { stream.addLine(expr); diff --git a/src/exceptions/SubstituteFailedException.java b/src/exceptions/SubstituteFailedException.java new file mode 100644 index 0000000..de4a0e2 --- /dev/null +++ b/src/exceptions/SubstituteFailedException.java @@ -0,0 +1,13 @@ +package exceptions; + +public class SubstituteFailedException extends RuntimeException { + + public SubstituteFailedException(String msg) { + super(msg); + } + + public SubstituteFailedException() { + super("substitute failed"); + } + +} diff --git a/src/inference/InferenceRule.java b/src/inference/InferenceRule.java index e99e7c4..c10c5d1 100644 --- a/src/inference/InferenceRule.java +++ b/src/inference/InferenceRule.java @@ -1,6 +1,5 @@ package inference; -import java.util.ArrayList; import java.util.Collection; import java.util.HashMap; import java.util.HashSet; @@ -53,15 +52,46 @@ } public boolean check(Collection assumptions, Formula conclusion) { + if (this.assumptions.size() > assumptions.size()) { return false; } - for(List assumption : permutation(assumptions, this.assumptions.size())) { - if (check(assumption, conclusion)) { - return true; + + Map binding = new HashMap<>(); + Map orderConstraints = new HashMap<>(); + this.conclusion.isMatchedBy(conclusion, binding, orderConstraints); + Set givenAssumptions = new HashSet<>(assumptions); + + for (MetaFormula assumption : this.assumptions) { + boolean flg = false; + for (Formula given : givenAssumptions) { + Map tmpBinding = new HashMap<>(binding); + Map tmpOrderConstraints = new HashMap<>(orderConstraints); + if (assumption.isMatchedBy(given, tmpBinding, tmpOrderConstraints)) { + binding.putAll(tmpBinding); + orderConstraints.putAll(tmpOrderConstraints); + flg = true; + givenAssumptions.remove(given); + break; + } + } + if (!flg) { + return false; } } - return false; + + if (this.defaultOrderConstraint != null) { + return defaultOrderConstraint.check(orderConstraints); + } + + return true; + +// for(List assumption : permutation(assumptions, this.assumptions.size())) { +// if (check(assumption, conclusion)) { +// return true; +// } +// } +// return false; } private boolean check(List assumptions, Formula conclusion) { @@ -81,28 +111,6 @@ return true; } - private List> permutation(Collection list, int n) { - List> res = new ArrayList<>(); - permutation(list, n, new ArrayList<>(), new HashSet<>(), res); - return res; - } - - private void permutation(Collection all, int n, List current, Set used, List> result) { - if (current.size() == n) { - result.add(new ArrayList<>(current)); - return; - } - for (T elem : all) { - if (! used.contains(elem)) { - current.add(elem); - used.add(elem); - permutation(all, n, current, used, result); - current.remove(current.size() - 1); - used.remove(elem); - } - } - } - public String toString() { StringBuilder sb = new StringBuilder(); diff --git a/src/inference/ProofSystem.java b/src/inference/ProofSystem.java index 887d4cb..e652591 100644 --- a/src/inference/ProofSystem.java +++ b/src/inference/ProofSystem.java @@ -1,12 +1,24 @@ package inference; +import java.util.ArrayDeque; +import java.util.ArrayList; import java.util.Collection; +import java.util.Deque; +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.Variable; +import models.formulas.EquationFormula; import models.formulas.Formula; import models.formulas.meta.MetaDependencyFormula; import models.formulas.meta.MetaEquationFormula; +import models.formulas.meta.MetaInFormula; +import models.terms.EvaluatableTerm; +import models.terms.meta.MetaDependencyVariable; import models.terms.meta.MetaEvaluatableTermVariable; import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaResourceVariable; @@ -14,14 +26,14 @@ public class ProofSystem { - private final static InferenceRule REFLEXIVE_LAW = new InferenceRule("relfexive law", List.of(), + public final static InferenceRule REFLEXIVE_LAW = new InferenceRule("relfexive law", List.of(), new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaEvaluatableTermVariable(new Variable("te")))); - private final static InferenceRule SYMMETRIC_LAW = new InferenceRule("symmetric law", + public final static InferenceRule SYMMETRIC_LAW = new InferenceRule("symmetric law", List.of(new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaEvaluatableTermVariable(new Variable("se")))), new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("te")))); - private final static InferenceRule TRANSITIVE_LAW = new InferenceRule("transitive law", + public final static InferenceRule TRANSITIVE_LAW = new InferenceRule("transitive law", List.of( new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("te"))), new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaEvaluatableTermVariable(new Variable("ue"))) @@ -29,12 +41,12 @@ new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("ue"))) ); - private final static InferenceRule IDENTITY_MAPPING = new InferenceRule("identity mapping", + public final static InferenceRule IDENTITY_MAPPING = new InferenceRule("identity mapping", List.of(new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("v")))), new MetaDependencyFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("v"))) ); - private final static InferenceRule COMPOSITE_MAPPING = new InferenceRule("composite mapping", + public final static InferenceRule COMPOSITE_MAPPING = new InferenceRule("composite mapping", List.of( new MetaDependencyFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("v"))), new MetaDependencyFormula(new MetaResourceVariable(new Variable("v")), new MetaResourceVariable(new Variable("w"))) @@ -42,7 +54,7 @@ new MetaDependencyFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("w"))) ); - private final static InferenceRule LEFT_PROJECTION = new InferenceRule("left projection", + public final static InferenceRule LEFT_PROJECTION = new InferenceRule("left projection", List.of(new MetaDependencyFormula( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), @@ -56,7 +68,7 @@ ) ); - private final static InferenceRule RIGHT_PROJECTION = new InferenceRule("left projection", + public final static InferenceRule RIGHT_PROJECTION = new InferenceRule("right projection", List.of(new MetaDependencyFormula( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), @@ -70,7 +82,7 @@ ) ); - private final static InferenceRule CONSTANT_MAPPING = new InferenceRule("constant mapping", + public final static InferenceRule CONSTANT_MAPPING = new InferenceRule("constant mapping", List.of(), new MetaDependencyFormula( new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), @@ -79,9 +91,13 @@ new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")) ); // 定値写像?? - private final static InferenceRule ORDER_DESCENTING = null; // 階数降下?? - - private final static InferenceRule RIGHT_REPLACEMENT = new InferenceRule("right replacement", + public final static InferenceRule ORDER_DESCENTING = new InferenceRule("order descenting", + List.of(new MetaDependencyFormula(new MetaDependencyVariable(new Variable("d"), new Variable("n")))), + new MetaDependencyFormula(new MetaRDLTerm(new MetaDependencyVariable(new Variable("d"), new Variable("n")))), + new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) + ); // 階数降下?? + + public final static InferenceRule RIGHT_REPLACEMENT = new InferenceRule("right replacement", List.of(new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaEvaluatableTermVariable(new Variable("ue")))), new MetaEquationFormula( new MetaRDLTerm( @@ -97,9 +113,54 @@ ) ); - private final static InferenceRule IDENTITY_LAW = null; + public final static InferenceRule LEFT_REPLACEMENT = new InferenceRule("left replacement", + List.of(new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("ue")))), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("v")), + new MetaEvaluatableTermVariable(new Variable("te")) + ), + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("ue")), + new MetaResourceVariable(new Variable("v")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ) + ); - private final static InferenceRule JOIN = new InferenceRule("join", + public final static InferenceRule CENTER_REPLACEMENT = new InferenceRule("center replacement", + List.of(new MetaEquationFormula(new MetaResourceVariable(new Variable("v")), new MetaResourceVariable(new Variable("w")))), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("v")), + new MetaEvaluatableTermVariable(new Variable("te")) + ), + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("w")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ) + ); + + public final static InferenceRule IDENTITY_LAW = new InferenceRule("identity law", + List.of(new MetaInFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaRDLTerm(new MetaResourceVariable(new Variable("v")))) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaResourceVariable(new Variable("v")), + new MetaResourceVariable(new Variable("v")), + new MetaEvaluatableTermVariable(new Variable("te")) + ), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ); + + public final static InferenceRule JOIN = new InferenceRule("join", List.of(new MetaEquationFormula(new MetaResourceVariable(new Variable("v")), new MetaResourceVariable(new Variable("w")))), new MetaEquationFormula( new MetaRDLTerm( @@ -119,14 +180,160 @@ ) ); - private final static InferenceRule CONSTANT_VALUE_LAW = null;//定値性?? - private final static InferenceRule LINEAR_RIGHT_NORMALIZE = null; - private final static InferenceRule PSEUDO_IDENTITY_LAW = null;//疑似恒等性?? - private final static InferenceRule SET_EQUIVALENCE = null;//集合同値性?? - private final static InferenceRule HOMOMORPHISM = null;//準同型性?? + public final static InferenceRule CONSTANT_VALUE_LAW = new InferenceRule("constant value law", + List.of(new MetaInFormula( + new MetaEvaluatableTermVariable(new Variable("t")), + new MetaRDLTerm(new MetaResourceVariable(new Variable("v"), new Variable("m")))) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), + new MetaResourceVariable(new Variable("v"), new Variable("m")), + new MetaEvaluatableTermVariable(new Variable("t")) + ), + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) + ), + new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")) + );//定値性?? + + public final static InferenceRule RIGHT_NORMALIZE = new InferenceRule("right normalize", + List.of( + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaResourceVariable(new Variable("v"), new Variable("n")) + ), + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("w"), new Variable("n")) + ) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaResourceVariable(new Variable("v"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("se")) + ), + new MetaResourceVariable(new Variable("w"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ), + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaResourceVariable(new Variable("v"), new Variable("n")), + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("w"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ) + ) + ), + new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) + ); + + public final static InferenceRule PSEUDO_IDENTITY_LAW = new InferenceRule("pseudo identity law", + List.of( + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), + new MetaResourceVariable(new Variable("v"), new Variable("n")) + ) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), + new MetaResourceVariable(new Variable("v"), new Variable("n")), + new MetaResourceVariable(new Variable("v"), new Variable("n")) + ), + new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")) + ), + new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) + );//疑似恒等性?? + + public final static InferenceRule SET_EQUIVALENCE = new InferenceRule("set equivalence", + List.of(new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")) + )), + new MetaEquationFormula( + new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))), + new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))) + ), + new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) + );//集合同値性?? + + public final static InferenceRule HOMOMORPHISM = new InferenceRule("homomorphism", + List.of(new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("v")) + )), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("v")), + new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"))) + ), + new MetaRDLTerm( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaResourceVariable(new Variable("v")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ) + ) + );//準同型性?? public static boolean check(Collection assumptions, Formula conclusion) { + if (equationTransitionCheck(assumptions, conclusion)) { + return true; + } return false; } + private static boolean equationTransitionCheck(Collection assumptions, Formula conclusion) { + if (! (conclusion instanceof EquationFormula)) { + return false; + } + EquationFormula equationConclusion = (EquationFormula) conclusion; + Map> graph = constructEquationGraph(assumptions); + Deque que = new ArrayDeque<>(); + Set visited = new HashSet<>(); + que.add(equationConclusion.getLeftSideHand()); + while (! que.isEmpty()) { + EvaluatableTerm curNode = que.pollFirst(); + if (curNode.equals(equationConclusion.getRightSideHand())) { + return true; + } + for (EvaluatableTerm nextNode : graph.getOrDefault(curNode, new ArrayList<>())) { + if (visited.contains(nextNode)) { + continue; + } + visited.add(nextNode); + que.add(nextNode); + } + } + return false; + } + + private static Map> constructEquationGraph(Collection assumptions) { + List equations = new ArrayList<>(); + for (Formula assumption : assumptions) { + if (assumption instanceof EquationFormula) { + equations.add((EquationFormula) assumption); + } + } + + Map> graph = new HashMap<>(); + for (EquationFormula equation : equations) { + EvaluatableTerm lsh = equation.getLeftSideHand(); + EvaluatableTerm rsh = equation.getRightSideHand(); + if (! graph.containsKey(lsh)) { + graph.put(lsh, new ArrayList<>()); + } + if (! graph.containsKey(rsh)) { + graph.put(rsh, new ArrayList<>()); + } + graph.get(lsh).add(rsh); + graph.get(rsh).add(lsh); + } + return graph; + } } diff --git a/src/inference/equivalence/MetaSemanticEquivalenceRelation.java b/src/inference/equivalence/MetaSemanticEquivalenceRelation.java new file mode 100644 index 0000000..6c73c1d --- /dev/null +++ b/src/inference/equivalence/MetaSemanticEquivalenceRelation.java @@ -0,0 +1,237 @@ +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(); + } + +} diff --git a/src/inference/equivalence/SemanticEquivalenceProofSystem.java b/src/inference/equivalence/SemanticEquivalenceProofSystem.java new file mode 100644 index 0000000..a2e8aa6 --- /dev/null +++ b/src/inference/equivalence/SemanticEquivalenceProofSystem.java @@ -0,0 +1,148 @@ +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.MetaResourceVariable; +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 MetaResourceVariable(new Variable("v"), 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("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 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, 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() { + + } + + 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 HashSet<>()); + } + 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 new file mode 100644 index 0000000..3dcc5d0 --- /dev/null +++ b/src/inference/equivalence/SemanticEquivalenceRelation.java @@ -0,0 +1,49 @@ +package inference.equivalence; + +import lombok.Getter; +import models.formulas.EquationFormula; +import models.terms.EvaluatableTerm; + +@Getter +public class SemanticEquivalenceRelation { + + private EvaluatableTerm leftSideHand; + private EvaluatableTerm rightSideHand; + private int order; + + public SemanticEquivalenceRelation(EvaluatableTerm lsh, EvaluatableTerm rsh, int order) { + leftSideHand = lsh; + rightSideHand = rsh; + this.order = order; + } + + public SemanticEquivalenceRelation(EquationFormula formula, int order) { + leftSideHand = formula.getLeftSideHand(); + rightSideHand = formula.getRightSideHand(); + this.order = order; + } + + public SemanticEquivalenceRelation linearRightNormalized() { + return new SemanticEquivalenceRelation(leftSideHand.linearRightNormalize(), rightSideHand.linearRightNormalize(), order); + } + + + @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/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() { diff --git a/src/models/terms/DependencyTerm.java b/src/models/terms/DependencyTerm.java index d7be3ac..bef9d63 100644 --- a/src/models/terms/DependencyTerm.java +++ b/src/models/terms/DependencyTerm.java @@ -25,8 +25,8 @@ } @Override - public boolean isLinearRightNormal() { - return isLinearRightNormal(0); + public boolean isLinearRightNormalized() { + return isLinearRightNormaled(0); } @Override @@ -43,10 +43,10 @@ return; } DependencyTerm dependencyTerm = (DependencyTerm) dependingTerm; - if(! dependencyTerm.isLinearRightNormal()) { + if(! dependencyTerm.isLinearRightNormalized()) { dependencyTerm.selfLinearRightNormalize(); } - if(! isLinearRightNormal()) { + if(! isLinearRightNormalized()) { EvaluatableTerm childArgumentTerm = dependencyTerm.getArgumentTerm(); DependencyTerm nextDependencyTerm = new DependencyTerm(childArgumentTerm, dependedVariable, argumentTerm); this.dependingTerm = dependencyTerm.getDependingTerm(); @@ -60,13 +60,13 @@ } - private boolean isLinearRightNormal(int depth) { + private boolean isLinearRightNormaled(int depth) { if(dependingTerm instanceof ResourceVariable || dependingTerm instanceof SetEvaluatableTerm) { return dependingTerm.getOrder() == dependedVariable.getOrder(); } DependencyTerm dependencyTerm = (DependencyTerm) dependingTerm; if( - dependencyTerm.isLinearRightNormal(depth + 1) && + dependencyTerm.isLinearRightNormaled(depth + 1) && dependencyTerm.getDependedVariable().getOrder() - 1 == dependedVariable.getOrder() && dependencyTerm.getOrder() == dependedVariable.getOrder() && argumentTerm.getOrder() <= dependencyTerm.getOrder() && @@ -75,7 +75,7 @@ return true; } if( - dependencyTerm.isLinearRightNormal(depth + 1) && + dependencyTerm.isLinearRightNormaled(depth + 1) && dependencyTerm.getDependedVariable().getOrder() - 1 == dependedVariable.getOrder() && dependencyTerm.getOrder() == dependedVariable.getOrder() && argumentTerm.getOrder() < dependencyTerm.getOrder() diff --git a/src/models/terms/EvaluatableTerm.java b/src/models/terms/EvaluatableTerm.java index 624f6f6..d75d77b 100644 --- a/src/models/terms/EvaluatableTerm.java +++ b/src/models/terms/EvaluatableTerm.java @@ -10,7 +10,13 @@ super(symbol, order); } - public abstract boolean isLinearRightNormal(); + public abstract boolean isLinearRightNormalized(); + public LinearRightNormalizedType getLinearRightNormalizedType() { + if (isLinearRightNormalized()) { + return LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED; + } + return LinearRightNormalizedType.NOT_LINEAR_RIGHT_NORMALIZED; + } public abstract EvaluatableTerm linearRightNormalize(); public abstract void selfLinearRightNormalize(); diff --git a/src/models/terms/LinearRightNormalizedType.java b/src/models/terms/LinearRightNormalizedType.java new file mode 100644 index 0000000..e043c08 --- /dev/null +++ b/src/models/terms/LinearRightNormalizedType.java @@ -0,0 +1,9 @@ +package models.terms; + +public enum LinearRightNormalizedType { + + LINEAR_RIGHT_NORMALIZED, + NOT_LINEAR_RIGHT_NORMALIZED, + UNDEFINED + +} diff --git a/src/models/terms/ResourceConstant.java b/src/models/terms/ResourceConstant.java index 1cdddfd..a7c2d1b 100644 --- a/src/models/terms/ResourceConstant.java +++ b/src/models/terms/ResourceConstant.java @@ -23,7 +23,7 @@ } @Override - public boolean isLinearRightNormal() { + public boolean isLinearRightNormalized() { return true; } diff --git a/src/models/terms/ResourceVariable.java b/src/models/terms/ResourceVariable.java index 909da7e..819f362 100644 --- a/src/models/terms/ResourceVariable.java +++ b/src/models/terms/ResourceVariable.java @@ -26,7 +26,7 @@ } @Override - public boolean isLinearRightNormal() { + public boolean isLinearRightNormalized() { return true; } diff --git a/src/models/terms/SetEvaluatableTerm.java b/src/models/terms/SetEvaluatableTerm.java index 5a70374..5a9c1c9 100644 --- a/src/models/terms/SetEvaluatableTerm.java +++ b/src/models/terms/SetEvaluatableTerm.java @@ -41,8 +41,8 @@ } @Override - public boolean isLinearRightNormal() { - return term.isLinearRightNormal(); + public boolean isLinearRightNormalized() { + return term.isLinearRightNormalized(); } diff --git a/src/models/terms/meta/MetaDependencyTermVariable.java b/src/models/terms/meta/MetaDependencyTermVariable.java index 80b6902..fc23e3a 100644 --- a/src/models/terms/meta/MetaDependencyTermVariable.java +++ b/src/models/terms/meta/MetaDependencyTermVariable.java @@ -20,5 +20,5 @@ public MetaDependencyTermVariable(Variable variableName, Expression order) { super(new Symbol(":", 3), MetaRDLTerm.TermType.META_DEPENDENCY_TERM_VARIABLE, variableName, OrderConstraint.EQ, order); } - + } diff --git a/src/models/terms/meta/MetaEvaluatableTermVariable.java b/src/models/terms/meta/MetaEvaluatableTermVariable.java index b99aa8c..dd049b4 100644 --- a/src/models/terms/meta/MetaEvaluatableTermVariable.java +++ b/src/models/terms/meta/MetaEvaluatableTermVariable.java @@ -4,6 +4,7 @@ import models.algebra.Expression; import models.algebra.Symbol; import models.algebra.Variable; +import models.terms.LinearRightNormalizedType; public class MetaEvaluatableTermVariable extends MetaVariable { @@ -19,4 +20,16 @@ super(new Symbol(":", 2), MetaRDLTerm.TermType.META_EVALUATABLE_TERM_VARIABLE, variableName, OrderConstraint.EQ, order); } + public MetaEvaluatableTermVariable(Variable variableName, OrderConstraint constraint, Expression order, LinearRightNormalizedType linearRIghtNormalizedType) { + super(new Symbol(":", 2), MetaRDLTerm.TermType.META_EVALUATABLE_TERM_VARIABLE, variableName, constraint, order, linearRIghtNormalizedType); + } + + public MetaEvaluatableTermVariable(Variable variableName, LinearRightNormalizedType linearRIghtNormalizedType) { + super(new Symbol(":", 2), MetaRDLTerm.TermType.META_EVALUATABLE_TERM_VARIABLE, variableName, OrderConstraint.ANY, new Constant("0"), linearRIghtNormalizedType); + } + + public MetaEvaluatableTermVariable(Variable variableName, Expression order, LinearRightNormalizedType linearRIghtNormalizedType) { + super(new Symbol(":", 2), MetaRDLTerm.TermType.META_EVALUATABLE_TERM_VARIABLE, variableName, OrderConstraint.EQ, order, linearRIghtNormalizedType); + } + } diff --git a/src/models/terms/meta/MetaRDLTerm.java b/src/models/terms/meta/MetaRDLTerm.java index 6a78803..efb0d65 100644 --- a/src/models/terms/meta/MetaRDLTerm.java +++ b/src/models/terms/meta/MetaRDLTerm.java @@ -1,15 +1,18 @@ package models.terms.meta; +import java.util.Collection; import java.util.HashMap; import java.util.Map; import exceptions.IllegalTypeException; +import exceptions.SubstituteFailedException; import lombok.Getter; import models.algebra.Symbol; import models.algebra.Variable; import models.terms.Dependency; import models.terms.DependencyTerm; import models.terms.EvaluatableTerm; +import models.terms.LinearRightNormalizedType; import models.terms.RDLTerm; import models.terms.ResourceVariable; import models.terms.SetEvaluatableTerm; @@ -17,32 +20,15 @@ @Getter public class MetaRDLTerm extends RDLTerm { - protected static enum TermType { - META_RDL_TERM(RDLTerm.class), - META_DEPENDENCY(Dependency.class), - META_DEPENDENCY_LIST(Dependency.class), - META_DEPENDENCY_VARIABLE(Dependency.class), - META_DEPENDENCY_TERM(DependencyTerm.class), - META_DEPENDENCY_TERM_VARIABLE(DependencyTerm.class), - META_EVALUATABLE_TERM_VARIABLE(EvaluatableTerm.class), - META_EVALUATABLE_TERM_SET(SetEvaluatableTerm.class), - META_EVALUATABLE_TERM_SET_VARIABLE(SetEvaluatableTerm.class), - META_RESOURCE_VARIABLE(ResourceVariable.class); - - @Getter - private Class baseTermClass; - - private TermType(Class clazz) { - this.baseTermClass = clazz; - } - - } - protected TermType termType; + protected LinearRightNormalizedType linearRightNormalizedType = LinearRightNormalizedType.UNDEFINED; protected MetaRDLTerm(Symbol symbol, TermType termType) { super(symbol, -1); this.termType = termType; + if (isResourceVariable()) { + linearRightNormalizedType = LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED; + } } //dependency @@ -159,6 +145,35 @@ this.termType = TermType.META_DEPENDENCY_TERM; } + public RDLTerm substitute(Map binding) { + if (isDependency()) { + RDLTerm dependingTerm = (RDLTerm) getChild(0); + RDLTerm dependedVariable = (RDLTerm) getChild(1); + if (dependingTerm instanceof MetaRDLTerm) { + dependingTerm = ((MetaRDLTerm) dependingTerm).substitute(binding); + } + if (dependedVariable instanceof MetaRDLTerm) { + dependedVariable = ((MetaRDLTerm) dependedVariable).substitute(binding); + } + return new Dependency(dependingTerm, (ResourceVariable) dependedVariable); + } + if (isDependencyTerm()) { + RDLTerm dependingTerm = (RDLTerm) getChild(0); + RDLTerm dependedVariable = (RDLTerm) getChild(1); + RDLTerm argumentTerm = (RDLTerm) getChild(2); + if (dependingTerm instanceof MetaRDLTerm) { + dependingTerm = ((MetaRDLTerm) dependingTerm).substitute(binding); + } + if (dependedVariable instanceof MetaRDLTerm) { + dependedVariable = ((MetaRDLTerm) dependedVariable).substitute(binding); + } + if (argumentTerm instanceof MetaRDLTerm) { + argumentTerm = ((MetaRDLTerm) argumentTerm).substitute(binding); + } + return new DependencyTerm((EvaluatableTerm) dependingTerm, (ResourceVariable) dependedVariable, (EvaluatableTerm) argumentTerm); + } + throw new SubstituteFailedException(); + } public boolean isVariable() { return false; @@ -175,6 +190,9 @@ if (this.getChildren().size() != another.getChildren().size()) { return false; } + if (isDependencyTerm() && (! islinearRightNormalizedMatchedBy(another))) { + return false; + } for (int i = 0; i < this.getChildren().size(); i++) { RDLTerm child = (RDLTerm) this.getChild(i); RDLTerm anotherChild = (RDLTerm) another.getChild(i); @@ -212,6 +230,32 @@ return checkTermType(ResourceVariable.class); } + public void setLinearRightNormalizedType(LinearRightNormalizedType next) { + if (isDependency()) { + return; + } + this.linearRightNormalizedType = next; + } + + public Collection getAllVariables() { + return getSubTerms(MetaVariable.class).values(); + } + + protected boolean islinearRightNormalizedMatchedBy(RDLTerm another) { + if (linearRightNormalizedType != LinearRightNormalizedType.UNDEFINED) { + if (another instanceof DependencyTerm) { + if (((DependencyTerm) another).getLinearRightNormalizedType() != linearRightNormalizedType) { + return false; + } + } + else if (another instanceof MetaRDLTerm) { + if (((MetaRDLTerm) another).getLinearRightNormalizedType() != linearRightNormalizedType) { + return false; + } + } + } + return true; + } @Override public String toString() { @@ -262,4 +306,25 @@ return null; } + protected static enum TermType { + META_RDL_TERM(RDLTerm.class), + META_DEPENDENCY(Dependency.class), + META_DEPENDENCY_LIST(Dependency.class), + META_DEPENDENCY_VARIABLE(Dependency.class), + META_DEPENDENCY_TERM(DependencyTerm.class), + META_DEPENDENCY_TERM_VARIABLE(DependencyTerm.class), + META_EVALUATABLE_TERM_VARIABLE(EvaluatableTerm.class), + META_EVALUATABLE_TERM_SET(SetEvaluatableTerm.class), + META_EVALUATABLE_TERM_SET_VARIABLE(SetEvaluatableTerm.class), + META_RESOURCE_VARIABLE(ResourceVariable.class); + + @Getter + private Class baseTermClass; + + private TermType(Class clazz) { + this.baseTermClass = clazz; + } + + } + } diff --git a/src/models/terms/meta/MetaVariable.java b/src/models/terms/meta/MetaVariable.java index 3d44a2b..ed96b12 100644 --- a/src/models/terms/meta/MetaVariable.java +++ b/src/models/terms/meta/MetaVariable.java @@ -4,16 +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 { @@ -30,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"); @@ -45,6 +44,29 @@ } orderConstant = constant; } + + protected MetaVariable(Symbol symbol, TermType termType, Variable name, OrderConstraint constraint, Expression order, LinearRightNormalizedType linearRIghtNormalizedType) { + super(symbol, termType); + this.variableName = name; + this.constraint = constraint; + this.orderExpression = order; + Map coefficients = new HashMap<>(); + int constant = 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; + } + orderConstant = constant; + this.linearRightNormalizedType = linearRIghtNormalizedType; + } @Override public boolean isVariable() { @@ -62,12 +84,24 @@ return false; } + if (! islinearRightNormalizedMatchedBy(another)) { + return false; + } + if (! binding.containsKey(this.variableName)) { binding.put(this.variableName, another); return true; } return binding.get(this.variableName).equals(another); } + + @Override + public RDLTerm substitute(Map binding) { + if (binding.containsKey(variableName)) { + return binding.get(variableName); + } + throw new SubstituteFailedException(); + } private boolean orderConstraintCheck(RDLTerm another, Map orderConstraints) { if (orderVariable == null) { @@ -95,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 d997e0d..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; @@ -30,6 +30,12 @@ return false; } + public int getOrder() { + if (isOk) { + return lower; + } + return -1; + } private boolean setEq(int eq) { return setUpper(eq) && setLower(eq); @@ -53,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 new file mode 100644 index 0000000..2eac027 --- /dev/null +++ b/src/tests/equivalence/SubstituteTest.java @@ -0,0 +1,78 @@ +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 { + + 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); + + @Test + void SubstituteTest1() { + MetaResourceVariable v = new MetaResourceVariable(new Variable("v"), Utils.parse("n + 1")); + MetaEvaluatableTermVariable t = new MetaEvaluatableTermVariable(new Variable("t"), Utils.parse("n")); + t.setLinearRightNormalizedType(LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED); + MetaSemanticEquivalenceRelation r1 = new MetaSemanticEquivalenceRelation(new MetaRDLTerm(v, v, t), t, new Variable("n")); + DependencyTerm t1 = new DependencyTerm(A, A, E); + var tmp = r1.substitute(t1, List.of(Ap, Bp, C, Cp, D, E, F, G)); + for(var a : tmp) { + System.out.println(a); + } + } + + @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/tests/inferencerule/InferenceRuleTest.java b/src/tests/inferencerule/InferenceRuleTest.java index f1e89bb..7cb7b04 100644 --- a/src/tests/inferencerule/InferenceRuleTest.java +++ b/src/tests/inferencerule/InferenceRuleTest.java @@ -3,10 +3,10 @@ import static org.junit.jupiter.api.Assertions.*; import static tests.Utils.*; -import org.junit.jupiter.api.Test; - import java.util.List; +import org.junit.jupiter.api.Test; + import inference.InferenceRule; import models.algebra.Variable; import models.formulas.DependencyFormula; diff --git a/src/tests/terms/LinearRightNormalTest.java b/src/tests/terms/LinearRightNormalTest.java index c5e7846..27e464b 100644 --- a/src/tests/terms/LinearRightNormalTest.java +++ b/src/tests/terms/LinearRightNormalTest.java @@ -5,9 +5,14 @@ import org.junit.jupiter.api.Test; import models.algebra.Type; +import models.algebra.Variable; import models.dataConstraintModel.DataConstraintModel; import models.terms.EvaluatableTerm; +import models.terms.LinearRightNormalizedType; import models.terms.ResourceVariable; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaResourceVariable; public class LinearRightNormalTest { @@ -29,13 +34,13 @@ EvaluatableTerm te2 = EvaluatableTerm.of(c, d, te1); EvaluatableTerm te3 = EvaluatableTerm.of(a, b, te2); //[a:b->[c:d->[e:f->g]]] - assertEquals(te3.isLinearRightNormal(), true); + assertEquals(te3.isLinearRightNormalized(), true); EvaluatableTerm te4 = EvaluatableTerm.of(a, b, c); EvaluatableTerm te5 = EvaluatableTerm.of(te4, d, e); EvaluatableTerm te6 = EvaluatableTerm.of(te5, f, g); //[[[a:b->c]:d->e]:f->g] - assertEquals(te6.isLinearRightNormal(), false); + assertEquals(te6.isLinearRightNormalized(), false); } @Test @@ -53,9 +58,38 @@ EvaluatableTerm te2 = EvaluatableTerm.of(te1, d, e); EvaluatableTerm te3 = EvaluatableTerm.of(te2, f, g); - assertEquals(te3.isLinearRightNormal(), false); + assertEquals(te3.isLinearRightNormalized(), false); te3.selfLinearRightNormalize(); - assertEquals(te3.isLinearRightNormal(), true); + assertEquals(te3.isLinearRightNormalized(), true); + } + + @Test + void linearRightNomalizedMatchTest() { + ResourceVariable a = EvaluatableTerm.of("A", INT, 2); + ResourceVariable b = EvaluatableTerm.of("B", INT, 2); + ResourceVariable c = EvaluatableTerm.of("C", INT, 2); + ResourceVariable d = EvaluatableTerm.of("D", INT, 2); + ResourceVariable e = EvaluatableTerm.of("E", INT, 2); + ResourceVariable f = EvaluatableTerm.of("F", INT, 2); + ResourceVariable g = EvaluatableTerm.of("G", INT, 1); + + EvaluatableTerm te1 = EvaluatableTerm.of(a, b, c); + EvaluatableTerm te2 = EvaluatableTerm.of(te1, d, e); + EvaluatableTerm te3 = EvaluatableTerm.of(te2, f, g); + + MetaEvaluatableTermVariable metaTerm = new MetaEvaluatableTermVariable(new Variable("x")); + MetaResourceVariable metaA = new MetaResourceVariable(new Variable("ma")); + MetaResourceVariable metaB = new MetaResourceVariable(new Variable("mb")); + MetaResourceVariable metaC = new MetaResourceVariable(new Variable("mc")); + MetaRDLTerm metaTerm2 = new MetaRDLTerm(metaA, metaB, metaC); + metaTerm2.setLinearRightNormalizedType(LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED); + + + metaTerm.setLinearRightNormalizedType(LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED); + assertEquals(metaTerm.isMatchedBy(te3), false); + te3.selfLinearRightNormalize(); + assertEquals(metaTerm.isMatchedBy(te3), true); + assertEquals(metaTerm2.isMatchedBy(te1), true); } } diff --git a/src/tests/terms/meta/SubstituteTest.java b/src/tests/terms/meta/SubstituteTest.java new file mode 100644 index 0000000..613b36b --- /dev/null +++ b/src/tests/terms/meta/SubstituteTest.java @@ -0,0 +1,49 @@ +package tests.terms.meta; + +import static org.junit.jupiter.api.Assertions.*; + +import java.util.HashMap; +import java.util.Map; + +import org.junit.jupiter.api.Test; + +import models.algebra.Variable; +import models.terms.DependencyTerm; +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.OrderVariableConstraint; +import tests.Utils; + +public class SubstituteTest { + + @Test + void MetaDependencyTermSubstituteTest() { + MetaResourceVariable x = new MetaResourceVariable(new Variable("x")); + MetaResourceVariable y = new MetaResourceVariable(new Variable("y")); + MetaEvaluatableTermVariable z = new MetaEvaluatableTermVariable(new Variable("z")); + + + MetaRDLTerm metaTerm1 = new MetaRDLTerm(x, y, z); + + ResourceVariable a = new ResourceVariable("a", Utils.INT, 1); + ResourceVariable b = new ResourceVariable("b", Utils.INT, 1); + ResourceVariable c = new ResourceVariable("c", Utils.INT, 1); + + DependencyTerm t1 = new DependencyTerm(a, b, c); + DependencyTerm t2 = new DependencyTerm(a, b, t1); + + Map binding = new HashMap<>(); + Map orderConstraint = new HashMap<>(); + metaTerm1.isMatchedBy(t1, binding, orderConstraint); + RDLTerm assignedTerm = metaTerm1.substitute(binding); + assertEquals(t1, assignedTerm); + binding.clear(); + orderConstraint.clear(); + metaTerm1.isMatchedBy(t2, binding, orderConstraint); + assertEquals(t2, metaTerm1.substitute(binding)); + } + +} diff --git a/src/tests/utils/DynamicDSUTest.java b/src/tests/utils/DynamicDSUTest.java new file mode 100644 index 0000000..fe15816 --- /dev/null +++ b/src/tests/utils/DynamicDSUTest.java @@ -0,0 +1,25 @@ +package tests.utils; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.jupiter.api.Test; + +import utils.DynamicDisjointSetUnion; + +public class DynamicDSUTest { + + @Test + void DDSUTest() { + DynamicDisjointSetUnion dsu = new DynamicDisjointSetUnion<>(); + dsu.add("a"); + dsu.add("b"); + dsu.add("c"); + dsu.union("a", "b"); + assertTrue(dsu.same("a", "b")); + assertFalse(dsu.same("a", "c")); + assertFalse(dsu.same("b", "c")); + + + } + +} diff --git a/src/utils/DynamicDisjointSetUnion.java b/src/utils/DynamicDisjointSetUnion.java new file mode 100644 index 0000000..06cc58e --- /dev/null +++ b/src/utils/DynamicDisjointSetUnion.java @@ -0,0 +1,66 @@ +package utils; + +import java.util.HashMap; +import java.util.Map; + +public class DynamicDisjointSetUnion { + + private Map parent; + private Map size; + + public DynamicDisjointSetUnion() { + parent = new HashMap<>(); + size = new HashMap<>(); + } + + public void add(T x) { + if (! parent.containsKey(x)) { + parent.put(x, x); + size.put(x, 1); + } + } + + public T find(T x) { + if (! parent.containsKey(x)) { + throw new RuntimeException(x.toString() + " does not exist"); + } + + if (! parent.get(x).equals(x)) { + parent.put(x, find(parent.get(x))); + } + return parent.get(x); + } + + public void union(T x, T y) { + add(x); + add(y); + + T rx = find(x); + T ry = find(y); + + if (rx.equals(ry)) { + return; + } + + if (size.get(rx) < size.get(ry)) { + T tmp = rx; + rx = ry; + ry = tmp; + } + + parent.put(ry, rx); + size.put(rx, size.get(rx) + size.get(ry)); + } + + public boolean same(T x, T y) { + if ((! parent.containsKey(x)) || (! parent.containsKey(y))) { + return false; + } + return find(x).equals(find(y)); + } + + public int componentSize(T x) { + return size.get(x); + } + +} 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()); + } + +} diff --git a/src/utils/Permutation.java b/src/utils/Permutation.java new file mode 100644 index 0000000..039b9f9 --- /dev/null +++ b/src/utils/Permutation.java @@ -0,0 +1,33 @@ +package utils; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.HashSet; +import java.util.List; +import java.util.Set; + +public class Permutation { + + public static List> permutation(Collection list, int n) { + List> res = new ArrayList<>(); + permutation(list, n, new ArrayList<>(), new HashSet<>(), res); + return res; + } + + private static void permutation(Collection all, int n, List current, Set used, List> result) { + if (current.size() == n) { + result.add(new ArrayList<>(current)); + return; + } + for (T elem : all) { + if (! used.contains(elem)) { + current.add(elem); + used.add(elem); + permutation(all, n, current, used, result); + current.remove(current.size() - 1); + used.remove(elem); + } + } + } + +}