diff --git a/src/main/java/Main.java b/src/main/java/Main.java index 12d7b28..6533984 100644 --- a/src/main/java/Main.java +++ b/src/main/java/Main.java @@ -100,30 +100,30 @@ 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 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); diff --git a/src/main/java/models/formulas/DependencyFormula.java b/src/main/java/models/formulas/DependencyFormula.java index 269aafd..cc70ee5 100644 --- a/src/main/java/models/formulas/DependencyFormula.java +++ b/src/main/java/models/formulas/DependencyFormula.java @@ -1,5 +1,7 @@ package models.formulas; +import java.util.List; + import lombok.Getter; import models.terms.Dependency; import models.terms.RDLTerm; @@ -14,8 +16,8 @@ this.dependency = dependency; } - public DependencyFormula(RDLTerm dependingTerm, Resource dependedVariable) { - this.dependency = new Dependency(dependingTerm, dependedVariable); + public DependencyFormula(RDLTerm dependingTerm, List dependedResources) { + this.dependency = new Dependency(dependingTerm, dependedResources); } diff --git a/src/main/java/models/terms/Dependency.java b/src/main/java/models/terms/Dependency.java index eee07c7..c0bcf00 100644 --- a/src/main/java/models/terms/Dependency.java +++ b/src/main/java/models/terms/Dependency.java @@ -1,5 +1,10 @@ package models.terms; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; +import java.util.stream.Collectors; + import lombok.Getter; import models.algebra.Symbol; @@ -7,46 +12,62 @@ public class Dependency extends RDLTerm{ private RDLTerm dependingTerm; - private Resource dependedVariable; + private List dependedResources; private Dependency dependency; private boolean isListType; - public Dependency(RDLTerm dependingTerm, Resource dependedVariable) { - super(new Symbol(":", 2), dependedVariable.getOrder(), dependingTerm.getSize() + dependedVariable.getSize()); +// public Dependency(RDLTerm dependingTerm, Resource dependedVariable) { +// super(new Symbol(":", 2), dependedVariable.getOrder(), dependingTerm.getSize() + dependedVariable.getSize()); +// this.dependingTerm = dependingTerm; +// this.dependedVariable = dependedVariable; +// this.dependency = null; +// this.addChild(dependingTerm); +// this.addChild(dependedVariable); +// this.isListType = false; +// } + + public Dependency(RDLTerm dependingTerm, List dependedResources) { + super(new Symbol(":", dependedResources.size() + 1), dependedResources.get(0).getOrder(), dependingTerm.getSize() + dependedResources.stream().mapToInt(v -> v.size).sum()); this.dependingTerm = dependingTerm; - this.dependedVariable = dependedVariable; + this.dependedResources = dependedResources; this.dependency = null; this.addChild(dependingTerm); - this.addChild(dependedVariable); + for (Resource dependedResource: dependedResources) { + this.addChild(dependedResource); + } this.isListType = false; } + public Dependency(RDLTerm dependingTerm, Resource ...dependedResources) { + this(dependingTerm, Arrays.asList(dependedResources)); + } + public Dependency(Dependency dependency) { super(new Symbol(":", 1), dependency.getOrder() - 1, dependency.getSize()); this.dependency = dependency; this.dependingTerm = null; - this.dependedVariable = null; + this.dependedResources = null; this.addChild(dependency); this.isListType = true; } - 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; - this.dependedVariable = dependedVariable; - this.addChild(dependingTerm); - this.addChild(dependedVariable); - this.dependency = null; - this.isListType = false; - } else { - this.dependency = new Dependency(dependingTerm, dependedVariable, order+1); - this.dependingTerm = null; - this.dependedVariable = null; - this.addChild(dependency); - this.isListType = true; - } - } +// 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; +// this.dependedResources = dependedVariable; +// this.addChild(dependingTerm); +// this.addChild(dependedVariable); +// this.dependency = null; +// this.isListType = false; +// } else { +// this.dependency = new Dependency(dependingTerm, dependedVariable, order+1); +// this.dependingTerm = null; +// this.dependedResources = null; +// this.addChild(dependency); +// this.isListType = true; +// } +// } public Dependency getDependency() { return this.dependency; @@ -61,28 +82,13 @@ return dependingTerm instanceof EvaluatableTerm; } - public void setDependingTerm(RDLTerm newTerm) { - setChild(0, newTerm); - this.dependingTerm = newTerm; - } - - public void setDependedVariable(Resource newVariable) { - setChild(1, newVariable); - this.dependedVariable = newVariable; - } - - public void setDependency(Dependency newDependency) { - setChild(0, newDependency); - this.dependency = newDependency; - } - @Override public String toString() { StringBuilder sb = new StringBuilder(); if(dependency == null) { sb.append(dependingTerm.toTermString()); sb.append(" : "); - sb.append(dependedVariable.toString()); + sb.append(dependedResources.toString()); } else { sb.append('['); sb.append(dependency.toString()); @@ -97,7 +103,7 @@ if(dependency == null) { sb.append(dependingTerm.toStringWithOrder()); sb.append(" : "); - sb.append(dependedVariable.toStringWithOrder()); + sb.append(dependedResources.stream().map(RDLTerm::toStringWithOrder).collect(Collectors.joining(", "))); } else { sb.append('['); sb.append(dependency.toStringWithOrder()); @@ -124,7 +130,7 @@ return anotherDep.getDependency().equals(dependency); } return anotherDep.getDependingTerm().equals(dependingTerm) - && anotherDep.getDependedVariable().equals(dependedVariable); + && anotherDep.getDependedResources().equals(dependedResources); } @Override @@ -134,7 +140,7 @@ @Override public Object clone() { - return new Dependency((RDLTerm) dependingTerm.clone(), (Resource) dependedVariable.clone()); + return new Dependency((RDLTerm) dependingTerm.clone(), new ArrayList<>(dependedResources)); } } diff --git a/src/main/java/models/terms/DependencyTerm.java b/src/main/java/models/terms/DependencyTerm.java index 64c17bc..667fa68 100644 --- a/src/main/java/models/terms/DependencyTerm.java +++ b/src/main/java/models/terms/DependencyTerm.java @@ -19,7 +19,7 @@ super( new Symbol(":", 1 + dependedTerms.size() + argumentTerms.size()), -1, - dependingTerm.getSize() + argumentTerms.get(0).getSize() + dependedTerms.get(0).getSize() + dependingTerm.getSize() + argumentTerms.stream().mapToInt(RDLTerm::getSize).sum() + dependedTerms.stream().mapToInt(RDLTerm::getSize).sum() ); int maxOrder = argumentTerms.stream().mapToInt(EvaluatableTerm::getOrder).max().orElse(-1); if (dependedTerms.get(0).getOrder() < maxOrder) {