diff --git a/src/Main.java b/src/Main.java index 9a1ea3c..26f705e 100644 --- a/src/Main.java +++ b/src/Main.java @@ -3,6 +3,7 @@ import inference.ProofSystem; import inference.equivalence.SemanticEquivalenceProofSystem; import inference.equivalence.SemanticEquivalenceRelation; +import inference.rewrite.RewriteInferenceSystem; import lombok.SneakyThrows; import models.algebra.Expression; import models.algebra.Type; @@ -13,8 +14,8 @@ import models.formulas.InFormula; import models.terms.Dependency; import models.terms.DependencyTerm; +import models.terms.Resource; import models.terms.ResourceConstant; -import models.terms.ResourceVariable; import models.terms.SetEvaluatableTerm; import parser.Parser; import parser.Parser.TokenStream; @@ -34,27 +35,20 @@ // sandbox3(); // sandbox4(); // ProofSystem.debug(); - ResourceVariable A = new ResourceVariable("A", Utils.INT, 1); - ResourceVariable B = new ResourceVariable("B", Utils.INT, 1); - ResourceVariable C = new ResourceVariable("C", Utils.INT, 1); - ResourceVariable D = new ResourceVariable("D", Utils.INT, 1); - ResourceVariable E = new ResourceVariable("E", Utils.INT, 1); - - DependencyTerm t1 = new DependencyTerm(A, B, C, D, E); - System.out.println(t1); + sandbox5(); } static void sandbox1() { - ResourceVariable A = new ResourceVariable("A", Utils.INT, 2); - ResourceVariable Ap = new ResourceVariable("A'", Utils.INT, 2); - ResourceVariable B = new ResourceVariable("B", Utils.INT, 2); - ResourceVariable Bp = new ResourceVariable("B'", Utils.INT, 2); - ResourceVariable C = new ResourceVariable("C", Utils.INT, 2); - ResourceVariable Cp = new ResourceVariable("C'", Utils.INT, 2); - ResourceVariable D = new ResourceVariable("D", Utils.INT, 2); - ResourceVariable E = new ResourceVariable("E", Utils.INT, 1); - ResourceVariable F = new ResourceVariable("F", Utils.INT, 1); - ResourceVariable G = new ResourceVariable("G", Utils.INT, 0); + Resource A = new Resource("A", Utils.INT, 2); + Resource Ap = new Resource("A'", Utils.INT, 2); + Resource B = new Resource("B", Utils.INT, 2); + Resource Bp = new Resource("B'", Utils.INT, 2); + Resource C = new Resource("C", Utils.INT, 2); + Resource Cp = new Resource("C'", Utils.INT, 2); + Resource D = new Resource("D", Utils.INT, 2); + Resource E = new Resource("E", Utils.INT, 1); + Resource F = new Resource("F", Utils.INT, 1); + Resource G = new Resource("G", Utils.INT, 0); DependencyTerm t1 = new DependencyTerm(A, B, C); DependencyTerm t2 = new DependencyTerm(Ap, Bp, Cp); EquationFormula assumptionFormula = new EquationFormula(t1, t2); @@ -80,12 +74,12 @@ } static void sandbox3() { - ResourceVariable followee = new ResourceVariable("followee", INT, 2); - ResourceVariable fno = new ResourceVariable("fno", INT, 2); + Resource followee = new Resource("followee", INT, 2); + Resource fno = new Resource("fno", INT, 2); ResourceConstant one = new ResourceConstant("1"); ResourceConstant A = new ResourceConstant("A"); ResourceConstant C = new ResourceConstant("C"); - ResourceVariable aid = new ResourceVariable("aid", INT, 1); + Resource aid = new Resource("aid", INT, 1); DependencyTerm t1 = new DependencyTerm(followee, fno, one); Dependency d1 = new Dependency(t1, aid); DependencyTerm t2 = new DependencyTerm(one, aid, A); @@ -110,10 +104,10 @@ } static void sandbox4() { - ResourceVariable X = new ResourceVariable("X", INT, 1); - ResourceVariable Y= new ResourceVariable("Y", INT, 1); - ResourceVariable U = new ResourceVariable("U", INT, 1); - ResourceVariable W = new ResourceVariable("W", INT, 1); + Resource X = new Resource("X", INT, 1); + Resource Y= new Resource("Y", INT, 1); + Resource U = new Resource("U", INT, 1); + Resource W = new Resource("W", INT, 1); EquationFormula f1 = new EquationFormula(X, Y); DependencyFormula f2 = new DependencyFormula(X, U); @@ -134,6 +128,23 @@ System.out.println(result); } + static void sandbox5() { + Resource a = new Resource("a", INT, 1); + Resource b = new Resource("b", INT, 1); + Resource c = new Resource("c", INT, 1); + Resource d = new Resource("d", INT, 1); + Resource e = new Resource("e", INT, 1); + Resource f = new Resource("f", INT, 1); + Resource x = new Resource("x", INT, 0); + Resource y = new Resource("y", INT, 0); + DependencyTerm t1 = new DependencyTerm(a, b, c, d, e); + DependencyTerm t2 = new DependencyTerm(x, f, t1); + EquationFormula fm = new EquationFormula(t2, y); + RewriteInferenceSystem tmp = new RewriteInferenceSystem(List.of(fm), null); + tmp.inference(); + } + + @SneakyThrows static Expression parse(String expr) { stream.addLine(expr); diff --git a/src/inference/ProofSystem.java b/src/inference/ProofSystem.java index abf190c..8d1b7be 100644 --- a/src/inference/ProofSystem.java +++ b/src/inference/ProofSystem.java @@ -25,7 +25,7 @@ import models.terms.RDLTerm; import models.terms.meta.MetaEvaluatableTermVariable; import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaResourceVariable; +import models.terms.meta.MetaResource; import models.terms.meta.OrderConstraint; import utils.Product; @@ -83,22 +83,22 @@ ), new MetaDependencyFormula( new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResourceVariable(new Variable("r")) + new MetaResource(new Variable("r")) ), new MetaInFormula( new MetaEvaluatableTermVariable(new Variable("te")), - new MetaRDLTerm(new MetaResourceVariable(new Variable("r"))) + new MetaRDLTerm(new MetaResource(new Variable("r"))) ) ), new MetaEquationFormula( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResourceVariable(new Variable("r")), + new MetaResource(new Variable("r")), new MetaEvaluatableTermVariable(new Variable("te")) ), new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResourceVariable(new Variable("r")), + new MetaResource(new Variable("r")), new MetaEvaluatableTermVariable(new Variable("ue")) ) ) @@ -113,22 +113,22 @@ ), new MetaDependencyFormula( new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResourceVariable(new Variable("r")) + new MetaResource(new Variable("r")) ), new MetaInFormula( new MetaEvaluatableTermVariable(new Variable("ue")), - new MetaRDLTerm(new MetaResourceVariable(new Variable("r"))) + new MetaRDLTerm(new MetaResource(new Variable("r"))) ) ), new MetaEquationFormula( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResourceVariable(new Variable("r")), + new MetaResource(new Variable("r")), new MetaEvaluatableTermVariable(new Variable("ue")) ), new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResourceVariable(new Variable("r")), + new MetaResource(new Variable("r")), new MetaEvaluatableTermVariable(new Variable("ue")) ) ) @@ -139,13 +139,13 @@ List.of( new MetaInFormula( new MetaEvaluatableTermVariable(new Variable("te")), - new MetaRDLTerm(new MetaResourceVariable(new Variable("r"))) + new MetaRDLTerm(new MetaResource(new Variable("r"))) ) ), new MetaEquationFormula( new MetaRDLTerm( - new MetaResourceVariable(new Variable("r")), - new MetaResourceVariable(new Variable("r")), + new MetaResource(new Variable("r")), + new MetaResource(new Variable("r")), new MetaEvaluatableTermVariable(new Variable("te")) ), new MetaEvaluatableTermVariable(new Variable("te")) @@ -157,30 +157,30 @@ List.of( new MetaDependencyFormula( new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResourceVariable(new Variable("r")) + new MetaResource(new Variable("r")) ), new MetaDependencyFormula( - new MetaResourceVariable(new Variable("r")), - new MetaResourceVariable(new Variable("p")) + new MetaResource(new Variable("r")), + new MetaResource(new Variable("p")) ), new MetaInFormula( new MetaEvaluatableTermVariable(new Variable("te")), - new MetaRDLTerm(new MetaResourceVariable(new Variable("p"))) + new MetaRDLTerm(new MetaResource(new Variable("p"))) ) ), new MetaEquationFormula( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResourceVariable(new Variable("r")), + new MetaResource(new Variable("r")), new MetaRDLTerm( - new MetaResourceVariable(new Variable("r")), - new MetaResourceVariable(new Variable("p")), + new MetaResource(new Variable("r")), + new MetaResource(new Variable("p")), new MetaEvaluatableTermVariable(new Variable("te")) ) ), new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResourceVariable(new Variable("p")), + new MetaResource(new Variable("p")), new MetaEvaluatableTermVariable(new Variable("te")) ) ) @@ -191,13 +191,13 @@ List.of( new MetaInFormula( new MetaEvaluatableTermVariable(new Variable("t1")), - new MetaRDLTerm(new MetaResourceVariable(new Variable("r1"), new Variable("m"))) + new MetaRDLTerm(new MetaResource(new Variable("r1"), new Variable("m"))) ) ), new MetaEquationFormula( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), - new MetaResourceVariable(new Variable("r1"), new Variable("m")), + new MetaResource(new Variable("r1"), new Variable("m")), new MetaEvaluatableTermVariable(new Variable("t1")) ), new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) @@ -211,13 +211,13 @@ new MetaDependencyFormula( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResourceVariable(new Variable("r"), new Variable("n")) + new MetaResource(new Variable("r"), new Variable("n")) ) ), new MetaDependencyFormula( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResourceVariable(new Variable("q"), new Variable("n")) + new MetaResource(new Variable("q"), new Variable("n")) ) ) ), @@ -225,18 +225,18 @@ new MetaRDLTerm( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResourceVariable(new Variable("r"), new Variable("n")), + new MetaResource(new Variable("r"), new Variable("n")), new MetaEvaluatableTermVariable(new Variable("se")) ), - new MetaResourceVariable(new Variable("q"), new Variable("n")), + new MetaResource(new Variable("q"), new Variable("n")), new MetaEvaluatableTermVariable(new Variable("ue")) ), new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResourceVariable(new Variable("r"), new Variable("n")), + new MetaResource(new Variable("r"), new Variable("n")), new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResourceVariable(new Variable("q"), new Variable("n")), + new MetaResource(new Variable("q"), new Variable("n")), new MetaEvaluatableTermVariable(new Variable("ue")) ) ) @@ -250,15 +250,15 @@ new MetaDependencyFormula( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), - new MetaResourceVariable(new Variable("r"), new Variable("n")) + new MetaResource(new Variable("r"), new Variable("n")) ) ) ), new MetaEquationFormula( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), - new MetaResourceVariable(new Variable("r"), new Variable("n")), - new MetaResourceVariable(new Variable("r"), 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")) ), @@ -272,12 +272,12 @@ List.of( new MetaEquationFormula( new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResourceVariable(new Variable("r")) + new MetaResource(new Variable("r")) ) ), new MetaDependencyFormula( new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResourceVariable(new Variable("r")) + new MetaResource(new Variable("r")) ) ); @@ -286,16 +286,16 @@ List.of( new MetaDependencyFormula( new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResourceVariable(new Variable("r")) + new MetaResource(new Variable("r")) ), new MetaDependencyFormula( new MetaEvaluatableTermVariable(new Variable("r")), - new MetaResourceVariable(new Variable("q")) + new MetaResource(new Variable("q")) ) ), new MetaDependencyFormula( new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResourceVariable(new Variable("q")) + new MetaResource(new Variable("q")) ) ); @@ -304,7 +304,7 @@ List.of(), new MetaDependencyFormula( new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), - new MetaResourceVariable(new Variable("r"), new Variable("m")) + new MetaResource(new Variable("r"), new Variable("m")) ), new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")) ); @@ -315,22 +315,22 @@ new MetaDependencyFormula( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResourceVariable(new Variable("r")) + new MetaResource(new Variable("r")) ), - new MetaResourceVariable(new Variable("p")) + new MetaResource(new Variable("p")) ), new MetaDependencyFormula( new MetaEvaluatableTermVariable(new Variable("te")), - new MetaResourceVariable(new Variable("p")) + new MetaResource(new Variable("p")) ) ), new MetaDependencyFormula( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResourceVariable(new Variable("r")), + new MetaResource(new Variable("r")), new MetaEvaluatableTermVariable(new Variable("te")) ), - new MetaResourceVariable(new Variable("p")) + new MetaResource(new Variable("p")) ) ); @@ -410,19 +410,19 @@ List.of( new MetaDependencyFormula( new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResourceVariable(new Variable("r")) + new MetaResource(new Variable("r")) ) ), new MetaEquationFormula( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResourceVariable(new Variable("r")), + new MetaResource(new Variable("r")), new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"))) ), new MetaRDLTerm( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResourceVariable(new Variable("r")), + new MetaResource(new Variable("r")), new MetaEvaluatableTermVariable(new Variable("te")) ) ) @@ -435,14 +435,14 @@ new MetaDependencyFormula( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), - new MetaResourceVariable(new Variable("r"), new Variable("m")) + new MetaResource(new Variable("r"), new Variable("m")) ), - new MetaResourceVariable(new Variable("q"), new Variable("l")) + new MetaResource(new Variable("q"), new Variable("l")) ) ), new MetaDependencyFormula( new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))), - new MetaResourceVariable(new Variable("q"), new Variable("l")) + new MetaResource(new Variable("q"), new Variable("l")) ) ); @@ -452,14 +452,14 @@ new MetaDependencyFormula( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), - new MetaResourceVariable(new Variable("r"), new Variable("m")) + new MetaResource(new Variable("r"), new Variable("m")) ), - new MetaResourceVariable(new Variable("q"), new Variable("l")) + new MetaResource(new Variable("q"), new Variable("l")) ) ), new MetaDependencyFormula( new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("r"), new Variable("m"))), - new MetaResourceVariable(new Variable("q"), new Variable("l")) + new MetaResource(new Variable("q"), new Variable("l")) ) ); @@ -470,24 +470,24 @@ new MetaRDLTerm( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResourceVariable(new Variable("r1")), + new MetaResource(new Variable("r1")), new MetaEvaluatableTermVariable(new Variable("t1")) ), - new MetaResourceVariable(new Variable("r2")), + new MetaResource(new Variable("r2")), new MetaEvaluatableTermVariable(new Variable("t2")) ), - new MetaResourceVariable(new Variable("c")) + new MetaResource(new Variable("c")) ) ), new MetaInFormula( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("t1")), - new MetaResourceVariable(new Variable("r2")), + new MetaResource(new Variable("r2")), new MetaEvaluatableTermVariable(new Variable("t2")) ), new MetaRDLTerm( - new MetaRDLTerm(new MetaResourceVariable(new Variable("r1"))), - new MetaResourceVariable(new Variable("r2")), + new MetaRDLTerm(new MetaResource(new Variable("r1"))), + new MetaResource(new Variable("r2")), new MetaEvaluatableTermVariable(new Variable("t2")) ) ) @@ -499,22 +499,22 @@ new MetaDependencyFormula( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResourceVariable(new Variable("r1")), + new MetaResource(new Variable("r1")), new MetaEvaluatableTermVariable(new Variable("t1")) ), - new MetaResourceVariable(new Variable("r2")) + new MetaResource(new Variable("r2")) ), new MetaInFormula( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("t1")), - new MetaResourceVariable(new Variable("r2")), + new MetaResource(new Variable("r2")), new MetaEvaluatableTermVariable(new Variable("t2")) ), new MetaRDLTerm( new MetaRDLTerm( - new MetaResourceVariable(new Variable("r1")) + new MetaResource(new Variable("r1")) ), - new MetaResourceVariable(new Variable("r2")), + new MetaResource(new Variable("r2")), new MetaEvaluatableTermVariable(new Variable("t2")) ) ) @@ -523,17 +523,17 @@ new MetaRDLTerm( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResourceVariable(new Variable("r1")), + new MetaResource(new Variable("r1")), new MetaEvaluatableTermVariable(new Variable("t1")) ), - new MetaResourceVariable(new Variable("r2")), + new MetaResource(new Variable("r2")), new MetaEvaluatableTermVariable(new Variable("t2")) ), new MetaRDLTerm( new MetaRDLTerm( - new MetaResourceVariable(new Variable("se")) + new MetaResource(new Variable("se")) ), - new MetaResourceVariable(new Variable("r2")), + new MetaResource(new Variable("r2")), new MetaEvaluatableTermVariable(new Variable("t2")) ) ) @@ -544,23 +544,23 @@ List.of( new MetaDependencyFormula( new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResourceVariable(new Variable("r1")) + new MetaResource(new Variable("r1")) ), new MetaInFormula( new MetaEvaluatableTermVariable(new Variable("t1")), new MetaRDLTerm( - new MetaResourceVariable(new Variable("r1")) + new MetaResource(new Variable("r1")) ) ) ), new MetaInFormula( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("se")), - new MetaResourceVariable(new Variable("r1")), + new MetaResource(new Variable("r1")), new MetaEvaluatableTermVariable(new Variable("t1")) ), new MetaRDLTerm( - new MetaResourceVariable(new Variable("se")) + new MetaResource(new Variable("se")) ) ) ); diff --git a/src/inference/equivalence/SemanticEquivalenceProofSystem.java b/src/inference/equivalence/SemanticEquivalenceProofSystem.java index d75b77c..876aad4 100644 --- a/src/inference/equivalence/SemanticEquivalenceProofSystem.java +++ b/src/inference/equivalence/SemanticEquivalenceProofSystem.java @@ -19,7 +19,7 @@ import models.terms.RDLTerm; import models.terms.meta.MetaEvaluatableTermVariable; import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaResourceVariable; +import models.terms.meta.MetaResource; import models.terms.meta.OrderConstraint; import models.terms.meta.OrderVariableConstraint; @@ -32,8 +32,8 @@ private static MetaSemanticEquivalenceRelation rule1 = new MetaSemanticEquivalenceRelation( new MetaRDLTerm( - new MetaResourceVariable(new Variable("v"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))), - new MetaResourceVariable(new Variable("v"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))), + new MetaResource(new Variable("v"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))), + new MetaResource(new Variable("v"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))), new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n"), LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED) ), new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n"), LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED), @@ -49,12 +49,12 @@ private static MetaSemanticEquivalenceRelation rule4_2 = new MetaSemanticEquivalenceRelation( new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("t"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))), - new MetaResourceVariable(new Variable("v"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))), + new MetaResource(new Variable("v"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))), new MetaEvaluatableTermVariable(new Variable("s"), OrderConstraint.LT, new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))) ), new MetaRDLTerm( new MetaEvaluatableTermVariable(new Variable("t'"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))), - new MetaResourceVariable(new Variable("v"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))), + new MetaResource(new Variable("v"), new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))), new MetaEvaluatableTermVariable(new Variable("s"), OrderConstraint.LT, new Term(DataConstraintModel.add, List.of(new Variable("n"), new Constant("1")))) ), new Variable("n") diff --git a/src/inference/rewrite/RewriteInferenceSystem.java b/src/inference/rewrite/RewriteInferenceSystem.java new file mode 100644 index 0000000..8ce7ec7 --- /dev/null +++ b/src/inference/rewrite/RewriteInferenceSystem.java @@ -0,0 +1,118 @@ +package inference.rewrite; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; + +import models.formulas.EquationFormula; +import models.formulas.Formula; +import models.formulas.Then; +import models.terms.DependencyTerm; +import models.terms.EvaluatableTerm; +import models.terms.PrimedTerm; +import models.terms.Resource; + +public class RewriteInferenceSystem { + + List constraintFormulas = new ArrayList<>(); + List invariantFormulas = new ArrayList<>(); + EquationFormula inputFormula; + List conditionalFormulas = new ArrayList<>(); + List otherFormulas = new ArrayList<>(); + Formula conclusion; + + public RewriteInferenceSystem(List assumptions, Formula conclusion) { + for (Formula assumption : assumptions) { + if (inputFormulaCheck(assumption)) { + inputFormula = (EquationFormula) assumption; + } else if(invariantFormulaCheck(assumption)) { + invariantFormulas.add(assumption); + } else if (assumption instanceof EquationFormula) { + constraintFormulas.add(assumption); + } else { + otherFormulas.add(assumption); + } + } + + if (conclusion instanceof Then then) { + conditionalFormulas.add(then.getCondition()); + this.conclusion = then.getResult(); + } else { + this.conclusion = conclusion; + } + + } + + public boolean inference() { + Map> resourceTree = new HashMap<>(); + Resource root = parseDependencyTerm(inputFormula.getLeftSideHand(), resourceTree, new ArrayList<>()); + return false; + } + + private Resource parseDependencyTerm(EvaluatableTerm term, Map> resourceTree, List tops) { + if (term instanceof Resource resource) { + if (tops.isEmpty()) { + resourceTree.put(resource, new ArrayList<>()); + tops.add(resource); + } else { + for (Resource top : tops) { + resourceTree.get(top).add(resource); + resourceTree.put(resource, new ArrayList<>()); + } + tops.clear(); + tops.add(resource); + } + return resource; + } + Resource root; + DependencyTerm depTerm = (DependencyTerm) term; + EvaluatableTerm dependingTerm = depTerm.getDependingTerm(); + List dependedTerms = depTerm.getDependedTerms(); + List argumentTerms = depTerm.getArgumentTerms(); + root = parseDependencyTerm(dependingTerm, resourceTree, tops); + List nextTops = new ArrayList<>(); + for (int i = 0; i < dependedTerms.size(); i++) { + List currentTops = new ArrayList<>(tops); + parseDependencyTerm(dependedTerms.get(i), resourceTree, currentTops); + parseDependencyTerm(argumentTerms.get(i), resourceTree, currentTops); + nextTops.addAll(currentTops); + } + tops.clear(); + tops.addAll(nextTops); + return root; + } + + + private boolean inputFormulaCheck(Formula formula) { + if (! (formula instanceof EquationFormula equation)) { + return false; + } + List resources = new ArrayList<>(equation.getLeftSideHand().getSubTerms(Resource.class).values()); + resources.addAll(equation.getRightSideHand().getSubTerms(Resource.class).values()); + for (Resource resource : resources) { + if (resource.getOrder() == 0) { + return true; + } + } + return false; + } + + private boolean invariantFormulaCheck(Formula formula) { + if (! (formula instanceof EquationFormula equation)) { + return false; + } + EvaluatableTerm leftSideHand = equation.getLeftSideHand(); + EvaluatableTerm rightSideHand = equation.getRightSideHand(); + + if (leftSideHand instanceof PrimedTerm) { + return ((PrimedTerm) leftSideHand).getPrimedTerm().equals(rightSideHand); + } else if (rightSideHand instanceof PrimedTerm) { + return ((PrimedTerm) rightSideHand).getPrimedTerm().equals(leftSideHand); + } + + return false; + } + + +} diff --git a/src/models/formulas/DependencyFormula.java b/src/models/formulas/DependencyFormula.java index bc83cd7..269aafd 100644 --- a/src/models/formulas/DependencyFormula.java +++ b/src/models/formulas/DependencyFormula.java @@ -3,7 +3,7 @@ import lombok.Getter; import models.terms.Dependency; import models.terms.RDLTerm; -import models.terms.ResourceVariable; +import models.terms.Resource; @Getter public class DependencyFormula extends Formula { @@ -14,7 +14,7 @@ this.dependency = dependency; } - public DependencyFormula(RDLTerm dependingTerm, ResourceVariable dependedVariable) { + public DependencyFormula(RDLTerm dependingTerm, Resource dependedVariable) { this.dependency = new Dependency(dependingTerm, dependedVariable); } diff --git a/src/models/formulas/Then.java b/src/models/formulas/Then.java new file mode 100644 index 0000000..6466300 --- /dev/null +++ b/src/models/formulas/Then.java @@ -0,0 +1,33 @@ +package models.formulas; + +import lombok.AllArgsConstructor; +import lombok.Getter; + +@Getter +@AllArgsConstructor +public class Then extends Formula { + + private Formula condition; + private Formula result; + + + @Override + public String toString() { + return condition.toString() + " => " + result.toString(); + } + + @Override + public int hashCode() { + return toString().hashCode(); + } + + @Override + public boolean equals(Object another) { + if (! (another instanceof Then)) { + return false; + } + Then then = (Then) another; + return this.condition.equals(then.getCondition()) && this.result.equals(then.getResult()); + } + +} diff --git a/src/models/formulas/meta/MetaDependencyFormula.java b/src/models/formulas/meta/MetaDependencyFormula.java index 12dd807..68f9888 100644 --- a/src/models/formulas/meta/MetaDependencyFormula.java +++ b/src/models/formulas/meta/MetaDependencyFormula.java @@ -11,7 +11,7 @@ import models.terms.RDLTerm; import models.terms.meta.MetaDependencyVariable; import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaResourceVariable; +import models.terms.meta.MetaResource; import models.terms.meta.OrderVariableConstraint; @Getter @@ -30,7 +30,7 @@ this.dependency = dependency; } - public MetaDependencyFormula(MetaRDLTerm dependingTerm, MetaResourceVariable dependedVariable) { + public MetaDependencyFormula(MetaRDLTerm dependingTerm, MetaResource dependedVariable) { this.dependency = new MetaRDLTerm(dependingTerm, dependedVariable); } diff --git a/src/models/terms/Dependency.java b/src/models/terms/Dependency.java index e334f94..eee07c7 100644 --- a/src/models/terms/Dependency.java +++ b/src/models/terms/Dependency.java @@ -7,11 +7,11 @@ public class Dependency extends RDLTerm{ private RDLTerm dependingTerm; - private ResourceVariable dependedVariable; + private Resource dependedVariable; private Dependency dependency; private boolean isListType; - public Dependency(RDLTerm dependingTerm, ResourceVariable dependedVariable) { + public Dependency(RDLTerm dependingTerm, Resource dependedVariable) { super(new Symbol(":", 2), dependedVariable.getOrder(), dependingTerm.getSize() + dependedVariable.getSize()); this.dependingTerm = dependingTerm; this.dependedVariable = dependedVariable; @@ -30,7 +30,7 @@ this.isListType = true; } - public Dependency(RDLTerm dependingTerm, ResourceVariable dependedVariable, int order) { + 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; @@ -66,7 +66,7 @@ this.dependingTerm = newTerm; } - public void setDependedVariable(ResourceVariable newVariable) { + public void setDependedVariable(Resource newVariable) { setChild(1, newVariable); this.dependedVariable = newVariable; } @@ -134,7 +134,7 @@ @Override public Object clone() { - return new Dependency((RDLTerm) dependingTerm.clone(), (ResourceVariable) dependedVariable.clone()); + return new Dependency((RDLTerm) dependingTerm.clone(), (Resource) dependedVariable.clone()); } } diff --git a/src/models/terms/PrimedTerm.java b/src/models/terms/PrimedTerm.java new file mode 100644 index 0000000..96eb108 --- /dev/null +++ b/src/models/terms/PrimedTerm.java @@ -0,0 +1,52 @@ +package models.terms; + +import lombok.Getter; + +@Getter +public class PrimedTerm extends EvaluatableTerm { + + private EvaluatableTerm primedTerm; + + protected PrimedTerm(EvaluatableTerm term) { + super(term.getSymbol(), term.getOrder(), term.getSize()); + this.primedTerm = term; + } + + @Override + public String toString() { + return primedTerm.toString() + "'"; + } + + @Override + public String toStringWithOrder() { + return toString() + "(" + primedTerm.getOrder() + ")"; + } + + @Override + public int hashCode() { + return toStringWithOrder().hashCode(); + } + + @Override + public Object clone() { + return new PrimedTerm(primedTerm); + } + + @Override + public boolean isLinearRightNormalized() { + return primedTerm.isLinearRightNormalized(); + } + + @Override + public EvaluatableTerm linearRightNormalize() { + return new PrimedTerm(primedTerm.linearRightNormalize()); + } + + @Override + public void selfLinearRightNormalize() { + primedTerm.selfLinearRightNormalize(); + } + + + +} diff --git a/src/models/terms/Resource.java b/src/models/terms/Resource.java new file mode 100644 index 0000000..e5274fb --- /dev/null +++ b/src/models/terms/Resource.java @@ -0,0 +1,63 @@ +package models.terms; + +import lombok.Getter; +import models.algebra.Symbol; +import models.algebra.Type; + +@Getter +public class Resource extends EvaluatableTerm { + + private String name; + private Type type; + + public Resource(String name, Type type, int order) { + super(new Symbol("", 0), order, 1); + this.name = name; + this.type = type; + } + + @Override + public EvaluatableTerm linearRightNormalize() { + return (Resource) clone(); + } + + @Override + public void selfLinearRightNormalize() { + } + + @Override + public boolean isLinearRightNormalized() { + return true; + } + + + @Override + public boolean equals(Object another) { + if(! (another instanceof Resource)) { + return false; + } + var vari = (Resource) another; + return vari.getOrder() == getOrder() && vari.getName().equals(getName()) && vari.getType().equals(getType()); + } + + @Override + public int hashCode() { + return ("Vari" + toStringWithOrder()).hashCode(); + } + + @Override + public String toString() { + return this.name; + } + + @Override + public String toStringWithOrder() { + return this.name + "(" + order + ")"; + } + + @Override + public Object clone() { + return new Resource(name, type, order); + } + +} diff --git a/src/models/terms/ResourceVariable.java b/src/models/terms/ResourceVariable.java deleted file mode 100644 index 57b0a9b..0000000 --- a/src/models/terms/ResourceVariable.java +++ /dev/null @@ -1,63 +0,0 @@ -package models.terms; - -import lombok.Getter; -import models.algebra.Symbol; -import models.algebra.Type; - -@Getter -public class ResourceVariable extends EvaluatableTerm{ - - private String name; - private Type type; - - public ResourceVariable(String name, Type type, int order) { - super(new Symbol("", 0), order, 1); - this.name = name; - this.type = type; - } - - @Override - public EvaluatableTerm linearRightNormalize() { - return (ResourceVariable) clone(); - } - - @Override - public void selfLinearRightNormalize() { - } - - @Override - public boolean isLinearRightNormalized() { - return true; - } - - - @Override - public boolean equals(Object another) { - if(! (another instanceof ResourceVariable)) { - return false; - } - var vari = (ResourceVariable) another; - return vari.getOrder() == getOrder() && vari.getName().equals(getName()) && vari.getType().equals(getType()); - } - - @Override - public int hashCode() { - return ("Vari" + toStringWithOrder()).hashCode(); - } - - @Override - public String toString() { - return this.name; - } - - @Override - public String toStringWithOrder() { - return this.name + "(" + order + ")"; - } - - @Override - public Object clone() { - return new ResourceVariable(name, type, order); - } - -} diff --git a/src/models/terms/meta/MetaRDLTerm.java b/src/models/terms/meta/MetaRDLTerm.java index 93600c5..2072bd5 100644 --- a/src/models/terms/meta/MetaRDLTerm.java +++ b/src/models/terms/meta/MetaRDLTerm.java @@ -14,7 +14,7 @@ import models.terms.EvaluatableTerm; import models.terms.LinearRightNormalizedType; import models.terms.RDLTerm; -import models.terms.ResourceVariable; +import models.terms.Resource; import models.terms.SetEvaluatableTerm; @Getter @@ -32,21 +32,21 @@ } //dependency - public MetaRDLTerm(RDLTerm dependingTerm, MetaResourceVariable dependedVariable) { + public MetaRDLTerm(RDLTerm 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, ResourceVariable dependedVariable) { + 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, MetaResourceVariable dependedVariable) { + public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaResource dependedVariable) { super(new Symbol(":", 2), dependedVariable.getOrder(), dependingTerm.getSize() + dependedVariable.getSize()); addChild(dependingTerm); addChild(dependedVariable); @@ -65,7 +65,7 @@ } //dependency term - public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaResourceVariable dependedVariable, MetaRDLTerm argumentTerm) { + public MetaRDLTerm(MetaRDLTerm dependingTerm, MetaResource dependedVariable, MetaRDLTerm argumentTerm) { super(new Symbol(":", 3), -1, dependingTerm.getSize() + dependedVariable.getSize() + argumentTerm.getSize()); if (! EvaluatableTerm.class.isAssignableFrom(dependingTerm.getTermType().getBaseTermClass())) { throw new IllegalTypeException(); @@ -90,7 +90,7 @@ this.termType = TermType.META_DEPENDENCY_TERM; } - public MetaRDLTerm(MetaRDLTerm dependingTerm, ResourceVariable dependedVariable, MetaRDLTerm argumentTerm) { + 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(); @@ -115,7 +115,7 @@ this.termType = TermType.META_DEPENDENCY_TERM; } - public MetaRDLTerm(MetaRDLTerm dependingTerm, ResourceVariable dependedVariable, EvaluatableTerm argumentTerm) { + 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(); @@ -126,7 +126,7 @@ this.termType = TermType.META_DEPENDENCY_TERM; } - public MetaRDLTerm(EvaluatableTerm dependingTerm, MetaResourceVariable dependedVariable, EvaluatableTerm argumentTerm) { + public MetaRDLTerm(EvaluatableTerm dependingTerm, MetaResource dependedVariable, EvaluatableTerm argumentTerm) { super(new Symbol(":", 3), -1, dependingTerm.getSize() + dependedVariable.getSize() + argumentTerm.getSize()); addChild(dependingTerm); addChild(dependedVariable); @@ -134,7 +134,7 @@ this.termType = TermType.META_DEPENDENCY_TERM; } - public MetaRDLTerm(EvaluatableTerm dependingTerm, ResourceVariable dependedVariable, MetaRDLTerm argumentTerm) { + 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(); @@ -155,8 +155,8 @@ if (dependedVariable instanceof MetaRDLTerm) { dependedVariable = ((MetaRDLTerm) dependedVariable).substitute(binding); } - if (dependedVariable instanceof ResourceVariable) { - return new Dependency(dependingTerm, (ResourceVariable) dependedVariable); + if (dependedVariable instanceof Resource) { + return new Dependency(dependingTerm, (Resource) dependedVariable); } } else if (isDependencyTerm()) { @@ -172,7 +172,7 @@ if (argumentTerm instanceof MetaRDLTerm) { argumentTerm = ((MetaRDLTerm) argumentTerm).substitute(binding); } - return new DependencyTerm((EvaluatableTerm) dependingTerm, (ResourceVariable) dependedVariable, (EvaluatableTerm) argumentTerm); + return new DependencyTerm((EvaluatableTerm) dependingTerm, (Resource) dependedVariable, (EvaluatableTerm) argumentTerm); } else if (isSetTerm()) { RDLTerm term = (RDLTerm) getChild(0); if (term instanceof MetaRDLTerm) { @@ -239,7 +239,7 @@ } public boolean isResourceVariable() { - return checkTermType(ResourceVariable.class); + return checkTermType(Resource.class); } public void setLinearRightNormalizedType(LinearRightNormalizedType next) { @@ -330,7 +330,7 @@ META_EVALUATABLE_TERM_VARIABLE(EvaluatableTerm.class), META_EVALUATABLE_TERM_SET(SetEvaluatableTerm.class), META_EVALUATABLE_TERM_SET_VARIABLE(SetEvaluatableTerm.class), - META_RESOURCE_VARIABLE(ResourceVariable.class); + META_RESOURCE_VARIABLE(Resource.class); @Getter private Class baseTermClass; diff --git a/src/models/terms/meta/MetaResource.java b/src/models/terms/meta/MetaResource.java new file mode 100644 index 0000000..d28b163 --- /dev/null +++ b/src/models/terms/meta/MetaResource.java @@ -0,0 +1,50 @@ +package models.terms.meta; + +import java.util.Map; + +import lombok.Getter; +import models.algebra.Constant; +import models.algebra.Expression; +import models.algebra.Symbol; +import models.algebra.Variable; +import models.terms.RDLTerm; +import models.terms.ResourceConstant; +import models.terms.Resource; + +@Getter +public class MetaResource extends MetaVariable { + + public MetaResource(Variable variableName, OrderConstraint constraint, Expression order) { + super(new Symbol("", 0), MetaRDLTerm.TermType.META_RESOURCE_VARIABLE, variableName, constraint, order); + } + + public MetaResource(Variable variableName) { + super(new Symbol("", 0), MetaRDLTerm.TermType.META_RESOURCE_VARIABLE, variableName, OrderConstraint.ANY, new Constant("0")); + } + + public MetaResource(Variable variableName, Expression order) { + super(new Symbol("", 0), MetaRDLTerm.TermType.META_RESOURCE_VARIABLE, variableName, OrderConstraint.EQ, order); + } + + @Override + public boolean isMatchedBy(RDLTerm another, Map binding, + Map orderConstraint) { + if ((! (another instanceof Resource)) && (! (another instanceof ResourceConstant))) { + return false; + } + + if (! orderConstraintCheck(another, orderConstraint)) { + return false; + } + + if (! islinearRightNormalizedMatchedBy(another)) { + return false; + } + + if (! binding.containsKey(this.variableName)) { + binding.put(this.variableName, another); + return true; + } + return binding.get(this.variableName).equals(another); + } +} diff --git a/src/models/terms/meta/MetaResourceVariable.java b/src/models/terms/meta/MetaResourceVariable.java deleted file mode 100644 index 19be600..0000000 --- a/src/models/terms/meta/MetaResourceVariable.java +++ /dev/null @@ -1,50 +0,0 @@ -package models.terms.meta; - -import java.util.Map; - -import lombok.Getter; -import models.algebra.Constant; -import models.algebra.Expression; -import models.algebra.Symbol; -import models.algebra.Variable; -import models.terms.RDLTerm; -import models.terms.ResourceConstant; -import models.terms.ResourceVariable; - -@Getter -public class MetaResourceVariable extends MetaVariable { - - public MetaResourceVariable(Variable variableName, OrderConstraint constraint, Expression order) { - super(new Symbol("", 0), MetaRDLTerm.TermType.META_RESOURCE_VARIABLE, variableName, constraint, order); - } - - public MetaResourceVariable(Variable variableName) { - super(new Symbol("", 0), MetaRDLTerm.TermType.META_RESOURCE_VARIABLE, variableName, OrderConstraint.ANY, new Constant("0")); - } - - public MetaResourceVariable(Variable variableName, Expression order) { - super(new Symbol("", 0), MetaRDLTerm.TermType.META_RESOURCE_VARIABLE, variableName, OrderConstraint.EQ, order); - } - - @Override - public boolean isMatchedBy(RDLTerm another, Map binding, - Map orderConstraint) { - if ((! (another instanceof ResourceVariable)) && (! (another instanceof ResourceConstant))) { - return false; - } - - if (! orderConstraintCheck(another, orderConstraint)) { - return false; - } - - if (! islinearRightNormalizedMatchedBy(another)) { - return false; - } - - if (! binding.containsKey(this.variableName)) { - binding.put(this.variableName, another); - return true; - } - return binding.get(this.variableName).equals(another); - } -} diff --git a/src/tests/equivalence/SubstituteTest.java b/src/tests/equivalence/SubstituteTest.java index 2eac027..15dfd37 100644 --- a/src/tests/equivalence/SubstituteTest.java +++ b/src/tests/equivalence/SubstituteTest.java @@ -12,30 +12,30 @@ import models.terms.DependencyTerm; import models.terms.LinearRightNormalizedType; import models.terms.RDLTerm; -import models.terms.ResourceVariable; +import models.terms.Resource; import models.terms.meta.MetaEvaluatableTermVariable; import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaResourceVariable; +import models.terms.meta.MetaResource; import models.terms.meta.OrderConstraint; import models.terms.meta.OrderVariableConstraint; import tests.Utils; public class SubstituteTest { - ResourceVariable A = new ResourceVariable("A", Utils.INT, 2); - ResourceVariable Ap = new ResourceVariable("A'", Utils.INT, 2); - ResourceVariable B = new ResourceVariable("B", Utils.INT, 2); - ResourceVariable Bp = new ResourceVariable("B'", Utils.INT, 2); - ResourceVariable C = new ResourceVariable("C", Utils.INT, 2); - ResourceVariable Cp = new ResourceVariable("C'", Utils.INT, 2); - ResourceVariable D = new ResourceVariable("D", Utils.INT, 2); - ResourceVariable E = new ResourceVariable("E", Utils.INT, 1); - ResourceVariable F = new ResourceVariable("F", Utils.INT, 1); - ResourceVariable G = new ResourceVariable("G", Utils.INT, 0); + Resource A = new Resource("A", Utils.INT, 2); + Resource Ap = new Resource("A'", Utils.INT, 2); + Resource B = new Resource("B", Utils.INT, 2); + Resource Bp = new Resource("B'", Utils.INT, 2); + Resource C = new Resource("C", Utils.INT, 2); + Resource Cp = new Resource("C'", Utils.INT, 2); + Resource D = new Resource("D", Utils.INT, 2); + Resource E = new Resource("E", Utils.INT, 1); + Resource F = new Resource("F", Utils.INT, 1); + Resource G = new Resource("G", Utils.INT, 0); @Test void SubstituteTest1() { - MetaResourceVariable v = new MetaResourceVariable(new Variable("v"), Utils.parse("n + 1")); + MetaResource v = new MetaResource(new Variable("v"), Utils.parse("n + 1")); MetaEvaluatableTermVariable t = new MetaEvaluatableTermVariable(new Variable("t"), Utils.parse("n")); t.setLinearRightNormalizedType(LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED); MetaSemanticEquivalenceRelation r1 = new MetaSemanticEquivalenceRelation(new MetaRDLTerm(v, v, t), t, new Variable("n")); @@ -56,7 +56,7 @@ DependencyTerm t1 = new DependencyTerm(A, B, C); DependencyTerm t2 = new DependencyTerm(Ap, Bp, Cp); SemanticEquivalenceRelation r2 = new SemanticEquivalenceRelation(t1, t2, 2); - MetaResourceVariable v = new MetaResourceVariable(new Variable("v"), Utils.parse("n + 1")); + 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), diff --git a/src/tests/formulas/meta/MetaEquationFormulaTest.java b/src/tests/formulas/meta/MetaEquationFormulaTest.java index 561ab6b..16f2126 100644 --- a/src/tests/formulas/meta/MetaEquationFormulaTest.java +++ b/src/tests/formulas/meta/MetaEquationFormulaTest.java @@ -13,27 +13,27 @@ import models.terms.Dependency; import models.terms.DependencyTerm; import models.terms.EvaluatableTerm; -import models.terms.ResourceVariable; +import models.terms.Resource; import models.terms.meta.MetaEvaluatableTermVariable; import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaResourceVariable; +import models.terms.meta.MetaResource; 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); + Resource a = new Resource("a", INT, 0); + Resource b = new Resource("b", INT, 0); + Resource c = new Resource("c", INT, 0); + Resource d = new Resource("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")); + MetaResource v = new MetaResource(new Variable("v")); MetaEvaluatableTermVariable te = new MetaEvaluatableTermVariable(new Variable("te")); MetaEvaluatableTermVariable ue = new MetaEvaluatableTermVariable(new Variable("ue")); MetaRDLTerm left = new MetaRDLTerm(se, v, te); @@ -47,16 +47,16 @@ @Test void MetaDependencyFormulaMatchingTest() { - ResourceVariable a = new ResourceVariable("a", INT, 0); - ResourceVariable b = new ResourceVariable("b", INT, 0); - ResourceVariable c = new ResourceVariable("c", INT, 0); + Resource a = new Resource("a", INT, 0); + Resource b = new Resource("b", INT, 0); + Resource c = new Resource("c", INT, 0); EvaluatableTerm te1 = new DependencyTerm(a, b, c); - ResourceVariable d = new ResourceVariable("d", INT, 0); + Resource d = new Resource("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")); + MetaResource w = new MetaResource(new Variable("w")); MetaRDLTerm dep = new MetaRDLTerm(te, w); MetaDependencyFormula metaDepF = new MetaDependencyFormula(dep); diff --git a/src/tests/inferencerule/InferenceRuleTest.java b/src/tests/inferencerule/InferenceRuleTest.java index 7cb7b04..dd70b94 100644 --- a/src/tests/inferencerule/InferenceRuleTest.java +++ b/src/tests/inferencerule/InferenceRuleTest.java @@ -15,18 +15,18 @@ import models.formulas.meta.MetaEquationFormula; import models.terms.Dependency; import models.terms.DependencyTerm; -import models.terms.ResourceVariable; +import models.terms.Resource; import models.terms.meta.MetaEvaluatableTermVariable; import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaResourceVariable; +import models.terms.meta.MetaResource; 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")); + MetaResource v = new MetaResource(new Variable("v")); + MetaResource w = new MetaResource(new Variable("w")); MetaRDLTerm metaD1 = new MetaRDLTerm(te, v); MetaRDLTerm metaD2 = new MetaRDLTerm(v, w); MetaRDLTerm metaD3 = new MetaRDLTerm(te, w); @@ -35,9 +35,9 @@ 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); + Resource a = new Resource("a", INT, 0); + Resource b = new Resource("b", INT, 0); + Resource c = new Resource("c", INT, 0); Dependency d1 = new Dependency(a, b); Dependency d2 = new Dependency(b, c); Dependency d3 = new Dependency(a, c); @@ -53,7 +53,7 @@ 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")); + MetaResource v = new MetaResource(new Variable("v")); MetaEquationFormula assump1 = new MetaEquationFormula(te, ue); MetaEquationFormula concl1 = new MetaEquationFormula(new MetaRDLTerm(se, v, te), new MetaRDLTerm(se, v, ue)); /* @@ -63,12 +63,12 @@ */ 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); + Resource a = new Resource("a", INT, 0); + Resource c = new Resource("c", INT, 0); + Resource d = new Resource("d", INT, 0); + Resource x = new Resource("x", INT, 0); + Resource y = new Resource("y", INT, 0); + Resource z = new Resource("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]] diff --git a/src/tests/terms/EqualsTest.java b/src/tests/terms/EqualsTest.java index 48ebe7e..282f58c 100644 --- a/src/tests/terms/EqualsTest.java +++ b/src/tests/terms/EqualsTest.java @@ -5,18 +5,18 @@ import org.junit.jupiter.api.Test; import models.terms.DependencyTerm; -import models.terms.ResourceVariable; +import models.terms.Resource; import tests.Utils; public class EqualsTest { @Test void DependencyTermEqualsTest() { - ResourceVariable A = new ResourceVariable("A", Utils.INT, 1); - ResourceVariable B = new ResourceVariable("B", Utils.INT, 1); - ResourceVariable C = new ResourceVariable("C", Utils.INT, 1); - ResourceVariable D = new ResourceVariable("D", Utils.INT, 1); - ResourceVariable E = new ResourceVariable("E", Utils.INT, 1); + 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); DependencyTerm t1 = new DependencyTerm(A, B, C, D, E); DependencyTerm t2 = new DependencyTerm(A, D, E, B, C); diff --git a/src/tests/terms/LinearRightNormalTest.java b/src/tests/terms/LinearRightNormalTest.java index 4491b6a..872a1f5 100644 --- a/src/tests/terms/LinearRightNormalTest.java +++ b/src/tests/terms/LinearRightNormalTest.java @@ -10,10 +10,10 @@ import models.terms.DependencyTerm; import models.terms.EvaluatableTerm; import models.terms.LinearRightNormalizedType; -import models.terms.ResourceVariable; +import models.terms.Resource; import models.terms.meta.MetaEvaluatableTermVariable; import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaResourceVariable; +import models.terms.meta.MetaResource; public class LinearRightNormalTest { @@ -23,13 +23,13 @@ void linearRightNormalTest() { - ResourceVariable a = new ResourceVariable("A", INT, 2); - ResourceVariable b = new ResourceVariable("B", INT, 2); - ResourceVariable c = new ResourceVariable("C", INT, 2); - ResourceVariable d = new ResourceVariable("D", INT, 2); - ResourceVariable e = new ResourceVariable("E", INT, 2); - ResourceVariable f = new ResourceVariable("F", INT, 2); - ResourceVariable g = new ResourceVariable("G", INT, 1); + Resource a = new Resource("A", INT, 2); + Resource b = new Resource("B", INT, 2); + Resource c = new Resource("C", INT, 2); + Resource d = new Resource("D", INT, 2); + Resource e = new Resource("E", INT, 2); + Resource f = new Resource("F", INT, 2); + Resource g = new Resource("G", INT, 1); EvaluatableTerm te1 = new DependencyTerm(e, f, g); EvaluatableTerm te2 = new DependencyTerm(c, d, te1); @@ -47,13 +47,13 @@ @Test void linearRightNormalizeTest() { - ResourceVariable a = new ResourceVariable("A", INT, 2); - ResourceVariable b = new ResourceVariable("B", INT, 2); - ResourceVariable c = new ResourceVariable("C", INT, 2); - ResourceVariable d = new ResourceVariable("D", INT, 2); - ResourceVariable e = new ResourceVariable("E", INT, 2); - ResourceVariable f = new ResourceVariable("F", INT, 2); - ResourceVariable g = new ResourceVariable("G", INT, 1); + Resource a = new Resource("A", INT, 2); + Resource b = new Resource("B", INT, 2); + Resource c = new Resource("C", INT, 2); + Resource d = new Resource("D", INT, 2); + Resource e = new Resource("E", INT, 2); + Resource f = new Resource("F", INT, 2); + Resource g = new Resource("G", INT, 1); EvaluatableTerm te1 = new DependencyTerm(a, b, c); EvaluatableTerm te2 = new DependencyTerm(te1, d, e); @@ -66,22 +66,22 @@ @Test void linearRightNomalizedMatchTest() { - ResourceVariable a = new ResourceVariable("A", INT, 2); - ResourceVariable b = new ResourceVariable("B", INT, 2); - ResourceVariable c = new ResourceVariable("C", INT, 2); - ResourceVariable d = new ResourceVariable("D", INT, 2); - ResourceVariable e = new ResourceVariable("E", INT, 2); - ResourceVariable f = new ResourceVariable("F", INT, 2); - ResourceVariable g = new ResourceVariable("G", INT, 1); + Resource a = new Resource("A", INT, 2); + Resource b = new Resource("B", INT, 2); + Resource c = new Resource("C", INT, 2); + Resource d = new Resource("D", INT, 2); + Resource e = new Resource("E", INT, 2); + Resource f = new Resource("F", INT, 2); + Resource g = new Resource("G", INT, 1); EvaluatableTerm te1 = new DependencyTerm(a, b, c); EvaluatableTerm te2 = new DependencyTerm(te1, d, e); EvaluatableTerm te3 = new DependencyTerm(te2, f, g); MetaEvaluatableTermVariable metaTerm = new MetaEvaluatableTermVariable(new Variable("x")); - MetaResourceVariable metaA = new MetaResourceVariable(new Variable("ma")); - MetaResourceVariable metaB = new MetaResourceVariable(new Variable("mb")); - MetaResourceVariable metaC = new MetaResourceVariable(new Variable("mc")); + MetaResource metaA = new MetaResource(new Variable("ma")); + MetaResource metaB = new MetaResource(new Variable("mb")); + MetaResource metaC = new MetaResource(new Variable("mc")); MetaRDLTerm metaTerm2 = new MetaRDLTerm(metaA, metaB, metaC); metaTerm2.setLinearRightNormalizedType(LinearRightNormalizedType.LINEAR_RIGHT_NORMALIZED); diff --git a/src/tests/terms/meta/MetaDependencyVariableTest.java b/src/tests/terms/meta/MetaDependencyVariableTest.java index 0f2e9f9..e893131 100644 --- a/src/tests/terms/meta/MetaDependencyVariableTest.java +++ b/src/tests/terms/meta/MetaDependencyVariableTest.java @@ -9,7 +9,7 @@ import models.algebra.Variable; import models.terms.Dependency; import models.terms.DependencyTerm; -import models.terms.ResourceVariable; +import models.terms.Resource; import models.terms.meta.MetaDependencyVariable; import models.terms.meta.OrderConstraint; @@ -17,9 +17,9 @@ @Test void MetaDependencyVariableMatchingWithoutOrderTest() { - ResourceVariable a = new ResourceVariable("a", INT, 1); - ResourceVariable b = new ResourceVariable("b", INT, 1); - ResourceVariable c = new ResourceVariable("c", INT, 1); + Resource a = new Resource("a", INT, 1); + 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); @@ -37,9 +37,9 @@ @Test void MetaDependencyVariableMatchingWithConstantOrderEQTest() { - ResourceVariable a = new ResourceVariable("a", INT, 1); - ResourceVariable b = new ResourceVariable("b", INT, 1); - ResourceVariable c = new ResourceVariable("c", INT, 2); + Resource a = new Resource("a", INT, 1); + Resource b = new Resource("b", INT, 1); + Resource c = new Resource("c", INT, 2); Dependency dep1 = new Dependency(a, b); Dependency dep2 = new Dependency(a, c); @@ -52,10 +52,10 @@ @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); + Resource a = new Resource("a", INT, 0); + Resource b = new Resource("b", INT, 1); + Resource c = new Resource("c", INT, 2); + Resource e = new Resource("e", INT, 0); Dependency dep1 = new Dependency(a, b); Dependency dep2 = new Dependency(a, c); Dependency dep3 = new Dependency(a, e); @@ -71,10 +71,10 @@ @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); + Resource a = new Resource("a", INT, 0); + Resource b = new Resource("b", INT, 1); + Resource c = new Resource("c", INT, 2); + Resource e = new Resource("e", INT, 0); Dependency dep1 = new Dependency(a, b); Dependency dep2 = new Dependency(a, c); Dependency dep3 = new Dependency(a, e); @@ -90,10 +90,10 @@ @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); + Resource a = new Resource("a", INT, 0); + Resource b = new Resource("b", INT, 1); + Resource c = new Resource("c", INT, 2); + Resource e = new Resource("e", INT, 0); Dependency dep1 = new Dependency(a, b); Dependency dep2 = new Dependency(a, c); Dependency dep3 = new Dependency(a, e); @@ -109,10 +109,10 @@ @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); + Resource a = new Resource("a", INT, 0); + Resource b = new Resource("b", INT, 1); + Resource c = new Resource("c", INT, 2); + Resource e = new Resource("e", INT, 0); Dependency dep1 = new Dependency(a, b); Dependency dep2 = new Dependency(a, c); Dependency dep3 = new Dependency(a, e); diff --git a/src/tests/terms/meta/MetaEvaluatableTermVariableTest.java b/src/tests/terms/meta/MetaEvaluatableTermVariableTest.java index 7f527c2..042f101 100644 --- a/src/tests/terms/meta/MetaEvaluatableTermVariableTest.java +++ b/src/tests/terms/meta/MetaEvaluatableTermVariableTest.java @@ -7,7 +7,7 @@ import models.algebra.Variable; import models.terms.DependencyTerm; import models.terms.ResourceConstant; -import models.terms.ResourceVariable; +import models.terms.Resource; import models.terms.meta.MetaEvaluatableTermVariable; import tests.Utils; @@ -17,9 +17,9 @@ void isMatchedByTest() { MetaEvaluatableTermVariable se = new MetaEvaluatableTermVariable(new Variable("se")); - ResourceVariable a = new ResourceVariable("a", Utils.INT, 1); - ResourceVariable b = new ResourceVariable("b", Utils.INT, 1); - ResourceVariable c = new ResourceVariable("c", Utils.INT, 1); + Resource a = new Resource("a", Utils.INT, 1); + Resource b = new Resource("b", Utils.INT, 1); + Resource c = new Resource("c", Utils.INT, 1); ResourceConstant one = new ResourceConstant("1"); DependencyTerm t1 = new DependencyTerm(a, b, c); diff --git a/src/tests/terms/meta/MetaRDLTermTest.java b/src/tests/terms/meta/MetaRDLTermTest.java index bc9baf7..2c5f28b 100644 --- a/src/tests/terms/meta/MetaRDLTermTest.java +++ b/src/tests/terms/meta/MetaRDLTermTest.java @@ -9,25 +9,25 @@ import models.algebra.Variable; import models.terms.Dependency; import models.terms.DependencyTerm; -import models.terms.ResourceVariable; +import models.terms.Resource; import models.terms.meta.MetaDependencyTermVariable; import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaResourceVariable; +import models.terms.meta.MetaResource; 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); + Resource a = new Resource("a", INT, 1); + Resource b = new Resource("b", INT, 1); + Resource c = new Resource("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")); + MetaResource v1 = new MetaResource(new Variable("v1")); + MetaResource v2 = new MetaResource(new Variable("v2")); + MetaResource v3 = new MetaResource(new Variable("v3")); MetaDependencyTermVariable vte = new MetaDependencyTermVariable(new Variable("vte")); MetaRDLTerm metaDep = new MetaRDLTerm(v1, v2); MetaRDLTerm metaDep2 = new MetaRDLTerm(vte, v2); @@ -49,17 +49,17 @@ @Test void MetaDependencyMatchingWithConstantOrderTest() { - MetaResourceVariable v1 = new MetaResourceVariable(new Variable("v1"), new Constant("1")); - MetaResourceVariable v2 = new MetaResourceVariable(new Variable("v2"), new Constant("2")); + MetaResource v1 = new MetaResource(new Variable("v1"), new Constant("1")); + MetaResource v2 = new MetaResource(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); + Resource a1 = new Resource("a1", INT, 1); + Resource a2 = new Resource("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); + Resource b1 = new Resource("b1", INT, 1); Dependency d2 = new Dependency(a1, b1); //[1 : 1] does not match [1 : 2] assertFalse(vd1.isMatchedBy(d2)); @@ -67,17 +67,17 @@ @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")); + MetaResource v1 = new MetaResource(new Variable("v1"), parse("x")); + MetaResource v2 = new MetaResource(new Variable("v2"), parse("x")); + MetaResource v3 = new MetaResource(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); + Resource a1 = new Resource("a1", INT, 1); + Resource a2 = new Resource("a2", INT, 2); + Resource b1 = new Resource("b1", INT, 1); + Resource b2 = new Resource("b2", INT, 2); Dependency d1 = new Dependency(a1, a2); Dependency d2 = new Dependency(a1, b1); Dependency d3 = new Dependency(new Dependency(a1, b1), a2); diff --git a/src/tests/terms/meta/MetaResourceVariableTest.java b/src/tests/terms/meta/MetaResourceVariableTest.java index 6c921ee..35f422a 100644 --- a/src/tests/terms/meta/MetaResourceVariableTest.java +++ b/src/tests/terms/meta/MetaResourceVariableTest.java @@ -8,25 +8,25 @@ import models.algebra.Variable; import models.terms.Dependency; import models.terms.DependencyTerm; -import models.terms.ResourceVariable; +import models.terms.Resource; import models.terms.meta.MetaDependencyTermVariable; import models.terms.meta.MetaDependencyVariable; import models.terms.meta.MetaEvaluatableTermVariable; import models.terms.meta.MetaRDLTermVariable; -import models.terms.meta.MetaResourceVariable; +import models.terms.meta.MetaResource; import models.terms.meta.OrderConstraint; public class MetaResourceVariableTest { @Test void MetaResourceVariableMathcingWithoutOrder() { - ResourceVariable a = new ResourceVariable("a", INT, 0); - ResourceVariable b = new ResourceVariable("b", INT, 0); - ResourceVariable c = new ResourceVariable("c", INT, 0); + Resource a = new Resource("a", INT, 0); + Resource b = new Resource("b", INT, 0); + Resource c = new Resource("c", INT, 0); Dependency dep = new Dependency(a, b); DependencyTerm depTerm = new DependencyTerm(a, b, c); - MetaResourceVariable x = new MetaResourceVariable(new Variable("x")); + MetaResource x = new MetaResource(new Variable("x")); MetaDependencyVariable d = new MetaDependencyVariable(new Variable("d")); MetaDependencyTermVariable dte = new MetaDependencyTermVariable(new Variable("dte")); MetaEvaluatableTermVariable te = new MetaEvaluatableTermVariable(new Variable("te")); @@ -50,9 +50,9 @@ @Test void MetaResourceVariableMathcingWithConstantOrderEQ() { - ResourceVariable a = new ResourceVariable("a", INT, 1); - MetaResourceVariable x = new MetaResourceVariable(new Variable("x"), parse("0")); - MetaResourceVariable y = new MetaResourceVariable(new Variable("y"), parse("1")); + Resource a = new Resource("a", INT, 1); + 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)); //a(1) matches y(=1) @@ -61,10 +61,10 @@ @Test void MetaResourceVariableMathcingWithConstantOrderLT() { - ResourceVariable a = new ResourceVariable("a", INT, 1); - MetaResourceVariable x = new MetaResourceVariable(new Variable("x"), OrderConstraint.LT, parse("0")); - MetaResourceVariable y = new MetaResourceVariable(new Variable("y"), OrderConstraint.LT, parse("1")); - MetaResourceVariable z = new MetaResourceVariable(new Variable("z"), OrderConstraint.LT, parse("2")); + Resource a = new Resource("a", INT, 1); + MetaResource x = new MetaResource(new Variable("x"), OrderConstraint.LT, parse("0")); + 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)); //a(1) matches y(<1) @@ -75,10 +75,10 @@ @Test void MetaResourceVariableMathcingWithConstantOrderLE() { - ResourceVariable a = new ResourceVariable("a", INT, 1); - MetaResourceVariable x = new MetaResourceVariable(new Variable("x"), OrderConstraint.LE, parse("0")); - MetaResourceVariable y = new MetaResourceVariable(new Variable("y"), OrderConstraint.LE, parse("1")); - MetaResourceVariable z = new MetaResourceVariable(new Variable("z"), OrderConstraint.LE, parse("2")); + Resource a = new Resource("a", INT, 1); + MetaResource x = new MetaResource(new Variable("x"), OrderConstraint.LE, parse("0")); + 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)); //a(1) matches y(<=1) @@ -89,10 +89,10 @@ @Test void MetaResourceVariableMathcingWithConstantOrderGT() { - ResourceVariable a = new ResourceVariable("a", INT, 1); - MetaResourceVariable x = new MetaResourceVariable(new Variable("x"), OrderConstraint.GT, parse("0")); - MetaResourceVariable y = new MetaResourceVariable(new Variable("y"), OrderConstraint.GT, parse("1")); - MetaResourceVariable z = new MetaResourceVariable(new Variable("z"), OrderConstraint.GT, parse("2")); + Resource a = new Resource("a", INT, 1); + MetaResource x = new MetaResource(new Variable("x"), OrderConstraint.GT, parse("0")); + 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)); //a(1) matches y(>1) @@ -103,10 +103,10 @@ @Test void MetaResourceVariableMathcingWithConstantOrderGE() { - ResourceVariable a = new ResourceVariable("a", INT, 1); - MetaResourceVariable x = new MetaResourceVariable(new Variable("x"), OrderConstraint.GE, parse("0")); - MetaResourceVariable y = new MetaResourceVariable(new Variable("y"), OrderConstraint.GE, parse("1")); - MetaResourceVariable z = new MetaResourceVariable(new Variable("z"), OrderConstraint.GE, parse("2")); + Resource a = new Resource("a", INT, 1); + MetaResource x = new MetaResource(new Variable("x"), OrderConstraint.GE, parse("0")); + 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)); //a(1) matches y(>=1) @@ -117,8 +117,8 @@ @Test void MetaResourceVariableMathcingWithVariableOrderEq() { - ResourceVariable a = new ResourceVariable("a", INT, 0); - MetaResourceVariable x = new MetaResourceVariable(new Variable("x"), parse("x")); + Resource a = new Resource("a", INT, 0); + MetaResource x = new MetaResource(new Variable("x"), parse("x")); //a(0) matches x(=x) assertTrue(x.isMatchedBy(a)); @@ -126,8 +126,8 @@ @Test void MetaResourceVariableMathcingWithVariableOrderLT() { - ResourceVariable a = new ResourceVariable("a", INT, 2); - MetaResourceVariable x = new MetaResourceVariable(new Variable("x"), OrderConstraint.LT, parse("x")); + Resource a = new Resource("a", INT, 2); + MetaResource x = new MetaResource(new Variable("x"), OrderConstraint.LT, parse("x")); //a(2) matches x(x) assertTrue(x.isMatchedBy(a)); @@ -153,8 +153,8 @@ @Test void MetaResourceVariableMathcingWithVariableOrderGE() { - ResourceVariable a = new ResourceVariable("a", INT, 2); - MetaResourceVariable x = new MetaResourceVariable(new Variable("x"), OrderConstraint.GE, parse("x")); + Resource a = new Resource("a", INT, 2); + MetaResource x = new MetaResource(new Variable("x"), OrderConstraint.GE, parse("x")); //a(2) matches x(