diff --git a/src/inference/InferenceOrderConstraint.java b/src/inference/InferenceOrderConstraint.java new file mode 100644 index 0000000..6c789e9 --- /dev/null +++ b/src/inference/InferenceOrderConstraint.java @@ -0,0 +1,83 @@ +package inference; +import java.util.Map; + +import exceptions.IllegalTypeException; +import lombok.Getter; +import models.algebra.Constant; +import models.algebra.Expression; +import models.algebra.Variable; +import models.terms.meta.OrderConstraint; +import models.terms.meta.OrderVariableConstraint; + +@Getter +public class InferenceOrderConstraint { + + private final Variable leftSideHandVariable; + private final int leftSideHandConstant; + private final OrderConstraint operator; + private final Variable rightSideHandVariable; + private final int rightSideHandConstant; + + public InferenceOrderConstraint(Expression left, OrderConstraint operator, Expression right) { + if ((left instanceof Constant) && (right instanceof Constant)) { + throw new IllegalTypeException("Both left and right can't be Constant"); + } + if (left instanceof Constant) { + leftSideHandConstant = Integer.parseInt(((Constant) left).toString()); + leftSideHandVariable = null; + } else if (left instanceof Variable) { + leftSideHandConstant = -1; + leftSideHandVariable = (Variable) left; + } else { + throw new IllegalTypeException("Left must be Constant or Variable"); + } + + this.operator = operator; + + if (right instanceof Constant) { + rightSideHandConstant = Integer.parseInt(((Constant) right).toString()); + rightSideHandVariable = null; + } else if (right instanceof Variable) { + rightSideHandConstant = -1; + rightSideHandVariable = (Variable) right; + } else { + throw new IllegalTypeException("Right must be Constant or Variable"); + } + } + + public boolean check(Map orderConstraints) { + switch(this.operator) { + case EQ: + return getLeftValue(orderConstraints) == getRightValue(orderConstraints); + case GE: + return getLeftValue(orderConstraints) >= getRightValue(orderConstraints); + case GT: + return getLeftValue(orderConstraints) > getRightValue(orderConstraints); + case LE: + return getLeftValue(orderConstraints) <= getRightValue(orderConstraints); + case LT: + return getLeftValue(orderConstraints) < getRightValue(orderConstraints); + default: + return false; + } + } + + private int getLeftValue(Map orderConstraints) { + if (this.leftSideHandVariable != null) { + OrderVariableConstraint constraint = orderConstraints.get(this.leftSideHandVariable); + return constraint.getLower(); + } else { + return this.leftSideHandConstant; + } + } + + private int getRightValue(Map orderConstraints) { + if (this.rightSideHandVariable != null) { + OrderVariableConstraint constraint = orderConstraints.get(this.rightSideHandVariable); + return constraint.getLower(); + } else { + return this.rightSideHandConstant; + } + } + +} diff --git a/src/inference/InferenceRule.java b/src/inference/InferenceRule.java index 140c103..a97ec3c 100644 --- a/src/inference/InferenceRule.java +++ b/src/inference/InferenceRule.java @@ -17,21 +17,25 @@ public class InferenceRule { - private final List assumptions; - private final MetaFormula conclusion; @Getter private final String name; - public InferenceRule(String name, List assumptions, MetaFormula conclusion) { + private final List assumptions; + private final MetaFormula conclusion; + private final InferenceOrderConstraint defaultOrderConstraint; + + public InferenceRule(String name, List assumptions, MetaFormula conclusion, InferenceOrderConstraint constraint) { + this.name = name; this.assumptions = assumptions; this.conclusion = conclusion; - this.name = name; + this.defaultOrderConstraint = constraint; } public InferenceRule(List assumptions, MetaFormula conclusion) { this.assumptions = assumptions; this.conclusion = conclusion; this.name = "undefined"; + this.defaultOrderConstraint = null; } public boolean check(Collection assumptions, Formula conclusion) { @@ -54,7 +58,13 @@ return false; } } - return this.conclusion.isMatchedBy(conclusion, binding, orderConstraints); + if (! this.conclusion.isMatchedBy(conclusion, binding, orderConstraints)) { + return false; + } + if (this.defaultOrderConstraint != null) { + return defaultOrderConstraint.check(orderConstraints); + } + return true; } private List> permutation(Collection list, int n) { diff --git a/src/models/formulas/InFormula.java b/src/models/formulas/InFormula.java new file mode 100644 index 0000000..7b95536 --- /dev/null +++ b/src/models/formulas/InFormula.java @@ -0,0 +1,36 @@ +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/models/formulas/meta/MetaFormula.java b/src/models/formulas/meta/MetaFormula.java index 949217f..cd43fbd 100644 --- a/src/models/formulas/meta/MetaFormula.java +++ b/src/models/formulas/meta/MetaFormula.java @@ -17,7 +17,7 @@ public abstract boolean isMatchedBy(Formula formula, Map binding, Map orderConstraint); public abstract String toString(); - public abstract boolean equals(Object anohter); + public abstract boolean equals(Object another); public abstract int hashCode(); } diff --git a/src/models/formulas/meta/MetaInFormula.java b/src/models/formulas/meta/MetaInFormula.java new file mode 100644 index 0000000..d446557 --- /dev/null +++ b/src/models/formulas/meta/MetaInFormula.java @@ -0,0 +1,61 @@ +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.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 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/models/terms/meta/MetaEvaluatableTermSet.java b/src/models/terms/meta/MetaEvaluatableTermSet.java new file mode 100644 index 0000000..8611340 --- /dev/null +++ b/src/models/terms/meta/MetaEvaluatableTermSet.java @@ -0,0 +1,22 @@ +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/models/terms/meta/MetaRDLTerm.java b/src/models/terms/meta/MetaRDLTerm.java index 57ac148..6a78803 100644 --- a/src/models/terms/meta/MetaRDLTerm.java +++ b/src/models/terms/meta/MetaRDLTerm.java @@ -12,6 +12,7 @@ import models.terms.EvaluatableTerm; import models.terms.RDLTerm; import models.terms.ResourceVariable; +import models.terms.SetEvaluatableTerm; @Getter public class MetaRDLTerm extends RDLTerm { @@ -24,6 +25,8 @@ META_DEPENDENCY_TERM(DependencyTerm.class), META_DEPENDENCY_TERM_VARIABLE(DependencyTerm.class), META_EVALUATABLE_TERM_VARIABLE(EvaluatableTerm.class), + META_EVALUATABLE_TERM_SET(SetEvaluatableTerm.class), + META_EVALUATABLE_TERM_SET_VARIABLE(SetEvaluatableTerm.class), META_RESOURCE_VARIABLE(ResourceVariable.class); @Getter @@ -64,11 +67,15 @@ this.termType = TermType.META_DEPENDENCY; } - //list type dependency - public MetaRDLTerm(MetaRDLTerm dependency) { - super(new Symbol(":", 1), dependency.getOrder() - 1); - addChild(dependency); - this.termType = TermType.META_DEPENDENCY_LIST; + //list type dependency or set term + public MetaRDLTerm(MetaRDLTerm term) { + super(new Symbol(":", 1), term.getOrder() - 1); + if (term.isDependency()) { + this.termType = TermType.META_DEPENDENCY_LIST; + } else if (term.isEvaluatableTerm()) { + this.termType = TermType.META_EVALUATABLE_TERM_SET; + } + addChild(term); } //dependency term diff --git a/src/models/terms/meta/OrderVariableConstraint.java b/src/models/terms/meta/OrderVariableConstraint.java index 41c7bd3..d997e0d 100644 --- a/src/models/terms/meta/OrderVariableConstraint.java +++ b/src/models/terms/meta/OrderVariableConstraint.java @@ -1,8 +1,10 @@ package models.terms.meta; +import lombok.Getter; import lombok.NoArgsConstructor; @NoArgsConstructor +@Getter public class OrderVariableConstraint { // lower <= x <= upper @@ -28,10 +30,6 @@ return false; } - public boolean isOk() { - return isOk; - } - private boolean setEq(int eq) { return setUpper(eq) && setLower(eq); diff --git a/src/tests/terms/meta/MetaDependencyVariableTest.java b/src/tests/terms/meta/MetaDependencyVariableTest.java new file mode 100644 index 0000000..0f2e9f9 --- /dev/null +++ b/src/tests/terms/meta/MetaDependencyVariableTest.java @@ -0,0 +1,129 @@ +package tests.terms.meta; + +import static org.junit.jupiter.api.Assertions.*; +import static tests.Utils.*; + +import org.junit.jupiter.api.Test; + +import models.algebra.Constant; +import models.algebra.Variable; +import models.terms.Dependency; +import models.terms.DependencyTerm; +import models.terms.ResourceVariable; +import models.terms.meta.MetaDependencyVariable; +import models.terms.meta.OrderConstraint; + +public class MetaDependencyVariableTest { + + @Test + void MetaDependencyVariableMatchingWithoutOrderTest() { + ResourceVariable a = new ResourceVariable("a", INT, 1); + ResourceVariable b = new ResourceVariable("b", INT, 1); + ResourceVariable c = new ResourceVariable("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) + assertFalse(d.isMatchedBy(te1)); + } + + @Test + void MetaDependencyVariableMatchingWithConstantOrderEQTest() { + ResourceVariable a = new ResourceVariable("a", INT, 1); + ResourceVariable b = new ResourceVariable("b", INT, 1); + ResourceVariable c = new ResourceVariable("c", INT, 2); + Dependency dep1 = new Dependency(a, b); + Dependency dep2 = new Dependency(a, c); + + MetaDependencyVariable d = new MetaDependencyVariable(new Variable("d"), new Constant("1")); + // [a : b](1) mathces d(=1) + assertTrue(d.isMatchedBy(dep1)); + // [a : c](2) does not mathc d(=1) + assertFalse(d.isMatchedBy(dep2)); + } + + @Test + void MetaDependencyVariableMatchingWithConstantOrderLTTest() { + ResourceVariable a = new ResourceVariable("a", INT, 0); + ResourceVariable b = new ResourceVariable("b", INT, 1); + ResourceVariable c = new ResourceVariable("c", INT, 2); + ResourceVariable e = new ResourceVariable("e", INT, 0); + Dependency dep1 = new Dependency(a, b); + Dependency dep2 = new Dependency(a, c); + Dependency dep3 = new Dependency(a, e); + + MetaDependencyVariable d = new MetaDependencyVariable(new Variable("d"), OrderConstraint.LT, new Constant("1")); + // [a : b](1) does not match d(<1) + assertFalse(d.isMatchedBy(dep1)); + // [a : c](2) does not match d(<1) + assertFalse(d.isMatchedBy(dep2)); + // [a : e](0) matches d(<1) + assertTrue(d.isMatchedBy(dep3)); + } + + @Test + void MetaDependencyVariableMatchingWithConstantOrderLETest() { + ResourceVariable a = new ResourceVariable("a", INT, 0); + ResourceVariable b = new ResourceVariable("b", INT, 1); + ResourceVariable c = new ResourceVariable("c", INT, 2); + ResourceVariable e = new ResourceVariable("e", INT, 0); + Dependency dep1 = new Dependency(a, b); + Dependency dep2 = new Dependency(a, c); + Dependency dep3 = new Dependency(a, e); + + MetaDependencyVariable d = new MetaDependencyVariable(new Variable("d"), OrderConstraint.LE, new Constant("1")); + // [a : b](1) matches d(<=1) + assertTrue(d.isMatchedBy(dep1)); + // [a : c](2) does not match d(<=1) + assertFalse(d.isMatchedBy(dep2)); + // [a : e](0) matches d(<=1) + assertTrue(d.isMatchedBy(dep3)); + } + + @Test + void MetaDependencyVariableMatchingWithConstantOrderGTTest() { + ResourceVariable a = new ResourceVariable("a", INT, 0); + ResourceVariable b = new ResourceVariable("b", INT, 1); + ResourceVariable c = new ResourceVariable("c", INT, 2); + ResourceVariable e = new ResourceVariable("e", INT, 0); + Dependency dep1 = new Dependency(a, b); + Dependency dep2 = new Dependency(a, c); + Dependency dep3 = new Dependency(a, e); + + MetaDependencyVariable d = new MetaDependencyVariable(new Variable("d"), OrderConstraint.GT, new Constant("1")); + // [a : b](1) does not match d(>1) + assertFalse(d.isMatchedBy(dep1)); + // [a : c](2) matches d(>1) + assertTrue(d.isMatchedBy(dep2)); + // [a : e](0) does not match d(>1) + assertFalse(d.isMatchedBy(dep3)); + } + + @Test + void MetaDependencyVariableMatchingWithConstantOrderGETest() { + ResourceVariable a = new ResourceVariable("a", INT, 0); + ResourceVariable b = new ResourceVariable("b", INT, 1); + ResourceVariable c = new ResourceVariable("c", INT, 2); + ResourceVariable e = new ResourceVariable("e", INT, 0); + Dependency dep1 = new Dependency(a, b); + Dependency dep2 = new Dependency(a, c); + Dependency dep3 = new Dependency(a, e); + + MetaDependencyVariable d = new MetaDependencyVariable(new Variable("d"), OrderConstraint.GE, new Constant("1")); + // [a : b](1) matches d(>=1) + assertTrue(d.isMatchedBy(dep1)); + // [a : c](2) matches d(>=1) + assertTrue(d.isMatchedBy(dep2)); + // [a : e](0) does not match d(>=1) + assertFalse(d.isMatchedBy(dep3)); + } + +} diff --git a/src/tests/terms/meta/MetaRDLTermTest.java b/src/tests/terms/meta/MetaRDLTermTest.java new file mode 100644 index 0000000..bc9baf7 --- /dev/null +++ b/src/tests/terms/meta/MetaRDLTermTest.java @@ -0,0 +1,99 @@ +package tests.terms.meta; + +import static org.junit.jupiter.api.Assertions.*; +import static tests.Utils.*; + +import org.junit.jupiter.api.Test; + +import models.algebra.Constant; +import models.algebra.Variable; +import models.terms.Dependency; +import models.terms.DependencyTerm; +import models.terms.ResourceVariable; +import models.terms.meta.MetaDependencyTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaResourceVariable; + +public class MetaRDLTermTest { + + @Test + void MetaDependencyMatchingWithoutOrderTest() { + ResourceVariable a = new ResourceVariable("a", INT, 1); + ResourceVariable b = new ResourceVariable("b", INT, 1); + ResourceVariable c = new ResourceVariable("c", INT, 1); + Dependency dep1 = new Dependency(a, b); + DependencyTerm te1 = new DependencyTerm(a, b, c); + Dependency dep2 = new Dependency(te1, b); + + MetaResourceVariable v1 = new MetaResourceVariable(new Variable("v1")); + MetaResourceVariable v2 = new MetaResourceVariable(new Variable("v2")); + MetaResourceVariable v3 = new MetaResourceVariable(new Variable("v3")); + MetaDependencyTermVariable vte = new MetaDependencyTermVariable(new Variable("vte")); + MetaRDLTerm metaDep = new MetaRDLTerm(v1, v2); + MetaRDLTerm metaDep2 = new MetaRDLTerm(vte, v2); + MetaRDLTerm metaTe = new MetaRDLTerm(v1, v2, v3); + MetaRDLTerm metaDep3 = new MetaRDLTerm(metaTe, v2); + MetaRDLTerm metaDep4 = new MetaRDLTerm(metaTe, v3); + + //[a : b] matches [v1 : v2] + assertTrue(metaDep.isMatchedBy(dep1)); + //[[a : b -> c] : b] does not match [v1 : v2] + assertFalse(metaDep.isMatchedBy(dep2)); + //[[a : b -> c] : b] matches [vte : v2] + assertTrue(metaDep2.isMatchedBy(dep2)); + //[[a : b -> c] : b] matches [[v1 : v2 -> v3] : v2] + assertTrue(metaDep3.isMatchedBy(dep2)); + //[[a : b -> c] : b] does not match [[v1 : v2 -> v3] : v3] + assertFalse(metaDep4.isMatchedBy(dep2)); + } + + @Test + void MetaDependencyMatchingWithConstantOrderTest() { + MetaResourceVariable v1 = new MetaResourceVariable(new Variable("v1"), new Constant("1")); + MetaResourceVariable v2 = new MetaResourceVariable(new Variable("v2"), new Constant("2")); + MetaRDLTerm vd1 = new MetaRDLTerm(v1, v2); + + ResourceVariable a1 = new ResourceVariable("a1", INT, 1); + ResourceVariable a2 = new ResourceVariable("a2", INT, 2); + Dependency d1 = new Dependency(a1, a2); + //[1 : 2] matches [1 : 2] + assertTrue(vd1.isMatchedBy(d1)); + + ResourceVariable b1 = new ResourceVariable("b1", INT, 1); + Dependency d2 = new Dependency(a1, b1); + //[1 : 1] does not match [1 : 2] + assertFalse(vd1.isMatchedBy(d2)); + } + + @Test + void MetaDependencyMatchingWithVariableOrderTest() { + MetaResourceVariable v1 = new MetaResourceVariable(new Variable("v1"), parse("x")); + MetaResourceVariable v2 = new MetaResourceVariable(new Variable("v2"), parse("x")); + MetaResourceVariable v3 = new MetaResourceVariable(new Variable("v3"), parse("y")); + MetaRDLTerm vd1 = new MetaRDLTerm(v1, v2); + MetaRDLTerm vd2 = new MetaRDLTerm(v1, v3); + MetaRDLTerm vd3 = new MetaRDLTerm(new MetaRDLTerm(v3, v1), v2); + + ResourceVariable a1 = new ResourceVariable("a1", INT, 1); + ResourceVariable a2 = new ResourceVariable("a2", INT, 2); + ResourceVariable b1 = new ResourceVariable("b1", INT, 1); + ResourceVariable b2 = new ResourceVariable("b2", INT, 2); + Dependency d1 = new Dependency(a1, a2); + Dependency d2 = new Dependency(a1, b1); + 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)); + //[1 : 1] matches [x : x] + assertTrue(vd1.isMatchedBy(d2)); + //[1 : 2] matches [x : y] + assertTrue(vd2.isMatchedBy(d1)); + //[1 : 1] matches [x : y] + assertTrue(vd2.isMatchedBy(d2)); + //[[1 : 1] : 2] does not match [[y : x] : x] + assertFalse(vd3.isMatchedBy(d3)); + //[[1 : 2] : 2] matches [[y : x] : x] + assertTrue(vd3.isMatchedBy(d4)); + } + +} diff --git a/src/tests/terms/meta/MetaResourceVariableTest.java b/src/tests/terms/meta/MetaResourceVariableTest.java index 30b1cc6..6c921ee 100644 --- a/src/tests/terms/meta/MetaResourceVariableTest.java +++ b/src/tests/terms/meta/MetaResourceVariableTest.java @@ -116,11 +116,47 @@ } @Test - void MetaResourceVariableMathcingWithEqOrder() { + void MetaResourceVariableMathcingWithVariableOrderEq() { ResourceVariable a = new ResourceVariable("a", INT, 0); MetaResourceVariable x = new MetaResourceVariable(new Variable("x"), parse("x")); - //a(0) matches x(x) + //a(0) matches x(=x) + assertTrue(x.isMatchedBy(a)); + } + + @Test + void MetaResourceVariableMathcingWithVariableOrderLT() { + ResourceVariable a = new ResourceVariable("a", INT, 2); + MetaResourceVariable x = new MetaResourceVariable(new Variable("x"), OrderConstraint.LT, parse("x")); + + //a(2) matches x(x) + assertTrue(x.isMatchedBy(a)); + } + + @Test + void MetaResourceVariableMathcingWithVariableOrderGE() { + ResourceVariable a = new ResourceVariable("a", INT, 2); + MetaResourceVariable x = new MetaResourceVariable(new Variable("x"), OrderConstraint.GE, parse("x")); + + //a(2) matches x(