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/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)); + } + +}