diff --git a/src/main/java/Main.java b/src/main/java/Main.java index 14ca9f9..1738ff9 100644 --- a/src/main/java/Main.java +++ b/src/main/java/Main.java @@ -281,10 +281,11 @@ // RewriteInferenceSystem ris = new RewriteInferenceSystem(List.of(), List.of(), List.of(eq3, eq4, eq5, eq6, eq7, eq8, eq9, eq10, eq11, eq12, eq13, eq14), eq15); //value copy new sales - RewriteInferenceSystem ris = new RewriteInferenceSystem(List.of(eq3, eq4, eq5, eq6, eq7, eq8), eq15); +// RewriteInferenceSystem ris = new RewriteInferenceSystem(List.of(eq3, eq4, eq5, eq6, eq7, eq8), eq15); //value copy change value -// RewriteInferenceSystem ris = new RewriteInferenceSystem(List.of(eq9, eq10, eq11, eq12, eq13, eq14), eq15); + RewriteInferenceSystem ris = new RewriteInferenceSystem(List.of(eq9, eq10, eq11, eq12, eq13, eq14), eq15); + ris.debug(); ris.inference(); // System.out.println("~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~"); @@ -306,7 +307,7 @@ //reference change value RewriteInferenceSystem ris2 = new RewriteInferenceSystem(List.of(eq1, eq2, eq9, eq10, eq11, eq12, eq13), th1); -// ris2.debug(); + ris2.debug(); ris2.inference(); } diff --git a/src/main/java/exceptions/SyntaxException.java b/src/main/java/exceptions/SyntaxException.java new file mode 100644 index 0000000..c93db96 --- /dev/null +++ b/src/main/java/exceptions/SyntaxException.java @@ -0,0 +1,13 @@ +package exceptions; + +public class SyntaxException extends RuntimeException{ + + public SyntaxException() { + super("syntax error"); + } + + public SyntaxException(String msg) { + super(msg); + } + +} diff --git a/src/main/java/inference/InferenceRule.java b/src/main/java/inference/InferenceRule.java index 1a3243b..ca3b6e7 100644 --- a/src/main/java/inference/InferenceRule.java +++ b/src/main/java/inference/InferenceRule.java @@ -1,21 +1,18 @@ package inference; 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.Variable; import models.formulas.Formula; import models.formulas.meta.MetaDependencyFormula; import models.formulas.meta.MetaEquationFormula; import models.formulas.meta.MetaFormula; import models.terms.RDLTerm; -import models.terms.meta.OrderVariableConstraint; +import models.terms.meta.MatchConstraint; import utils.Permutation; public class InferenceRule { @@ -63,19 +60,14 @@ return false; } - Map binding = new HashMap<>(); - Map orderConstraints = new HashMap<>(); - this.conclusion.isMatchedBy(conclusion, binding, orderConstraints); + Set matchResult = this.conclusion.isMatchedBy(conclusion); 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); + matchResult = assumption.isMatchedBy(given, matchResult); + if (! matchResult.isEmpty()) { flg = true; givenAssumptions.remove(given); break; @@ -87,7 +79,12 @@ } if (this.defaultOrderConstraint != null) { - return defaultOrderConstraint.check(orderConstraints); + for (MatchConstraint constraint: matchResult) { + if (defaultOrderConstraint.check(constraint.getOrderConstraint())) { + return true; + } + } + return false; } return true; @@ -101,18 +98,24 @@ } private boolean check(List assumptions, Formula conclusion) { - Map binding = new HashMap<>(); - Map orderConstraints = new HashMap<>(); - for (int i = 0; i < assumptions.size(); i++) { - if (! this.assumptions.get(i).isMatchedBy(assumptions.get(i), binding, orderConstraints)) { + Set matchResult = this.assumptions.get(0).isMatchedBy(assumptions.get(0)); + for (int i = 1; i < assumptions.size(); i++) { + matchResult = this.assumptions.get(i).isMatchedBy(assumptions.get(i), matchResult); + if (matchResult.isEmpty()) { return false; } } - if (! this.conclusion.isMatchedBy(conclusion, binding, orderConstraints)) { + + if (this.conclusion.isMatchedBy(conclusion, matchResult).isEmpty()) { return false; } if (this.defaultOrderConstraint != null) { - return defaultOrderConstraint.check(orderConstraints); + for (MatchConstraint constraint: matchResult) { + if (defaultOrderConstraint.check(constraint.getOrderConstraint())) { + return true; + } + } + return false; } return true; } @@ -122,14 +125,14 @@ if (assumptions.size() != getAssumptionSize()) { return null; } - Map binding = new HashMap<>(); - Map orderConstraint = new HashMap<>(); + Set result = this.assumptions.get(0).isMatchedBy(assumptions.get(0)); for (int i = 0; i < getAssumptionSize(); i++) { - if (! this.assumptions.get(i).isMatchedBy(assumptions.get(i), binding, orderConstraint)) { + result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result); + if (result.isEmpty()) { return null; } } - return conclusion.substitution(binding); + return conclusion.substitution(result.iterator().next().getBinding()); } public Set apply(List assumptions, Set existTerms) { @@ -137,43 +140,37 @@ if (assumptions.size() != getAssumptionSize()) { return null; } - Map binding = new HashMap<>(); - Map orderConstraint = new HashMap<>(); + Set res = this.assumptions.get(0).isMatchedBy(assumptions.get(0)); for (int i = 0; i < getAssumptionSize(); i++) { - if (! this.assumptions.get(i).isMatchedBy(assumptions.get(i), binding, orderConstraint)) { + res = this.assumptions.get(i).isMatchedBy(assumptions.get(i), res); + if (res.isEmpty()) { return result; } } - try { - result.add(conclusion.substitution(binding)); - } catch (SubstituteFailedException e) { - + for (MatchConstraint constraint : res) { + try { + result.add(conclusion.substitution(constraint.getBinding())); + } catch (SubstituteFailedException e) {} } for (RDLTerm term : existTerms) { - Map localBinding = new HashMap<>(binding); - Map localOrderConstraint = new HashMap<>(orderConstraint); - if (conclusion instanceof MetaEquationFormula) { - MetaEquationFormula equation = (MetaEquationFormula) conclusion; - if (equation.getLeftSideHand().isMatchedBy(term, localBinding, localOrderConstraint)) { - result.add(conclusion.substitution(localBinding)); - } + Set localConstraints = new HashSet<>(res.stream().map(v -> new MatchConstraint(v)).toList()); + if (conclusion instanceof MetaEquationFormula equation) { + localConstraints= equation.getLeftSideHand().isMatchedBy(term, localConstraints); } - else if (conclusion instanceof MetaDependencyFormula) { - MetaDependencyFormula dependency = (MetaDependencyFormula) conclusion; - if (dependency.getDependency().isMatchedBy(term, localBinding, localOrderConstraint)) { - result.add(conclusion.substitution(localBinding)); - } + else if (conclusion instanceof MetaDependencyFormula dependency) { + localConstraints = dependency.getDependency().isMatchedBy(term, localConstraints); } + for (MatchConstraint constraint : localConstraints) { + result.add(conclusion.substitution(constraint.getBinding())); + } } - for (RDLTerm term : existTerms) { - Map localBinding = new HashMap<>(binding); - Map localOrderConstraint = new HashMap<>(orderConstraint); - if (conclusion instanceof MetaEquationFormula) { - MetaEquationFormula equation = (MetaEquationFormula) conclusion; - if (equation.getRightSideHand().isMatchedBy(term, localBinding, localOrderConstraint)) { - result.add(conclusion.substitution(localBinding)); - } + Set localConstraints = new HashSet<>(res.stream().map(v -> new MatchConstraint(v)).toList()); + if (conclusion instanceof MetaEquationFormula equation) { + localConstraints= equation.getRightSideHand().isMatchedBy(term, localConstraints); + } + for (MatchConstraint constraint : localConstraints) { + result.add(conclusion.substitution(constraint.getBinding())); } } return result; @@ -186,7 +183,8 @@ for (List assumptionList : Permutation.permutation(assumptions, assumptions.size())) { boolean matchFailed = false; for (int i = 0; i < getAssumptionSize(); i++) { - if (! this.assumptions.get(i).isMatchedBy(assumptionList.get(i))) { + Set result = this.assumptions.get(i).isMatchedBy(assumptionList.get(i)); + if (result.isEmpty()) { matchFailed = true; break; } diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index 8d1b7be..1c48625 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -12,584 +12,574 @@ import java.util.Set; import java.util.stream.Collectors; -import models.algebra.Constant; -import models.algebra.Variable; import models.formulas.DependencyFormula; import models.formulas.EquationFormula; import models.formulas.Formula; -import models.formulas.InFormula; -import models.formulas.meta.MetaDependencyFormula; -import models.formulas.meta.MetaEquationFormula; -import models.formulas.meta.MetaInFormula; import models.terms.EvaluatableTerm; import models.terms.RDLTerm; -import models.terms.meta.MetaEvaluatableTermVariable; -import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaResource; -import models.terms.meta.OrderConstraint; import utils.Product; public class ProofSystem { //======================Equality Axioms============================= - private static final InferenceRule reflexivity = new InferenceRule( - "Reflexivity", - List.of(), - new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ); - - private static final InferenceRule symmetry = new InferenceRule( - "Symmetry", - 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 static final InferenceRule transitivity = new InferenceRule( - "Transitivity", - 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")) - ) - ), - new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ) - ); - - private static final InferenceRule rightSubstitution = new InferenceRule( - "Right Substitution", - List.of( - new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ), - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r")) - ), - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaRDLTerm(new MetaResource(new Variable("r"))) - ) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r")), - new MetaEvaluatableTermVariable(new Variable("te")) - ), - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ) - ) - ); - - private static final InferenceRule leftSubstitution = new InferenceRule( - "Left Substitution", - List.of( - new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("te")) - ), - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r")) - ), - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("ue")), - new MetaRDLTerm(new MetaResource(new Variable("r"))) - ) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ), - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResource(new Variable("r")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ) - ) - ); - - private static final InferenceRule identity = new InferenceRule( - "Identity", - List.of( - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaRDLTerm(new MetaResource(new Variable("r"))) - ) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaResource(new Variable("r")), - new MetaResource(new Variable("r")), - new MetaEvaluatableTermVariable(new Variable("te")) - ), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ); - - private static final InferenceRule mapComposition = new InferenceRule( - "Map Composition", - List.of( - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r")) - ), - new MetaDependencyFormula( - new MetaResource(new Variable("r")), - new MetaResource(new Variable("p")) - ), - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaRDLTerm(new MetaResource(new Variable("p"))) - ) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r")), - new MetaRDLTerm( - new MetaResource(new Variable("r")), - new MetaResource(new Variable("p")), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ), - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("p")), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ) - ); - - private static final InferenceRule constantness = new InferenceRule( - "Constantness", - List.of( - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("t1")), - new MetaRDLTerm(new MetaResource(new Variable("r1"), new Variable("m"))) - ) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), - new MetaResource(new Variable("r1"), new Variable("m")), - new MetaEvaluatableTermVariable(new Variable("t1")) - ), - new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) - ), - new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")) - ); - - private static final InferenceRule rightNormalization = new InferenceRule( - "Right Normalization", - List.of( - new MetaDependencyFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResource(new Variable("r"), new Variable("n")) - ) - ), - new MetaDependencyFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("q"), new Variable("n")) - ) - ) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResource(new Variable("r"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("se")) - ), - new MetaResource(new Variable("q"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ), - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResource(new Variable("r"), new Variable("n")), - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("q"), new Variable("n")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ) - ) - ), - new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) - ); - - private static final InferenceRule pseudoConstantness = new InferenceRule( - "Pseudo-Constantness", - List.of( - new MetaDependencyFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), - new MetaResource(new Variable("r"), new Variable("n")) - ) - ) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), - new MetaResource(new Variable("r"), new Variable("n")), - new MetaResource(new Variable("r"), new Variable("n")) - ), - new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")) - ), - new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) - ); - - //======================Dependency Axioms============================= - - private static final InferenceRule identityMapping = new InferenceRule( - "Identity Mapping", - List.of( - new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResource(new Variable("r")) - ) - ), - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResource(new Variable("r")) - ) - ); - - private static final InferenceRule compositeMapping = new InferenceRule( - "Composite Mapping", - List.of( - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResource(new Variable("r")) - ), - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("r")), - new MetaResource(new Variable("q")) - ) - ), - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResource(new Variable("q")) - ) - ); - - private static final InferenceRule constantMapping = new InferenceRule( - "Constant Mapping", - List.of(), - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), - new MetaResource(new Variable("r"), new Variable("m")) - ), - new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")) - ); - - private static final InferenceRule slicedMapping = new InferenceRule( - "Sliced Mapping", - List.of( - new MetaDependencyFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r")) - ), - new MetaResource(new Variable("p")) - ), - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResource(new Variable("p")) - ) - ), - new MetaDependencyFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r")), - new MetaEvaluatableTermVariable(new Variable("te")) - ), - new MetaResource(new Variable("p")) - ) - ); - - //======================Set-Theoretic Axioms============================= - - private static final InferenceRule memberSubstitution = new InferenceRule( - "Member Substitution", - List.of( - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ), - new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ), - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ) - ); - - private static final InferenceRule membershipChain = new InferenceRule( - "Membership Chain", - List.of( - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("te")) - ), - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ) - ), - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ) - ); - - private static final InferenceRule collectionSubstitution = new InferenceRule( - "Collection Substitution", - List.of( - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("te")) - ), - new MetaEquationFormula( - new MetaEvaluatableTermVariable(new Variable("te")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ) - ), - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("ue")) - ) - ); - - private static final InferenceRule setEquivelence = new InferenceRule( - "Set Equivelence", - 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")) - ); - - private static final InferenceRule setHomomorphism = new InferenceRule( - "Set Homomorphism", - List.of( - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r")) - ) - ), - new MetaEquationFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r")), - new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"))) - ), - new MetaRDLTerm( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r")), - new MetaEvaluatableTermVariable(new Variable("te")) - ) - ) - ) - ); - - private static final InferenceRule leftProjection = new InferenceRule( - "Left Projection", - List.of( - new MetaDependencyFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), - new MetaResource(new Variable("r"), new Variable("m")) - ), - new MetaResource(new Variable("q"), new Variable("l")) - ) - ), - new MetaDependencyFormula( - new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))), - new MetaResource(new Variable("q"), new Variable("l")) - ) - ); - - private static final InferenceRule rightProjection = new InferenceRule( - "Right Projection", - List.of( - new MetaDependencyFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), - new MetaResource(new Variable("r"), new Variable("m")) - ), - new MetaResource(new Variable("q"), new Variable("l")) - ) - ), - new MetaDependencyFormula( - new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("r"), new Variable("m"))), - new MetaResource(new Variable("q"), new Variable("l")) - ) - ); - - private static final InferenceRule domainMembership = new InferenceRule( - "Domain Membership", - List.of( - new MetaEquationFormula( - new MetaRDLTerm( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r1")), - new MetaEvaluatableTermVariable(new Variable("t1")) - ), - new MetaResource(new Variable("r2")), - new MetaEvaluatableTermVariable(new Variable("t2")) - ), - new MetaResource(new Variable("c")) - ) - ), - new MetaInFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("t1")), - new MetaResource(new Variable("r2")), - new MetaEvaluatableTermVariable(new Variable("t2")) - ), - new MetaRDLTerm( - new MetaRDLTerm(new MetaResource(new Variable("r1"))), - new MetaResource(new Variable("r2")), - new MetaEvaluatableTermVariable(new Variable("t2")) - ) - ) - ); - - private static final InferenceRule codomainMembership = new InferenceRule( - "Codomain Membership", - List.of( - new MetaDependencyFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r1")), - new MetaEvaluatableTermVariable(new Variable("t1")) - ), - new MetaResource(new Variable("r2")) - ), - new MetaInFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("t1")), - new MetaResource(new Variable("r2")), - new MetaEvaluatableTermVariable(new Variable("t2")) - ), - new MetaRDLTerm( - new MetaRDLTerm( - new MetaResource(new Variable("r1")) - ), - new MetaResource(new Variable("r2")), - new MetaEvaluatableTermVariable(new Variable("t2")) - ) - ) - ), - new MetaInFormula( - new MetaRDLTerm( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r1")), - new MetaEvaluatableTermVariable(new Variable("t1")) - ), - new MetaResource(new Variable("r2")), - new MetaEvaluatableTermVariable(new Variable("t2")) - ), - new MetaRDLTerm( - new MetaRDLTerm( - new MetaResource(new Variable("se")) - ), - new MetaResource(new Variable("r2")), - new MetaEvaluatableTermVariable(new Variable("t2")) - ) - ) - ); - - private static final InferenceRule codomainMembership2 = new InferenceRule( - "Codomain Membership2", - List.of( - new MetaDependencyFormula( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r1")) - ), - new MetaInFormula( - new MetaEvaluatableTermVariable(new Variable("t1")), - new MetaRDLTerm( - new MetaResource(new Variable("r1")) - ) - ) - ), - new MetaInFormula( - new MetaRDLTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResource(new Variable("r1")), - new MetaEvaluatableTermVariable(new Variable("t1")) - ), - new MetaRDLTerm( - new MetaResource(new Variable("se")) - ) - ) - ); +// private static final InferenceRule reflexivity = new InferenceRule( +// "Reflexivity", +// List.of(), +// new MetaEquationFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ) +// ); +// +// private static final InferenceRule symmetry = new InferenceRule( +// "Symmetry", +// 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 static final InferenceRule transitivity = new InferenceRule( +// "Transitivity", +// 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")) +// ) +// ), +// new MetaEquationFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ) +// ); +// +// private static final InferenceRule rightSubstitution = new InferenceRule( +// "Right Substitution", +// List.of( +// new MetaEquationFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ), +// new MetaDependencyFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r")) +// ), +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaRDLTerm(new MetaResource(new Variable("r"))) +// ) +// ), +// new MetaEquationFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r")), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ), +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ) +// ) +// ); +// +// private static final InferenceRule leftSubstitution = new InferenceRule( +// "Left Substitution", +// List.of( +// new MetaEquationFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ), +// new MetaDependencyFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r")) +// ), +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("ue")), +// new MetaRDLTerm(new MetaResource(new Variable("r"))) +// ) +// ), +// new MetaEquationFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ), +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaResource(new Variable("r")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ) +// ) +// ); +// +// private static final InferenceRule identity = new InferenceRule( +// "Identity", +// List.of( +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaRDLTerm(new MetaResource(new Variable("r"))) +// ) +// ), +// new MetaEquationFormula( +// new MetaRDLTerm( +// new MetaResource(new Variable("r")), +// new MetaResource(new Variable("r")), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ) +// ); +// +// private static final InferenceRule mapComposition = new InferenceRule( +// "Map Composition", +// List.of( +// new MetaDependencyFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r")) +// ), +// new MetaDependencyFormula( +// new MetaResource(new Variable("r")), +// new MetaResource(new Variable("p")) +// ), +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaRDLTerm(new MetaResource(new Variable("p"))) +// ) +// ), +// new MetaEquationFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r")), +// new MetaRDLTerm( +// new MetaResource(new Variable("r")), +// new MetaResource(new Variable("p")), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ) +// ), +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("p")), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ) +// ) +// ); +// +// private static final InferenceRule constantness = new InferenceRule( +// "Constantness", +// List.of( +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("t1")), +// new MetaRDLTerm(new MetaResource(new Variable("r1"), new Variable("m"))) +// ) +// ), +// new MetaEquationFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), +// new MetaResource(new Variable("r1"), new Variable("m")), +// new MetaEvaluatableTermVariable(new Variable("t1")) +// ), +// new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) +// ), +// new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")) +// ); +// +// private static final InferenceRule rightNormalization = new InferenceRule( +// "Right Normalization", +// List.of( +// new MetaDependencyFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaResource(new Variable("r"), new Variable("n")) +// ) +// ), +// new MetaDependencyFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("q"), new Variable("n")) +// ) +// ) +// ), +// new MetaEquationFormula( +// new MetaRDLTerm( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaResource(new Variable("r"), new Variable("n")), +// new MetaEvaluatableTermVariable(new Variable("se")) +// ), +// new MetaResource(new Variable("q"), new Variable("n")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ), +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaResource(new Variable("r"), new Variable("n")), +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("q"), new Variable("n")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ) +// ) +// ), +// new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) +// ); +// +// private static final InferenceRule pseudoConstantness = new InferenceRule( +// "Pseudo-Constantness", +// List.of( +// new MetaDependencyFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), +// new MetaResource(new Variable("r"), new Variable("n")) +// ) +// ) +// ), +// new MetaEquationFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), +// new MetaResource(new Variable("r"), new Variable("n")), +// new MetaResource(new Variable("r"), new Variable("n")) +// ), +// new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")) +// ), +// new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) +// ); +// +// //======================Dependency Axioms============================= +// +// private static final InferenceRule identityMapping = new InferenceRule( +// "Identity Mapping", +// List.of( +// new MetaEquationFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaResource(new Variable("r")) +// ) +// ), +// new MetaDependencyFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaResource(new Variable("r")) +// ) +// ); +// +// private static final InferenceRule compositeMapping = new InferenceRule( +// "Composite Mapping", +// List.of( +// new MetaDependencyFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaResource(new Variable("r")) +// ), +// new MetaDependencyFormula( +// new MetaEvaluatableTermVariable(new Variable("r")), +// new MetaResource(new Variable("q")) +// ) +// ), +// new MetaDependencyFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaResource(new Variable("q")) +// ) +// ); +// +// private static final InferenceRule constantMapping = new InferenceRule( +// "Constant Mapping", +// List.of(), +// new MetaDependencyFormula( +// new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), +// new MetaResource(new Variable("r"), new Variable("m")) +// ), +// new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")) +// ); +// +// private static final InferenceRule slicedMapping = new InferenceRule( +// "Sliced Mapping", +// List.of( +// new MetaDependencyFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r")) +// ), +// new MetaResource(new Variable("p")) +// ), +// new MetaDependencyFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaResource(new Variable("p")) +// ) +// ), +// new MetaDependencyFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r")), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ), +// new MetaResource(new Variable("p")) +// ) +// ); +// +// //======================Set-Theoretic Axioms============================= +// +// private static final InferenceRule memberSubstitution = new InferenceRule( +// "Member Substitution", +// List.of( +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ), +// new MetaEquationFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ) +// ), +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ) +// ); +// +// private static final InferenceRule membershipChain = new InferenceRule( +// "Membership Chain", +// List.of( +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ), +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ) +// ), +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ) +// ); +// +// private static final InferenceRule collectionSubstitution = new InferenceRule( +// "Collection Substitution", +// List.of( +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ), +// new MetaEquationFormula( +// new MetaEvaluatableTermVariable(new Variable("te")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ) +// ), +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaEvaluatableTermVariable(new Variable("ue")) +// ) +// ); +// +// private static final InferenceRule setEquivelence = new InferenceRule( +// "Set Equivelence", +// 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")) +// ); +// +// private static final InferenceRule setHomomorphism = new InferenceRule( +// "Set Homomorphism", +// List.of( +// new MetaDependencyFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r")) +// ) +// ), +// new MetaEquationFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r")), +// new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"))) +// ), +// new MetaRDLTerm( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r")), +// new MetaEvaluatableTermVariable(new Variable("te")) +// ) +// ) +// ) +// ); +// +// private static final InferenceRule leftProjection = new InferenceRule( +// "Left Projection", +// List.of( +// new MetaDependencyFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), +// new MetaResource(new Variable("r"), new Variable("m")) +// ), +// new MetaResource(new Variable("q"), new Variable("l")) +// ) +// ), +// new MetaDependencyFormula( +// new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))), +// new MetaResource(new Variable("q"), new Variable("l")) +// ) +// ); +// +// private static final InferenceRule rightProjection = new InferenceRule( +// "Right Projection", +// List.of( +// new MetaDependencyFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), +// new MetaResource(new Variable("r"), new Variable("m")) +// ), +// new MetaResource(new Variable("q"), new Variable("l")) +// ) +// ), +// new MetaDependencyFormula( +// new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("r"), new Variable("m"))), +// new MetaResource(new Variable("q"), new Variable("l")) +// ) +// ); +// +// private static final InferenceRule domainMembership = new InferenceRule( +// "Domain Membership", +// List.of( +// new MetaEquationFormula( +// new MetaRDLTerm( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r1")), +// new MetaEvaluatableTermVariable(new Variable("t1")) +// ), +// new MetaResource(new Variable("r2")), +// new MetaEvaluatableTermVariable(new Variable("t2")) +// ), +// new MetaResource(new Variable("c")) +// ) +// ), +// new MetaInFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("t1")), +// new MetaResource(new Variable("r2")), +// new MetaEvaluatableTermVariable(new Variable("t2")) +// ), +// new MetaRDLTerm( +// new MetaRDLTerm(new MetaResource(new Variable("r1"))), +// new MetaResource(new Variable("r2")), +// new MetaEvaluatableTermVariable(new Variable("t2")) +// ) +// ) +// ); +// +// private static final InferenceRule codomainMembership = new InferenceRule( +// "Codomain Membership", +// List.of( +// new MetaDependencyFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r1")), +// new MetaEvaluatableTermVariable(new Variable("t1")) +// ), +// new MetaResource(new Variable("r2")) +// ), +// new MetaInFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("t1")), +// new MetaResource(new Variable("r2")), +// new MetaEvaluatableTermVariable(new Variable("t2")) +// ), +// new MetaRDLTerm( +// new MetaRDLTerm( +// new MetaResource(new Variable("r1")) +// ), +// new MetaResource(new Variable("r2")), +// new MetaEvaluatableTermVariable(new Variable("t2")) +// ) +// ) +// ), +// new MetaInFormula( +// new MetaRDLTerm( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r1")), +// new MetaEvaluatableTermVariable(new Variable("t1")) +// ), +// new MetaResource(new Variable("r2")), +// new MetaEvaluatableTermVariable(new Variable("t2")) +// ), +// new MetaRDLTerm( +// new MetaRDLTerm( +// new MetaResource(new Variable("se")) +// ), +// new MetaResource(new Variable("r2")), +// new MetaEvaluatableTermVariable(new Variable("t2")) +// ) +// ) +// ); +// +// private static final InferenceRule codomainMembership2 = new InferenceRule( +// "Codomain Membership2", +// List.of( +// new MetaDependencyFormula( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r1")) +// ), +// new MetaInFormula( +// new MetaEvaluatableTermVariable(new Variable("t1")), +// new MetaRDLTerm( +// new MetaResource(new Variable("r1")) +// ) +// ) +// ), +// new MetaInFormula( +// new MetaRDLTerm( +// new MetaEvaluatableTermVariable(new Variable("se")), +// new MetaResource(new Variable("r1")), +// new MetaEvaluatableTermVariable(new Variable("t1")) +// ), +// new MetaRDLTerm( +// new MetaResource(new Variable("se")) +// ) +// ) +// ); private static final List axioms = List.of( // reflexivity, - symmetry, - transitivity, - rightSubstitution, - leftSubstitution, - identity, - mapComposition, - constantness, - rightNormalization, - pseudoConstantness, - identityMapping, - compositeMapping, - constantMapping, - slicedMapping, - memberSubstitution, - membershipChain, - collectionSubstitution, - setEquivelence, - setHomomorphism, - leftProjection, - rightProjection, - domainMembership, - codomainMembership, - codomainMembership2 +// symmetry, +// transitivity, +// rightSubstitution, +// leftSubstitution, +// identity, +// mapComposition, +// constantness, +// rightNormalization, +// pseudoConstantness, +// identityMapping, +// compositeMapping, +// constantMapping, +// slicedMapping, +// memberSubstitution, +// membershipChain, +// collectionSubstitution, +// setEquivelence, +// setHomomorphism, +// leftProjection, +// rightProjection, +// domainMembership, +// codomainMembership, +// codomainMembership2 ); public static void debug() { @@ -693,7 +683,7 @@ for (int i = 0; i < axiom.getAssumptionSize(); i++) { matchedFormulas.add(new ArrayList<>()); for (Formula formula : formulas) { - if (axiom.getAssumptions().get(i).isMatchedBy(formula)) { + if (! axiom.getAssumptions().get(i).isMatchedBy(formula).isEmpty()) { matchedFormulas.get(i).add(formula); } } @@ -724,12 +714,7 @@ } else if (formula instanceof DependencyFormula) { RDLTerm dependency = ((DependencyFormula) formula).getDependency(); existTerms.addAll(dependency.getSubTerms(RDLTerm.class).values()); - } else if (formula instanceof InFormula){ - RDLTerm leftSideHand = ((InFormula) formula).getLeftSideHand(); - RDLTerm rightSideHand = ((InFormula) formula).getRightSideHand(); - existTerms.addAll(leftSideHand.getSubTerms(RDLTerm.class).values()); - existTerms.addAll(rightSideHand.getSubTerms(RDLTerm.class).values()); - } + } } private static boolean equationTransitionCheck(Collection assumptions, Formula conclusion) { diff --git a/src/main/java/inference/rewrite/RewriteInferenceSystem.java b/src/main/java/inference/rewrite/RewriteInferenceSystem.java index 15643a0..0f214b0 100644 --- a/src/main/java/inference/rewrite/RewriteInferenceSystem.java +++ b/src/main/java/inference/rewrite/RewriteInferenceSystem.java @@ -79,8 +79,10 @@ System.out.println("Loop is detected"); return false; } + Set conclusionLeftResult = new HashSet<>(); + Set conclusionRightResult = new HashSet<>(); for (EquationFormula inputFormula : inputFormulas) { - System.out.println("---------------------------" + inputFormula + "-------------------------------------------------"); +// System.out.println("---------------------------" + inputFormula + "-------------------------------------------------"); // ResourceTree baseTree = expandTree(i); // System.out.println("baseTree: " + baseTree); // Set result = rewriteTree(baseTree, i); @@ -96,12 +98,9 @@ // System.out.println("====================================="); Map> leftRewriteGraph = new HashMap<>(); Map> rightRewriteGraph = new HashMap<>(); - Set conclusionLeftResult = rewriteTree(new ResourceTree(conclusion.getLeftSideHand()), inputFormula, leftRewriteGraph); - Set conclusionRightResult = rewriteTree(new ResourceTree(conclusion.getRightSideHand()), inputFormula, rightRewriteGraph); -// System.out.println(conclusionLeftResult); + conclusionLeftResult.addAll(rewriteTree(new ResourceTree(conclusion.getLeftSideHand()), inputFormula, leftRewriteGraph)); + conclusionRightResult.addAll(rewriteTree(new ResourceTree(conclusion.getRightSideHand()), inputFormula, rightRewriteGraph)); // System.out.println(conclusionRightResult); - conclusionLeftResult.retainAll(conclusionRightResult); - System.out.println(conclusionLeftResult.size() != 0); // if (conclusionLeftResult.size() != 0) { // ResourceTree resultRoot = conclusionLeftResult.iterator().next(); // showRewriteGraph(resultRoot, leftRewriteGraph); @@ -111,8 +110,9 @@ // } } - - return false; + conclusionLeftResult.retainAll(conclusionRightResult); +// System.out.println(conclusionLeftResult.size() != 0); + return conclusionLeftResult.size() != 0; } diff --git a/src/main/java/models/formulas/DependencyFormula.java b/src/main/java/models/formulas/DependencyFormula.java index ce737d9..2d0d5b6 100644 --- a/src/main/java/models/formulas/DependencyFormula.java +++ b/src/main/java/models/formulas/DependencyFormula.java @@ -1,6 +1,7 @@ package models.formulas; -import java.util.List; +import java.util.Set; +import java.util.TreeSet; import lombok.Getter; import models.terms.Dependency; @@ -16,8 +17,8 @@ this.dependency = dependency; } - public DependencyFormula(RDLTerm dependingTerm, List dependedResources) { - this.dependency = new Dependency(dependingTerm, dependedResources); + public DependencyFormula(RDLTerm dependingTerm, Set dependedResources) { + this.dependency = new Dependency(dependingTerm, new TreeSet<>(dependedResources)); } diff --git a/src/main/java/models/formulas/InFormula.java b/src/main/java/models/formulas/InFormula.java deleted file mode 100644 index 7b95536..0000000 --- a/src/main/java/models/formulas/InFormula.java +++ /dev/null @@ -1,36 +0,0 @@ -package models.formulas; - -import lombok.Getter; -import models.terms.EvaluatableTerm; - -@Getter -public class InFormula extends Formula { - - private EvaluatableTerm leftSideHand; - private EvaluatableTerm rightSideHand; - - public InFormula(EvaluatableTerm leftSideHand, EvaluatableTerm rightSideHand) { - this.leftSideHand = leftSideHand; - this.rightSideHand = rightSideHand; - } - - @Override - public String toString() { - return leftSideHand.toString() + " in " + rightSideHand.toString(); - } - - @Override - public boolean equals(Object another) { - if (! (another instanceof InFormula)) { - return false; - } - InFormula formula = (InFormula) another; - return leftSideHand.equals(formula.getLeftSideHand()) && rightSideHand.equals(formula.getRightSideHand()); - } - - @Override - public int hashCode() { - return toString().hashCode(); - } - -} diff --git a/src/main/java/models/formulas/meta/MetaDependencyFormula.java b/src/main/java/models/formulas/meta/MetaDependencyFormula.java index 68f9888..d6757bb 100644 --- a/src/main/java/models/formulas/meta/MetaDependencyFormula.java +++ b/src/main/java/models/formulas/meta/MetaDependencyFormula.java @@ -1,6 +1,9 @@ package models.formulas.meta; +import java.util.Arrays; +import java.util.HashSet; import java.util.Map; +import java.util.Set; import exceptions.IllegalTypeException; import lombok.Getter; @@ -9,10 +12,9 @@ import models.formulas.Formula; import models.terms.Dependency; import models.terms.RDLTerm; +import models.terms.meta.MatchConstraint; import models.terms.meta.MetaDependencyVariable; import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaResource; -import models.terms.meta.OrderVariableConstraint; @Getter public class MetaDependencyFormula extends MetaFormula { @@ -30,18 +32,21 @@ this.dependency = dependency; } - public MetaDependencyFormula(MetaRDLTerm dependingTerm, MetaResource dependedVariable) { - this.dependency = new MetaRDLTerm(dependingTerm, dependedVariable); + public MetaDependencyFormula(MetaRDLTerm dependingTerm, Set dependedTerms) { + this.dependency = new MetaRDLTerm(dependingTerm, dependedTerms); + } + + public MetaDependencyFormula(MetaRDLTerm dependingTerm, MetaRDLTerm ...dependedTerms) { + this(dependingTerm, new HashSet<>(Arrays.asList(dependedTerms))); } @Override - public boolean isMatchedBy(Formula formula, Map binding, - Map orderConstraint) { + public Set isMatchedBy(Formula formula, MatchConstraint constraint) { if (! (formula instanceof DependencyFormula)) { - return false; + return new HashSet<>(); } DependencyFormula dep = (DependencyFormula) formula; - return dependency.isMatchedBy(dep.getDependency(), binding, orderConstraint); + return dependency.isMatchedBy(dep.getDependency(), constraint); } diff --git a/src/main/java/models/formulas/meta/MetaEquationFormula.java b/src/main/java/models/formulas/meta/MetaEquationFormula.java index 7f27ff5..8c07b25 100644 --- a/src/main/java/models/formulas/meta/MetaEquationFormula.java +++ b/src/main/java/models/formulas/meta/MetaEquationFormula.java @@ -1,6 +1,8 @@ package models.formulas.meta; +import java.util.HashSet; import java.util.Map; +import java.util.Set; import exceptions.IllegalTypeException; import lombok.Getter; @@ -9,8 +11,8 @@ import models.formulas.Formula; import models.terms.EvaluatableTerm; import models.terms.RDLTerm; +import models.terms.meta.MatchConstraint; import models.terms.meta.MetaRDLTerm; -import models.terms.meta.OrderVariableConstraint; @Getter public class MetaEquationFormula extends MetaFormula { @@ -31,13 +33,14 @@ } @Override - public boolean isMatchedBy(Formula formula, Map binding, - Map orderConstraint) { + public Set isMatchedBy(Formula formula, MatchConstraint constraint) { + Set result = new HashSet<>(); if (! (formula instanceof EquationFormula)) { - return false; + return result; } EquationFormula eq = (EquationFormula) formula; - return leftSideHand.isMatchedBy(eq.getLeftSideHand(), binding, orderConstraint) && rightSideHand.isMatchedBy(eq.getRightSideHand(), binding, orderConstraint); + result = leftSideHand.isMatchedBy(eq.getLeftSideHand(), constraint); + return rightSideHand.isMatchedBy(eq.getRightSideHand(), result); } @Override diff --git a/src/main/java/models/formulas/meta/MetaFormula.java b/src/main/java/models/formulas/meta/MetaFormula.java index 6115a2b..0340d09 100644 --- a/src/main/java/models/formulas/meta/MetaFormula.java +++ b/src/main/java/models/formulas/meta/MetaFormula.java @@ -1,20 +1,31 @@ package models.formulas.meta; import java.util.HashMap; +import java.util.HashSet; import java.util.Map; +import java.util.Set; import models.algebra.Variable; import models.formulas.Formula; import models.terms.RDLTerm; -import models.terms.meta.OrderVariableConstraint; +import models.terms.meta.MatchConstraint; public abstract class MetaFormula { - public boolean isMatchedBy(Formula formula) { - return isMatchedBy(formula, new HashMap<>(), new HashMap<>()); + public Set isMatchedBy(Formula formula) { + return isMatchedBy(formula, new MatchConstraint(new HashMap<>(), new HashMap<>())); } - public abstract boolean isMatchedBy(Formula formula, Map binding, Map orderConstraint); + public abstract Set isMatchedBy(Formula formula, MatchConstraint constraint); + + public Set isMatchedBy(Formula formula, Set constraints) { + Set result = new HashSet<>(); + for (MatchConstraint constraint: constraints) { + result.addAll(isMatchedBy(formula, constraint)); + } + return result; + } + public abstract Formula substitution(Map binding); diff --git a/src/main/java/models/formulas/meta/MetaInFormula.java b/src/main/java/models/formulas/meta/MetaInFormula.java deleted file mode 100644 index 900faff..0000000 --- a/src/main/java/models/formulas/meta/MetaInFormula.java +++ /dev/null @@ -1,68 +0,0 @@ -package models.formulas.meta; - -import java.util.Map; - -import exceptions.IllegalTypeException; -import lombok.Getter; -import models.algebra.Variable; -import models.formulas.Formula; -import models.formulas.InFormula; -import models.terms.EvaluatableTerm; -import models.terms.RDLTerm; -import models.terms.meta.MetaRDLTerm; -import models.terms.meta.OrderVariableConstraint; - -@Getter -public class MetaInFormula extends MetaFormula { - - private MetaRDLTerm leftSideHand; - private MetaRDLTerm rightSideHand; - - public MetaInFormula(MetaRDLTerm leftSideHand, MetaRDLTerm rightSideHand) { - if (! leftSideHand.isEvaluatableTerm()) { - throw new IllegalTypeException(); - } - if(! rightSideHand.isEvaluatableTerm()) { - throw new IllegalTypeException(); - } - this.leftSideHand = leftSideHand; - this.rightSideHand = rightSideHand; - } - - @Override - public boolean isMatchedBy(Formula formula, Map binding, - Map orderConstraint) { - if (! (formula instanceof InFormula)) { - return false; - } - InFormula inFormula = (InFormula) formula; - return leftSideHand.isMatchedBy(inFormula.getLeftSideHand(), binding, orderConstraint) - && rightSideHand.isMatchedBy(inFormula.getRightSideHand(), binding, orderConstraint); - } - - @Override - public InFormula substitution(Map binding) { - return new InFormula((EvaluatableTerm) leftSideHand.substitute(binding), (EvaluatableTerm) rightSideHand.substitute(binding)); - } - - - @Override - public String toString() { - return leftSideHand.toString() + " in " + rightSideHand.toString(); - } - - @Override - public boolean equals(Object anohter) { - if (! (anohter instanceof MetaInFormula)) { - return false; - } - MetaInFormula formula = (MetaInFormula) anohter; - return leftSideHand.equals(formula.getLeftSideHand()) && rightSideHand.equals(formula.getRightSideHand()); - } - - @Override - public int hashCode() { - return toString().hashCode(); - } - -} diff --git a/src/main/java/models/terms/Dependency.java b/src/main/java/models/terms/Dependency.java index 8edefba..d382318 100644 --- a/src/main/java/models/terms/Dependency.java +++ b/src/main/java/models/terms/Dependency.java @@ -1,10 +1,11 @@ package models.terms; -import java.util.ArrayList; import java.util.Arrays; -import java.util.List; +import java.util.Set; +import java.util.TreeSet; import java.util.stream.Collectors; +import exceptions.SyntaxException; import lombok.Getter; import models.algebra.Symbol; @@ -12,65 +13,26 @@ public class Dependency extends RDLTerm{ private RDLTerm dependingTerm; - private List dependedTerms; - private Dependency dependency; - private boolean isListType; + private TreeSet dependedTerms; -// public Dependency(RDLTerm dependingTerm, Resource dependedVariable) { -// super(new Symbol(":", 2), dependedVariable.getOrder(), dependingTerm.getSize() + dependedVariable.getSize()); -// this.dependingTerm = dependingTerm; -// this.dependedVariable = dependedVariable; -// this.dependency = null; -// this.addChild(dependingTerm); -// this.addChild(dependedVariable); -// this.isListType = false; -// } - - public Dependency(RDLTerm dependingTerm, List dependedTerms) { - super(new Symbol(":", dependedTerms.size() + 1), dependedTerms.get(0).getOrder(), dependingTerm.getSize() + dependedTerms.stream().mapToInt(v -> v.size).sum()); + public Dependency(RDLTerm dependingTerm, Set dependedTerms) { + super(new Symbol(":", dependedTerms.size() + 1), dependedTerms.iterator().next().getOrder(), dependingTerm.getSize() + dependedTerms.stream().mapToInt(v -> v.size).sum()); this.dependingTerm = dependingTerm; - this.dependedTerms = dependedTerms; - this.dependency = null; + this.dependedTerms = new TreeSet<>(dependedTerms); this.addChild(dependingTerm); - for (EvaluatableTerm dependedResource: dependedTerms) { - this.addChild(dependedResource); + if (dependingTerm.getTermOrder() > getOrder()) { + throw new SyntaxException("dependingTerm's order must be less than " + (getOrder() + 1) + ", but " + dependingTerm + "'s order is " + dependingTerm.getOrder()); } - this.isListType = false; + for (EvaluatableTerm dependedTerm: dependedTerms) { + this.addChild(dependedTerm); + if (dependedTerm.getTermOrder() != getOrder()) { + throw new SyntaxException(dependedTerm + " order is not " + getOrder()); + } + } } - public Dependency(RDLTerm dependingTerm, Resource ...dependedResources) { - this(dependingTerm, Arrays.asList(dependedResources)); - } - - public Dependency(Dependency dependency) { - super(new Symbol(":", 1), dependency.getOrder() - 1, dependency.getSize()); - this.dependency = dependency; - this.dependingTerm = null; - this.dependedTerms = null; - this.addChild(dependency); - this.isListType = true; - } - -// public Dependency(RDLTerm dependingTerm, Resource dependedVariable, int order) { -// super(new Symbol(":", order == dependedVariable.order ? 2 : 1), order, dependingTerm.getSize() + dependedVariable.getSize()); -// if(order == dependedVariable.order) { -// this.dependingTerm = dependingTerm; -// this.dependedResources = dependedVariable; -// this.addChild(dependingTerm); -// this.addChild(dependedVariable); -// this.dependency = null; -// this.isListType = false; -// } else { -// this.dependency = new Dependency(dependingTerm, dependedVariable, order+1); -// this.dependingTerm = null; -// this.dependedResources = null; -// this.addChild(dependency); -// this.isListType = true; -// } -// } - - public Dependency getDependency() { - return this.dependency; + public Dependency(RDLTerm dependingTerm, EvaluatableTerm ...dependedTerms) { + this(dependingTerm, new TreeSet<>(Arrays.asList(dependedTerms))); } @Override @@ -85,30 +47,18 @@ @Override public String toString() { StringBuilder sb = new StringBuilder(); - if(dependency == null) { - sb.append(dependingTerm.toTermString()); - sb.append(" : "); - sb.append(dependedTerms.toString()); - } else { - sb.append('['); - sb.append(dependency.toString()); - sb.append(']'); - } + sb.append(dependingTerm.toTermString()); + sb.append(" : "); + sb.append(dependedTerms.stream().map(RDLTerm::toString).collect(Collectors.joining(", "))); return sb.toString(); } @Override public String toStringWithOrder() { StringBuilder sb = new StringBuilder(); - if(dependency == null) { - sb.append(dependingTerm.toStringWithOrder()); - sb.append(" : "); - sb.append(dependedTerms.stream().map(RDLTerm::toStringWithOrder).collect(Collectors.joining(", "))); - } else { - sb.append('['); - sb.append(dependency.toStringWithOrder()); - sb.append(']'); - } + sb.append(dependingTerm.toStringWithOrder()); + sb.append(" : "); + sb.append(dependedTerms.stream().map(RDLTerm::toStringWithOrder).collect(Collectors.joining(", "))); return sb.toString() + "(" + order + ")"; } @@ -123,12 +73,6 @@ return false; } Dependency anotherDep = (Dependency) another; - if(anotherDep.isListType() != isListType()) { - return false; - } - if(isListType()) { - return anotherDep.getDependency().equals(dependency); - } return anotherDep.getDependingTerm().equals(dependingTerm) && anotherDep.getDependedTerms().equals(dependedTerms); } @@ -140,7 +84,7 @@ @Override public Object clone() { - return new Dependency((RDLTerm) dependingTerm.clone(), new ArrayList<>(dependedTerms)); + return new Dependency((RDLTerm) dependingTerm.clone(), new TreeSet<>(dependedTerms)); } } diff --git a/src/main/java/models/terms/DependencyTerm.java b/src/main/java/models/terms/DependencyTerm.java index 46d871e..981bd56 100644 --- a/src/main/java/models/terms/DependencyTerm.java +++ b/src/main/java/models/terms/DependencyTerm.java @@ -1,9 +1,12 @@ package models.terms; import java.util.ArrayList; +import java.util.Arrays; import java.util.List; +import java.util.TreeMap; import java.util.stream.IntStream; +import exceptions.SyntaxException; import lombok.Getter; import models.algebra.Symbol; @@ -11,50 +14,45 @@ public class DependencyTerm extends EvaluatableTerm{ private EvaluatableTerm dependingTerm; - private List dependedTerms = new ArrayList<>(); - private List argumentTerms = new ArrayList<>(); + private TreeMap termPairs; - public DependencyTerm(EvaluatableTerm dependingTerm, List dependedTerms, List argumentTerms) { + public DependencyTerm(EvaluatableTerm dependingTerm, List terms) { super( - new Symbol(":", 1 + dependedTerms.size() + argumentTerms.size()), - -1, - dependingTerm.getSize() + argumentTerms.stream().mapToInt(RDLTerm::getSize).sum() + dependedTerms.stream().mapToInt(RDLTerm::getSize).sum() + new Symbol(":", 1 + terms.size()), + -1, + -1 ); - int maxOrder = argumentTerms.stream().mapToInt(EvaluatableTerm::getOrder).max().orElse(-1); - if (dependedTerms.get(0).getOrder() < maxOrder) { - this.order = dependingTerm.getOrder() + (maxOrder - dependedTerms.get(0).getOrder()); - } else if (dependedTerms.get(0).getOrder() == maxOrder) { - this.order = dependingTerm.getOrder(); + if (terms.size() % 2 != 0) { + throw new SyntaxException("Args size must be odd."); + } + this.size = dependingTerm.getSize(); + int maxArgOrder = IntStream.range(0, terms.size()).filter(i -> i % 2 == 1).map(i -> terms.get(i).getOrder()).max().orElse(0); + int maxDependedOrder = IntStream.range(0, terms.size()).filter(i -> i % 2 == 0).map(i -> terms.get(i).getOrder()).max().orElse(0); + boolean argOrderType = maxDependedOrder <= maxArgOrder; + if (argOrderType) { + this.order = maxArgOrder; } else { - this.order = dependingTerm.getOrder() - 1; - } - - for(int i = 0; i < dependedTerms.size(); i++) { - if (dependedTerms.get(0).getOrder() != dependedTerms.get(i).getOrder()) { - throw new RuntimeException("dependedTerms order not equals"); - } - } - - if (dependedTerms.size() != argumentTerms.size()) { - throw new RuntimeException("Size not equals"); + this.order = maxDependedOrder - 1; } this.dependingTerm = dependingTerm; - this.dependedTerms = new ArrayList<>(dependedTerms); - this.argumentTerms = new ArrayList<>(argumentTerms); + this.termPairs = new TreeMap<>(); addChild(dependingTerm); - for (int i = 0; i < dependedTerms.size(); i++) { - addChild(dependedTerms.get(i)); - addChild(argumentTerms.get(i)); + for (int i = 0; i < terms.size() / 2; i++) { + EvaluatableTerm dependedTerm = terms.get(2 * i); + EvaluatableTerm argTerm = terms.get(2 * i + 1); + termPairs.put(dependedTerm, argTerm); + this.size += dependedTerm.getSize(); + this.size += argTerm.getSize(); + } + for (EvaluatableTerm dependedTerm : termPairs.keySet()) { + addChild(dependedTerm); + addChild(termPairs.get(dependedTerm)); } } public DependencyTerm(EvaluatableTerm dependingTerm, EvaluatableTerm ...terms) { - this( - dependingTerm, - IntStream.range(0, terms.length).filter(i -> i % 2 == 0).mapToObj(i -> terms[i]).toList(), - IntStream.range(0, terms.length).filter(i -> i % 2 == 1).mapToObj(i -> terms[i]).toList() - ); + this(dependingTerm, Arrays.asList(terms)); } @Override @@ -71,54 +69,20 @@ @Override public void selfLinearRightNormalize() { -// if(dependingTerm instanceof ResourceVariable || dependingTerm instanceof SetEvaluatableTerm) { -// argumentTerm.selfLinearRightNormalize(); -// return; -// } -// DependencyTerm dependencyTerm = (DependencyTerm) dependingTerm; -// if(! dependencyTerm.isLinearRightNormalized()) { -// dependencyTerm.selfLinearRightNormalize(); -// } -// if(! isLinearRightNormalized()) { -// EvaluatableTerm childArgumentTerm = dependencyTerm.getArgumentTerm(); -// DependencyTerm nextDependencyTerm = new DependencyTerm(childArgumentTerm, dependedVariable, argumentTerm); -// this.dependingTerm = dependencyTerm.getDependingTerm(); -// this.dependedVariable = dependencyTerm.getDependedVariable(); -// this.argumentTerm = nextDependencyTerm; -// this.setChild(2, nextDependencyTerm); -// this.setChild(0, dependencyTerm.getDependingTerm()); -// this.setChild(1, dependencyTerm.getDependedVariable()); -// } -// argumentTerm.selfLinearRightNormalize(); - } private boolean isLinearRightNormaled(int depth) { -// if(dependingTerm instanceof ResourceVariable || dependingTerm instanceof SetEvaluatableTerm) { -// return dependingTerm.getOrder() == dependedVariable.getOrder(); -// } -// DependencyTerm dependencyTerm = (DependencyTerm) dependingTerm; -// if( -// dependencyTerm.isLinearRightNormaled(depth + 1) && -// dependencyTerm.getDependedVariable().getOrder() - 1 == dependedVariable.getOrder() && -// dependencyTerm.getOrder() == dependedVariable.getOrder() && -// argumentTerm.getOrder() <= dependencyTerm.getOrder() && -// depth == 0 -// ) { -// return true; -// } -// if( -// dependencyTerm.isLinearRightNormaled(depth + 1) && -// dependencyTerm.getDependedVariable().getOrder() - 1 == dependedVariable.getOrder() && -// dependencyTerm.getOrder() == dependedVariable.getOrder() && -// argumentTerm.getOrder() < dependencyTerm.getOrder() -// ) { -// return true; -// } - return false; } + public List getDependedTerms() { + return new ArrayList<>(termPairs.keySet()); + } + + public List getArgumentTerms() { + return new ArrayList<>(termPairs.values()); + } + @Override public String toString() { @@ -126,10 +90,11 @@ sb.append('['); sb.append(getDependingTerm().toString()); sb.append(" : "); - for (int i = 0; i < dependedTerms.size(); i++) { - sb.append(dependedTerms.get(i).toString()); + for (EvaluatableTerm dependedTerm: termPairs.keySet()) { + EvaluatableTerm argTerm = termPairs.get(dependedTerm); + sb.append(dependedTerm.toString()); sb.append(" -> "); - sb.append(argumentTerms.get(i).toString()); + sb.append(argTerm.toString()); sb.append(", "); } sb.deleteCharAt(sb.length() - 1); @@ -144,13 +109,15 @@ sb.append('['); sb.append(getDependingTerm().toStringWithOrder()); sb.append(" : "); - for (int i = 0; i < dependedTerms.size(); i++) { - sb.append(dependedTerms.get(i).toStringWithOrder()); + for (EvaluatableTerm dependedTerm: termPairs.keySet()) { + EvaluatableTerm argTerm = termPairs.get(dependedTerm); + sb.append(dependedTerm.toStringWithOrder()); sb.append(" -> "); - sb.append(argumentTerms.get(i).toStringWithOrder()); + sb.append(argTerm.toStringWithOrder()); sb.append(", "); } sb.deleteCharAt(sb.length() - 1); + sb.deleteCharAt(sb.length() - 1); sb.append(']'); sb.append('('); sb.append(order); @@ -166,8 +133,7 @@ DependencyTerm term = (DependencyTerm) another; return dependingTerm.equals(term.getDependingTerm()) && - dependedTerms.stream().sorted().toList().equals(term.getDependedTerms().stream().sorted().toList()) && - argumentTerms.stream().sorted().toList().equals(term.getArgumentTerms().stream().sorted().toList()); + termPairs.equals(term.getTermPairs()); } @Override @@ -177,10 +143,14 @@ @Override public Object clone() { + List termPairs = new ArrayList<>(); + for (EvaluatableTerm dependedTerm : this.termPairs.keySet()) { + termPairs.add(dependedTerm); + termPairs.add(this.termPairs.get(dependedTerm)); + } return new DependencyTerm( (EvaluatableTerm) dependingTerm.clone(), - new ArrayList<>(dependedTerms), - new ArrayList<>(argumentTerms) + termPairs ); } diff --git a/src/main/java/models/terms/SetEvaluatableTerm.java b/src/main/java/models/terms/SetEvaluatableTerm.java deleted file mode 100644 index 05fc8e2..0000000 --- a/src/main/java/models/terms/SetEvaluatableTerm.java +++ /dev/null @@ -1,86 +0,0 @@ -package models.terms; - -import lombok.Getter; -import models.algebra.Symbol; - -@Getter -public class SetEvaluatableTerm extends EvaluatableTerm{ - - private EvaluatableTerm term; - - public SetEvaluatableTerm(EvaluatableTerm term) { - super(new Symbol("", 1), term.getOrder() - 1, term.getSize()); - this.term = term; - this.addChild(term); - } - - public SetEvaluatableTerm(EvaluatableTerm term, int order) { - super(new Symbol("", 1), order, term.getSize()); - if(term.getOrder() > order + 1) { - var childTerm = new SetEvaluatableTerm(term, order+1); - this.term = childTerm; - this.addChild(childTerm); - } else { - this.term = term; - this.addChild(term); - } - } - - public void setTerm(EvaluatableTerm newTerm) { - setChild(0, newTerm); - this.term = newTerm; - } - - @Override - public EvaluatableTerm linearRightNormalize() { - return (SetEvaluatableTerm) clone(); - } - - @Override - public void selfLinearRightNormalize() { - } - - @Override - public boolean isLinearRightNormalized() { - return term.isLinearRightNormalized(); - } - - - @Override - public boolean equals(Object another) { - if(! (another instanceof SetEvaluatableTerm)) { - return false; - } - var term = (SetEvaluatableTerm) another; - return term.getTerm().equals(getTerm()); - } - - @Override - public int hashCode() { - return ("SET" + toString()).hashCode(); - } - - @Override - public String toString() { - StringBuilder sb = new StringBuilder(); - sb.append('{'); - sb.append(term.toString()); - sb.append('}'); - return sb.toString(); - } - - @Override - public String toStringWithOrder() { - StringBuilder sb = new StringBuilder(); - sb.append('{'); - sb.append(term.toStringWithOrder()); - sb.append('}'); - return sb.toString() + "(" + order + ")"; - } - - @Override - public Object clone() { - return new SetEvaluatableTerm((EvaluatableTerm) term.clone(), order); - } - -} diff --git a/src/main/java/models/terms/meta/MatchConstraint.java b/src/main/java/models/terms/meta/MatchConstraint.java new file mode 100644 index 0000000..05adc4b --- /dev/null +++ b/src/main/java/models/terms/meta/MatchConstraint.java @@ -0,0 +1,36 @@ +package models.terms.meta; +import java.util.HashMap; +import java.util.Map; + +import lombok.EqualsAndHashCode; +import lombok.RequiredArgsConstructor; +import lombok.ToString; +import models.algebra.Variable; +import models.terms.RDLTerm; + +@RequiredArgsConstructor +@EqualsAndHashCode +@ToString +public class MatchConstraint { + + private final Map binding; + private final Map orderConstraint; + + public MatchConstraint(MatchConstraint constraint) { + this.binding = constraint.getBinding(); + this.orderConstraint = constraint.getOrderConstraint(); + } + + public Map getBinding() { + return new HashMap<>(binding); + } + + public Map getOrderConstraint() { + Map res = new HashMap<>(); + for (var key : orderConstraint.keySet()) { + res.put(key, (OrderVariableConstraint) orderConstraint.get(key).clone()); + } + return res; + } + +} diff --git a/src/main/java/models/terms/meta/MetaDependencyGenerator.java b/src/main/java/models/terms/meta/MetaDependencyGenerator.java new file mode 100644 index 0000000..191ecf1 --- /dev/null +++ b/src/main/java/models/terms/meta/MetaDependencyGenerator.java @@ -0,0 +1,10 @@ +package models.terms.meta; + +import models.terms.RDLTerm; + +@FunctionalInterface +public interface MetaDependencyGenerator { + + RDLTerm generate(int i, int size); + +} diff --git a/src/main/java/models/terms/meta/MetaDependencyTermGenerator.java b/src/main/java/models/terms/meta/MetaDependencyTermGenerator.java new file mode 100644 index 0000000..2974988 --- /dev/null +++ b/src/main/java/models/terms/meta/MetaDependencyTermGenerator.java @@ -0,0 +1,12 @@ +package models.terms.meta; + +import models.terms.RDLTerm; + +@FunctionalInterface +public interface MetaDependencyTermGenerator { + + record TermPair(RDLTerm dependedTerm, RDLTerm argTerm) {}; + + TermPair generate(int i, int size); + +} diff --git a/src/main/java/models/terms/meta/MetaEvaluatableTermSet.java b/src/main/java/models/terms/meta/MetaEvaluatableTermSet.java deleted file mode 100644 index 8611340..0000000 --- a/src/main/java/models/terms/meta/MetaEvaluatableTermSet.java +++ /dev/null @@ -1,22 +0,0 @@ -package models.terms.meta; - -import models.algebra.Constant; -import models.algebra.Expression; -import models.algebra.Symbol; -import models.algebra.Variable; - -public class MetaEvaluatableTermSet extends MetaVariable{ - - public MetaEvaluatableTermSet(Variable name, OrderConstraint constraint, Expression order) { - super(new Symbol(":", 1), TermType.META_EVALUATABLE_TERM_SET_VARIABLE, name, constraint, order); - } - - public MetaEvaluatableTermSet(Variable variableName) { - super(new Symbol(":", 1), MetaRDLTerm.TermType.META_EVALUATABLE_TERM_SET_VARIABLE, variableName, OrderConstraint.ANY, new Constant("0")); - } - - public MetaEvaluatableTermSet(Variable variableName, Expression order) { - super(new Symbol(":", 1), MetaRDLTerm.TermType.META_EVALUATABLE_TERM_SET_VARIABLE, variableName, OrderConstraint.EQ, order); - } - -} diff --git a/src/main/java/models/terms/meta/MetaRDLTerm.java b/src/main/java/models/terms/meta/MetaRDLTerm.java index 2072bd5..1993240 100644 --- a/src/main/java/models/terms/meta/MetaRDLTerm.java +++ b/src/main/java/models/terms/meta/MetaRDLTerm.java @@ -1,12 +1,23 @@ package models.terms.meta; +import java.util.ArrayList; +import java.util.Arrays; 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 java.util.TreeMap; +import java.util.TreeSet; +import java.util.stream.Collectors; +import java.util.stream.IntStream; import exceptions.IllegalTypeException; import exceptions.SubstituteFailedException; +import exceptions.SyntaxException; import lombok.Getter; +import models.algebra.Expression; import models.algebra.Symbol; import models.algebra.Variable; import models.terms.Dependency; @@ -15,14 +26,20 @@ import models.terms.LinearRightNormalizedType; import models.terms.RDLTerm; import models.terms.Resource; -import models.terms.SetEvaluatableTerm; +import models.terms.meta.MetaDependencyTermGenerator.TermPair; +import utils.Permutation; -@Getter public class MetaRDLTerm extends RDLTerm { + @Getter protected TermType termType; + @Getter protected LinearRightNormalizedType linearRightNormalizedType = LinearRightNormalizedType.UNDEFINED; + private boolean isDynamic = false; + private MetaDependencyTermGenerator metaDependencyTermGenerator; + private MetaDependencyGenerator metaDependencyGenerator; + protected MetaRDLTerm(Symbol symbol, TermType termType, int size) { super(symbol, -1, size); this.termType = termType; @@ -32,117 +49,76 @@ } //dependency - public MetaRDLTerm(RDLTerm dependingTerm, MetaResource dependedVariable) { - super(new Symbol(":", 2), dependedVariable.getOrder(), dependingTerm.getSize() + dependedVariable.getSize()); + public MetaRDLTerm(MetaRDLTerm dependingTerm, Set dependedTerms) { + super(new Symbol(":", 1 + dependedTerms.size()), -1, -1); + int size = dependingTerm.getSize(); addChild(dependingTerm); - addChild(dependedVariable); - this.termType = TermType.META_DEPENDENCY; - } - - public MetaRDLTerm(MetaRDLTerm dependingTerm, Resource dependedVariable) { - super(new Symbol(":", 2), dependedVariable.getOrder(), dependingTerm.getSize() + dependedVariable.getSize()); - addChild(dependingTerm); - addChild(dependedVariable); - this.termType = TermType.META_DEPENDENCY; - } - - public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaResource dependedVariable) { - super(new Symbol(":", 2), dependedVariable.getOrder(), dependingTerm.getSize() + dependedVariable.getSize()); - addChild(dependingTerm); - addChild(dependedVariable); - this.termType = TermType.META_DEPENDENCY; - } - - //list type dependency or set term - public MetaRDLTerm(MetaRDLTerm term) { - super(new Symbol(":", 1), term.getOrder() - 1, term.getSize()); - if (term.isDependency()) { - this.termType = TermType.META_DEPENDENCY_LIST; - } else if (term.isEvaluatableTerm()) { - this.termType = TermType.META_EVALUATABLE_TERM_SET; + for (MetaRDLTerm dependedTerm: new TreeSet<>(dependedTerms)) { + addChild(dependedTerm); + size += dependedTerm.getSize(); } - addChild(term); + this.size = size; + this.termType = TermType.META_DEPENDENCY; + this.metaDependencyGenerator = (i, j) -> (RDLTerm) this.getChild(i + 1); + } + + public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaRDLTerm dependedTerm) { + this(dependingTerm, new TreeSet<>(Set.of(dependedTerm))); + } + + public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaDependencyGenerator generator) { + super(new Symbol(":", 1), -1, -1); + addChild(dependingTerm); + this.metaDependencyGenerator = generator; + this.termType = TermType.META_DEPENDENCY; + this.isDynamic = true; } //dependency term - public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaResource dependedVariable, MetaRDLTerm argumentTerm) { - super(new Symbol(":", 3), -1, dependingTerm.getSize() + dependedVariable.getSize() + argumentTerm.getSize()); + public MetaRDLTerm(MetaRDLTerm dependingTerm, List terms) { + super(new Symbol(":", terms.size() + 1), -1, -1); if (! EvaluatableTerm.class.isAssignableFrom(dependingTerm.getTermType().getBaseTermClass())) { throw new IllegalTypeException(); } - if(! EvaluatableTerm.class.isAssignableFrom(argumentTerm.getTermType().getBaseTermClass())) { - throw new IllegalTypeException(); + if (terms.size() % 2 != 0) { + throw new SyntaxException(""); } + int size = dependingTerm.getSize(); addChild(dependingTerm); - addChild(dependedVariable); - addChild(argumentTerm); + TreeMap sortedTerms = new TreeMap<>(); + for (int i = 0; i < terms.size() / 2; i++) { + MetaRDLTerm dependedTerm = terms.get(2 * i); + MetaRDLTerm argTerm = terms.get(2 * i + 1); + size += dependedTerm.getSize(); + size += argTerm.getSize(); + if (! EvaluatableTerm.class.isAssignableFrom(dependedTerm.getTermType().getBaseTermClass())) { + throw new IllegalTypeException(); + } + if (! EvaluatableTerm.class.isAssignableFrom(argTerm.getTermType().getBaseTermClass())) { + throw new IllegalTypeException(); + } + sortedTerms.put(dependedTerm, argTerm); + } + this.size = size; + for (MetaRDLTerm dependedTerm: sortedTerms.keySet()) { + MetaRDLTerm argTerm = sortedTerms.get(dependedTerm); + addChild(dependedTerm); + addChild(argTerm); + } this.termType = TermType.META_DEPENDENCY_TERM; + this.metaDependencyTermGenerator = (i, j) -> new TermPair((RDLTerm) this.getChild(i * 2 + 1), (RDLTerm) this.getChild(i * 2 + 2)); } - public MetaRDLTerm(EvaluatableTerm dependingTerm, MetaRDLTerm dependedVariable, MetaRDLTerm argumentTerm) { - super(new Symbol(":", 3), -1, dependingTerm.getSize() + dependedVariable.getSize() + argumentTerm.getSize()); - if(! EvaluatableTerm.class.isAssignableFrom(argumentTerm.getTermType().getBaseTermClass())) { - throw new IllegalTypeException(); - } - addChild(dependingTerm); - addChild(dependedVariable); - addChild(argumentTerm); - this.termType = TermType.META_DEPENDENCY_TERM; + public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaRDLTerm ...terms) { + this(dependingTerm, Arrays.asList(terms)); } - public MetaRDLTerm(MetaRDLTerm dependingTerm, Resource dependedVariable, MetaRDLTerm argumentTerm) { - super(new Symbol(":", 3), -1, dependingTerm.getSize() + dependedVariable.getSize() + argumentTerm.getSize()); - if (! EvaluatableTerm.class.isAssignableFrom(dependingTerm.getTermType().getBaseTermClass())) { - throw new IllegalTypeException(); - } - if(! EvaluatableTerm.class.isAssignableFrom(argumentTerm.getTermType().getBaseTermClass())) { - throw new IllegalTypeException(); - } + public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaDependencyTermGenerator generator) { + super(new Symbol(":", 1), -1, -1); addChild(dependingTerm); - addChild(dependedVariable); - addChild(argumentTerm); + this.metaDependencyTermGenerator = generator; this.termType = TermType.META_DEPENDENCY_TERM; - } - - public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaRDLTerm dependedVariable, EvaluatableTerm argumentTerm) { - super(new Symbol(":", 3), -1, dependingTerm.getSize() + dependedVariable.getSize() + argumentTerm.getSize()); - if (! EvaluatableTerm.class.isAssignableFrom(dependingTerm.getTermType().getBaseTermClass())) { - throw new IllegalTypeException(); - } - addChild(dependingTerm); - addChild(dependedVariable); - addChild(argumentTerm); - this.termType = TermType.META_DEPENDENCY_TERM; - } - - public MetaRDLTerm(MetaRDLTerm dependingTerm, Resource dependedVariable, EvaluatableTerm argumentTerm) { - super(new Symbol(":", 3), -1, dependingTerm.getSize() + dependedVariable.getSize() + argumentTerm.getSize()); - if (! EvaluatableTerm.class.isAssignableFrom(dependingTerm.getTermType().getBaseTermClass())) { - throw new IllegalTypeException(); - } - addChild(dependingTerm); - addChild(dependedVariable); - addChild(argumentTerm); - this.termType = TermType.META_DEPENDENCY_TERM; - } - - public MetaRDLTerm(EvaluatableTerm dependingTerm, MetaResource dependedVariable, EvaluatableTerm argumentTerm) { - super(new Symbol(":", 3), -1, dependingTerm.getSize() + dependedVariable.getSize() + argumentTerm.getSize()); - addChild(dependingTerm); - addChild(dependedVariable); - addChild(argumentTerm); - this.termType = TermType.META_DEPENDENCY_TERM; - } - - public MetaRDLTerm(EvaluatableTerm dependingTerm, Resource dependedVariable, MetaRDLTerm argumentTerm) { - super(new Symbol(":", 3), -1, dependingTerm.getSize() + dependedVariable.getSize() + argumentTerm.getSize()); - if(! EvaluatableTerm.class.isAssignableFrom(argumentTerm.getTermType().getBaseTermClass())) { - throw new IllegalTypeException(); - } - addChild(dependingTerm); - addChild(dependedVariable); - addChild(argumentTerm); - this.termType = TermType.META_DEPENDENCY_TERM; + this.isDynamic = true; } public RDLTerm substitute(Map binding) { @@ -161,24 +137,18 @@ } else 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 (dependingTerm instanceof MetaRDLTerm metaDependingTerm) { + dependingTerm = metaDependingTerm.substitute(binding); } - if (dependedVariable instanceof MetaRDLTerm) { - dependedVariable = ((MetaRDLTerm) dependedVariable).substitute(binding); + List terms = new ArrayList<>(); + for (int i = 1; i < getArity(); i++) { + RDLTerm term = (RDLTerm) getChild(i); + if (term instanceof MetaRDLTerm metaTerm) { + term = metaTerm.substitute(binding); + } + terms.add((EvaluatableTerm) term); } - if (argumentTerm instanceof MetaRDLTerm) { - argumentTerm = ((MetaRDLTerm) argumentTerm).substitute(binding); - } - return new DependencyTerm((EvaluatableTerm) dependingTerm, (Resource) dependedVariable, (EvaluatableTerm) argumentTerm); - } else if (isSetTerm()) { - RDLTerm term = (RDLTerm) getChild(0); - if (term instanceof MetaRDLTerm) { - term = ((MetaRDLTerm) term).substitute(binding); - } - return new SetEvaluatableTerm((EvaluatableTerm) term); + return new DependencyTerm((EvaluatableTerm) dependingTerm, terms); } throw new SubstituteFailedException(); } @@ -187,35 +157,112 @@ return false; } - public boolean isMatchedBy(RDLTerm another) { - return isMatchedBy(another, new HashMap<>(), new HashMap<>()); + public Set isMatchedBy(RDLTerm another) { + return isMatchedBy(another, new MatchConstraint(new HashMap<>(), new HashMap<>())); } - public boolean isMatchedBy(RDLTerm another, Map binding, Map orderConstraint) { - if (! another.getClass().isAssignableFrom(this.termType.getBaseTermClass())) { - return false; + public Set isMatchedBy(RDLTerm another, Set constraints) { + Set result = new HashSet<>(); + for (MatchConstraint constraint : constraints) { + result.addAll(isMatchedBy(another, constraint)); } - if (this.getChildren().size() != another.getChildren().size()) { - return false; + return result; + } + + public Set isMatchedBy(RDLTerm another, MatchConstraint constraint) { + Set result = new HashSet<>(); + if (! another.getClass().isAssignableFrom(this.termType.getBaseTermClass())) { + return result; + } + if (!isDynamic && this.getChildren().size() != another.getChildren().size()) { + return result; } if (isDependencyTerm() && (! islinearRightNormalizedMatchedBy(another))) { - return false; + return result; } - for (int i = 0; i < this.getChildren().size(); i++) { - RDLTerm child = (RDLTerm) this.getChild(i); - RDLTerm anotherChild = (RDLTerm) another.getChild(i); - if (child instanceof MetaRDLTerm) { - MetaRDLTerm metaChild = (MetaRDLTerm) child; - if (! metaChild.isMatchedBy(anotherChild, binding, orderConstraint)) { - return false; - } - } else { - if (!(child.equals(anotherChild))) { - return false; - } + RDLTerm dependingChild = (RDLTerm) this.getChild(0); + RDLTerm anotherDependingChild = (RDLTerm) another.getChild(0); + Set res = new HashSet<>(); + if (dependingChild instanceof MetaRDLTerm) { + MetaRDLTerm metaChild = (MetaRDLTerm) dependingChild; + res = metaChild.isMatchedBy(anotherDependingChild, constraint); + } else { + if (!(dependingChild.equals(anotherDependingChild))) { + return result; } } - return true; + if (isDependencyTerm() && !isVariable()) { + for (List perm : Permutation.permutation((another.getChildren().size() - 1) / 2)) { + Set res2 = new HashSet<>(res); + boolean flg = true; + for (int i = 0; i < perm.size(); i++) { + int j = perm.get(i); + TermPair termPair = this.metaDependencyTermGenerator.generate(j, perm.size()); + RDLTerm dependedChild = termPair.dependedTerm(); + RDLTerm argChild = termPair.argTerm(); + RDLTerm anotherDependedChild = (RDLTerm) another.getChild(i * 2 + 1); + RDLTerm anotherArgChild = (RDLTerm) another.getChild(i * 2 + 2); + if (dependedChild instanceof MetaRDLTerm) { + MetaRDLTerm metaChild = (MetaRDLTerm) dependedChild; + res2 = metaChild.isMatchedBy(anotherDependedChild, res2); + if (res2.isEmpty()) { + flg = false; + break; + } + } else { + if (!(dependedChild.equals(anotherDependedChild))) { + flg = false; + break; + } + } + if (argChild instanceof MetaRDLTerm) { + MetaRDLTerm metaChild = (MetaRDLTerm) argChild; + res2 = metaChild.isMatchedBy(anotherArgChild, res2); + if (res2.isEmpty()) { + flg = false; + break; + } + } else { + if (!(argChild.equals(anotherArgChild))) { + flg = false; + break; + } + } + } + if (flg) { + result.addAll(res2); + } + } + return result; + } else if (isDependency() && !isVariable()) { + for (List perm : Permutation.permutation(another.getChildren().size() - 1)) { + Set res2 = new HashSet<>(res); + boolean flg = true; + for (int i = 0; i < perm.size(); i++) { + int j = perm.get(i); + RDLTerm dependedChild = this.metaDependencyGenerator.generate(j, perm.size()); + RDLTerm anotherDependedChild = (RDLTerm) another.getChild(i + 1); + if (dependedChild instanceof MetaRDLTerm) { + MetaRDLTerm metaChild = (MetaRDLTerm) dependedChild; + res2 = metaChild.isMatchedBy(anotherDependedChild, res2); + if (res2.isEmpty()) { + flg = false; + break; + } + } else { + if (!(dependedChild.equals(anotherDependedChild))) { + flg = false; + break; + } + } + } + if (flg) { + result.addAll(res2); + } + } + return result; + } + return result; } public boolean checkTermType(Class clazz) { @@ -234,10 +281,6 @@ return checkTermType(DependencyTerm.class); } - public boolean isSetTerm() { - return checkTermType(SetEvaluatableTerm.class); - } - public boolean isResourceVariable() { return checkTermType(Resource.class); } @@ -273,13 +316,10 @@ public String toString() { switch(termType) { case META_DEPENDENCY: - return "[" + getChild(0).toString() + " : " + getChild(1).toString() + "]"; - case META_DEPENDENCY_LIST: - return "[" + getChild(0).toString() + "]"; + return "[" + getChild(0).toString() + " : " + getChildren().stream().skip(1).map(Expression::toString).collect(Collectors.joining(",")) + "]"; case META_DEPENDENCY_TERM: - return "[" + getChild(0).toString() + " : " + getChild(1).toString() + " -> " + getChild(2).toString() + "]"; - case META_EVALUATABLE_TERM_SET: - return "{" + getChild(0).toString() + "}"; + return "[" + getChild(0).toString() + " : " + IntStream.range(0, (getChildren().size() - 1) / 2) + .mapToObj(i -> getChild(i * 2 + 1).toString() + " -> " + getChild(i * 2 + 2)).collect(Collectors.joining(",")) + "]"; default: return ""; } @@ -328,8 +368,6 @@ 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(Resource.class); @Getter diff --git a/src/main/java/models/terms/meta/MetaResource.java b/src/main/java/models/terms/meta/MetaResource.java index d28b163..6c58980 100644 --- a/src/main/java/models/terms/meta/MetaResource.java +++ b/src/main/java/models/terms/meta/MetaResource.java @@ -1,6 +1,8 @@ package models.terms.meta; +import java.util.HashSet; import java.util.Map; +import java.util.Set; import lombok.Getter; import models.algebra.Constant; @@ -8,8 +10,8 @@ import models.algebra.Symbol; import models.algebra.Variable; import models.terms.RDLTerm; -import models.terms.ResourceConstant; import models.terms.Resource; +import models.terms.ResourceConstant; @Getter public class MetaResource extends MetaVariable { @@ -27,24 +29,29 @@ } @Override - public boolean isMatchedBy(RDLTerm another, Map binding, - Map orderConstraint) { + public Set isMatchedBy(RDLTerm another, MatchConstraint constraint) { + Set result = new HashSet<>(); + Map binding = constraint.getBinding(); + Map orderConstraint = constraint.getOrderConstraint(); if ((! (another instanceof Resource)) && (! (another instanceof ResourceConstant))) { - return false; + return result; } if (! orderConstraintCheck(another, orderConstraint)) { - return false; + return result; } if (! islinearRightNormalizedMatchedBy(another)) { - return false; + return result; } if (! binding.containsKey(this.variableName)) { binding.put(this.variableName, another); - return true; + result.add(new MatchConstraint(binding, orderConstraint)); } - return binding.get(this.variableName).equals(another); + else if (binding.get(this.variableName).equals(another)) { + result.add(new MatchConstraint(binding, orderConstraint)); + } + return result; } } diff --git a/src/main/java/models/terms/meta/MetaVariable.java b/src/main/java/models/terms/meta/MetaVariable.java index 804f1c2..fdad533 100644 --- a/src/main/java/models/terms/meta/MetaVariable.java +++ b/src/main/java/models/terms/meta/MetaVariable.java @@ -1,7 +1,9 @@ package models.terms.meta; import java.util.HashMap; +import java.util.HashSet; import java.util.Map; +import java.util.Set; import exceptions.CoefficientNotOneException; import exceptions.SubstituteFailedException; @@ -74,25 +76,30 @@ } @Override - public boolean isMatchedBy(RDLTerm another, Map binding, - Map orderConstraint) { + public Set isMatchedBy(RDLTerm another, MatchConstraint constraint) { + Set result = new HashSet<>(); + Map binding = constraint.getBinding(); + Map orderConstraint = constraint.getOrderConstraint(); if (! this.termType.getBaseTermClass().isAssignableFrom(another.getClass())) { - return false; + return result; } if (! orderConstraintCheck(another, orderConstraint)) { - return false; + return result; } if (! islinearRightNormalizedMatchedBy(another)) { - return false; + return result; } if (! binding.containsKey(this.variableName)) { binding.put(this.variableName, another); - return true; + result.add(new MatchConstraint(binding, orderConstraint)); } - return binding.get(this.variableName).equals(another); + else if (binding.get(this.variableName).equals(another)) { + result.add(new MatchConstraint(binding, orderConstraint)); + } + return result; } @Override diff --git a/src/main/java/models/terms/meta/OrderVariableConstraint.java b/src/main/java/models/terms/meta/OrderVariableConstraint.java index 7a80c79..10cda04 100644 --- a/src/main/java/models/terms/meta/OrderVariableConstraint.java +++ b/src/main/java/models/terms/meta/OrderVariableConstraint.java @@ -60,6 +60,11 @@ } @Override + public String toString() { + return "[" + lower + ", " + (upper + 1) + ")"; + } + + @Override public Object clone() { OrderVariableConstraint constraint = new OrderVariableConstraint(); constraint.isOk = isOk; diff --git a/src/main/java/utils/Permutation.java b/src/main/java/utils/Permutation.java index 039b9f9..f52227f 100644 --- a/src/main/java/utils/Permutation.java +++ b/src/main/java/utils/Permutation.java @@ -14,6 +14,18 @@ return res; } + public static List> permutation(int i) { + return permutation(0, i); + } + + public static List> permutation(int i, int j) { + List perms = new ArrayList<>(); + for (int ii = i; ii < j; ii++) { + perms.add(ii); + } + return permutation(perms, j - i); + } + private static void permutation(Collection all, int n, List current, Set used, List> result) { if (current.size() == n) { result.add(new ArrayList<>(current)); diff --git a/src/test/java/equivalence/SubstituteTest.java b/src/test/java/equivalence/SubstituteTest.java index b46ea79..10f54d8 100644 --- a/src/test/java/equivalence/SubstituteTest.java +++ b/src/test/java/equivalence/SubstituteTest.java @@ -2,22 +2,16 @@ import org.junit.jupiter.api.Test; -import java.util.HashMap; import java.util.List; -import java.util.Map; 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.Resource; import models.terms.meta.MetaEvaluatableTermVariable; import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaResource; -import models.terms.meta.OrderConstraint; -import models.terms.meta.OrderVariableConstraint; import utils.Utils; public class SubstituteTest { @@ -46,33 +40,33 @@ } } - @Test - void SubstituteTest2() { - MetaEvaluatableTermVariable t = new MetaEvaluatableTermVariable(new Variable("t"), Utils.parse("n + 1")); - t.setLinearRightNormalizedType(LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED); - MetaEvaluatableTermVariable tp = new MetaEvaluatableTermVariable(new Variable("t'"), Utils.parse("n + 1")); - tp.setLinearRightNormalizedType(LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED); - MetaSemanticEquivalenceRelation r1 = new MetaSemanticEquivalenceRelation(t, tp, Utils.parse("n + 1")); - DependencyTerm t1 = new DependencyTerm(A, B, C); - DependencyTerm t2 = new DependencyTerm(Ap, Bp, Cp); - SemanticEquivalenceRelation r2 = new SemanticEquivalenceRelation(t1, t2, 2); - MetaResource v = new MetaResource(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); - } - } +// @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); +// MetaResource v = new MetaResource(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/test/java/formulas/meta/MetaEquationFormulaTest.java b/src/test/java/formulas/meta/MetaEquationFormulaTest.java index e77d072..7bb19eb 100644 --- a/src/test/java/formulas/meta/MetaEquationFormulaTest.java +++ b/src/test/java/formulas/meta/MetaEquationFormulaTest.java @@ -41,7 +41,7 @@ MetaEquationFormula metaFormula = new MetaEquationFormula(left, right); // [a : b -> c] = [a : b -> d] matches [se : v -> te] = [se : v -> ue] - assertTrue(metaFormula.isMatchedBy(formula)); + assertTrue(!metaFormula.isMatchedBy(formula).isEmpty()); } @@ -61,7 +61,7 @@ MetaDependencyFormula metaDepF = new MetaDependencyFormula(dep); //[a : b -> c] : d matches te : w - assertTrue(metaDepF.isMatchedBy(depF)); + assertTrue(! metaDepF.isMatchedBy(depF).isEmpty()); } } diff --git a/src/test/java/rewrite/RewriteInferenceTest.java b/src/test/java/rewrite/RewriteInferenceTest.java new file mode 100644 index 0000000..d9d445b --- /dev/null +++ b/src/test/java/rewrite/RewriteInferenceTest.java @@ -0,0 +1,107 @@ +package rewrite; +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.jupiter.api.Test; + +import java.util.List; + +import inference.rewrite.RewriteInferenceSystem; +import models.formulas.EquationFormula; +import models.formulas.Then; +import models.terms.DependencyTerm; +import models.terms.PrimedTerm; +import models.terms.Resource; +import utils.Utils; + +public class RewriteInferenceTest { + + @Test + void RewriteInferenceTest1() { + Resource totalAmount = new Resource("totalAmount", Utils.INT, 1); + Resource quantity = new Resource("quantity", Utils.INT, 1); + Resource unitPrice = new Resource("unitPrice", Utils.INT, 1); + Resource productId = new Resource("productID", Utils.INT, 1); + Resource productName = new Resource("productName", Utils.INT, 1); + Resource soledProductId = new Resource("soledProductId", Utils.INT, 1); + PrimedTerm totalAmountP = new PrimedTerm(totalAmount); + PrimedTerm quantityP = new PrimedTerm(quantity); + PrimedTerm unitPriceP = new PrimedTerm(unitPrice); + PrimedTerm productIdP = new PrimedTerm(productId); + PrimedTerm productNameP = new PrimedTerm(productName); + PrimedTerm soledProductIdP = new PrimedTerm(soledProductId); + Resource a = new Resource("a", Utils.INT, 0); + Resource b = new Resource("b", Utils.INT, 0); + Resource c = new Resource("c", Utils.INT, 0); + Resource d = new Resource("d", Utils.INT, 0); + Resource e = new Resource("e", Utils.INT, 0); + Resource salesId = new Resource("salesId", Utils.INT, 1); + PrimedTerm salesIdP = new PrimedTerm(salesId); + Resource mul = new Resource("mul", Utils.INT, 1); + Resource mul1= new Resource("mul1", Utils.INT, 1); + Resource mul2 = new Resource("mul2", Utils.INT, 1); + + // reference1 + DependencyTerm te1 = new DependencyTerm(unitPrice, productId, soledProductId); + DependencyTerm te2 = new DependencyTerm(mul, mul1, quantity, mul2, te1); + EquationFormula eq1 = new EquationFormula(totalAmount, te2); + + //reference2 + DependencyTerm te3 = new DependencyTerm(unitPriceP, productIdP, soledProductIdP); + DependencyTerm te4 = new DependencyTerm(mul, mul1, quantityP, mul2, te3); + EquationFormula eq2 = new EquationFormula(totalAmountP, te4); + + //input1 + DependencyTerm te5 = new DependencyTerm(soledProductIdP, salesIdP, a); + EquationFormula eq3 = new EquationFormula(te5, b); + + //input2 + DependencyTerm te6 = new DependencyTerm(quantityP, salesIdP, a); + EquationFormula eq4 = new EquationFormula(te6, c); + + //input3, 4, 5 + EquationFormula eq5 = new EquationFormula(productIdP, productId); + EquationFormula eq6 = new EquationFormula(productNameP, productName); + EquationFormula eq7 = new EquationFormula(unitPriceP, unitPrice); + + // value copy + DependencyTerm te7 = new DependencyTerm(totalAmountP, salesIdP, a); + DependencyTerm te8 = new DependencyTerm(unitPriceP, productIdP, b); + DependencyTerm te9 = new DependencyTerm(mul, mul1, c, mul2, te8); + EquationFormula eq8 = new EquationFormula(te7, te9); + + + //----------------------change value------------------- + //input6 + DependencyTerm te10 = new DependencyTerm(unitPriceP, productIdP, d); + EquationFormula eq9 = new EquationFormula(te10, e); + + //input7, 8, 9, 10 + EquationFormula eq10 = new EquationFormula(productNameP, productName); + EquationFormula eq11 = new EquationFormula(salesIdP, salesId); + EquationFormula eq12 = new EquationFormula(soledProductIdP, soledProductId); + EquationFormula eq13 = new EquationFormula(quantityP, quantity); + + //value copy + EquationFormula eq14 = new EquationFormula(totalAmountP, totalAmount); + + //value copy conclusion + DependencyTerm te11 = new DependencyTerm(totalAmountP, salesIdP, a); + DependencyTerm te12 = new DependencyTerm(totalAmount, salesId, a); + EquationFormula eq15 = new EquationFormula(te11, te12); + + //value copy change value + RewriteInferenceSystem ris = new RewriteInferenceSystem(List.of(eq9, eq10, eq11, eq12, eq13, eq14), eq15); + assertTrue(ris.inference()); + + //reference conclusion + DependencyTerm te13 = new DependencyTerm(soledProductId, salesId, a); + EquationFormula eq16 = new EquationFormula(d, te13); + Then th1 = new Then(eq16, eq15); + + //reference change value + RewriteInferenceSystem ris2 = new RewriteInferenceSystem(List.of(eq1, eq2, eq9, eq10, eq11, eq12, eq13), th1); + + assertFalse(ris2.inference()); + } + +} diff --git a/src/test/java/terms/DependencyTermTest.java b/src/test/java/terms/DependencyTermTest.java new file mode 100644 index 0000000..39835cf --- /dev/null +++ b/src/test/java/terms/DependencyTermTest.java @@ -0,0 +1,178 @@ +package terms; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.jupiter.api.Test; + +import java.util.HashMap; +import java.util.Map; +import java.util.Set; + +import models.algebra.Variable; +import models.terms.DependencyTerm; +import models.terms.RDLTerm; +import models.terms.Resource; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDependencyTermGenerator; +import models.terms.meta.MetaDependencyTermGenerator.TermPair; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaResource; +import models.terms.meta.OrderVariableConstraint; +import utils.Utils; + +public class DependencyTermTest { + + Resource a = new Resource("a", Utils.INT, 1); + Resource b = new Resource("b", Utils.INT, 1); + Resource c = new Resource("c", Utils.INT, 1); + Resource d = new Resource("d", Utils.INT, 1); + Resource e = new Resource("e", Utils.INT, 1); + Resource f = new Resource("f", Utils.INT, 1); + Resource g = new Resource("g", Utils.INT, 1); + + @Test + void EqualsTest() { + DependencyTerm t1 = new DependencyTerm(a, b, c); + DependencyTerm t2 = new DependencyTerm(a, b, c); + assertEquals(t1, t2); + + DependencyTerm t3 = new DependencyTerm(a, b, c, b, c); + assertEquals(t1, t3); + + DependencyTerm t4 = new DependencyTerm(a, c, b); + assertFalse(t1.equals(t4)); + + DependencyTerm t5 = new DependencyTerm(a, b, c, d, e); + DependencyTerm t6 = new DependencyTerm(a, d, e, b, c); + DependencyTerm t7 = new DependencyTerm(a, b, e, d, c); + assertEquals(t5, t6); + assertFalse(t5.equals(t7)); + + DependencyTerm t8 = new DependencyTerm(t1, t5, t6); + DependencyTerm t9 = new DependencyTerm(t1, t6, t5); + assertEquals(t8, t9); + + } + + @Test + void MatchTest() { + DependencyTerm t1 = new DependencyTerm(a, b, c, d, e); + DependencyTerm t2 = new DependencyTerm(a, g, f, b, c); + MetaResource x = new MetaResource(new Variable("x")); + MetaResource y = new MetaResource(new Variable("y")); + MetaResource z = new MetaResource(new Variable("z")); + MetaResource w = new MetaResource(new Variable("w")); + MetaResource p = new MetaResource(new Variable("p")); + MetaResource o = new MetaResource(new Variable("o")); + MetaResource n = new MetaResource(new Variable("n")); + MetaRDLTerm mt1 = new MetaRDLTerm(x, y, z, w, p); + MetaRDLTerm mt2 = new MetaRDLTerm(x, w, p, y, z); + MetaRDLTerm mt3 = new MetaRDLTerm(x, p, w, y, z); + MetaRDLTerm mt4 = new MetaRDLTerm(x, n, o, w, p); + Map binding = new HashMap<>(); + Map orderConstraint = new HashMap<>(); + Map correctBinding = new HashMap<>(); + correctBinding.put(x.getVariableName(), a); + correctBinding.put(y.getVariableName(), d); + correctBinding.put(z.getVariableName(), e); + correctBinding.put(w.getVariableName(), b); + correctBinding.put(p.getVariableName(), c); + mt4.toString(); + Set tmp = mt1.isMatchedBy(t1, new MatchConstraint(binding, orderConstraint)); + assertTrue(! tmp.isEmpty()); + tmp = mt2.isMatchedBy(t1, tmp); + assertTrue(! tmp.isEmpty()); + assertFalse(! mt3.isMatchedBy(t1, tmp).isEmpty()); + assertTrue(! mt4.isMatchedBy(t2, tmp).isEmpty()); + RDLTerm t = mt1.substitute(tmp.iterator().next().getBinding()); + assertEquals(t, t1); + } + + @Test + void MatchTest2() { + MetaResource x = new MetaResource(new Variable("x")); + MetaResource y = new MetaResource(new Variable("y")); + MetaResource z = new MetaResource(new Variable("z")); + MetaResource v = new MetaResource(new Variable("v")); + MetaResource w = new MetaResource(new Variable("w")); + MetaResource p = new MetaResource(new Variable("p")); + MetaResource q = new MetaResource(new Variable("q")); + + DependencyTerm t1 = new DependencyTerm(a, b, c, d, e); + DependencyTerm t2 = new DependencyTerm(a, d, e, f, g); + MetaRDLTerm mt1 = new MetaRDLTerm(x, p, q, v, w); + MetaRDLTerm mt2 = new MetaRDLTerm(x, v, w, y, z); + Map binding = new HashMap<>(); + Map orderConstraint = new HashMap<>(); + Set tmp = mt1.isMatchedBy(t1, new MatchConstraint(binding, orderConstraint)); + assertTrue(! tmp.isEmpty()); + tmp = mt2.isMatchedBy(t2, tmp); + assertTrue(! tmp.isEmpty()); + } + + @Test + void MatchTest3() { + DependencyTerm t1 = new DependencyTerm(a, b, c, d, e); + DependencyTerm t2 = new DependencyTerm(c, f, g); + MetaResource o = new MetaResource(new Variable("o")); + MetaResource p = new MetaResource(new Variable("p")); + MetaResource q = new MetaResource(new Variable("q")); + MetaResource r = new MetaResource(new Variable("r")); + MetaResource s = new MetaResource(new Variable("s")); + MetaResource t = new MetaResource(new Variable("t")); + MetaResource u = new MetaResource(new Variable("u")); + MetaRDLTerm mt1 = new MetaRDLTerm(o, p, q, r, s); + MetaRDLTerm mt2 = new MetaRDLTerm(s, t, u); + Set tmp = mt1.isMatchedBy(t1); + assertTrue(! tmp.isEmpty()); + tmp = mt2.isMatchedBy(t2, tmp); + assertTrue(! tmp.isEmpty()); + } + + @Test + void DynamicMatchTest() { + Resource a1 = new Resource("a1", Utils.INT, 3); + Resource a2 = new Resource("a2", Utils.INT, 1); + Resource a3 = new Resource("a3", Utils.INT, 4); + Resource a4 = new Resource("a4", Utils.INT, 2); + Resource a5 = new Resource("a5", Utils.INT, 4); + DependencyTerm t1 = new DependencyTerm(a1, a2, a3, a4, a5); + MetaResource x = new MetaResource(new Variable("x"), new Variable("n")); + MetaRDLTerm mt1 = new MetaRDLTerm(x, + (MetaDependencyTermGenerator) (i, j) -> + new TermPair( + new MetaResource(new Variable("x" + (2*i + 1)), Utils.parse("n-1-" + i)), + new MetaResource(new Variable("x" + (2*i + 2)), Utils.parse("n+1")) + ) + ); + Set tmp = mt1.isMatchedBy(t1); + System.out.println(tmp); + + assertTrue(! tmp.isEmpty()); + } + + @Test + void DynamicMatchTest2() { + MetaResource x = new MetaResource(new Variable("x")); + MetaRDLTerm mt1 = new MetaRDLTerm(x, (MetaDependencyTermGenerator) (i, j) -> new TermPair(new MetaResource(new Variable("x" + i)), new MetaResource(new Variable("y"+i)))); + DependencyTerm d1 = new DependencyTerm(a, b, c); + DependencyTerm d2 = new DependencyTerm(a, b, c, d, e); + assertTrue(! mt1.isMatchedBy(d1).isEmpty()); + assertTrue(! mt1.isMatchedBy(d2).isEmpty()); + } + + @Test + void OrderTest() { + Resource text = new Resource("text", Utils.INT, 2); + Resource wNo = new Resource("wNo", Utils.INT, 2); + Resource v = new Resource("v", Utils.INT, 1); + Resource scId = new Resource("scId", Utils.INT, 1); + Resource curScId = new Resource("curScId", Utils.INT, 0); + Resource curWNo = new Resource("curWNo", Utils.INT, 1); + + DependencyTerm t1 = new DependencyTerm(text, wNo, v); + DependencyTerm t2 = new DependencyTerm(t1, scId, curScId, v, curWNo); + assertEquals(t2.getOrder(), 1); + } + +} diff --git a/src/test/java/terms/DependencyTest.java b/src/test/java/terms/DependencyTest.java new file mode 100644 index 0000000..916c3b1 --- /dev/null +++ b/src/test/java/terms/DependencyTest.java @@ -0,0 +1,121 @@ +package terms; +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.jupiter.api.Test; + +import java.util.HashMap; +import java.util.HashSet; +import java.util.Map; +import java.util.Set; + +import exceptions.SyntaxException; +import models.algebra.Variable; +import models.terms.Dependency; +import models.terms.RDLTerm; +import models.terms.Resource; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaResource; +import models.terms.meta.OrderVariableConstraint; +import utils.Utils; + +public class DependencyTest { + + Resource a = new Resource("a", Utils.INT, 1); + Resource b = new Resource("b", Utils.INT, 1); + Resource c = new Resource("c", Utils.INT, 1); + Resource d = new Resource("d", Utils.INT, 2); + Resource e = new Resource("e", Utils.INT, 1); + Resource f = new Resource("f", Utils.INT, 1); + + @Test + void EqualsTest() { + + Dependency d1 = new Dependency(a, b); + Dependency d2 = new Dependency(a, b, b); + assertEquals(d1, d2); + + Dependency d3 = new Dependency(a, c); + assertFalse(d1.equals(d3)); + + Dependency d4 = new Dependency(a, b, c); + Dependency d5 = new Dependency(a, c, b); + assertEquals(d4, d5); + + Dependency d6 = new Dependency(b, a); + assertFalse(d1.equals(d6)); + } + + @Test + void OrderTest() { + + assertThrows(SyntaxException.class, () -> { + new Dependency(d, a); + }); + + assertThrows(SyntaxException.class, () -> { + new Dependency(a, b, d); + }); + + Dependency d1 = new Dependency(a, b); + assertEquals(d1.getOrder(), 1); + assertEquals(d1.getTermOrder(), 0); + + Dependency d2 = new Dependency(a, d); + assertEquals(d2.getOrder(), 2); + assertEquals(d2.getTermOrder(), 1); + + Dependency d3 = new Dependency(a, b, c); + assertEquals(d3.getOrder(), 1); + } + + @Test + void StringTest() { + Dependency d1 = new Dependency(a, b); + assertEquals(d1.toString(), "a : b"); + + Dependency d2 = new Dependency(a, b, c); + assertEquals(d2.toString(), "a : b, c"); + + Dependency d3 = new Dependency(a, c, b); + assertEquals(d3.toString(), "a : b, c"); + } + + @Test + void MatchTest() { + MetaResource p = new MetaResource(new Variable("p")); + MetaResource q = new MetaResource(new Variable("q")); + MetaResource r = new MetaResource(new Variable("r")); + MetaResource s = new MetaResource(new Variable("s")); + MetaResource t = new MetaResource(new Variable("t")); + + MetaRDLTerm mt1 = new MetaRDLTerm(p, q); + MetaRDLTerm mt2 = new MetaRDLTerm(p, Set.of(q, r, s)); + MetaRDLTerm mt3 = new MetaRDLTerm(p, Set.of(r, q, s)); + MetaRDLTerm mt4 = new MetaRDLTerm(p, Set.of(s, r, q)); + + Dependency d1 = new Dependency(a, b); + Dependency d2 = new Dependency(a, b, c, f); + Dependency d3 = new Dependency(a, f, c, b); + Dependency d4 = new Dependency(a, b, f, c); + Dependency d5 = new Dependency(a, b, e, f); + + + Map binding = new HashMap<>(); + Map orderConst = new HashMap<>(); + Set tmp = new HashSet<>(); + tmp = mt1.isMatchedBy(d1, new MatchConstraint(binding, orderConst)); + assertTrue(! tmp.isEmpty()); + assertEquals(tmp.iterator().next().getBinding().get(p.getVariableName()), a); + assertEquals(tmp.iterator().next().getBinding().get(q.getVariableName()), b); + tmp = mt2.isMatchedBy(d2, new MatchConstraint(binding, orderConst)); + assertTrue(!tmp.isEmpty()); + tmp = mt3.isMatchedBy(d2, tmp); + assertTrue(!tmp.isEmpty()); + tmp = mt4.isMatchedBy(d2, tmp); + assertTrue(!tmp.isEmpty()); + tmp = mt4.isMatchedBy(d5, tmp); + assertFalse(!tmp.isEmpty()); + } + +} diff --git a/src/test/java/terms/OrderTest.java b/src/test/java/terms/OrderTest.java index 930c154..57ee41b 100644 --- a/src/test/java/terms/OrderTest.java +++ b/src/test/java/terms/OrderTest.java @@ -40,14 +40,8 @@ DependencyTerm t1 = new DependencyTerm(A, B, C, D, E); assertEquals(t1.getOrder(), 1); - DependencyTerm t2 = new DependencyTerm(A, B, C, D, F); - assertEquals(t2.getOrder(), 2); - - DependencyTerm t3 = new DependencyTerm(A, B, C, D, G); - assertEquals(t3.getOrder(), 1); - assertThrows(RuntimeException.class, () -> { - new DependencyTerm(A, B, C, G, D); + new DependencyTerm(A, B, C, D, G); }); } diff --git a/src/test/java/terms/meta/MetaDependencyVariableTest.java b/src/test/java/terms/meta/MetaDependencyVariableTest.java index e04205f..1d47997 100644 --- a/src/test/java/terms/meta/MetaDependencyVariableTest.java +++ b/src/test/java/terms/meta/MetaDependencyVariableTest.java @@ -21,18 +21,15 @@ Resource b = new Resource("b", INT, 1); Resource c = new Resource("c", INT, 1); Dependency dep1 = new Dependency(a, b); - Dependency dep2 = new Dependency(dep1); DependencyTerm te1 = new DependencyTerm(a, b, c); MetaDependencyVariable d = new MetaDependencyVariable(new Variable("d")); // [a : b] mathces d(dependency) - assertTrue(d.isMatchedBy(dep1)); - // [[a : b]] mathces d(dependency) - assertTrue(d.isMatchedBy(dep2)); + assertTrue(! d.isMatchedBy(dep1).isEmpty()); // a does not mathc d(dependency) - assertFalse(d.isMatchedBy(a)); + assertFalse(! d.isMatchedBy(a).isEmpty()); // [a : b -> c] does not mathc d(dependency) - assertFalse(d.isMatchedBy(te1)); + assertFalse(! d.isMatchedBy(te1).isEmpty()); } @Test @@ -45,9 +42,9 @@ MetaDependencyVariable d = new MetaDependencyVariable(new Variable("d"), new Constant("1")); // [a : b](1) mathces d(=1) - assertTrue(d.isMatchedBy(dep1)); + assertTrue(! d.isMatchedBy(dep1).isEmpty()); // [a : c](2) does not mathc d(=1) - assertFalse(d.isMatchedBy(dep2)); + assertFalse(! d.isMatchedBy(dep2).isEmpty()); } @Test @@ -62,11 +59,11 @@ MetaDependencyVariable d = new MetaDependencyVariable(new Variable("d"), OrderConstraint.LT, new Constant("1")); // [a : b](1) does not match d(<1) - assertFalse(d.isMatchedBy(dep1)); + assertFalse(! d.isMatchedBy(dep1).isEmpty()); // [a : c](2) does not match d(<1) - assertFalse(d.isMatchedBy(dep2)); + assertFalse(! d.isMatchedBy(dep2).isEmpty()); // [a : e](0) matches d(<1) - assertTrue(d.isMatchedBy(dep3)); + assertTrue(! d.isMatchedBy(dep3).isEmpty()); } @Test @@ -81,11 +78,11 @@ MetaDependencyVariable d = new MetaDependencyVariable(new Variable("d"), OrderConstraint.LE, new Constant("1")); // [a : b](1) matches d(<=1) - assertTrue(d.isMatchedBy(dep1)); + assertTrue(! d.isMatchedBy(dep1).isEmpty()); // [a : c](2) does not match d(<=1) - assertFalse(d.isMatchedBy(dep2)); + assertFalse(! d.isMatchedBy(dep2).isEmpty()); // [a : e](0) matches d(<=1) - assertTrue(d.isMatchedBy(dep3)); + assertTrue(! d.isMatchedBy(dep3).isEmpty()); } @Test @@ -100,11 +97,11 @@ MetaDependencyVariable d = new MetaDependencyVariable(new Variable("d"), OrderConstraint.GT, new Constant("1")); // [a : b](1) does not match d(>1) - assertFalse(d.isMatchedBy(dep1)); + assertFalse(! d.isMatchedBy(dep1).isEmpty()); // [a : c](2) matches d(>1) - assertTrue(d.isMatchedBy(dep2)); + assertTrue(! d.isMatchedBy(dep2).isEmpty()); // [a : e](0) does not match d(>1) - assertFalse(d.isMatchedBy(dep3)); + assertFalse(! d.isMatchedBy(dep3).isEmpty()); } @Test @@ -119,11 +116,11 @@ MetaDependencyVariable d = new MetaDependencyVariable(new Variable("d"), OrderConstraint.GE, new Constant("1")); // [a : b](1) matches d(>=1) - assertTrue(d.isMatchedBy(dep1)); + assertTrue(! d.isMatchedBy(dep1).isEmpty()); // [a : c](2) matches d(>=1) - assertTrue(d.isMatchedBy(dep2)); + assertTrue(! d.isMatchedBy(dep2).isEmpty()); // [a : e](0) does not match d(>=1) - assertFalse(d.isMatchedBy(dep3)); + assertFalse(! d.isMatchedBy(dep3).isEmpty()); } } diff --git a/src/test/java/terms/meta/MetaEvaluatableTermVariableTest.java b/src/test/java/terms/meta/MetaEvaluatableTermVariableTest.java index 804a07f..9c2e9c5 100644 --- a/src/test/java/terms/meta/MetaEvaluatableTermVariableTest.java +++ b/src/test/java/terms/meta/MetaEvaluatableTermVariableTest.java @@ -24,9 +24,9 @@ ResourceConstant one = new ResourceConstant("1"); DependencyTerm t1 = new DependencyTerm(a, b, c); - assertTrue(se.isMatchedBy(a)); - assertTrue(se.isMatchedBy(one)); - assertTrue(se.isMatchedBy(t1)); + assertTrue(! se.isMatchedBy(a).isEmpty()); + assertTrue(! se.isMatchedBy(one).isEmpty()); + assertTrue(! se.isMatchedBy(t1).isEmpty()); } } diff --git a/src/test/java/terms/meta/MetaRDLTermTest.java b/src/test/java/terms/meta/MetaRDLTermTest.java index 0aca615..9570299 100644 --- a/src/test/java/terms/meta/MetaRDLTermTest.java +++ b/src/test/java/terms/meta/MetaRDLTermTest.java @@ -35,15 +35,15 @@ MetaRDLTerm metaDep4 = new MetaRDLTerm(metaTe, v3); //[a : b] matches [v1 : v2] - assertTrue(metaDep.isMatchedBy(dep1)); + assertTrue(! metaDep.isMatchedBy(dep1).isEmpty()); //[[a : b -> c] : b] does not match [v1 : v2] - assertFalse(metaDep.isMatchedBy(dep2)); + assertFalse(! metaDep.isMatchedBy(dep2).isEmpty()); //[[a : b -> c] : b] matches [vte : v2] - assertTrue(metaDep2.isMatchedBy(dep2)); + assertTrue(! metaDep2.isMatchedBy(dep2).isEmpty()); //[[a : b -> c] : b] matches [[v1 : v2 -> v3] : v2] - assertTrue(metaDep3.isMatchedBy(dep2)); + assertTrue(! metaDep3.isMatchedBy(dep2).isEmpty()); //[[a : b -> c] : b] does not match [[v1 : v2 -> v3] : v3] - assertFalse(metaDep4.isMatchedBy(dep2)); + assertFalse(! metaDep4.isMatchedBy(dep2).isEmpty()); } @Test @@ -56,12 +56,12 @@ Resource a2 = new Resource("a2", INT, 2); Dependency d1 = new Dependency(a1, a2); //[1 : 2] matches [1 : 2] - assertTrue(vd1.isMatchedBy(d1)); + assertTrue(! vd1.isMatchedBy(d1).isEmpty()); Resource b1 = new Resource("b1", INT, 1); Dependency d2 = new Dependency(a1, b1); //[1 : 1] does not match [1 : 2] - assertFalse(vd1.isMatchedBy(d2)); + assertFalse(! vd1.isMatchedBy(d2).isEmpty()); } @Test @@ -82,17 +82,17 @@ Dependency d3 = new Dependency(new Dependency(a1, b1), a2); Dependency d4 = new Dependency(new Dependency(a1, a2), b2); //[1 : 2] does not match [x : x] - assertFalse(vd1.isMatchedBy(d1)); + assertFalse(! vd1.isMatchedBy(d1).isEmpty()); //[1 : 1] matches [x : x] - assertTrue(vd1.isMatchedBy(d2)); + assertTrue(! vd1.isMatchedBy(d2).isEmpty()); //[1 : 2] matches [x : y] - assertTrue(vd2.isMatchedBy(d1)); + assertTrue(! vd2.isMatchedBy(d1).isEmpty()); //[1 : 1] matches [x : y] - assertTrue(vd2.isMatchedBy(d2)); + assertTrue(! vd2.isMatchedBy(d2).isEmpty()); //[[1 : 1] : 2] does not match [[y : x] : x] - assertFalse(vd3.isMatchedBy(d3)); + assertFalse(! vd3.isMatchedBy(d3).isEmpty()); //[[1 : 2] : 2] matches [[y : x] : x] - assertTrue(vd3.isMatchedBy(d4)); + assertTrue(! vd3.isMatchedBy(d4).isEmpty()); } } diff --git a/src/test/java/terms/meta/MetaResourceVariableTest.java b/src/test/java/terms/meta/MetaResourceVariableTest.java index f076729..5dd30dc 100644 --- a/src/test/java/terms/meta/MetaResourceVariableTest.java +++ b/src/test/java/terms/meta/MetaResourceVariableTest.java @@ -32,19 +32,19 @@ MetaRDLTermVariable t = new MetaRDLTermVariable(new Variable("t")); // a matches x(resource variable) - assertTrue(x.isMatchedBy(a)); + assertTrue(! x.isMatchedBy(a).isEmpty()); // a does not match d(dependency) - assertFalse(d.isMatchedBy(a)); + assertFalse(! d.isMatchedBy(a).isEmpty()); // a does not match dte(dependency term) - assertFalse(dte.isMatchedBy(a)); + assertFalse(! dte.isMatchedBy(a).isEmpty()); // a matches te(evaluatable term) - assertTrue(te.isMatchedBy(a)); + assertTrue(! te.isMatchedBy(a).isEmpty()); // a matches t(term) - assertTrue(t.isMatchedBy(a)); + assertTrue(! t.isMatchedBy(a).isEmpty()); // [a : b] does not match x(resource variable) - assertFalse(x.isMatchedBy(dep)); + assertFalse(! x.isMatchedBy(dep).isEmpty()); // [a : b -> c] does not match x(resource variable) - assertFalse(x.isMatchedBy(depTerm)); + assertFalse(! x.isMatchedBy(depTerm).isEmpty()); } @Test @@ -53,9 +53,9 @@ MetaResource x = new MetaResource(new Variable("x"), parse("0")); MetaResource y = new MetaResource(new Variable("y"), parse("1")); //a(1) does not match x(=0) - assertFalse(x.isMatchedBy(a)); + assertFalse(! x.isMatchedBy(a).isEmpty()); //a(1) matches y(=1) - assertTrue(y.isMatchedBy(a)); + assertTrue(! y.isMatchedBy(a).isEmpty()); } @Test @@ -65,11 +65,11 @@ MetaResource y = new MetaResource(new Variable("y"), OrderConstraint.LT, parse("1")); MetaResource z = new MetaResource(new Variable("z"), OrderConstraint.LT, parse("2")); //a(1) does not match x(<0) - assertFalse(x.isMatchedBy(a)); + assertFalse(! x.isMatchedBy(a).isEmpty()); //a(1) matches y(<1) - assertFalse(y.isMatchedBy(a)); + assertFalse(! y.isMatchedBy(a).isEmpty()); //a(1) matches z(<2) - assertTrue(z.isMatchedBy(a)); + assertTrue(! z.isMatchedBy(a).isEmpty()); } @Test @@ -79,11 +79,11 @@ MetaResource y = new MetaResource(new Variable("y"), OrderConstraint.LE, parse("1")); MetaResource z = new MetaResource(new Variable("z"), OrderConstraint.LE, parse("2")); //a(1) does not match x(<=0) - assertFalse(x.isMatchedBy(a)); + assertFalse(! x.isMatchedBy(a).isEmpty()); //a(1) matches y(<=1) - assertTrue(y.isMatchedBy(a)); + assertTrue(! y.isMatchedBy(a).isEmpty()); //a(1) matches z(<=2) - assertTrue(z.isMatchedBy(a)); + assertTrue(! z.isMatchedBy(a).isEmpty()); } @Test @@ -93,11 +93,11 @@ MetaResource y = new MetaResource(new Variable("y"), OrderConstraint.GT, parse("1")); MetaResource z = new MetaResource(new Variable("z"), OrderConstraint.GT, parse("2")); //a(1) does not match x(>0) - assertTrue(x.isMatchedBy(a)); + assertTrue(! x.isMatchedBy(a).isEmpty()); //a(1) matches y(>1) - assertFalse(y.isMatchedBy(a)); + assertFalse(! y.isMatchedBy(a).isEmpty()); //a(1) matches z(>2) - assertFalse(z.isMatchedBy(a)); + assertFalse(! z.isMatchedBy(a).isEmpty()); } @Test @@ -107,11 +107,11 @@ MetaResource y = new MetaResource(new Variable("y"), OrderConstraint.GE, parse("1")); MetaResource z = new MetaResource(new Variable("z"), OrderConstraint.GE, parse("2")); //a(1) does not match x(>=0) - assertTrue(x.isMatchedBy(a)); + assertTrue(! x.isMatchedBy(a).isEmpty()); //a(1) matches y(>=1) - assertTrue(y.isMatchedBy(a)); + assertTrue(! y.isMatchedBy(a).isEmpty()); //a(1) matches z(>2) - assertFalse(z.isMatchedBy(a)); + assertFalse(! z.isMatchedBy(a).isEmpty()); } @Test @@ -120,7 +120,7 @@ MetaResource x = new MetaResource(new Variable("x"), parse("x")); //a(0) matches x(=x) - assertTrue(x.isMatchedBy(a)); + assertTrue(! x.isMatchedBy(a).isEmpty()); } @Test @@ -129,7 +129,7 @@ MetaResource x = new MetaResource(new Variable("x"), OrderConstraint.LT, parse("x")); //a(2) matches x(x) - assertTrue(x.isMatchedBy(a)); + assertTrue(! x.isMatchedBy(a).isEmpty()); } @Test @@ -156,7 +156,7 @@ MetaResource x = new MetaResource(new Variable("x"), OrderConstraint.GE, parse("x")); //a(2) matches x( 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)); + Set result = metaTerm1.isMatchedBy(t1); + for (MatchConstraint constraint: result) { + RDLTerm assignedTerm = metaTerm1.substitute(constraint.getBinding()); + assertEquals(t1, assignedTerm); + } + result = metaTerm1.isMatchedBy(t2); + for (MatchConstraint constraint: result) { + RDLTerm assignedTerm = metaTerm1.substitute(constraint.getBinding()); + assertEquals(t2, assignedTerm); + } } }