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/models/formulas/meta/MetaDependencyFormula.java b/src/main/java/models/formulas/meta/MetaDependencyFormula.java index 68f9888..d16b9fa 100644 --- a/src/main/java/models/formulas/meta/MetaDependencyFormula.java +++ b/src/main/java/models/formulas/meta/MetaDependencyFormula.java @@ -1,6 +1,7 @@ package models.formulas.meta; import java.util.Map; +import java.util.Set; import exceptions.IllegalTypeException; import lombok.Getter; @@ -11,7 +12,6 @@ import models.terms.RDLTerm; import models.terms.meta.MetaDependencyVariable; import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaResource; import models.terms.meta.OrderVariableConstraint; @Getter @@ -30,8 +30,8 @@ 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); } @Override diff --git a/src/main/java/models/terms/DependencyTerm.java b/src/main/java/models/terms/DependencyTerm.java index 2a1ac1f..20c6882 100644 --- a/src/main/java/models/terms/DependencyTerm.java +++ b/src/main/java/models/terms/DependencyTerm.java @@ -29,12 +29,12 @@ boolean argOrderType = terms.get(0).getOrder() <= terms.get(1).getOrder(); if (argOrderType) { this.order = terms.get(1).getOrder(); - if (dependingTerm.getOrder() > getOrder() + 1) { + if (dependingTerm.getOrder() > getOrder()) { throw new SyntaxException("order invalid"); } } else { this.order = terms.get(0).getOrder() - 1; - if (dependingTerm.getOrder() > getOrder()) { + if (dependingTerm.getOrder() > terms.get(0).getOrder()) { throw new SyntaxException("order invalid"); } } 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 1d11c02..3353cb2 100644 --- a/src/main/java/models/terms/meta/MetaRDLTerm.java +++ b/src/main/java/models/terms/meta/MetaRDLTerm.java @@ -1,11 +1,18 @@ package models.terms.meta; +import java.util.ArrayList; +import java.util.Arrays; import java.util.Collection; import java.util.HashMap; +import java.util.List; import java.util.Map; +import java.util.Set; +import java.util.TreeMap; +import java.util.TreeSet; import exceptions.IllegalTypeException; import exceptions.SubstituteFailedException; +import exceptions.SyntaxException; import lombok.Getter; import models.algebra.Symbol; import models.algebra.Variable; @@ -15,7 +22,6 @@ import models.terms.LinearRightNormalizedType; import models.terms.RDLTerm; import models.terms.Resource; -import models.terms.SetEvaluatableTerm; @Getter public class MetaRDLTerm extends RDLTerm { @@ -32,106 +38,58 @@ } //dependency - public MetaRDLTerm(RDLTerm dependingTerm, MetaResource dependedVariable) { - super(new Symbol(":", 2), dependedVariable.getOrder(), dependingTerm.getSize() + dependedVariable.getSize()); + public MetaRDLTerm(MetaRDLTerm dependingTerm, TreeSet dependedTerms) { + super(new Symbol(":", 1 + dependedTerms.size()), -1, -1); + int size = dependingTerm.getSize(); addChild(dependingTerm); - addChild(dependedVariable); + for (MetaRDLTerm dependedTerm: dependedTerms) { + addChild(dependedTerm); + size += dependedTerm.getSize(); + } + this.size = size; 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; + public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaRDLTerm dependedTerm) { + this(dependingTerm, new TreeSet<>(Set.of(dependedTerm))); } //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); + } + for (MetaRDLTerm dependedTerm: sortedTerms.keySet()) { + MetaRDLTerm argTerm = sortedTerms.get(dependedTerm); + addChild(dependedTerm); + addChild(argTerm); + } + this.size = size; this.termType = TermType.META_DEPENDENCY_TERM; } - 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, 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(); - } - addChild(dependingTerm); - addChild(dependedVariable); - addChild(argumentTerm); - 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; + public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaRDLTerm ...terms) { + this(dependingTerm, Arrays.asList(terms)); } public RDLTerm substitute(Map binding) { @@ -149,25 +107,32 @@ } } 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 (dependedVariable instanceof MetaRDLTerm) { +// dependedVariable = ((MetaRDLTerm) dependedVariable).substitute(binding); +// } +// if (argumentTerm instanceof MetaRDLTerm) { +// argumentTerm = ((MetaRDLTerm) argumentTerm).substitute(binding); +// } +// return new DependencyTerm((EvaluatableTerm) dependingTerm, (Resource) dependedVariable, (EvaluatableTerm) argumentTerm); 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(); } @@ -223,10 +188,6 @@ return checkTermType(DependencyTerm.class); } - public boolean isSetTerm() { - return checkTermType(SetEvaluatableTerm.class); - } - public boolean isResourceVariable() { return checkTermType(Resource.class); } @@ -267,8 +228,6 @@ return "[" + getChild(0).toString() + "]"; case META_DEPENDENCY_TERM: return "[" + getChild(0).toString() + " : " + getChild(1).toString() + " -> " + getChild(2).toString() + "]"; - case META_EVALUATABLE_TERM_SET: - return "{" + getChild(0).toString() + "}"; default: return ""; } @@ -317,8 +276,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/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/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/DependencyTermTest.java b/src/test/java/terms/meta/DependencyTermTest.java index 993f94b..a97bd9f 100644 --- a/src/test/java/terms/meta/DependencyTermTest.java +++ b/src/test/java/terms/meta/DependencyTermTest.java @@ -4,8 +4,16 @@ import org.junit.jupiter.api.Test; +import java.util.HashMap; +import java.util.Map; + +import models.algebra.Variable; import models.terms.DependencyTerm; +import models.terms.RDLTerm; import models.terms.Resource; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaResource; +import models.terms.meta.OrderVariableConstraint; import utils.Utils; public class DependencyTermTest { @@ -40,4 +48,23 @@ } + @Test + void MatchTest() { + DependencyTerm t1 = new DependencyTerm(a, b, c, d, e); + 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")); + 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); + Map binding = new HashMap<>(); + Map orderConstraint = new HashMap<>(); + assertTrue(mt1.isMatchedBy(t1, binding, orderConstraint)); + assertTrue(mt2.isMatchedBy(t1, binding, orderConstraint)); + assertFalse(mt3.isMatchedBy(t1, binding, orderConstraint)); + RDLTerm t = mt1.substitute(binding); + assertEquals(t, t1); + } } diff --git a/src/test/java/terms/meta/MetaDependencyVariableTest.java b/src/test/java/terms/meta/MetaDependencyVariableTest.java index e04205f..b6df427 100644 --- a/src/test/java/terms/meta/MetaDependencyVariableTest.java +++ b/src/test/java/terms/meta/MetaDependencyVariableTest.java @@ -21,14 +21,11 @@ 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)); // a does not mathc d(dependency) assertFalse(d.isMatchedBy(a)); // [a : b -> c] does not mathc d(dependency)