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 db3985d..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; @@ -112,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/equivalence/MetaSemanticEquivalenceRelation.java b/src/inference/equivalence/MetaSemanticEquivalenceRelation.java new file mode 100644 index 0000000..f1c9342 --- /dev/null +++ b/src/inference/equivalence/MetaSemanticEquivalenceRelation.java @@ -0,0 +1,164 @@ +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.SubstituteFailedException; +import lombok.Getter; +import models.algebra.Expression; +import models.algebra.Variable; +import models.terms.RDLTerm; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaVariable; +import models.terms.meta.OrderVariableConstraint; +import utils.Permutation; + +@Getter +public class MetaSemanticEquivalenceRelation { + + private MetaRDLTerm leftSideHand; + private MetaRDLTerm rightSideHand; + private Expression order; + + public MetaSemanticEquivalenceRelation(MetaRDLTerm lsh, MetaRDLTerm rsh, Expression order) { + leftSideHand = lsh; + rightSideHand = rsh; + this.order = order; + } + + 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(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(order)) { + return null; + } + int order = orderConstraint.get(this.order).getOrder(); + if (order == -1) { + return null; + } + + 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(leftSideHand.substitute(binding), rightSideHand.substitute(binding), order)); + for (int i = 0; i < leftVariables.size(); i++) { + binding.remove(leftVariables.get(i)); + } + } + try { + result.add(new SemanticEquivalenceRelation(leftSideHand.substitute(binding), rightSideHand.substitute(binding), order)); + } 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(order)) { + return null; + } + int order = orderConstraint.get(this.order).getOrder(); + if (order == -1) { + return null; + } + + 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(leftSideHand.substitute(binding), rightSideHand.substitute(binding), order)); + for (int i = 0; i < leftVariables.size(); i++) { + binding.remove(leftVariables.get(i)); + } + } + try { + result.add(new SemanticEquivalenceRelation(leftSideHand.substitute(binding), rightSideHand.substitute(binding), order)); + } 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..7bccd5d --- /dev/null +++ b/src/inference/equivalence/SemanticEquivalenceProofSystem.java @@ -0,0 +1,68 @@ +package inference.equivalence; + +import java.util.ArrayList; +import java.util.Collection; +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.terms.LinearRightNormalizedType; +import models.terms.RDLTerm; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaResourceVariable; + +public class SemanticEquivalenceProofSystem { + + private Map> assumptions; + private SemanticEquivalenceRelation conclusion; + 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"))) + ); + + public SemanticEquivalenceProofSystem(Collection assumptions, SemanticEquivalenceRelation conclusion) { + for(SemanticEquivalenceRelation assumption : assumptions) { + maxOrder = Math.max(maxOrder, assumption.getOrder()); + if (! this.assumptions.containsKey(assumption.getOrder())) { + this.assumptions.put(assumption.getOrder(), new ArrayList<>()); + } + } + this.conclusion = conclusion; + } + + public boolean proof() { + Set existTerms = new HashSet<>(); + for(int key : assumptions.keySet()) { + for(SemanticEquivalenceRelation relation : assumptions.get(key)) { + existTerms.addAll(relation.getLeftSideHand().getSubTerms(RDLTerm.class).values()); + existTerms.add(relation.getLeftSideHand()); + existTerms.addAll(relation.getRightSideHand().getSubTerms(RDLTerm.class).values()); + existTerms.add(relation.getRightSideHand()); + } + } + for (int i = maxOrder; i > 0; i--) { + + } + return false; + } + +} diff --git a/src/inference/equivalence/SemanticEquivalenceRelation.java b/src/inference/equivalence/SemanticEquivalenceRelation.java new file mode 100644 index 0000000..f21698a --- /dev/null +++ b/src/inference/equivalence/SemanticEquivalenceRelation.java @@ -0,0 +1,38 @@ +package inference.equivalence; + +import lombok.Getter; +import models.terms.RDLTerm; + +@Getter +public class SemanticEquivalenceRelation { + + private RDLTerm leftSideHand; + private RDLTerm rightSideHand; + private int order; + + public SemanticEquivalenceRelation(RDLTerm lsh, RDLTerm rsh, int order) { + leftSideHand = lsh; + rightSideHand = rsh; + this.order = 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/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 1d170a1..efb0d65 100644 --- a/src/models/terms/meta/MetaRDLTerm.java +++ b/src/models/terms/meta/MetaRDLTerm.java @@ -1,9 +1,11 @@ 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; @@ -19,7 +21,7 @@ public class MetaRDLTerm extends RDLTerm { protected TermType termType; - protected LinearRightNormalizedType linearRightNormalizedType; + protected LinearRightNormalizedType linearRightNormalizedType = LinearRightNormalizedType.UNDEFINED; protected MetaRDLTerm(Symbol symbol, TermType termType) { super(symbol, -1); @@ -143,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; @@ -206,6 +237,10 @@ this.linearRightNormalizedType = next; } + public Collection getAllVariables() { + return getSubTerms(MetaVariable.class).values(); + } + protected boolean islinearRightNormalizedMatchedBy(RDLTerm another) { if (linearRightNormalizedType != LinearRightNormalizedType.UNDEFINED) { if (another instanceof DependencyTerm) { diff --git a/src/models/terms/meta/MetaVariable.java b/src/models/terms/meta/MetaVariable.java index e9bc690..e3c9595 100644 --- a/src/models/terms/meta/MetaVariable.java +++ b/src/models/terms/meta/MetaVariable.java @@ -5,6 +5,7 @@ import exceptions.CoefficientNotOneException; import exceptions.NonLinearExpressionException; +import exceptions.SubstituteFailedException; import exceptions.TooManyVariablesException; import lombok.Getter; import models.algebra.Constant; @@ -13,6 +14,7 @@ import models.algebra.Term; import models.algebra.Variable; import models.dataConstraintModel.DataConstraintModel; +import models.terms.LinearRightNormalizedType; import models.terms.RDLTerm; @Getter @@ -45,6 +47,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 = 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() { @@ -72,6 +97,14 @@ } 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) { diff --git a/src/models/terms/meta/OrderVariableConstraint.java b/src/models/terms/meta/OrderVariableConstraint.java index d997e0d..00ab2cd 100644 --- a/src/models/terms/meta/OrderVariableConstraint.java +++ b/src/models/terms/meta/OrderVariableConstraint.java @@ -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); diff --git a/src/tests/equivalence/SubstituteTest.java b/src/tests/equivalence/SubstituteTest.java new file mode 100644 index 0000000..27eed7e --- /dev/null +++ b/src/tests/equivalence/SubstituteTest.java @@ -0,0 +1,43 @@ +package tests.equivalence; + +import java.util.List; + +import org.junit.jupiter.api.Test; + +import inference.equivalence.MetaSemanticEquivalenceRelation; +import models.algebra.Variable; +import models.terms.DependencyTerm; +import models.terms.LinearRightNormalizedType; +import models.terms.ResourceVariable; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaResourceVariable; +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); + } + } + +} 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/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); + } + } + } + +}