diff --git a/src/Main.java b/src/Main.java index f17ba0d..725541c 100644 --- a/src/Main.java +++ b/src/Main.java @@ -1,14 +1,19 @@ +import java.util.List; + +import inference.InferenceRule; import lombok.SneakyThrows; import models.algebra.Expression; import models.algebra.Type; import models.algebra.Variable; import models.dataConstraintModel.DataConstraintModel; import models.dataFlowModel.DataTransferModel; -import models.terms.EvaluatableTerm; +import models.formulas.EquationFormula; +import models.formulas.meta.MetaEquationFormula; +import models.terms.DependencyTerm; import models.terms.ResourceVariable; +import models.terms.meta.MetaEvaluatableTermVariable; import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaResourceVariable; -import models.terms.meta.OrderConstraint; import parser.Parser; import parser.Parser.TokenStream; @@ -18,26 +23,37 @@ static Parser parser = new Parser(stream); static DataTransferModel model = new DataTransferModel(); + static Type INT = DataConstraintModel.typeInt; + public static void main(String[] args) { - Type INT = DataConstraintModel.typeInt; - - var a = new ResourceVariable("a", INT, 2); - var b = new ResourceVariable("b", INT, 2); - var c = new ResourceVariable("c", INT, 1); - var d = EvaluatableTerm.of(a, b, c); - - var v1 = new MetaResourceVariable(new Variable("v1"), OrderConstraint.LE, parse("x + 1")); - var v2 = new MetaResourceVariable(new Variable("v1"), OrderConstraint.EQ, parse("x + 1")); - var v3 = new MetaResourceVariable(new Variable("v3"), OrderConstraint.LE, parse("x")); - var te = new MetaRDLTerm(v1, v2, v3); - - System.out.println(d.toString()); - System.out.println(te.toString()); - System.out.println(te.isMatchedBy(d)); - - } + MetaEvaluatableTermVariable te = new MetaEvaluatableTermVariable(new Variable("te")); + MetaEvaluatableTermVariable ue = new MetaEvaluatableTermVariable(new Variable("ue")); + MetaEvaluatableTermVariable se = new MetaEvaluatableTermVariable(new Variable("se")); + MetaResourceVariable v = new MetaResourceVariable(new Variable("v")); + MetaEquationFormula assump1 = new MetaEquationFormula(te, ue); + MetaEquationFormula concl1 = new MetaEquationFormula(new MetaRDLTerm(se, v, te), new MetaRDLTerm(se, v, ue)); + /* + * te = ue + * ---------------------------------------- + * [se : v -> te] = [se : v -> ue] + */ + InferenceRule rightReplacement = new InferenceRule(List.of(assump1), concl1); + ResourceVariable a = new ResourceVariable("a", INT, 0); + ResourceVariable b = new ResourceVariable("b", INT, 0); + ResourceVariable c = new ResourceVariable("c", INT, 0); + ResourceVariable d = new ResourceVariable("d", INT, 0); + ResourceVariable x = new ResourceVariable("x", INT, 0); + ResourceVariable y = new ResourceVariable("y", INT, 0); + ResourceVariable z = new ResourceVariable("z", INT, 0); + DependencyTerm xyz = new DependencyTerm(x, y, z); + EquationFormula assump2 = new EquationFormula(a, xyz); // a = [x : y -> z] + EquationFormula concl2 = new EquationFormula(new DependencyTerm(c, d, a), new DependencyTerm(c, d, xyz)); // [c : d -> a] = [c : d -> [x : y -> z]] + + System.out.println(rightReplacement.check(List.of(assump2), concl2)); + } + @SneakyThrows static Expression parse(String expr) { stream.addLine(expr); diff --git a/src/inference/InferenceRule.java b/src/inference/InferenceRule.java new file mode 100644 index 0000000..7f5798b --- /dev/null +++ b/src/inference/InferenceRule.java @@ -0,0 +1,90 @@ +package inference; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import lombok.RequiredArgsConstructor; +import models.algebra.Variable; +import models.formulas.Formula; +import models.formulas.meta.MetaFormula; +import models.terms.RDLTerm; +import models.terms.meta.OrderVariableConstraint; + +@RequiredArgsConstructor +public class InferenceRule { + + private final List assumptions; + private final MetaFormula conclusion; + + public boolean check(Collection assumptions, Formula conclusion) { + if (this.assumptions.size() > assumptions.size()) { + return false; + } + for(List assumption : permutation(assumptions, this.assumptions.size())) { + if (check(assumption, conclusion)) { + return true; + } + } + return false; + } + + 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)) { + return false; + } + } + return this.conclusion.isMatchedBy(conclusion, binding, orderConstraints); + } + + private List> permutation(Collection list, int n) { + List> res = new ArrayList<>(); + permutation(list, n, new ArrayList<>(), new HashSet<>(), res); + return res; + } + + private void permutation(Collection all, int n, List current, Set used, List> result) { + if (current.size() == n) { + result.add(new ArrayList<>(current)); + return; + } + for (T elem : all) { + if (! used.contains(elem)) { + current.add(elem); + used.add(elem); + permutation(all, n, current, used, result); + current.remove(current.size() - 1); + used.remove(elem); + } + } + } + + + public String toString() { + StringBuilder sb = new StringBuilder(); + for (int i = 0; i < assumptions.size(); i++) { + sb.append(assumptions.get(i).toString()); + if (i != assumptions.size() - 1) { + sb.append(", "); + } + } + String assumpStr = sb.toString(); + String concluStr = conclusion.toString(); + String line = "-".repeat(Math.max(assumpStr.length(), concluStr.length())); + sb = new StringBuilder(); + sb.append(assumpStr); + sb.append("\n"); + sb.append(line); + sb.append("\n"); + sb.append(concluStr); + return sb.toString(); + } + +} diff --git a/src/models/formulas/DependencyFormula.java b/src/models/formulas/DependencyFormula.java new file mode 100644 index 0000000..480d17d --- /dev/null +++ b/src/models/formulas/DependencyFormula.java @@ -0,0 +1,35 @@ +package models.formulas; + +import lombok.Getter; +import models.terms.Dependency; + +@Getter +public class DependencyFormula extends Formula { + + private Dependency dependency; + + public DependencyFormula(Dependency dependency) { + this.dependency = dependency; + } + + + @Override + public String toString() { + return dependency.toString(); + } + + @Override + public boolean equals(Object another) { + if(! (another instanceof DependencyFormula)) { + return false; + } + DependencyFormula anotherFormula = (DependencyFormula) another; + return dependency.equals(anotherFormula.getDependency()); + } + + @Override + public int hashCode() { + return ("DF" + toString()).hashCode(); + } + +} diff --git a/src/models/formulas/EquationFormula.java b/src/models/formulas/EquationFormula.java new file mode 100644 index 0000000..e12dc46 --- /dev/null +++ b/src/models/formulas/EquationFormula.java @@ -0,0 +1,37 @@ +package models.formulas; + +import lombok.Getter; +import models.terms.EvaluatableTerm; + +@Getter +public class EquationFormula extends Formula { + + private EvaluatableTerm leftSideHand; + private EvaluatableTerm rightSideHand; + + public EquationFormula(EvaluatableTerm leftTerm, EvaluatableTerm rightTerm) { + this.leftSideHand = leftTerm; + this.rightSideHand = rightTerm; + } + + + @Override + public String toString() { + return leftSideHand.toString() + " = " + rightSideHand.toString(); + } + + @Override + public boolean equals(Object another) { + if (! (another instanceof EquationFormula)) { + return false; + } + EquationFormula anotherFormula = (EquationFormula) another; + return leftSideHand.equals(anotherFormula.getLeftSideHand()) && rightSideHand.equals(anotherFormula.getRightSideHand()); + } + + @Override + public int hashCode() { + return toString().hashCode(); + } + +} diff --git a/src/models/formulas/Formula.java b/src/models/formulas/Formula.java new file mode 100644 index 0000000..f1813f4 --- /dev/null +++ b/src/models/formulas/Formula.java @@ -0,0 +1,9 @@ +package models.formulas; + +public abstract class Formula { + + public abstract String toString(); + public abstract boolean equals(Object another); + public abstract int hashCode(); + +} diff --git a/src/models/formulas/meta/MetaDependencyFormula.java b/src/models/formulas/meta/MetaDependencyFormula.java new file mode 100644 index 0000000..f3dcf08 --- /dev/null +++ b/src/models/formulas/meta/MetaDependencyFormula.java @@ -0,0 +1,53 @@ +package models.formulas.meta; + +import java.util.Map; + +import exceptions.IllegalTypeException; +import lombok.Getter; +import models.algebra.Variable; +import models.formulas.DependencyFormula; +import models.formulas.Formula; +import models.terms.RDLTerm; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.OrderVariableConstraint; + +@Getter +public class MetaDependencyFormula extends MetaFormula { + + private MetaRDLTerm dependency; + + public MetaDependencyFormula(MetaRDLTerm term) { + if (! term.isDependency()) { + throw new IllegalTypeException(); + } + this.dependency = term; + } + + @Override + public boolean isMatchedBy(Formula formula, Map binding, + Map orderConstraint) { + if (! (formula instanceof DependencyFormula)) { + return false; + } + DependencyFormula dep = (DependencyFormula) formula; + return dependency.isMatchedBy(dep.getDependency(), binding, orderConstraint); + } + + + public String toString() { + return dependency.toString(); + } + + public boolean equals(Object another) { + if (! (another instanceof MetaDependencyFormula)) { + return false; + } + MetaDependencyFormula anohterFormula = (MetaDependencyFormula) another; + return dependency.equals(anohterFormula.getDependency()); + } + + public int hashCode() { + return ("MDF" + toString()).hashCode(); + } + +} diff --git a/src/models/formulas/meta/MetaEquationFormula.java b/src/models/formulas/meta/MetaEquationFormula.java new file mode 100644 index 0000000..9c4ddd9 --- /dev/null +++ b/src/models/formulas/meta/MetaEquationFormula.java @@ -0,0 +1,59 @@ +package models.formulas.meta; + +import java.util.Map; + +import exceptions.IllegalTypeException; +import lombok.Getter; +import models.algebra.Variable; +import models.formulas.EquationFormula; +import models.formulas.Formula; +import models.terms.RDLTerm; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.OrderVariableConstraint; + +@Getter +public class MetaEquationFormula extends MetaFormula { + + private MetaRDLTerm leftSideHand; + private MetaRDLTerm rightSideHand; + + public MetaEquationFormula(MetaRDLTerm left, MetaRDLTerm right) { + if (! left.isEvaluatableTerm()) { + throw new IllegalTypeException(); + } + if (! right.isEvaluatableTerm()) { + throw new IllegalTypeException(); + } + + this.leftSideHand = left; + this.rightSideHand = right; + } + + @Override + public boolean isMatchedBy(Formula formula, Map binding, + Map orderConstraint) { + if (! (formula instanceof EquationFormula)) { + return false; + } + EquationFormula eq = (EquationFormula) formula; + return leftSideHand.isMatchedBy(eq.getLeftSideHand(), binding, orderConstraint) && rightSideHand.isMatchedBy(eq.getRightSideHand(), binding, orderConstraint); + } + + + public String toString() { + return leftSideHand.toString() + " = " + rightSideHand.toString(); + } + + public boolean equals(Object another) { + if (! (another instanceof MetaEquationFormula)) { + return false; + } + MetaEquationFormula anohterFormula = (MetaEquationFormula) another; + return leftSideHand.equals(anohterFormula.getLeftSideHand()) && rightSideHand.equals(anohterFormula.getRightSideHand()); + } + + public int hashCode() { + return ("MEF" + toString()).hashCode(); + } + +} diff --git a/src/models/formulas/meta/MetaFormula.java b/src/models/formulas/meta/MetaFormula.java new file mode 100644 index 0000000..949217f --- /dev/null +++ b/src/models/formulas/meta/MetaFormula.java @@ -0,0 +1,23 @@ +package models.formulas.meta; + +import java.util.HashMap; +import java.util.Map; + +import models.algebra.Variable; +import models.formulas.Formula; +import models.terms.RDLTerm; +import models.terms.meta.OrderVariableConstraint; + +public abstract class MetaFormula { + + public boolean isMatchedBy(Formula formula) { + return isMatchedBy(formula, new HashMap<>(), new HashMap<>()); + } + + public abstract boolean isMatchedBy(Formula formula, Map binding, Map orderConstraint); + + public abstract String toString(); + public abstract boolean equals(Object anohter); + public abstract int hashCode(); + +} diff --git a/src/tests/formulas/meta/MetaEquationFormulaTest.java b/src/tests/formulas/meta/MetaEquationFormulaTest.java new file mode 100644 index 0000000..561ab6b --- /dev/null +++ b/src/tests/formulas/meta/MetaEquationFormulaTest.java @@ -0,0 +1,67 @@ +package tests.formulas.meta; + +import static org.junit.jupiter.api.Assertions.*; +import static tests.Utils.*; + +import org.junit.jupiter.api.Test; + +import models.algebra.Variable; +import models.formulas.DependencyFormula; +import models.formulas.EquationFormula; +import models.formulas.meta.MetaDependencyFormula; +import models.formulas.meta.MetaEquationFormula; +import models.terms.Dependency; +import models.terms.DependencyTerm; +import models.terms.EvaluatableTerm; +import models.terms.ResourceVariable; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaResourceVariable; + +public class MetaEquationFormulaTest { + + @Test + void MetaEquationFormulaMatchingTest() { + + ResourceVariable a = new ResourceVariable("a", INT, 0); + ResourceVariable b = new ResourceVariable("b", INT, 0); + ResourceVariable c = new ResourceVariable("c", INT, 0); + ResourceVariable d = new ResourceVariable("d", INT, 0); + EvaluatableTerm te1 = new DependencyTerm(a, b, c); + EvaluatableTerm te2 = new DependencyTerm(a, b, d); + EquationFormula formula = new EquationFormula(te1, te2); + + + MetaEvaluatableTermVariable se = new MetaEvaluatableTermVariable(new Variable("se")); + MetaResourceVariable v = new MetaResourceVariable(new Variable("v")); + MetaEvaluatableTermVariable te = new MetaEvaluatableTermVariable(new Variable("te")); + MetaEvaluatableTermVariable ue = new MetaEvaluatableTermVariable(new Variable("ue")); + MetaRDLTerm left = new MetaRDLTerm(se, v, te); + MetaRDLTerm right = new MetaRDLTerm(se, v, ue); + MetaEquationFormula metaFormula = new MetaEquationFormula(left, right); + + // [a : b -> c] = [a : b -> d] matches [se : v -> te] = [se : v -> ue] + assertTrue(metaFormula.isMatchedBy(formula)); + + } + + @Test + void MetaDependencyFormulaMatchingTest() { + ResourceVariable a = new ResourceVariable("a", INT, 0); + ResourceVariable b = new ResourceVariable("b", INT, 0); + ResourceVariable c = new ResourceVariable("c", INT, 0); + EvaluatableTerm te1 = new DependencyTerm(a, b, c); + ResourceVariable d = new ResourceVariable("d", INT, 0); + Dependency d1 = new Dependency(te1, d); + DependencyFormula depF = new DependencyFormula(d1); + + MetaEvaluatableTermVariable te = new MetaEvaluatableTermVariable(new Variable("te")); + MetaResourceVariable w = new MetaResourceVariable(new Variable("w")); + MetaRDLTerm dep = new MetaRDLTerm(te, w); + MetaDependencyFormula metaDepF = new MetaDependencyFormula(dep); + + //[a : b -> c] : d matches te : w + assertTrue(metaDepF.isMatchedBy(depF)); + } + +} diff --git a/src/tests/inferencerule/InferenceRuleTest.java b/src/tests/inferencerule/InferenceRuleTest.java new file mode 100644 index 0000000..f1e89bb --- /dev/null +++ b/src/tests/inferencerule/InferenceRuleTest.java @@ -0,0 +1,79 @@ +package tests.inferencerule; + +import static org.junit.jupiter.api.Assertions.*; +import static tests.Utils.*; + +import org.junit.jupiter.api.Test; + +import java.util.List; + +import inference.InferenceRule; +import models.algebra.Variable; +import models.formulas.DependencyFormula; +import models.formulas.EquationFormula; +import models.formulas.meta.MetaDependencyFormula; +import models.formulas.meta.MetaEquationFormula; +import models.terms.Dependency; +import models.terms.DependencyTerm; +import models.terms.ResourceVariable; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaResourceVariable; + +public class InferenceRuleTest { + + @Test + void InferenceRuleTerst1() { + MetaEvaluatableTermVariable te = new MetaEvaluatableTermVariable(new Variable("te")); + MetaResourceVariable v = new MetaResourceVariable(new Variable("v")); + MetaResourceVariable w = new MetaResourceVariable(new Variable("w")); + MetaRDLTerm metaD1 = new MetaRDLTerm(te, v); + MetaRDLTerm metaD2 = new MetaRDLTerm(v, w); + MetaRDLTerm metaD3 = new MetaRDLTerm(te, w); + MetaDependencyFormula metaDf1 = new MetaDependencyFormula(metaD1); + MetaDependencyFormula metaDf2 = new MetaDependencyFormula(metaD2); + MetaDependencyFormula metaDf3 = new MetaDependencyFormula(metaD3); + InferenceRule goseShazo = new InferenceRule(List.of(metaDf1, metaDf2), metaDf3); + + ResourceVariable a = new ResourceVariable("a", INT, 0); + ResourceVariable b = new ResourceVariable("b", INT, 0); + ResourceVariable c = new ResourceVariable("c", INT, 0); + Dependency d1 = new Dependency(a, b); + Dependency d2 = new Dependency(b, c); + Dependency d3 = new Dependency(a, c); + DependencyFormula df1 = new DependencyFormula(d1); // a : b + DependencyFormula df2 = new DependencyFormula(d2); // b : c + DependencyFormula df3 = new DependencyFormula(d3); // a : c + assertTrue(goseShazo.check(List.of(df1, df2), df3)); + + } + + @Test + void InferencuRuleTest2() { + MetaEvaluatableTermVariable te = new MetaEvaluatableTermVariable(new Variable("te")); + MetaEvaluatableTermVariable ue = new MetaEvaluatableTermVariable(new Variable("ue")); + MetaEvaluatableTermVariable se = new MetaEvaluatableTermVariable(new Variable("se")); + MetaResourceVariable v = new MetaResourceVariable(new Variable("v")); + MetaEquationFormula assump1 = new MetaEquationFormula(te, ue); + MetaEquationFormula concl1 = new MetaEquationFormula(new MetaRDLTerm(se, v, te), new MetaRDLTerm(se, v, ue)); + /* + * te = ue + * ---------------------------------------- + * [se : v -> te] = [se : v -> ue] + */ + InferenceRule rightReplacement = new InferenceRule(List.of(assump1), concl1); + + ResourceVariable a = new ResourceVariable("a", INT, 0); + ResourceVariable c = new ResourceVariable("c", INT, 0); + ResourceVariable d = new ResourceVariable("d", INT, 0); + ResourceVariable x = new ResourceVariable("x", INT, 0); + ResourceVariable y = new ResourceVariable("y", INT, 0); + ResourceVariable z = new ResourceVariable("z", INT, 0); + DependencyTerm xyz = new DependencyTerm(x, y, z); + EquationFormula assump2 = new EquationFormula(a, xyz); // a = [x : y -> z] + EquationFormula concl2 = new EquationFormula(new DependencyTerm(c, d, a), new DependencyTerm(c, d, xyz)); // [c : d -> a] = [c : d -> [x : y -> z]] + + assertTrue(rightReplacement.check(List.of(assump2), concl2)); + } + +}