diff --git a/src/main/java/Main.java b/src/main/java/Main.java index 22f4326..382c6c8 100644 --- a/src/main/java/Main.java +++ b/src/main/java/Main.java @@ -11,6 +11,7 @@ import models.formulas.EquationFormula; import models.formulas.Then; import models.terms.DependencyTerm; +import models.terms.PrimedTerm; import models.terms.Resource; import parser.Parser; import parser.Parser.TokenStream; @@ -24,11 +25,12 @@ static Type INT = DataConstraintModel.typeInt; public static void main(String[] args) { - sandbox4(); - System.out.println("================================================================="); - System.out.println("================================================================="); - System.out.println("================================================================="); - sandbox5(); +// sandbox4(); +// System.out.println("================================================================="); +// System.out.println("================================================================="); +// System.out.println("================================================================="); +// sandbox5(); + sandbox9(); } static void sandbox1() { @@ -193,6 +195,95 @@ rt.debug(new Position(List.of(0))); } + static void sandbox8() { + Resource A = new Resource("A", INT, 1); + Resource B = new Resource("B", INT, 1); + Resource C = new Resource("C", INT, 1); + DependencyTerm te = new DependencyTerm(A, B, C); + EquationFormula eq1 = new EquationFormula(A, te); + RewriteInferenceSystem ris = new RewriteInferenceSystem(List.of(eq1), eq1); + ris.inference(); + } + + static void sandbox9() { + Resource totalAmount = new Resource("totalAmount", INT, 1); + Resource quantity = new Resource("quantity", INT, 1); + Resource unitPrice = new Resource("unitPrice", INT, 1); + Resource productId = new Resource("productID", INT, 1); + Resource productName = new Resource("productName", INT, 1); + Resource soledProductId = new Resource("soledProductId", INT, 1); + PrimedTerm totalAmountP = new PrimedTerm(totalAmount); + PrimedTerm quantityP = new PrimedTerm(quantity); + PrimedTerm unitPriceP = new PrimedTerm(unitPrice); + PrimedTerm productIdP = new PrimedTerm(productId); + PrimedTerm productNameP = new PrimedTerm(productName); + PrimedTerm soledProductIdP = new PrimedTerm(soledProductId); + 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); + Resource e = new Resource("e", INT, 0); + Resource salesId = new Resource("salesId", INT, 1); + PrimedTerm salesIdP = new PrimedTerm(salesId); + Resource mul = new Resource("mul", INT, 1); + Resource mul1= new Resource("mul1", INT, 1); + Resource mul2 = new Resource("mul2", INT, 1); + + // reference1 + DependencyTerm te1 = new DependencyTerm(unitPrice, productId, soledProductId); + DependencyTerm te2 = new DependencyTerm(mul, mul1, quantity, mul2, te1); + EquationFormula eq1 = new EquationFormula(totalAmount, te2); + + //reference2 + DependencyTerm te3 = new DependencyTerm(unitPriceP, productIdP, soledProductIdP); + DependencyTerm te4 = new DependencyTerm(mul, mul1, quantityP, mul2, te3); + EquationFormula eq2 = new EquationFormula(totalAmountP, te4); + + DependencyTerm te5 = new DependencyTerm(soledProductIdP, salesIdP, a); + EquationFormula eq3 = new EquationFormula(te5, b); + + DependencyTerm te6 = new DependencyTerm(quantityP, salesIdP, a); + EquationFormula eq4 = new EquationFormula(te6, c); + + EquationFormula eq5 = new EquationFormula(productIdP, productId); + EquationFormula eq6 = new EquationFormula(productNameP, productName); + EquationFormula eq7 = new EquationFormula(unitPriceP, unitPrice); + + // value copy + DependencyTerm te7 = new DependencyTerm(totalAmountP, salesIdP, a); + DependencyTerm te8 = new DependencyTerm(unitPriceP, productIdP, b); + DependencyTerm te9 = new DependencyTerm(mul, mul1, c, mul2, te8); + EquationFormula eq8 = new EquationFormula(te7, te9); + + DependencyTerm te10 = new DependencyTerm(unitPriceP, productIdP, d); + EquationFormula eq9 = new EquationFormula(te10, e); + + EquationFormula eq10 = new EquationFormula(productNameP, productName); + EquationFormula eq11 = new EquationFormula(salesIdP, salesId); + EquationFormula eq12 = new EquationFormula(soledProductIdP, soledProductId); + EquationFormula eq13 = new EquationFormula(quantityP, quantity); + + //value copy +// EquationFormula eq14 = new EquationFormula(totalAmountP, totalAmount); + + DependencyTerm te11 = new DependencyTerm(totalAmountP, salesIdP, a); + DependencyTerm te12 = new DependencyTerm(totalAmount, salesId, a); + EquationFormula eq15 = new EquationFormula(te11, te12); +// RewriteInferenceSystem ris = new RewriteInferenceSystem(List.of(eq3, eq4, eq5, eq6,eq7,eq8,eq9,eq10,eq11,eq12,eq13,eq14), eq15); +// ris.inference(); + + DependencyTerm te13 = new DependencyTerm(soledProductId, salesId, a); + EquationFormula eq16 = new EquationFormula(d, te13); + Then th1 = new Then(eq16, eq15); + + RewriteInferenceSystem ris2 = new RewriteInferenceSystem(List.of(eq3, eq4, eq5, eq6,eq7,eq1,eq9,eq10,eq11,eq12,eq13,eq2), th1); +// ris2.debug(); + ris2.inference(); + + } + + + @SneakyThrows static Expression parse(String expr) { diff --git a/src/main/java/inference/rewrite/ResourceTree.java b/src/main/java/inference/rewrite/ResourceTree.java index 1762dcc..effe013 100644 --- a/src/main/java/inference/rewrite/ResourceTree.java +++ b/src/main/java/inference/rewrite/ResourceTree.java @@ -10,14 +10,15 @@ import lombok.Getter; import models.terms.DependencyTerm; import models.terms.EvaluatableTerm; +import models.terms.PrimedTerm; import models.terms.Resource; public class ResourceTree { @Getter - private Resource root; + private EvaluatableTerm root; private Map> tree; - private Map resourceMap; + private Map resourceMap; public ResourceTree(EvaluatableTerm term) { tree = new HashMap<>(); @@ -26,14 +27,14 @@ root = resourceMap.get(new Position(List.of(0))); } - public ResourceTree(Map> tree, Map resourceMap) { + public ResourceTree(Map> tree, Map resourceMap) { this.tree = tree; this.resourceMap = resourceMap; root = resourceMap.get(new Position(List.of(0))); } - public Resource getResource(Position pos) { + public EvaluatableTerm getResource(Position pos) { if (pos == null) { return null; } @@ -78,6 +79,37 @@ } } return resultPositions; + } else if (term instanceof PrimedTerm pt) { + if (pt.isResource()) { + resourceMap.put(top, pt); + if (! tree.containsKey(top)) { + tree.put(top, new ArrayList<>()); + } + return List.of(top); + } else { + DependencyTerm depTerm = (DependencyTerm) (pt.getPrimedTerm()); + EvaluatableTerm dependingTerm = depTerm.getDependingTerm(); + List dependedResources = depTerm.getDependedTerms(); + List argumentTerms = depTerm.getArgumentTerms(); + List dependingTermPositions = constructResourceTree(dependingTerm, top); + List resultPositions = new ArrayList<>(); + for (Position pos: dependingTermPositions) { + tree.put(pos, new ArrayList<>()); + } + for (int i = 0; i < dependedResources.size(); i++) { + for (Position pos : dependingTermPositions) { + Position nextPos = pos.addPath(i); + tree.get(pos).add(nextPos); + Position dependedResourcePosition= constructResourceTree(dependedResources.get(i), nextPos).get(0); + tree.put(dependedResourcePosition, new ArrayList<>()); + Position argumentTermPosition = dependedResourcePosition.addPath(0); + tree.get(dependedResourcePosition).add(argumentTermPosition); + tree.put(argumentTermPosition, new ArrayList<>()); + resultPositions.addAll(constructResourceTree(argumentTerms.get(i), argumentTermPosition)); + } + } + return resultPositions; + } } else { return null; } @@ -87,7 +119,7 @@ public String toString() { List result = new ArrayList<>(); toStringAllPath(new Position(), new ArrayList<>(), result); - return result.stream().collect(Collectors.joining("\n")); + return "<" + result.stream().collect(Collectors.joining("\n")) + ">"; } public void debug(Position pos) { @@ -103,10 +135,10 @@ debugAllPath(new Position(), new ArrayList<>()); } - private void debugAllPath(Position pos, List curPath) { + private void debugAllPath(Position pos, List curPath) { curPath.add(resourceMap.get(pos)); if (tree.get(pos).size() == 0) { - System.out.println(curPath.stream().map(Resource::toString).collect(Collectors.joining("-"))); + System.out.println(curPath.stream().map(EvaluatableTerm::toString).collect(Collectors.joining("-"))); } else { for (Position nextPos: tree.get(pos)) { debugAllPath(nextPos, curPath); @@ -115,10 +147,10 @@ curPath.remove(curPath.size() - 1); } - private void toStringAllPath(Position pos, List curPath, List result) { + private void toStringAllPath(Position pos, List curPath, List result) { curPath.add(resourceMap.get(pos)); if (tree.get(pos).size() == 0) { - result.add(curPath.stream().map(Resource::toString).collect(Collectors.joining("-"))); + result.add(curPath.stream().map(EvaluatableTerm::toString).collect(Collectors.joining("-"))); } else { for (Position nextPos: tree.get(pos)) { toStringAllPath(nextPos, curPath, result); diff --git a/src/main/java/inference/rewrite/RewriteInferenceSystem.java b/src/main/java/inference/rewrite/RewriteInferenceSystem.java index 1e01814..211387d 100644 --- a/src/main/java/inference/rewrite/RewriteInferenceSystem.java +++ b/src/main/java/inference/rewrite/RewriteInferenceSystem.java @@ -12,6 +12,7 @@ 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; @@ -20,7 +21,7 @@ List constraintFormulas = new ArrayList<>(); List invariantFormulas = new ArrayList<>(); - EquationFormula inputFormula; + List inputFormulas = new ArrayList<>(); List conditionalFormulas = new ArrayList<>(); List otherFormulas = new ArrayList<>(); EquationFormula conclusion; @@ -29,7 +30,7 @@ public RewriteInferenceSystem(List assumptions, Formula conclusion) { for (Formula assumption : assumptions) { if (inputFormulaCheck(assumption)) { - inputFormula = (EquationFormula) assumption; + inputFormulas.add((EquationFormula) assumption); } else if(invariantFormulaCheck(assumption)) { invariantFormulas.add((EquationFormula) assumption); } else if (assumption instanceof EquationFormula) { @@ -51,25 +52,56 @@ public void debug() { System.out.println("constraintFormulas: " + constraintFormulas.toString()); System.out.println("invariantFormulas: " + invariantFormulas.toString()); - System.out.println("inputFormula: " + inputFormula.toString()); + System.out.println("inputFormula: " + inputFormulas.toString()); System.out.println("conditionalFormulas: " + conditionalFormulas.toString()); System.out.println("conclusion: " + conclusion.toString()); } public boolean inference() { - ResourceTree baseTree = expandTree(); - System.out.println("baseTree: " + baseTree); - Set result = rewriteTree(baseTree); - for (ResourceTree tree: result) { - System.out.println("====================================="); - tree.debugAllPath(); + EquationFormula defCheck = definitonFormulaCheck(); + if (defCheck != null) { + System.out.println("non definition formula is detected. " + defCheck.toString() ); + return false; } + if (!loopCheck()) { + System.out.println("Loop is detected"); + return false; + } + for (EquationFormula inputFormula : inputFormulas) { + System.out.println("---------------------------" + inputFormula + "-------------------------------------------------"); +// ResourceTree baseTree = expandTree(i); +// System.out.println("baseTree: " + baseTree); +// Set result = rewriteTree(baseTree, i); +// System.out.println("=================result===================="); +// for (ResourceTree tree: result) { +// tree.debugAllPath(); +// } +// if (result.contains(new ResourceTree(conclusion.getLeftSideHand())) && result.contains(new ResourceTree(conclusion.getRightSideHand()))) { +// System.out.println("yes"); +// } else { +// System.out.println("no"); +// } +// System.out.println("====================================="); + Map> leftRewriteGraph = new HashMap<>(); + Map> rightRewriteGraph = new HashMap<>(); + Set conclusionLeftResult = rewriteTree(new ResourceTree(conclusion.getLeftSideHand()), inputFormula, leftRewriteGraph); + Set conclusionRightResult = rewriteTree(new ResourceTree(conclusion.getRightSideHand()), inputFormula, rightRewriteGraph); + conclusionLeftResult.retainAll(conclusionRightResult); + ResourceTree resultRoot = conclusionLeftResult.iterator().next(); + showRewriteGraph(resultRoot, leftRewriteGraph); + System.out.println("=============================================================----"); + showRewriteGraph(resultRoot, rightRewriteGraph); +// System.out.println(conclusionLeftResult); + System.out.println(conclusionLeftResult.size() != 0); + + } + return false; } - private ResourceTree expandTree() { - ResourceTree inputResourceTree = new ResourceTree(inputFormula.getLeftSideHand()); + private ResourceTree expandTree(int inputFormulaIndex) { + ResourceTree inputResourceTree = new ResourceTree(inputFormulas.get(inputFormulaIndex).getLeftSideHand()); List constraintResourceTree = constraintFormulas.stream().map(v -> new ResourceTree(v.getRightSideHand())).toList(); List conditionalResourceTree = conditionalFormulas.stream().map(v -> new ResourceTree(v.getLeftSideHand())).toList(); boolean rewrited = true; @@ -147,7 +179,7 @@ private ResourceTree joinTree(ResourceTree leftTree, Position joinPos, ResourceTree rightTree) { Map> tree = new HashMap<>(); - Map resourceMap = new HashMap<>(); + Map resourceMap = new HashMap<>(); Deque positionQue = new ArrayDeque<>(); Position rootPos = new Position(); @@ -185,23 +217,80 @@ } + private void showRewriteGraph(ResourceTree root, Map> rewriteGraph) { + List> result = new ArrayList<>(); + result.add(new HashSet<>()); + result.get(0).add(root); + boolean isChanged = true; + while (isChanged) { + Set nextTrees = new HashSet<>(); + isChanged = false; + for (ResourceTree curTree : result.get(result.size() - 1)) { + if (rewriteGraph.containsKey(curTree)) { + isChanged |= !rewriteGraph.get(curTree).isEmpty(); + for (RewriteGraphNode node: rewriteGraph.get(curTree)) { + nextTrees.add(node.baseTree()); + } + } + } + result.add(nextTrees); + } + result.remove(result.size() - 1); + for (int i = result.size() - 1; i >= 0; i--) { + Set curTrees = result.get(i); + StringBuilder sb = new StringBuilder(); + for (ResourceTree rt : curTrees) { + sb.append(rewriteGraph.get(rt)); + sb.append(", \n"); + } + sb.delete(sb.length() - 1, sb.length()); + System.out.println(sb.toString()); + System.out.println("--------------------------"); + } + System.out.println(root); + } - private Set rewriteTree(ResourceTree expandedInputResourceTree) { + private record RewriteGraphNode(ResourceTree baseTree, ResourceTree leftSideHand, ResourceTree rightSideHand, ResourceTree result) { + @Override + public String toString() { + return baseTree.toString() + " --( " + leftSideHand.toString() + " = " + rightSideHand.toString() + " )--> " + result ; + } + @Override + public int hashCode() { + return toString().hashCode(); + } + @Override + public boolean equals(Object another) { + if ( ! (another instanceof RewriteGraphNode)) { + return false; + } + RewriteGraphNode node = (RewriteGraphNode) another; + return this.baseTree.equals(node.baseTree()) && this.leftSideHand.equals(node.leftSideHand()) && this.rightSideHand.equals(node.rightSideHand()) && this.result.equals(node.result()); + } + }; + + private Set rewriteTree(ResourceTree expandedInputResourceTree, EquationFormula inputFormula, Map> rewriteGraph) { Set result = new HashSet<>(); - result.add(expandedInputResourceTree); Map rewritable = new HashMap<>(); for (EquationFormula formula : constraintFormulas) { - rewritable.put(new ResourceTree(formula.getRightSideHand()), new ResourceTree(formula.getLeftSideHand())); + rewritable.put(new ResourceTree(formula.getLeftSideHand()), new ResourceTree(formula.getRightSideHand())); } for (EquationFormula formula : conditionalFormulas) { - rewritable.put(new ResourceTree(formula.getRightSideHand()), new ResourceTree(formula.getLeftSideHand())); + rewritable.put(new ResourceTree(formula.getLeftSideHand()), new ResourceTree(formula.getRightSideHand())); + } + for (EquationFormula formula : invariantFormulas) { + rewritable.put(new ResourceTree(formula.getLeftSideHand()), new ResourceTree(formula.getRightSideHand())); } rewritable.put(new ResourceTree(inputFormula.getLeftSideHand()), new ResourceTree(inputFormula.getRightSideHand())); Deque treeQueue = new ArrayDeque<>(); treeQueue.add(expandedInputResourceTree); + Set used = new HashSet<>(); while (! treeQueue.isEmpty()) { ResourceTree curBaseTree = treeQueue.pollFirst(); + if (result.contains(curBaseTree)) { + continue; + } result.add(curBaseTree); for (ResourceTree from: rewritable.keySet()) { ResourceTree to = rewritable.get(from); @@ -210,6 +299,14 @@ continue; } ResourceTree res = rewrite(curBaseTree, matchPositions, to); + if (! rewriteGraph.containsKey(res)) { + rewriteGraph.put(res, new HashSet<>()); + } + RewriteGraphNode nextNode = new RewriteGraphNode(curBaseTree, from, to, res); + if (!used.contains(nextNode)) { + rewriteGraph.get(res).add(nextNode); + used.add(nextNode); + } treeQueue.add(res); } } @@ -268,7 +365,7 @@ private ResourceTree rewrite(ResourceTree baseTree, Set matchPositions, ResourceTree toTree) { Map> resultTree = new HashMap<>(); - Map resultResourceMap = new HashMap<>(); + Map resultResourceMap = new HashMap<>(); Position resultCurPos = new Position(); Position baseCurPos = new Position(); Position toCurPos = new Position(); @@ -353,20 +450,141 @@ return new ResourceTree(resultTree, resultResourceMap); } + private boolean loopCheck() { + Map equationGraph = new HashMap<>(); + for (EquationFormula formula : constraintFormulas) { + equationGraph.put(formula.getLeftSideHand(), formula.getRightSideHand()); + } + for (EquationFormula formula : invariantFormulas) { + equationGraph.put(formula.getLeftSideHand(), formula.getRightSideHand()); + } + for (EquationFormula inputFormula : inputFormulas) { + equationGraph.put(inputFormula.getLeftSideHand(), inputFormula.getRightSideHand()); + } + for (EquationFormula formula : conditionalFormulas) { + equationGraph.put(formula.getLeftSideHand(), formula.getRightSideHand()); + } + for (EvaluatableTerm leftTerm : equationGraph.keySet()) { + Set used = new HashSet<>(); + used.add(leftTerm); + EvaluatableTerm rightTerm = equationGraph.get(leftTerm); + if (checkUsedTerms(used, rightTerm)) { + return false; + } + while (equationGraph.containsKey(rightTerm)) { + leftTerm = rightTerm; + used.add(leftTerm); + rightTerm = equationGraph.get(leftTerm); + if (checkUsedTerms(used, rightTerm)) { + return false; + } + } + } + return true; + } + + private boolean checkUsedTerms(Set used, EvaluatableTerm term) { + if (used.contains(term)) { + return true; + } + if (term instanceof DependencyTerm depTerm) { + if (checkUsedTerms(used, depTerm.getDependingTerm())) { + return true; + } + for (EvaluatableTerm te : depTerm.getDependedTerms()) { + if (checkUsedTerms(used, te)) { + return true; + } + } + for (EvaluatableTerm te : depTerm.getArgumentTerms()) { + if (checkUsedTerms(used, te)) { + return true; + } + } + } + return false; + } + + private EquationFormula definitonFormulaCheck() { + for (EquationFormula eq : constraintFormulas) { + if (!definitionFormulaCheck(eq)) { + return eq; + } + } + for (EquationFormula inputFormula : inputFormulas) { + if (!definitionFormulaCheck(inputFormula)) { + return inputFormula; + } + } + for (EquationFormula eq : invariantFormulas) { + if (!definitionFormulaCheck(eq)) { + return eq; + } + } + for (EquationFormula eq : conditionalFormulas) { + if (!definitionFormulaCheck(eq)) { + return eq; + } + } + return null; + } + private boolean definitionFormulaCheck(Formula formula) { if (formula instanceof EquationFormula equation) { - EvaluatableTerm left = equation.getLeftSideHand(); - return left.getSize() <= 3; + return singleTermCheck(equation.getLeftSideHand()); } else if (formula instanceof Then then) { Formula f1 = then.getCondition(); Formula f2 = then.getResult(); if (f1 instanceof EquationFormula eq1 && f2 instanceof EquationFormula eq2) { - return eq1.getLeftSideHand().getSize() <= 3 && eq2.getLeftSideHand().getSize() <= 3; + return singleTermCheck(eq1.getLeftSideHand()) && singleTermCheck(eq2.getLeftSideHand()); } } return false; } + private boolean singleTermCheck(EvaluatableTerm term) { + if (term instanceof PrimedTerm primedTerm) { + return singleTermCheck(primedTerm.getPrimedTerm()); + } + if (term instanceof Resource) { + return true; + } + DependencyTerm depTerm = (DependencyTerm) term; + if (!(depTerm.getDependingTerm() instanceof Resource)) { + if (depTerm.getDependingTerm() instanceof PrimedTerm primedTerm) { + if (! (primedTerm.getPrimedTerm() instanceof Resource)) { + return false; + } + } else { + return false; + } + } + for (EvaluatableTerm te : depTerm.getDependedTerms()) { + if (!(te instanceof Resource)) { + if (te instanceof PrimedTerm primedTerm) { + if (! (primedTerm.getPrimedTerm() instanceof Resource)) { + return false; + } + } else { + return false; + } + } + + } + for (EvaluatableTerm te : depTerm.getArgumentTerms()) { + if (!(te instanceof Resource)) { + if (te instanceof PrimedTerm primedTerm) { + if (! (primedTerm.getPrimedTerm() instanceof Resource)) { + return false; + } + } else { + return false; + } + } + } + return true; + } + private boolean inputFormulaCheck(Formula formula) { if (! (formula instanceof EquationFormula equation)) { return false; diff --git a/src/main/java/models/terms/PrimedTerm.java b/src/main/java/models/terms/PrimedTerm.java index 6de8ae5..2afd229 100644 --- a/src/main/java/models/terms/PrimedTerm.java +++ b/src/main/java/models/terms/PrimedTerm.java @@ -6,10 +6,12 @@ public class PrimedTerm extends EvaluatableTerm { private EvaluatableTerm primedTerm; + private boolean isResource; public PrimedTerm(EvaluatableTerm term) { super(term.getSymbol(), term.getOrder(), term.getSize()); this.primedTerm = term; + this.isResource = term instanceof Resource; } @Override @@ -26,6 +28,16 @@ public int hashCode() { return toStringWithOrder().hashCode(); } + + @Override + public boolean equals(Object other) { + if (! (other instanceof PrimedTerm)) { + return false; + } + PrimedTerm otherPrimed = (PrimedTerm) other; + EvaluatableTerm otherTerm = otherPrimed.getPrimedTerm(); + return this.primedTerm.equals(otherTerm); + } @Override public Object clone() {