diff --git a/pom.xml b/pom.xml index 487b135..64d94ac 100644 --- a/pom.xml +++ b/pom.xml @@ -36,7 +36,6 @@ - diff --git a/src/main/java/Main.java b/src/main/java/Main.java index 6533984..14ca9f9 100644 --- a/src/main/java/Main.java +++ b/src/main/java/Main.java @@ -1,20 +1,18 @@ import java.util.List; -import inference.ProofSystem; +import inference.rewrite.Position; +import inference.rewrite.ResourceTree; import inference.rewrite.RewriteInferenceSystem; import lombok.SneakyThrows; import models.algebra.Expression; import models.algebra.Type; import models.dataConstraintModel.DataConstraintModel; import models.dataFlowModel.DataTransferModel; -import models.formulas.DependencyFormula; import models.formulas.EquationFormula; -import models.formulas.InFormula; -import models.terms.Dependency; +import models.formulas.Then; import models.terms.DependencyTerm; +import models.terms.PrimedTerm; import models.terms.Resource; -import models.terms.ResourceConstant; -import models.terms.SetEvaluatableTerm; import parser.Parser; import parser.Parser.TokenStream; @@ -27,157 +25,295 @@ static Type INT = DataConstraintModel.typeInt; public static void main(String[] args) { -// sandbox1(); -// sandbox2(); -// sandbox3(); // sandbox4(); -// ProofSystem.debug(); - sandbox6(); +// System.out.println("================================================================="); +// System.out.println("================================================================="); +// System.out.println("================================================================="); +// sandbox5(); + sandbox9(); } -// static void sandbox1() { -// Resource A = new Resource("A", INT, 2); -// Resource Ap = new Resource("A'", INT, 2); -// Resource B = new Resource("B", 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); -// EquationFormula conclusionFormula = new EquationFormula( -// new DependencyTerm(new DependencyTerm(new DependencyTerm(A, B, C), D, E), F, G), -// new DependencyTerm(new DependencyTerm(new DependencyTerm(Ap, Bp, Cp), D, E), F, G) -// ); -// -// SemanticEquivalenceProofSystem proofSystem = new SemanticEquivalenceProofSystem( -// List.of(new SemanticEquivalenceRelation(assumptionFormula, 2)), -// conclusionFormula -// ); -// SemanticEquivalenceProofSystem.debug(); -// System.out.println(); -// System.out.println(assumptionFormula); -// System.out.println(conclusionFormula); -//// System.out.println(conclusionFormula.linearRightNormalized()); -// System.out.println(proofSystem.proof()); -// } + static void sandbox1() { + 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 G = new Resource("G", INT, 1); + DependencyTerm t1 = new DependencyTerm(A, B, C, D, E); + DependencyTerm t2 = new DependencyTerm(t1, F, G); + System.out.println(t2); + ResourceTree rt = new ResourceTree(t2); + System.out.println(rt); + rt.debug(new Position(List.of(0))); + } static void sandbox2() { - ProofSystem.debug(); + 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 G = new Resource("G", INT, 1); + Resource H = new Resource("H", INT, 1); + Resource I = new Resource("I", INT, 1); + Resource J = new Resource("J", INT, 1); + Resource K = new Resource("K", INT, 1); + Resource L = new Resource("L", INT, 1); + Resource M = new Resource("M", INT, 1); + Resource N = new Resource("N", INT, 1); + Resource O = new Resource("O", INT, 1); + Resource P = new Resource("P", INT, 1); + Resource Q = new Resource("Q", INT, 1); + + DependencyTerm t1 = new DependencyTerm(A, B, C, D, E); + DependencyTerm t2 = new DependencyTerm(G, H, I, J, K); + DependencyTerm t3 = new DependencyTerm(M, N, O, P, Q); + DependencyTerm t4 = new DependencyTerm(t1, F, t2, L, t3); + System.out.println(t4); + ResourceTree rt = new ResourceTree(t4); + System.out.println(rt); + rt.debug(new Position()); + rt.debugAllPath(); + } static void sandbox3() { - 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"); - 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); - DependencyTerm t3 = new DependencyTerm(new SetEvaluatableTerm(fno), aid, A); - DependencyTerm t4 = new DependencyTerm(t1, aid, A); + 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 x = new Resource("x", INT, 0); + Resource y = new Resource("y", INT, 1); + DependencyTerm t1 = new DependencyTerm(A, B, C); + DependencyTerm t2 = new DependencyTerm(B, C, D); + EquationFormula f1 = new EquationFormula(t1, x); + EquationFormula f2 = new EquationFormula(y, t2); + RewriteInferenceSystem ris = new RewriteInferenceSystem(List.of(f1, f2), null); + ris.inference(); - DependencyFormula f1 = new DependencyFormula(d1); - InFormula f2 = new InFormula(t2, t3); - EquationFormula f3 = new EquationFormula(t4, C); - DependencyFormula f4 = new DependencyFormula(new Dependency(new SetEvaluatableTerm(followee), aid)); - InFormula f5 = new InFormula(A, new SetEvaluatableTerm(aid)); - InFormula conclusion = new InFormula(C, new SetEvaluatableTerm(new SetEvaluatableTerm(followee))); - - System.out.println(f1); - System.out.println(f2); - System.out.println(f3); - System.out.println(conclusion); - System.out.println(); - boolean result = ProofSystem.check(List.of(f1, f2, f3, f4, f5), conclusion); - System.out.println(); - System.out.println(result); } -// static void sandbox4() { -// 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); -// DependencyFormula f3 = new DependencyFormula(U, W); -// DependencyTerm t1 = new DependencyTerm(X, U, U); -// DependencyTerm t2 = new DependencyTerm(t1, W, W); -// DependencyTerm t3 = new DependencyTerm(Y, U, U); -// DependencyTerm t4 = new DependencyTerm(t3, W, W); -//// EquationFormula f4 = new EquationFormula(t1, X); -//// EquationFormula f4 = new EquationFormula(X, t1); -//// EquationFormula f4 = new EquationFormula(t2, X); -//// EquationFormula f4 = new EquationFormula(t3, Y); -//// EquationFormula f4 = new EquationFormula(t4, Y); -// EquationFormula f4 = new EquationFormula(t2, t4); -//// DependencyFormula f4 = new DependencyFormula(Y, U); -// System.out.println(f1 + ", " + f2 + ", " + f3); -// boolean result = ProofSystem.check(List.of(f1, f2, f3), f4); -// 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); + static void sandbox4() { + Resource uadd = new Resource("uadd", INT, 1); + Resource add = new Resource("add", INT, 1); + Resource cid = new Resource("cid", INT, 1); + Resource org = new Resource("org", INT, 1); + Resource uid = new Resource("uid", 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(t1, f, x); - EquationFormula fm = new EquationFormula(t2, y); - System.out.println(t1); - System.out.println(t2); - System.out.println(fm); - RewriteInferenceSystem tmp = new RewriteInferenceSystem(List.of(fm), null); - tmp.debug(); - tmp.inference(); + DependencyTerm t1 = new DependencyTerm(add, cid, org); + DependencyTerm t2 = new DependencyTerm(org, uid, x); + DependencyTerm t3 = new DependencyTerm(uadd, uid, x); + DependencyTerm t4 = new DependencyTerm(add, cid, y); + EquationFormula f1 = new EquationFormula(uadd, t1); + EquationFormula f2 = new EquationFormula(t2, y); + EquationFormula f3 = new EquationFormula(t3, t4); + + + RewriteInferenceSystem ris = new RewriteInferenceSystem(List.of(f1, f2), f3); + ris.debug(); + ris.inference(); + + } + + static void sandbox5() { + Resource uadd = new Resource("uadd", INT, 1); + Resource add = new Resource("add", INT, 1); + Resource cid = new Resource("cid", INT, 1); + Resource org = new Resource("org", INT, 1); + Resource uid = new Resource("uid", INT, 1); + Resource x = new Resource("x", INT, 0); + Resource y = new Resource("y", INT, 0); + Resource z = new Resource("z", INT, 0); + DependencyTerm t1 = new DependencyTerm(add, cid, org); + DependencyTerm t2 = new DependencyTerm(add, cid, x); + DependencyTerm t3 = new DependencyTerm(org, uid, z); + DependencyTerm t4 = new DependencyTerm(uadd, uid, z); + + EquationFormula f1 = new EquationFormula(uadd, t1); + EquationFormula f2 = new EquationFormula(t2, y); + EquationFormula f3 = new EquationFormula(t3, x); + EquationFormula f4 = new EquationFormula(t4, y); + Then f5 = new Then(f3, f4); + + RewriteInferenceSystem ris = new RewriteInferenceSystem(List.of(f1, f2), f5); + ris.debug(); + ris.inference(); + } static void sandbox6() { - Resource uid = new Resource("uid", INT, 1); - Resource org = new Resource("org", INT, 1); - Resource uadd = new Resource("uadd", INT, 1); - Resource cid = new Resource("cid", INT, 1); Resource add = new Resource("add", INT, 1); - Resource addP = new Resource("add'", INT, 1); - Resource cidP = new Resource("cid'", INT, 1); - Resource orgP = new Resource("org'", INT, 1); - Resource uidP = new Resource("uid'", INT, 1); - Resource uaddP = new Resource("uadd'", INT, 1); + Resource cid = new Resource("cid", INT, 1); + Resource org = new Resource("org", INT, 1); + Resource uid = new Resource("uid", INT, 1); Resource x = new Resource("x", INT, 0); Resource y = new Resource("y", INT, 0); Resource z = new Resource("z", INT, 0); - DependencyTerm t1 = new DependencyTerm(add, cid, org); - DependencyTerm t2 = new DependencyTerm(addP, cidP, orgP); - DependencyTerm t3 = new DependencyTerm(orgP, uidP, x); - DependencyTerm t4 = new DependencyTerm(add, cid, y); - DependencyTerm t5 = new DependencyTerm(uaddP, uidP, x); - - EquationFormula f1 = new EquationFormula(uadd, t1); - EquationFormula f2 = new EquationFormula(uaddP, t2); + DependencyTerm t1 = new DependencyTerm(add, cid, x); + DependencyTerm t2 = new DependencyTerm(cid, uid, z); + DependencyTerm t3 = new DependencyTerm(add, cid, t2); + EquationFormula f1 = new EquationFormula(t1, y); + EquationFormula f2 = new EquationFormula(t2, x); EquationFormula f3 = new EquationFormula(t3, y); - EquationFormula f4 = new EquationFormula(t4, t5); - - RewriteInferenceSystem tmp = new RewriteInferenceSystem(List.of(f1, f2, f3), f4); - tmp.debug(); - tmp.inference(); + Then f4 = new Then(f2, f3); + RewriteInferenceSystem ris = new RewriteInferenceSystem(List.of(f1), f4); + ris.inference(); } + static void sandbox7() { + 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 G = new Resource("G", INT, 1); + Resource H = new Resource("H", INT, 1); + Resource I = new Resource("I", INT, 1); + Resource J = new Resource("J", INT, 1); + Resource K = new Resource("K", INT, 1); + Resource L = new Resource("L", INT, 1); + Resource M = new Resource("M", INT, 1); + Resource N = new Resource("N", INT, 1); + Resource O = new Resource("O", INT, 1); + + DependencyTerm t1 = new DependencyTerm(A, B, C); + DependencyTerm t2 = new DependencyTerm(I, J, K); + DependencyTerm t3 = new DependencyTerm(M, N, O); + DependencyTerm t4 = new DependencyTerm(E, F, G, H, t2); + DependencyTerm t5 = new DependencyTerm(t1, D, t4, L, t3); + + ResourceTree rt = new ResourceTree(t5); +// System.out.println(rt); + 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); + + //input1 + DependencyTerm te5 = new DependencyTerm(soledProductIdP, salesIdP, a); + EquationFormula eq3 = new EquationFormula(te5, b); + + //input2 + DependencyTerm te6 = new DependencyTerm(quantityP, salesIdP, a); + EquationFormula eq4 = new EquationFormula(te6, c); + + //input3, 4, 5 + 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); + + + //----------------------change value------------------- + //input6 + DependencyTerm te10 = new DependencyTerm(unitPriceP, productIdP, d); + EquationFormula eq9 = new EquationFormula(te10, e); + + //input7, 8, 9, 10 + 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); + + //value copy conclusion + 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); +// RewriteInferenceSystem ris = new RewriteInferenceSystem(List.of(), List.of(), List.of(eq3, eq4, eq5, eq6, eq7, eq8, eq9, eq10, eq11, eq12, eq13, eq14), eq15); + + //value copy new sales + RewriteInferenceSystem ris = new RewriteInferenceSystem(List.of(eq3, eq4, eq5, eq6, eq7, eq8), eq15); + + //value copy change value +// RewriteInferenceSystem ris = new RewriteInferenceSystem(List.of(eq9, eq10, eq11, eq12, eq13, eq14), eq15); + ris.inference(); +// + System.out.println("~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~"); + System.out.println("~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~"); + System.out.println("~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~"); + + //reference conclusion + 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); +// RewriteInferenceSystem ris2 = new RewriteInferenceSystem(List.of(eq1, eq2), List.of(), List.of(eq3, eq4, eq5, eq6, eq7,eq9, eq10, eq11, eq12, eq13), th1); + + //reference new sales +// RewriteInferenceSystem ris2 = new RewriteInferenceSystem(List.of(eq1, eq2, eq3, eq4, eq5, eq6, eq7), th1); + + //reference change value + RewriteInferenceSystem ris2 = new RewriteInferenceSystem(List.of(eq1, eq2, eq9, eq10, eq11, eq12, eq13), th1); + +// ris2.debug(); + ris2.inference(); + + } + + + + @SneakyThrows static Expression parse(String expr) { stream.addLine(expr); diff --git a/src/main/java/inference/rewrite/Position.java b/src/main/java/inference/rewrite/Position.java new file mode 100644 index 0000000..61755b5 --- /dev/null +++ b/src/main/java/inference/rewrite/Position.java @@ -0,0 +1,68 @@ +package inference.rewrite; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; + +import lombok.Getter; + +public class Position { + + @Getter + private List paths; + + public Position(List paths) { + this.paths = Collections.unmodifiableList(paths); + } + + public Position() { + this.paths = Collections.unmodifiableList(List.of(0)); + } + + public Position addPath(int index) { + List nextPaths = new ArrayList<>(paths); + nextPaths.add(index); + return new Position(Collections.unmodifiableList(nextPaths)); + } + + public boolean startWith(Position pos) { + for (int i = 0; i < pos.size(); i++) { + if (getPath(i) != pos.getPath(i)) { + return false; + } + } + return true; + } + + public int size() { + return paths.size(); + } + + private int getPath(int index) { + if (index >= size()) { + return -1; + } + return paths.get(index); + } + + + @Override + public boolean equals(Object another) { + if (! (another instanceof Position)) { + return false; + } + Position position = (Position) another; + return paths.equals(position.getPaths()); + } + + @Override + public int hashCode() { + return this.paths.hashCode(); + } + + @Override + public String toString() { + return paths.toString(); + } + +} diff --git a/src/main/java/inference/rewrite/ResourceTree.java b/src/main/java/inference/rewrite/ResourceTree.java new file mode 100644 index 0000000..cfe6929 --- /dev/null +++ b/src/main/java/inference/rewrite/ResourceTree.java @@ -0,0 +1,177 @@ +package inference.rewrite; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.Objects; +import java.util.stream.Collectors; + +import lombok.Getter; +import models.terms.DependencyTerm; +import models.terms.EvaluatableTerm; +import models.terms.PrimedTerm; +import models.terms.Resource; + +public class ResourceTree { + + @Getter + private EvaluatableTerm root; + private Map> tree; + private Map resourceMap; + + public ResourceTree(EvaluatableTerm term) { + tree = new HashMap<>(); + resourceMap = new HashMap<>(); + constructResourceTree(term, new Position(List.of(0))); + root = resourceMap.get(new Position(List.of(0))); + } + + public ResourceTree(Map> tree, Map resourceMap) { + this.tree = tree; + this.resourceMap = resourceMap; + root = resourceMap.get(new Position(List.of(0))); + } + + + public EvaluatableTerm getResource(Position pos) { + if (pos == null) { + return null; + } + return resourceMap.get(pos); + } + + public List getChildren(Position pos) { + if (tree.get(pos) == null) { + return List.of(); + } + return tree.get(pos); + } + + + + private List constructResourceTree(EvaluatableTerm term, Position top) { + if (term instanceof Resource resource) { + resourceMap.put(top, resource); + if (! tree.containsKey(top)) { + tree.put(top, new ArrayList<>()); + } + return List.of(top); + } else if (term instanceof DependencyTerm depTerm) { + 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 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; + } + } + + @Override + public String toString() { + List result = new ArrayList<>(); + toStringAllPath(new Position(), new ArrayList<>(), result); + return "<" + result.stream().collect(Collectors.joining("|\n")) + ">"; + } + + public void debug(Position pos) { + System.out.println(pos + ", " + resourceMap.get(pos)); + if (tree.containsKey(pos)) { + for (Position nextPos : tree.get(pos)) { + debug(nextPos); + } + } + } + + public void debugAllPath() { + debugAllPath(new Position(), new ArrayList<>()); + } + + private void debugAllPath(Position pos, List curPath) { + curPath.add(resourceMap.get(pos)); + if (tree.get(pos).size() == 0) { + System.out.println(curPath.stream().map(EvaluatableTerm::toString).collect(Collectors.joining("-"))); + } else { + for (Position nextPos: tree.get(pos)) { + debugAllPath(nextPos, curPath); + } + } + curPath.remove(curPath.size() - 1); + } + + 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(EvaluatableTerm::toString).collect(Collectors.joining("-"))); + } else { + for (Position nextPos: tree.get(pos)) { + toStringAllPath(nextPos, curPath, result); + } + } + curPath.remove(curPath.size() - 1); + } + + + @Override + public boolean equals(Object another) { + if (another instanceof ResourceTree tree) { + return this.tree.equals(tree.tree) && this.resourceMap.equals(tree.resourceMap); + } + return false; + } + + @Override + public int hashCode() { + return Objects.hash(this.tree, this.resourceMap); + } + +} + diff --git a/src/main/java/inference/rewrite/RewriteInferenceSystem.java b/src/main/java/inference/rewrite/RewriteInferenceSystem.java index 303ea2e..15643a0 100644 --- a/src/main/java/inference/rewrite/RewriteInferenceSystem.java +++ b/src/main/java/inference/rewrite/RewriteInferenceSystem.java @@ -1,9 +1,13 @@ package inference.rewrite; +import java.util.ArrayDeque; import java.util.ArrayList; +import java.util.Deque; import java.util.HashMap; +import java.util.HashSet; import java.util.List; import java.util.Map; +import java.util.Set; import models.formulas.EquationFormula; import models.formulas.Formula; @@ -15,83 +19,576 @@ public class RewriteInferenceSystem { - List constraintFormulas = new ArrayList<>(); - List invariantFormulas = new ArrayList<>(); - EquationFormula inputFormula; - List conditionalFormulas = new ArrayList<>(); - List otherFormulas = new ArrayList<>(); - Formula conclusion; + private List constraintFormulas = new ArrayList<>(); + private List invariantFormulas = new ArrayList<>(); + private List inputFormulas = new ArrayList<>(); + private List conditionalFormulas = new ArrayList<>(); + private List otherFormulas = new ArrayList<>(); + private EquationFormula conclusion; + 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(assumption); + invariantFormulas.add((EquationFormula) assumption); } else if (assumption instanceof EquationFormula) { - constraintFormulas.add(assumption); + constraintFormulas.add((EquationFormula) assumption); } else { otherFormulas.add(assumption); } } if (conclusion instanceof Then then) { - conditionalFormulas.add(then.getCondition()); - this.conclusion = then.getResult(); + conditionalFormulas.add((EquationFormula) then.getCondition()); + this.conclusion = (EquationFormula) then.getResult(); } else { - this.conclusion = conclusion; + this.conclusion = (EquationFormula) conclusion; } - } + public RewriteInferenceSystem(List constraintFormulas, List invariantFormulas, List inputFormulas, Formula conclusion) { + this.constraintFormulas = constraintFormulas; + this.invariantFormulas = invariantFormulas; + this.inputFormulas = inputFormulas; + if (conclusion instanceof Then then) { + conditionalFormulas.add((EquationFormula) then.getCondition()); + this.conclusion = (EquationFormula) then.getResult(); + } else { + this.conclusion = (EquationFormula) conclusion; + } + } + + 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() { - Map> resourceTree = new HashMap<>(); - Resource root = parseDependencyTerm(inputFormula.getLeftSideHand(), resourceTree, new ArrayList<>()); - System.out.println(resourceTree); + 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); +// System.out.println(conclusionLeftResult); +// System.out.println(conclusionRightResult); + conclusionLeftResult.retainAll(conclusionRightResult); + System.out.println(conclusionLeftResult.size() != 0); +// if (conclusionLeftResult.size() != 0) { +// ResourceTree resultRoot = conclusionLeftResult.iterator().next(); +// showRewriteGraph(resultRoot, leftRewriteGraph); +// System.out.println("=============================================================----"); +// showRewriteGraph(resultRoot, rightRewriteGraph); +// System.out.println(conclusionLeftResult); +// } + + } + 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<>()); + + 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; + while (rewrited) { + rewrited = false; + inputResourceTree.debugAllPath(); + for (ResourceTree tree: constraintResourceTree) { + Position matchPos = treeJoinCheck(inputResourceTree, tree); + if (matchPos != null) { + inputResourceTree = joinTree(inputResourceTree, matchPos, tree); + rewrited = true; + } else { + matchPos = treeJoinCheck(tree, inputResourceTree); + if (matchPos != null) { + inputResourceTree = joinTree(tree, matchPos, inputResourceTree); + rewrited = true; + } } - tops.clear(); - tops.add(resource); } - return resource; + for (ResourceTree tree: conditionalResourceTree) { + Position matchPos = treeJoinCheck(inputResourceTree, tree); + if (matchPos != null) { + inputResourceTree = joinTree(inputResourceTree, matchPos, tree); + rewrited = true; + } else { + matchPos = treeJoinCheck(tree, inputResourceTree); + if (matchPos != null) { + inputResourceTree = joinTree(tree, matchPos, inputResourceTree); + rewrited = true; + } + } + } } - Resource root; - DependencyTerm depTerm = (DependencyTerm) term; - EvaluatableTerm dependingTerm = depTerm.getDependingTerm(); - List dependedTerms = depTerm.getDependedResources(); - 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; + return inputResourceTree; } + private Position treeJoinCheck(ResourceTree leftTree, ResourceTree rightTree) { + Deque positionQueue = new ArrayDeque<>(); + for (Position nextPos: leftTree.getChildren(new Position())) { + positionQueue.add(nextPos); + } + while(! positionQueue.isEmpty()) { + Position curPos = positionQueue.pollFirst(); + if (treeJoinCheck(leftTree, curPos, rightTree, new Position())) { + return curPos; + } + for (Position nextPos: leftTree.getChildren(curPos)) { + positionQueue.add(nextPos); + } + } + return null; + } + + private boolean treeJoinCheck(ResourceTree leftTree, Position leftTreePos, ResourceTree rightTree, Position rightTreePos) { + if (leftTree.getResource(leftTreePos).equals(rightTree.getResource(rightTreePos))) { + boolean result = true; + Set used = new HashSet<>(); + for (Position nextLeftPos: leftTree.getChildren(leftTreePos)) { + boolean someTreeMatched = false; + for (Position nextRightPos: rightTree.getChildren(rightTreePos)) { + if (treeJoinCheck(leftTree, nextLeftPos, rightTree, nextRightPos)) { + used.add(nextRightPos); + someTreeMatched = true; + break; + } + } + result &= someTreeMatched; + } + return result; + } + return false; + } + + private record PositionPair(Position resultPos, Position rightPos) {}; + + private ResourceTree joinTree(ResourceTree leftTree, Position joinPos, ResourceTree rightTree) { + Map> tree = new HashMap<>(); + Map resourceMap = new HashMap<>(); + + Deque positionQue = new ArrayDeque<>(); + Position rootPos = new Position(); + positionQue.add(new PositionPair(rootPos, null)); + tree.put(rootPos, new ArrayList<>()); + resourceMap.put(rootPos, leftTree.getResource(rootPos)); + while (! positionQue.isEmpty()) { + PositionPair curPosPair = positionQue.pollFirst(); + Position curPos = curPosPair.resultPos(); + Position curRightPos = curPosPair.rightPos(); + if (curRightPos == null) { + for (Position nextPos: leftTree.getChildren(curPos)) { + tree.get(curPos).add(nextPos); + tree.put(nextPos, new ArrayList<>()); + resourceMap.put(nextPos, leftTree.getResource(nextPos)); + if (nextPos.startWith(joinPos)) { + positionQue.add(new PositionPair(nextPos, new Position())); + } else { + positionQue.add(new PositionPair(nextPos, null)); + } + } + } else { + for (int i = 0; i < rightTree.getChildren(curRightPos).size(); i++) { + Position nextRightPos = rightTree.getChildren(curRightPos).get(i); + Position nextResultPos = curPos.addPath(i); + tree.get(curPos).add(nextResultPos); + tree.put(nextResultPos, new ArrayList<>()); + resourceMap.put(nextResultPos, rightTree.getResource(nextRightPos)); + positionQue.add(new PositionPair(nextResultPos, nextRightPos)); + } + } + } + + return new ResourceTree(tree, resourceMap); + + } + + private void showRewriteGraph(ResourceTree root, Map> rewriteGraph) { + List result = new ArrayList<>(); + List resultNodes = new ArrayList<>(); + result.add(root); + boolean isChanged = true; + while (isChanged) { + ResourceTree curTree = result.get(result.size() - 1); + isChanged = false; + if (rewriteGraph.containsKey(curTree)) { + isChanged |= !rewriteGraph.get(curTree).isEmpty(); + RewriteGraphNode nextNode = rewriteGraph.get(curTree).iterator().next(); + result.add(nextNode.baseTree()); + resultNodes.add(nextNode); + } + } + for (int i = resultNodes.size() - 1; i >= 0; i--) { + System.out.println(resultNodes.get(i)); + System.out.println("--------------------------"); + } + System.out.println(root); + } + + 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<>(); + Map rewritable = new HashMap<>(); + for (EquationFormula formula : constraintFormulas) { + rewritable.put(new ResourceTree(formula.getLeftSideHand()), new ResourceTree(formula.getRightSideHand())); + } + for (EquationFormula formula : conditionalFormulas) { + 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); + Set matchPositions = treeMatchCheck(curBaseTree, from); + if (matchPositions == null) { + 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); + } + } + + return result; + } + + private Set treeMatchCheck(ResourceTree baseTree, ResourceTree matchTree) { + Deque positionQueue = new ArrayDeque<>(); + positionQueue.add(new Position()); + while (! positionQueue.isEmpty()) { + Position curPos = positionQueue.pollFirst(); + Set result = treeMatchCheck(baseTree, curPos, matchTree); + if (result != null) { + return result; + } + for (Position child: baseTree.getChildren(curPos)) { + positionQueue.add(child); + } + } + return null; + } + + private Set treeMatchCheck(ResourceTree baseTree, Position startPosition, ResourceTree matchTree) { + Set result = new HashSet<>(); + Deque basePosQueue = new ArrayDeque<>(); + Deque matchPosQueue = new ArrayDeque<>(); + basePosQueue.add(startPosition); + matchPosQueue.add(new Position()); + if (! baseTree.getResource(startPosition).equals(matchTree.getResource(new Position()))) { + return null; + } + while (! basePosQueue.isEmpty()) { + Position curBasePos = basePosQueue.pollFirst(); + Position curMatchPos = matchPosQueue.pollFirst(); + result.add(curBasePos); + if (matchTree.getChildren(curMatchPos).size() == 0) { + continue; + } + Set used = new HashSet<>(); + for (Position nextBasePos: baseTree.getChildren(curBasePos)) { + for (Position nextMatchPos: matchTree.getChildren(curMatchPos)) { + if (used.contains(nextMatchPos)) continue; + if (baseTree.getResource(nextBasePos).equals(matchTree.getResource(nextMatchPos))) { + used.add(nextMatchPos); + basePosQueue.add(nextBasePos); + matchPosQueue.add(nextMatchPos); + break; + } + return null; + } + } + } + return result; + } + + private ResourceTree rewrite(ResourceTree baseTree, Set matchPositions, ResourceTree toTree) { + Map> resultTree = new HashMap<>(); + Map resultResourceMap = new HashMap<>(); + Position resultCurPos = new Position(); + Position baseCurPos = new Position(); + Position toCurPos = new Position(); + Deque resultPosQueue = new ArrayDeque<>(); + Deque basePosQueue = new ArrayDeque<>(); + Deque toPosQueue = new ArrayDeque<>(); + + resultPosQueue.add(resultCurPos); + basePosQueue.add(baseCurPos); + toPosQueue.add(toCurPos); + + + while (! basePosQueue.isEmpty()) { + baseCurPos = basePosQueue.pollFirst(); + if (matchPositions.contains(baseCurPos)) { + List lastPositions = new ArrayList<>(); + Deque matchPosQueue = new ArrayDeque<>(); + matchPosQueue.add(baseCurPos); + while (! matchPosQueue.isEmpty()) { + Position matchPos = matchPosQueue.pollFirst(); + for (Position nextMatchPos: baseTree.getChildren(matchPos)) { + if (matchPositions.contains(nextMatchPos)) { + matchPosQueue.add(nextMatchPos); + } else { + lastPositions.add(nextMatchPos); + } + } + } + List resultLastPositions = new ArrayList<>(); + while (! toPosQueue.isEmpty()) { + toCurPos = toPosQueue.pollFirst(); + resultCurPos = resultPosQueue.pollFirst(); + resultTree.put(resultCurPos, new ArrayList<>()); + resultResourceMap.put(resultCurPos, toTree.getResource(toCurPos)); + if (toTree.getChildren(toCurPos).size() == 0) { + resultLastPositions.add(resultCurPos); + continue; + } + for (int i = 0; i < toTree.getChildren(toCurPos).size(); i++) { + Position resultNextPos = resultCurPos.addPath(i); + resultTree.get(resultCurPos).add(resultNextPos); + resultPosQueue.add(resultNextPos); + toPosQueue.add(toCurPos.addPath(i)); + } + } + + for (Position resultLastPos: resultLastPositions) { + Deque resultLastPosQueue = new ArrayDeque<>(); + Deque lastPosQueue = new ArrayDeque<>(); + for (int i = 0; i < lastPositions.size(); i++) { + Position nextResultLastPos = resultLastPos.addPath(i); + resultTree.get(resultLastPos).add(nextResultLastPos); + resultLastPosQueue.add(nextResultLastPos); + lastPosQueue.add(lastPositions.get(i)); + } + while (! resultLastPosQueue.isEmpty()) { + Position curResultLastPos = resultLastPosQueue.pollFirst(); + Position curLastPos = lastPosQueue.pollFirst(); + resultTree.put(curResultLastPos, new ArrayList<>()); + resultResourceMap.put(curResultLastPos, baseTree.getResource(curLastPos)); + for (int i = 0; i < baseTree.getChildren(curLastPos).size(); i++) { + Position nextResultLastPos = curResultLastPos.addPath(i); + resultTree.get(curResultLastPos).add(nextResultLastPos); + resultLastPosQueue.add(nextResultLastPos); + lastPosQueue.add(curLastPos.addPath(i)); + } + } + } + } else { + resultCurPos = resultPosQueue.pollFirst(); + resultTree.put(resultCurPos, new ArrayList<>()); + resultResourceMap.put(resultCurPos, baseTree.getResource(baseCurPos)); + for (int i = 0; i < baseTree.getChildren(baseCurPos).size(); i++) { + Position resultNextPos = resultCurPos.addPath(i); + resultTree.get(resultCurPos).add(resultNextPos); + resultPosQueue.add(resultNextPos); + basePosQueue.add(baseCurPos.addPath(i)); + } + } + } + + 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) { + 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 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)) { @@ -124,4 +621,5 @@ } + } 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() {