diff --git a/src/main/java/Main.java b/src/main/java/Main.java index 2bbb7a3..0959b6f 100644 --- a/src/main/java/Main.java +++ b/src/main/java/Main.java @@ -1,23 +1,15 @@ -import java.util.HashMap; -import java.util.List; -import java.util.Map; import java.util.Set; import constants.Types; import inference.ProofSystem; +import models.Position; import models.algebra.Type; -import models.algebra.Variable; import models.formulas.DependencyFormula; import models.formulas.EquationFormula; -import models.terms.Dependency; import models.terms.DependencyTerm; import models.terms.EvaluatableTerm; import models.terms.Resource; -import models.terms.meta.MatchConstraint; -import models.terms.meta.MetaDynamicDependency; -import models.terms.meta.MetaEvaluatableTermVariable; -import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaTermGenerator; +import models.terms.ResourceConstant; public class Main { @@ -25,108 +17,60 @@ public static void main(String[] args) { // - sandbox5(); + sandbox3(); } static void sandbox() { - EvaluatableTerm t = new DependencyTerm(new Resource("a", 1), new Resource("b", 1), new Resource("c", 1)); - System.out.println(t.getSubTerms(EvaluatableTerm.class).values()); + Resource x = new Resource("x", 1); + Resource y = new Resource("y", 1); + Resource z = new Resource("z", 1); + DependencyTerm t1 = new DependencyTerm(x, y, z); + DependencyTerm t2 = new DependencyTerm(t1, y, z); + var tmp = t2.getSubTerms(EvaluatableTerm.class); + System.out.println(tmp); + for (var pos: tmp.keySet()) { + System.out.println(Position.convertPosition(pos) + ", " + tmp.get(pos)); + } } - + static void sandbox2() { - Resource a = new Resource("a", 1); - Resource b = new Resource("b", 1); - Resource c = new Resource("c", 1); - Resource d = new Resource("d", 1); - DependencyFormula d1 = new DependencyFormula(a, b); - DependencyFormula d2 = new DependencyFormula(b, c); - DependencyFormula d3 = new DependencyFormula(c, d); - DependencyFormula d4 = new DependencyFormula(a, d); - ProofSystem ps = new ProofSystem(Set.of(d1, d2, d3), d4); - ps.dependencyInference(); - System.out.println(ps.getState().getHistory().getHistoryString(d4)); + Resource x = new Resource("x", 1); + Resource y = new Resource("y", 1); + Resource z = new Resource("z", 1); + DependencyFormula d1 = new DependencyFormula(x, y); + DependencyFormula d2 = new DependencyFormula(y, z); + DependencyFormula d3 = new DependencyFormula(x, z); + DependencyTerm t1 = new DependencyTerm(x, y, new ResourceConstant("2")); + DependencyTerm t2 = new DependencyTerm(y, z, new ResourceConstant("4")); + DependencyTerm t3 = new DependencyTerm(x, z, new ResourceConstant("4")); + EquationFormula eq1 = new EquationFormula(t1, new ResourceConstant("3")); + EquationFormula eq2 = new EquationFormula(t2, new ResourceConstant("2")); + EquationFormula eq3 = new EquationFormula(t3, new ResourceConstant("2")); + ProofSystem ps = new ProofSystem(Set.of(d1, d2, eq1, eq2), eq3); + ps.inference(); + System.out.println(ps.getInferenceHistoryString()); + } static void sandbox3() { - Resource a = new Resource("a", 1); - Resource b = new Resource("b", 1); - Resource c = new Resource("c", 1); - Resource d = new Resource("d", 1); - Resource e = new Resource("e", 1); - DependencyFormula d1 = new DependencyFormula(a, b); - DependencyFormula d2 = new DependencyFormula(b, c); - DependencyFormula d3 = new DependencyFormula(c, d); - DependencyFormula d4 = new DependencyFormula(d, e); - DependencyFormula d5 = new DependencyFormula(a, e); - ProofSystem ps = new ProofSystem(Set.of(d1, d2, d3, d4), d5); - ps.dependencyInference(); - System.out.println(ps.getState().getHistory().getHistoryString(d5)); - } - - static void sandbox4() { - Resource a = new Resource("a", 2); - Resource b = new Resource("b", 2); - Resource c = new Resource("c", 1); - Resource d = new Resource("d", 1); - DependencyFormula d2 = new DependencyFormula(new Dependency(a, b), c); - EquationFormula eq1 = new EquationFormula(d, d); - DependencyFormula d3 = new DependencyFormula(new DependencyTerm(a, b, d), c, d); - ProofSystem ps = new ProofSystem(Set.of(d2, eq1), d3); - ps.dependencyInference(); - System.out.println(ps.getState().getHistory().getHistoryString(d3)); - } - - static void sandbox5() { - Resource a = new Resource("a", 1); - Resource b = new Resource("b", 1); - Resource c = new Resource("c", 1); - Resource d = new Resource("d", 1); - Resource e = new Resource("e", 1); - Resource f = new Resource("f", 2); - Resource g = new Resource("g", 2); - Resource h = new Resource("h", 3); - Resource i = new Resource("i", 3); - Dependency d1 = new Dependency(new DependencyTerm(f, g, b), b); - var tmp = ProofSystem.argumentExtension.getAssumptions().get(0).isMatchedBy(new DependencyFormula(d1)); - var tmp1 = ProofSystem.argumentExtension.derive(List.of(new DependencyFormula(d1)), Set.of(a)); - System.out.println(tmp1); - } - - static void sandBox8() { - MetaDynamicDependency md = new MetaDynamicDependency( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - if (curDepth == maxDepth && curIndex == 0) { - return new MetaEvaluatableTermVariable(new Variable("se")); - } else if (curIndex == 0) { - return new MetaDynamicDependency(this); - } - curIndex -= 1; - return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex)); - } - } - ); - MetaRDLTerm mt = md.generate(1, 2, 3, new HashMap<>()); - System.out.println(mt); - MetaRDLTerm mt2 = md.allGenerate(2, 3, new HashMap<>()); - System.out.println(mt2); - Resource a = new Resource("a", 1); - Resource b = new Resource("b", 1); - Resource c = new Resource("c", 1); - Resource d = new Resource("d", 1); - Resource e = new Resource("e", 1); - Resource f = new Resource("f", 1); - Resource g = new Resource("g", 1); - Dependency d1 = new Dependency(a, b); - Dependency d2 = new Dependency(d1, c, d); - System.out.println(md.isMatchedBy(d1)); - System.out.println(md.isMatchedBy(d2)); - Dependency d3 = new Dependency(d2, e, f, g); - MatchConstraint constraint = md.isMatchedBy(d3).iterator().next(); - System.out.println(md.isMatchedBy(d3)); - constraint.getContext().put("maxDepth", d3.getMaxDepth()); - System.out.println(md.substitute(constraint.getBinding(), constraint.getContext())); + Resource x = new Resource("x", 1); + Resource y = new Resource("y", 1); + Resource z = new Resource("z", 1); + Resource w = new Resource("w", 1); + DependencyFormula d1 = new DependencyFormula(x, y); + DependencyFormula d2 = new DependencyFormula(y, z); + DependencyFormula d3 = new DependencyFormula(z, w); + DependencyTerm t1 = new DependencyTerm(x, y, new ResourceConstant("1")); + DependencyTerm t2 = new DependencyTerm(y, z, new ResourceConstant("3")); + DependencyTerm t3 = new DependencyTerm(z, w, new ResourceConstant("4")); + DependencyTerm t4 = new DependencyTerm(x, w, new ResourceConstant("4")); + EquationFormula eq1 = new EquationFormula(t1, new ResourceConstant("2")); + EquationFormula eq2 = new EquationFormula(t2, new ResourceConstant("1")); + EquationFormula eq3 = new EquationFormula(t3, new ResourceConstant("3")); + EquationFormula eq4 = new EquationFormula(t4, new ResourceConstant("2")); + ProofSystem ps = new ProofSystem(Set.of(d1, d2, d3, eq1, eq2, eq3), eq4); + ps.inference(); + System.out.println(ps.getInferenceHistoryString()); } } diff --git a/src/main/java/inference/EquationAxiom.java b/src/main/java/inference/EquationAxiom.java index 0959493..0f014ef 100644 --- a/src/main/java/inference/EquationAxiom.java +++ b/src/main/java/inference/EquationAxiom.java @@ -20,6 +20,7 @@ import models.terms.Resource; import models.terms.meta.MatchConstraint; import models.terms.meta.MetaRDLTerm; +import utils.Permutation; public class EquationAxiom extends InferenceRule { @@ -34,6 +35,14 @@ protected EquationAxiom(String name) { super(name); } + + public Set apply(Set assumptions, EvaluatableTerm term) { + Set result = new HashSet<>(); + for (List perm: Permutation.permutation(assumptions, assumptions.size())) { + result.addAll(apply(perm, term)); + } + return result; + } public Set apply(List assumptions, EvaluatableTerm term) { return apply(assumptions, term, MatchConstraint.createDefault()); @@ -67,9 +76,9 @@ } try { if (isLeft) { - result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getRightSideHand()).substitute(matchRes.getBinding(), matchRes.getContext())); + result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getRightHandSide()).substitute(matchRes.getBinding(), matchRes.getContext())); } else { - result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getLeftSideHand()).substitute(matchRes.getBinding(), matchRes.getContext())); + result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getLeftHandSide()).substitute(matchRes.getBinding(), matchRes.getContext())); } } catch (SubstituteFailedException e) { continue; @@ -81,12 +90,12 @@ protected Set conclusionLeftSideHandMatch(EvaluatableTerm term, Set matchResult) { MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion; - return ((MetaRDLTerm) metaConclusion.getLeftSideHand()).isMatchedBy(term, matchResult); + return ((MetaRDLTerm) metaConclusion.getLeftHandSide()).isMatchedBy(term, matchResult); } protected Set conclusionRightSideHandMatch(EvaluatableTerm term, Set matchResult) { MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion; - return ((MetaRDLTerm) metaConclusion.getRightSideHand()).isMatchedBy(term, matchResult); + return ((MetaRDLTerm) metaConclusion.getRightHandSide()).isMatchedBy(term, matchResult); } diff --git a/src/main/java/inference/In.java b/src/main/java/inference/In.java index e15ec86..5833adc 100644 --- a/src/main/java/inference/In.java +++ b/src/main/java/inference/In.java @@ -139,7 +139,7 @@ Set result = new HashSet<>(); Set constraints = domainMembershipAssumption.isMatchedBy(equationFormula); for (MatchConstraint constraint : constraints) { - constraint.getContext().put("maxDepth", equationFormula.getLeftSideHand().getMaxDepth() - 1); + constraint.getContext().put("maxDepth", equationFormula.getLeftHandSide().getMaxDepth() - 1); constraint.getContext().put("maxIndex", 10000); RDLTerm left = domainMembershipConclusionLeftSideHand.substitute(constraint.getBinding(), constraint.getContext()); RDLTerm right = domainMembershipConclusionRightSideHand.substitute(constraint.getBinding(), constraint.getContext()); diff --git a/src/main/java/inference/InferenceHistory.java b/src/main/java/inference/InferenceHistory.java index 0c8c756..b3c4a0a 100644 --- a/src/main/java/inference/InferenceHistory.java +++ b/src/main/java/inference/InferenceHistory.java @@ -21,6 +21,27 @@ inferenceHistory = new HashMap<>(); } + public List getHistoryByBFS(Formula conclusion) { + List result = new ArrayList<>(); + if (! inferenceHistory.containsKey(conclusion)) { + return result; + } + Deque q = new ArrayDeque<>(); + q.add(conclusion); + while (q.size() != 0) { + Formula formula = q.pollFirst(); + if (! inferenceHistory.containsKey(formula)) { + continue; + } + InferenceHistoryNode node = inferenceHistory.get(formula).iterator().next(); + result.add(node); + for (Formula f: node.getAssumptions()) { + q.add(f); + } + } + return result; + } + public void addHistory(Formula conclusion, InferenceHistoryNode node) { this.inferenceHistory.computeIfAbsent(conclusion, k -> new HashSet<>()).add(node); } @@ -31,6 +52,7 @@ } List result = new ArrayList<>(); Deque q = new ArrayDeque<>(); + Set used = new HashSet<>(); q.add(conclusion); result.add(conclusion.toString()); while (! q.isEmpty()) { @@ -38,6 +60,10 @@ if (! inferenceHistory.containsKey(formula)) { continue; } + if (used.contains(formula)) { + continue; + } + used.add(formula); InferenceHistoryNode node = inferenceHistory.get(formula).iterator().next(); result.add("--------------------------------" + node.getUsedRule().getName()); result.add(node.getAssumptions().stream().map(v -> v.toString()).collect(Collectors.joining(", "))); diff --git a/src/main/java/inference/InferenceHistoryNode.java b/src/main/java/inference/InferenceHistoryNode.java index fab43be..7486d1d 100644 --- a/src/main/java/inference/InferenceHistoryNode.java +++ b/src/main/java/inference/InferenceHistoryNode.java @@ -1,8 +1,8 @@ package inference; -import com.google.common.base.Objects; - import java.util.List; +import com.google.common.base.Objects; + import lombok.Getter; import models.formulas.Formula; @@ -32,4 +32,9 @@ return Objects.hashCode(assumptions, conclusion, usedRule); } + @Override + public String toString() { + return assumptions + "---(" + usedRule.getName() + ")--->" + conclusion; + } + } diff --git a/src/main/java/inference/ProofState.java b/src/main/java/inference/ProofState.java index ba42b0b..f52ac1b 100644 --- a/src/main/java/inference/ProofState.java +++ b/src/main/java/inference/ProofState.java @@ -13,6 +13,7 @@ import models.formulas.Formula; import models.formulas.meta.MetaEquationFormula; import models.terms.Dependency; +import models.terms.DependencyTerm; import models.terms.EvaluatableTerm; import models.terms.RDLTerm; import models.terms.meta.MetaRDLTerm; @@ -29,7 +30,10 @@ private Map matchedTerms = new HashMap<>(); private InferenceHistory history = new InferenceHistory(); - public ProofState(Set existFormulas) { + private Set definitionFormulas = new HashSet<>(); + private Map> dependencyMap = new HashMap<>(); + + public ProofState(Set existFormulas) { for (Formula formula: existFormulas) { formulas.add(formula); if (formula instanceof DependencyFormula df) { @@ -38,10 +42,23 @@ this.evaluatableTerms.addAll(df.getDependency().getSubTerms(EvaluatableTerm.class).values()); } else if (formula instanceof EquationFormula eq) { this.equationFormulas.add(eq); - this.evaluatableTerms.addAll(eq.getLeftSideHand().getSubTerms(EvaluatableTerm.class).values()); - this.evaluatableTerms.addAll(eq.getRightSideHand().getSubTerms(EvaluatableTerm.class).values()); + this.definitionFormulas.add(eq); + EquationFormula eq2 = new EquationFormula(eq.getRightHandSide(), eq.getLeftHandSide()); + this.equationFormulas.add(eq2); + addHistory(List.of(eq), ProofSystem.symmetry, eq2); + this.evaluatableTerms.addAll(eq.getLeftHandSide().getSubTerms(EvaluatableTerm.class).values()); + this.evaluatableTerms.addAll(eq.getRightHandSide().getSubTerms(EvaluatableTerm.class).values()); + if (eq.getLeftHandSide() instanceof DependencyTerm dt) { + dependencyMap.computeIfAbsent(dt.getNoArgumentDependency(), k -> new HashSet<>()).add(dt); + } + } } + for (EvaluatableTerm te: evaluatableTerms) { + EquationFormula eq = new EquationFormula(te, te); + this.equationFormulas.add(eq); + addHistory(List.of(), ProofSystem.reflexivity, eq); + } for (InferenceRule rule: ProofSystem.dependencyAxioms) { List> terms = new ArrayList<>(); for (int i = 0; i < rule.getAssumptionSize(); i++) { @@ -61,8 +78,8 @@ } for (EquationAxiom rule: ProofSystem.equationAxioms) { List> formulas = new ArrayList<>(); - MetaRDLTerm conclusionLeft = (MetaRDLTerm) ((MetaEquationFormula) rule.getConclusion()).getLeftSideHand(); - MetaRDLTerm conclusionRight = (MetaRDLTerm) ((MetaEquationFormula) rule.getConclusion()).getRightSideHand(); + MetaRDLTerm conclusionLeft = (MetaRDLTerm) ((MetaEquationFormula) rule.getConclusion()).getLeftHandSide(); + MetaRDLTerm conclusionRight = (MetaRDLTerm) ((MetaEquationFormula) rule.getConclusion()).getRightHandSide(); Set lhs = new HashSet<>(); Set rhs = new HashSet<>(); for (EvaluatableTerm term : evaluatableTerms) { @@ -104,8 +121,11 @@ this.evaluatableTerms.addAll(df.getDependency().getSubTerms(EvaluatableTerm.class).values()); } else if (formula instanceof EquationFormula eq) { this.equationFormulas.add(eq); - this.evaluatableTerms.addAll(eq.getLeftSideHand().getSubTerms(EvaluatableTerm.class).values()); - this.evaluatableTerms.addAll(eq.getRightSideHand().getSubTerms(EvaluatableTerm.class).values()); + this.evaluatableTerms.addAll(eq.getLeftHandSide().getSubTerms(EvaluatableTerm.class).values()); + this.evaluatableTerms.addAll(eq.getRightHandSide().getSubTerms(EvaluatableTerm.class).values()); + if (eq.getLeftHandSide() instanceof DependencyTerm dt) { + dependencyMap.computeIfAbsent(dt.getNoArgumentDependency(), k -> new HashSet<>()).add(dt); + } } } for (InferenceRule rule: ProofSystem.dependencyAxioms) { @@ -127,8 +147,8 @@ } for (EquationAxiom rule: ProofSystem.equationAxioms) { List> formulas = new ArrayList<>(); - MetaRDLTerm conclusionLeft = (MetaRDLTerm) ((MetaEquationFormula) rule.getConclusion()).getLeftSideHand(); - MetaRDLTerm conclusionRight = (MetaRDLTerm) ((MetaEquationFormula) rule.getConclusion()).getRightSideHand(); + MetaRDLTerm conclusionLeft = (MetaRDLTerm) ((MetaEquationFormula) rule.getConclusion()).getLeftHandSide(); + MetaRDLTerm conclusionRight = (MetaRDLTerm) ((MetaEquationFormula) rule.getConclusion()).getRightHandSide(); Set lhs = new HashSet<>(); Set rhs = new HashSet<>(); for (EvaluatableTerm term : evaluatableTerms) { diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index 333725a..0cfd112 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -1,8 +1,10 @@ package inference; import java.util.ArrayList; +import java.util.HashMap; import java.util.HashSet; import java.util.List; +import java.util.Map; import java.util.Set; import inference.axioms.ArgumentConstraint; @@ -27,11 +29,14 @@ import models.formulas.meta.MetaDependencyFormula; import models.formulas.meta.MetaEquationFormula; import models.terms.Dependency; +import models.terms.DependencyTerm; import models.terms.EvaluatableTerm; import models.terms.RDLTerm; import models.terms.Resource; +import models.terms.ResourceConstant; import models.terms.meta.MetaEvaluatableTermVariable; import models.terms.meta.OrderConstraint; +import utils.Permutation; import utils.Product; public class ProofSystem { @@ -186,24 +191,115 @@ dependencyExtension ); - private Set assumptions; + private Set assumptions; private Formula conclusion; @Getter private ProofState state; - public ProofSystem(Set assumptions, Formula conclusion) { + public ProofSystem(Set assumptions, Formula conclusion) { this(assumptions, conclusion, Set.of()); } - public ProofSystem(Set assumptions, Formula conclusion, Set existResources) { + public ProofSystem(Set assumptions, Formula conclusion, Set existResources) { state = new ProofState(assumptions); this.assumptions = assumptions; this.conclusion = conclusion; state.getEvaluatableTerms().addAll(existResources); + checkDefinitionFormulaFormat(); + } + + private void checkDefinitionFormulaFormat() { + Set leftSideHands = new HashSet<>(assumptions.stream() + .filter(f -> f instanceof EquationFormula) + .map(v -> ((EquationFormula) v).getLeftHandSide()) + .toList()); + for (EvaluatableTerm te: leftSideHands) { + if (te instanceof Resource | te instanceof ResourceConstant) { + throw new IllegalArgumentException("Resource or ResourceConstant can't be placed left-hand side."); + } + Set dependencies = state.getDependencies(); + DependencyTerm dt = (DependencyTerm) te; + Set requiredDependencies = dt.requiredDependenciesForAdmissible(); + requiredDependencies.retainAll(dependencies); + if (requiredDependencies.isEmpty()) { + for (Dependency d: dt.requiredDependenciesForAdmissible()) { + if (! dependencyInference(new DependencyFormula(d))) { + throw new IllegalArgumentException(dt.toString() + "is not definition formula format."); + } + } + } + } } public void inference() { + if (conclusion instanceof DependencyFormula) { + dependencyInference(); + return; + } + EquationFormula conclusion = (EquationFormula) this.conclusion; + DependencyTerm dt = (DependencyTerm) conclusion.getLeftHandSide(); + DependencyFormula df = new DependencyFormula(dt.getNoArgumentDependency()); + dependencyInference(df); + List inferenceHisotries = this.state.getHistory().getHistoryByBFS(df); +// Collections.reverse(inferenceHisotry); + Set curTerms = new HashSet<>(); + curTerms.add(conclusion.getLeftHandSide()); + for (InferenceHistoryNode history: inferenceHisotries) { + Set nextTerms = new HashSet<>(); + for (EvaluatableTerm curTerm: curTerms) { + Set inferenceRes = new HashSet<>(); + if (history.getUsedRule() == compositeMapping) { + inferenceRes = applyAxiom(new HashSet<>(history.getAssumptions()), curTerm, mapComposition); + } + for (EvaluatableTerm te: inferenceRes) { + for (EquationFormula eq: state.getDefinitionFormulas()) { + nextTerms.addAll(applyAxiom(Set.of(eq, new DependencyFormula(te.getDependency())), te, rightSubstitution)); + nextTerms.addAll(applyAxiom(Set.of(eq), te, leftSubstitution)); + } + } + } + curTerms = nextTerms; + } + applyTransitivity(); + } + + private Set applyAxiom (Set assumptions, EvaluatableTerm term, EquationAxiom axiom) { + Set res = new HashSet<>(); + for (List perm: Permutation.permutation(assumptions, assumptions.size())) { + for (EvaluatableTerm rsh: axiom.apply(perm, term)) { + res.add(rsh); + state.addHistory(perm, axiom, new EquationFormula(term, rsh)); + state.addFormuals(Set.of(new EquationFormula(term, rsh))); + } + } + return res; + } + + private void applyTransitivity() { + Set eq = new HashSet<>(state.getEquationFormulas()); + Map> used = new HashMap<>(); + while (true) { + Set derived = new HashSet<>(); + for (EquationFormula eq1: eq) { + for (EquationFormula eq2: eq) { + if (used.computeIfAbsent(eq1, k -> new HashSet<>()).contains(eq2)) { + continue; + } + used.computeIfAbsent(eq1, k -> new HashSet<>()).add(eq2); + Set formulas = transitivity.derive(List.of(eq1, eq2)); + for (Formula f: formulas) { + derived.add((EquationFormula) f); + state.addHistory(List.of(eq1, eq2), transitivity, f); + } + } + } + if (derived.isEmpty()) { + break; + } + eq.addAll(derived); + } + } public String getInferenceHistoryString() { @@ -211,9 +307,13 @@ } public boolean dependencyInference() { + return dependencyInference(this.conclusion); + } + + public boolean dependencyInference(Formula conclusion) { if (conclusion instanceof EquationFormula eq) { - RDLTerm lhs = eq.getLeftSideHand(); - RDLTerm rhs = eq.getRightSideHand(); + RDLTerm lhs = eq.getLeftHandSide(); + RDLTerm rhs = eq.getRightHandSide(); Dependency leftDependency = lhs.getDependency(); Dependency rightDependency = rhs.getDependency(); while((! state.getDependencies().contains(leftDependency)) && (! state.getDependencies().contains(rightDependency))) { @@ -298,4 +398,15 @@ return result; } + private void checkAdmissibility(DependencyTerm dt) { + checkRequiredDependency(dt); + checkMembership(dt); + } + + private void checkRequiredDependency(DependencyTerm dt) { + } + + private void checkMembership(DependencyTerm dt) { + } + } diff --git a/src/main/java/inference/axioms/Identity.java b/src/main/java/inference/axioms/Identity.java index 64dbebc..0b72c61 100644 --- a/src/main/java/inference/axioms/Identity.java +++ b/src/main/java/inference/axioms/Identity.java @@ -62,9 +62,9 @@ for (MatchConstraint matchRes: conclusionMatchResult) { try { if (isLeft) { - result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getRightSideHand()).substitute(matchRes.getBinding(), matchRes.getContext())); + result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getRightHandSide()).substitute(matchRes.getBinding(), matchRes.getContext())); } else { - result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getLeftSideHand()).substitute(matchRes.getBinding(), matchRes.getContext())); + result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getLeftHandSide()).substitute(matchRes.getBinding(), matchRes.getContext())); } } catch (SubstituteFailedException e) { continue; diff --git a/src/main/java/inference/axioms/MapComposition.java b/src/main/java/inference/axioms/MapComposition.java index 41c9e81..e279a92 100644 --- a/src/main/java/inference/axioms/MapComposition.java +++ b/src/main/java/inference/axioms/MapComposition.java @@ -60,7 +60,7 @@ @Override public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { curIndex -= 3; - int tIndex = (Integer) context.get("tIndex"); + int tIndex = (Integer) context.getOrDefault("tIndex", 0); if (curIndex >= tIndex * 2) { return null; } @@ -133,7 +133,11 @@ return new HashSet<>(); } Set matchResult = assumptionMatch(assumptions, constraint); - + for (MatchConstraint con : matchResult) { + if (! con.getContext().containsKey("tIndex")) { + con.getContext().put("tIndex", 0); + } + } Set conclusionLeftMatchResult = conclusionLeftSideHandMatch(term, matchResult); for (MatchConstraint leftConst: conclusionLeftMatchResult) { @@ -156,14 +160,14 @@ int n = (Integer) matchRes.getContext().get(new Position()); int k = (Integer) matchRes.getContext().get(new Position(0, 2)); matchRes.getContext().put(new Position(), n + k - 3); - EvaluatableTerm rightSide = (EvaluatableTerm) ((MetaRDLTerm) metaConclusion.getRightSideHand()).substitute(matchRes.getBinding(), matchRes.getContext()); + EvaluatableTerm rightSide = (EvaluatableTerm) ((MetaRDLTerm) metaConclusion.getRightHandSide()).substitute(matchRes.getBinding(), matchRes.getContext()); result.add(rightSide); } else { int n = (Integer) matchRes.getContext().get(new Position()); int k = (Integer) matchRes.getContext().get("uIndex") * 2; matchRes.getContext().put(new Position(), n - k + 2); matchRes.getContext().put(new Position(0, 2), k + 1); - EvaluatableTerm leftSide = (EvaluatableTerm) ((MetaRDLTerm) metaConclusion.getLeftSideHand()).substitute(matchRes.getBinding(), matchRes.getContext()); + EvaluatableTerm leftSide = (EvaluatableTerm) ((MetaRDLTerm) metaConclusion.getLeftHandSide()).substitute(matchRes.getBinding(), matchRes.getContext()); result.add(leftSide); } } catch (SubstituteFailedException e) { diff --git a/src/main/java/inference/axioms/PseudoConstantness.java b/src/main/java/inference/axioms/PseudoConstantness.java index ed88ecf..c4e357d 100644 --- a/src/main/java/inference/axioms/PseudoConstantness.java +++ b/src/main/java/inference/axioms/PseudoConstantness.java @@ -86,10 +86,10 @@ } try { if (isLeft) { - result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getRightSideHand()).substitute(matchRes.getBinding(), matchRes.getContext())); + result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getRightHandSide()).substitute(matchRes.getBinding(), matchRes.getContext())); } else { matchRes.getContext().put(new Position(), ((DependencyFormula) assumptions.get(0)).getDependency().getMaxIndex() * 2 - 1); - result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getLeftSideHand()).substitute(matchRes.getBinding(), matchRes.getContext())); + result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getLeftHandSide()).substitute(matchRes.getBinding(), matchRes.getContext())); } } catch (SubstituteFailedException e) { continue; diff --git a/src/main/java/inference/axioms/Uncurrying.java b/src/main/java/inference/axioms/Uncurrying.java index f5e8299..9f073f7 100644 --- a/src/main/java/inference/axioms/Uncurrying.java +++ b/src/main/java/inference/axioms/Uncurrying.java @@ -141,10 +141,10 @@ try { if (isLeft) { matchRes.getContext().put(new Position(), (Integer) matchRes.getContext().get(new Position()) - 2); - result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getRightSideHand()).substitute(matchRes.getBinding(), matchRes.getContext())); + result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getRightHandSide()).substitute(matchRes.getBinding(), matchRes.getContext())); } else { matchRes.getContext().put(new Position(), (Integer) matchRes.getContext().get(new Position()) + 2); - result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getLeftSideHand()).substitute(matchRes.getBinding(), matchRes.getContext())); + result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getLeftHandSide()).substitute(matchRes.getBinding(), matchRes.getContext())); } } catch (SubstituteFailedException e) { continue; diff --git a/src/main/java/inference/equivalence/SemanticEquivalenceRelation.java b/src/main/java/inference/equivalence/SemanticEquivalenceRelation.java index 3dcc5d0..266c015 100644 --- a/src/main/java/inference/equivalence/SemanticEquivalenceRelation.java +++ b/src/main/java/inference/equivalence/SemanticEquivalenceRelation.java @@ -18,8 +18,8 @@ } public SemanticEquivalenceRelation(EquationFormula formula, int order) { - leftSideHand = formula.getLeftSideHand(); - rightSideHand = formula.getRightSideHand(); + leftSideHand = formula.getLeftHandSide(); + rightSideHand = formula.getRightHandSide(); this.order = order; } diff --git a/src/main/java/inference/rewrite/RewriteInferenceSystem.java b/src/main/java/inference/rewrite/RewriteInferenceSystem.java index dea1f97..bd24b1d 100644 --- a/src/main/java/inference/rewrite/RewriteInferenceSystem.java +++ b/src/main/java/inference/rewrite/RewriteInferenceSystem.java @@ -90,7 +90,7 @@ // for (ResourceTree tree: result) { // tree.debugAllPath(); // } -// if (result.contains(new ResourceTree(conclusion.getLeftSideHand())) && result.contains(new ResourceTree(conclusion.getRightSideHand()))) { +// if (result.contains(new ResourceTree(conclusion.getLeftHandSide())) && result.contains(new ResourceTree(conclusion.getRightHandSide()))) { // System.out.println("yes"); // } else { // System.out.println("no"); @@ -98,8 +98,8 @@ // System.out.println("====================================="); Map> leftRewriteGraph = new HashMap<>(); Map> rightRewriteGraph = new HashMap<>(); - conclusionLeftResult.addAll(rewriteTree(new ResourceTree(conclusion.getLeftSideHand()), inputFormula, leftRewriteGraph)); - conclusionRightResult.addAll(rewriteTree(new ResourceTree(conclusion.getRightSideHand()), inputFormula, rightRewriteGraph)); + conclusionLeftResult.addAll(rewriteTree(new ResourceTree(conclusion.getLeftHandSide()), inputFormula, leftRewriteGraph)); + conclusionRightResult.addAll(rewriteTree(new ResourceTree(conclusion.getRightHandSide()), inputFormula, rightRewriteGraph)); // System.out.println(conclusionRightResult); // if (conclusionLeftResult.size() != 0) { // ResourceTree resultRoot = conclusionLeftResult.iterator().next(); @@ -117,9 +117,9 @@ 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(); + ResourceTree inputResourceTree = new ResourceTree(inputFormulas.get(inputFormulaIndex).getLeftHandSide()); + List constraintResourceTree = constraintFormulas.stream().map(v -> new ResourceTree(v.getRightHandSide())).toList(); + List conditionalResourceTree = conditionalFormulas.stream().map(v -> new ResourceTree(v.getLeftHandSide())).toList(); boolean rewrited = true; while (rewrited) { rewrited = false; @@ -278,15 +278,15 @@ Set result = new HashSet<>(); Map rewritable = new HashMap<>(); for (EquationFormula formula : constraintFormulas) { - rewritable.put(new ResourceTree(formula.getLeftSideHand()), new ResourceTree(formula.getRightSideHand())); + rewritable.put(new ResourceTree(formula.getLeftHandSide()), new ResourceTree(formula.getRightHandSide())); } for (EquationFormula formula : conditionalFormulas) { - rewritable.put(new ResourceTree(formula.getLeftSideHand()), new ResourceTree(formula.getRightSideHand())); + rewritable.put(new ResourceTree(formula.getLeftHandSide()), new ResourceTree(formula.getRightHandSide())); } for (EquationFormula formula : invariantFormulas) { - rewritable.put(new ResourceTree(formula.getLeftSideHand()), new ResourceTree(formula.getRightSideHand())); + rewritable.put(new ResourceTree(formula.getLeftHandSide()), new ResourceTree(formula.getRightHandSide())); } - rewritable.put(new ResourceTree(inputFormula.getLeftSideHand()), new ResourceTree(inputFormula.getRightSideHand())); + rewritable.put(new ResourceTree(inputFormula.getLeftHandSide()), new ResourceTree(inputFormula.getRightHandSide())); Deque treeQueue = new ArrayDeque<>(); treeQueue.add(expandedInputResourceTree); @@ -458,16 +458,16 @@ private boolean loopCheck() { Map equationGraph = new HashMap<>(); for (EquationFormula formula : constraintFormulas) { - equationGraph.put(formula.getLeftSideHand(), formula.getRightSideHand()); + equationGraph.put(formula.getLeftHandSide(), formula.getRightHandSide()); } for (EquationFormula formula : invariantFormulas) { - equationGraph.put(formula.getLeftSideHand(), formula.getRightSideHand()); + equationGraph.put(formula.getLeftHandSide(), formula.getRightHandSide()); } for (EquationFormula inputFormula : inputFormulas) { - equationGraph.put(inputFormula.getLeftSideHand(), inputFormula.getRightSideHand()); + equationGraph.put(inputFormula.getLeftHandSide(), inputFormula.getRightHandSide()); } for (EquationFormula formula : conditionalFormulas) { - equationGraph.put(formula.getLeftSideHand(), formula.getRightSideHand()); + equationGraph.put(formula.getLeftHandSide(), formula.getRightHandSide()); } for (EvaluatableTerm leftTerm : equationGraph.keySet()) { Set used = new HashSet<>(); @@ -536,12 +536,12 @@ private boolean definitionFormulaCheck(Formula formula) { if (formula instanceof EquationFormula equation) { - return singleTermCheck(equation.getLeftSideHand()); + return singleTermCheck(equation.getLeftHandSide()); } 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 singleTermCheck(eq1.getLeftHandSide()) && singleTermCheck(eq2.getLeftHandSide()); } } return false; @@ -573,8 +573,8 @@ 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()); + List resources = new ArrayList<>(equation.getLeftHandSide().getSubTerms(Resource.class).values()); + resources.addAll(equation.getRightHandSide().getSubTerms(Resource.class).values()); for (Resource resource : resources) { if (resource.getOrder() == 0) { return true; diff --git a/src/main/java/models/Position.java b/src/main/java/models/Position.java index 5d4b247..4ee3236 100644 --- a/src/main/java/models/Position.java +++ b/src/main/java/models/Position.java @@ -51,6 +51,12 @@ return paths.get(index); } + public static Position convertPosition(models.algebra.Position position) { + List orders = new ArrayList<>(position.getOrders()); + orders.add(0, 0); + return new Position(orders); + } + @Override public boolean equals(Object another) { diff --git a/src/main/java/models/algebra/Position.java b/src/main/java/models/algebra/Position.java index 243e274..32ab965 100644 --- a/src/main/java/models/algebra/Position.java +++ b/src/main/java/models/algebra/Position.java @@ -49,4 +49,9 @@ public int hashCode() { return orders.hashCode(); } + + @Override + public String toString() { + return this.orders.toString(); + } } diff --git a/src/main/java/models/formulas/EquationFormula.java b/src/main/java/models/formulas/EquationFormula.java index 4ed83f6..3b94685 100644 --- a/src/main/java/models/formulas/EquationFormula.java +++ b/src/main/java/models/formulas/EquationFormula.java @@ -6,22 +6,22 @@ @Getter public class EquationFormula extends Formula { - private EvaluatableTerm leftSideHand; - private EvaluatableTerm rightSideHand; + private EvaluatableTerm leftHandSide; + private EvaluatableTerm rightHandSide; public EquationFormula(EvaluatableTerm leftTerm, EvaluatableTerm rightTerm) { - this.leftSideHand = leftTerm; - this.rightSideHand = rightTerm; + this.leftHandSide = leftTerm; + this.rightHandSide = rightTerm; } public EquationFormula linearRightNormalized() { - return new EquationFormula(leftSideHand.linearRightNormalize(), rightSideHand.linearRightNormalize()); + return new EquationFormula(leftHandSide.linearRightNormalize(), rightHandSide.linearRightNormalize()); } @Override public String toString() { - return leftSideHand.toString() + " = " + rightSideHand.toString(); + return leftHandSide.toString() + " = " + rightHandSide.toString(); } @Override @@ -30,7 +30,7 @@ return false; } EquationFormula anotherFormula = (EquationFormula) another; - return leftSideHand.equals(anotherFormula.getLeftSideHand()) && rightSideHand.equals(anotherFormula.getRightSideHand()); + return leftHandSide.equals(anotherFormula.getLeftHandSide()) && rightHandSide.equals(anotherFormula.getRightHandSide()); } @Override diff --git a/src/main/java/models/formulas/meta/MetaEquationFormula.java b/src/main/java/models/formulas/meta/MetaEquationFormula.java index 9df78c7..ce00bdf 100644 --- a/src/main/java/models/formulas/meta/MetaEquationFormula.java +++ b/src/main/java/models/formulas/meta/MetaEquationFormula.java @@ -18,8 +18,8 @@ @Getter public class MetaEquationFormula extends MetaFormula { - private RDLTerm leftSideHand; - private RDLTerm rightSideHand; + private RDLTerm leftHandSide; + private RDLTerm rightHandSide; public MetaEquationFormula(RDLTerm left, RDLTerm right) { if (! left.isEvaluatableTerm()) { @@ -28,8 +28,8 @@ if (! right.isEvaluatableTerm()) { throw new IllegalTypeException(); } - this.leftSideHand = left; - this.rightSideHand = right; + this.leftHandSide = left; + this.rightHandSide = right; } @Override @@ -40,17 +40,17 @@ } result.add(constraint); EquationFormula eq = (EquationFormula) formula; - if (leftSideHand instanceof MetaRDLTerm metaLeft) { - result = metaLeft.isMatchedBy(eq.getLeftSideHand(), result); + if (leftHandSide instanceof MetaRDLTerm metaLeft) { + result = metaLeft.isMatchedBy(eq.getLeftHandSide(), result); } else { - if (! leftSideHand.equals(eq.getLeftSideHand())) { + if (! leftHandSide.equals(eq.getLeftHandSide())) { return new HashSet<>(); } } - if (rightSideHand instanceof MetaRDLTerm metaRight) { - result = metaRight.isMatchedBy(eq.getRightSideHand(), result); + if (rightHandSide instanceof MetaRDLTerm metaRight) { + result = metaRight.isMatchedBy(eq.getRightHandSide(), result); } else { - if (! rightSideHand.equals(eq.getRightSideHand())) { + if (! rightHandSide.equals(eq.getRightHandSide())) { return new HashSet<>(); } } @@ -59,12 +59,12 @@ @Override public EquationFormula substitution(Map binding, Map context) { - RDLTerm left = leftSideHand; - RDLTerm right = rightSideHand; - if (leftSideHand instanceof MetaRDLTerm metaLeft) { + RDLTerm left = leftHandSide; + RDLTerm right = rightHandSide; + if (leftHandSide instanceof MetaRDLTerm metaLeft) { left = metaLeft.substitute(binding, context); } - if (rightSideHand instanceof MetaRDLTerm metaRight) { + if (rightHandSide instanceof MetaRDLTerm metaRight) { right = metaRight.substitute(binding, context); } return new EquationFormula((EvaluatableTerm) left, (EvaluatableTerm) right); @@ -72,12 +72,12 @@ @Override public MetaEquationFormula replace(Map mapping) { - RDLTerm left = leftSideHand; - RDLTerm right = rightSideHand; - if (leftSideHand instanceof MetaRDLTerm metaLeft) { + RDLTerm left = leftHandSide; + RDLTerm right = rightHandSide; + if (leftHandSide instanceof MetaRDLTerm metaLeft) { left = metaLeft.replace(mapping); } - if (rightSideHand instanceof MetaRDLTerm metaRight) { + if (rightHandSide instanceof MetaRDLTerm metaRight) { right = metaRight.replace(mapping); } return new MetaEquationFormula(left, right); @@ -86,17 +86,17 @@ @Override public Set getAllVariables() { Set result = new HashSet<>(); - if (leftSideHand instanceof MetaRDLTerm metaLeft) { + if (leftHandSide instanceof MetaRDLTerm metaLeft) { result.addAll(metaLeft.getAllVariables()); } - if (rightSideHand instanceof MetaRDLTerm metaRight) { + if (rightHandSide instanceof MetaRDLTerm metaRight) { result.addAll(metaRight.getAllVariables()); } return result; } public String toString() { - return leftSideHand.toString() + " = " + rightSideHand.toString(); + return leftHandSide.toString() + " = " + rightHandSide.toString(); } public boolean equals(Object another) { @@ -104,7 +104,7 @@ return false; } MetaEquationFormula anohterFormula = (MetaEquationFormula) another; - return leftSideHand.equals(anohterFormula.getLeftSideHand()) && rightSideHand.equals(anohterFormula.getRightSideHand()); + return leftHandSide.equals(anohterFormula.getLeftHandSide()) && rightHandSide.equals(anohterFormula.getRightHandSide()); } public int hashCode() { @@ -114,8 +114,8 @@ @Override public Set getSubTerms(Class clazz) { Set result = new HashSet<>(); - result.addAll(leftSideHand.getSubTerms(clazz).values()); - result.addAll(rightSideHand.getSubTerms(clazz).values()); + result.addAll(leftHandSide.getSubTerms(clazz).values()); + result.addAll(rightHandSide.getSubTerms(clazz).values()); return result; } diff --git a/src/main/java/models/terms/Dependency.java b/src/main/java/models/terms/Dependency.java index 6b2ecb8..af88546 100644 --- a/src/main/java/models/terms/Dependency.java +++ b/src/main/java/models/terms/Dependency.java @@ -17,7 +17,7 @@ private RDLTerm dependingTerm; private TreeMultiset dependedTerms; - public Dependency(RDLTerm dependingTerm, List dependedTerms) { + public Dependency(RDLTerm dependingTerm, List dependedTerms) { super(dependedTerms.iterator().next().getOrder(), dependingTerm.getSize() + dependedTerms.stream().mapToInt(v -> v.size).sum()); this.dependingTerm = dependingTerm; this.dependedTerms = TreeMultiset.create(dependedTerms); diff --git a/src/main/java/models/terms/DependencyTerm.java b/src/main/java/models/terms/DependencyTerm.java index 2949ec5..c3e4721 100644 --- a/src/main/java/models/terms/DependencyTerm.java +++ b/src/main/java/models/terms/DependencyTerm.java @@ -2,7 +2,9 @@ import java.util.ArrayList; import java.util.Arrays; +import java.util.HashSet; import java.util.List; +import java.util.Set; import java.util.TreeMap; import com.google.common.collect.TreeMultiset; @@ -95,17 +97,45 @@ @Override public Dependency getDependency() { - RDLTerm dependingTerm; - List dependedTerms = new ArrayList<>(); - if (this.dependingTerm instanceof Resource || this.dependingTerm instanceof ResourceConstant) { - dependingTerm = this.dependingTerm; + return new Dependency(dependingTerm, getDependedTerms()); + } + + public Dependency getNoArgumentDependency() { + if (dependingTerm instanceof DependencyTerm dt) { + return new Dependency(dt.getNoArgumentDependency(), getDependedTerms()); + } + return getDependency(); + } + + public Set requiredDependenciesForDefinitionFormulaLeftHandSide() { + Set result = new HashSet<>(); + result.add(getDependency()); + if (this.dependingTerm instanceof DependencyTerm dt) { + for (Dependency d : dt.requiredDependenciesForDefinitionFormulaLeftHandSide()) { + result.add(new Dependency(d, getDependedTerms())); + } + } + return result; + } + + public Set requiredDependenciesForAdmissible() { + Set result = new HashSet<>(); + if (dependingTerm instanceof Resource) { + result.add(getDependency()); } else { - dependingTerm = this.dependingTerm.getDependency(); + DependencyTerm dt = (DependencyTerm) dependingTerm; + for (Dependency d: dt.requiredDependenciesForAdmissible()) { + DependencyTerm dependingTerm = new DependencyTerm((EvaluatableTerm) d.getDependingTerm(), getDependedTerms(), getArgumentTerms()); + List dts = new ArrayList<>(); + for (EvaluatableTerm te: d.getDependedTerms()) { + dts.add(new DependencyTerm(te, getDependedTerms(), getArgumentTerms())); + } + result.add(new Dependency(dependingTerm, dts)); + } + } - for (EvaluatableTerm dependedTerm: this.termPairs.keySet()) { - dependedTerms.add(dependedTerm); - } - return new Dependency(dependingTerm, dependedTerms); + + return result; } @Override diff --git a/src/test/java/inference/ProofSystemTest.java b/src/test/java/inference/ProofSystemTest.java new file mode 100644 index 0000000..535f249 --- /dev/null +++ b/src/test/java/inference/ProofSystemTest.java @@ -0,0 +1,40 @@ +package inference; + +import static org.junit.jupiter.api.Assertions.*; + +import java.util.Set; + +import org.junit.jupiter.api.Test; + +import models.formulas.EquationFormula; +import models.terms.DependencyTerm; +import models.terms.Resource; + +public class ProofSystemTest { + + Resource a = new Resource("a", 1); + Resource b = new Resource("b", 1); + Resource c = new Resource("c", 1); + Resource d = new Resource("d", 1); + Resource e = new Resource("e", 1); + Resource f = new Resource("f", 1); + Resource g = new Resource("g", 1); + + @Test + void AdmissibleTest() { + DependencyTerm t1 = new DependencyTerm(a, b, c); + EquationFormula eq1 = new EquationFormula(t1, a); + assertThrows(IllegalArgumentException.class, () -> new ProofSystem(Set.of(eq1), eq1)); + EquationFormula eq2 = new EquationFormula(a, t1); + assertThrows(IllegalArgumentException.class, () -> new ProofSystem(Set.of(eq2), eq1)); + + DependencyTerm t2 = new DependencyTerm(a, a, b); + EquationFormula eq3 = new EquationFormula(t2, b); + assertDoesNotThrow(() -> { + new ProofSystem(Set.of(eq3), eq3); + } + ); + + } + +} diff --git a/src/test/java/terms/DependencyTermTest.java b/src/test/java/terms/DependencyTermTest.java index a8592c8..114c288 100644 --- a/src/test/java/terms/DependencyTermTest.java +++ b/src/test/java/terms/DependencyTermTest.java @@ -6,6 +6,7 @@ import exceptions.SyntaxException; import models.Position; +import models.terms.Dependency; import models.terms.DependencyTerm; import models.terms.Resource; @@ -106,4 +107,34 @@ assertEquals(t2.replace(new Position(0, 0, 0), t1), new DependencyTerm(new DependencyTerm(t1, b, c), d, e)); } + @Test + void RequiredDependenciesForDefinitionFormulaLeftHandSideTest() { + DependencyTerm t1 = new DependencyTerm(a, b, c); + Dependency d1 = new Dependency(a, b); + assertTrue(t1.requiredDependenciesForDefinitionFormulaLeftHandSide().contains(d1)); + DependencyTerm t2 = new DependencyTerm(t1, d, e); + Dependency d2 = new Dependency(d1, d); + Dependency d3 = new Dependency(t1, d); + assertTrue(t2.requiredDependenciesForDefinitionFormulaLeftHandSide().contains(d2)); + assertTrue(t2.requiredDependenciesForDefinitionFormulaLeftHandSide().contains(d3)); + DependencyTerm t3 = new DependencyTerm(t2, f, g); + Dependency d4 = new Dependency(d2, f); + Dependency d5 = new Dependency(d3, f); + Dependency d6 = new Dependency(t2, f); + assertTrue(t3.requiredDependenciesForDefinitionFormulaLeftHandSide().contains(d4)); + assertTrue(t3.requiredDependenciesForDefinitionFormulaLeftHandSide().contains(d5)); + assertTrue(t3.requiredDependenciesForDefinitionFormulaLeftHandSide().contains(d6)); + } + + @Test + void NoArgsDependencyTest() { + DependencyTerm t1 = new DependencyTerm(a, b, c); + Dependency d1 = new Dependency(a, b); + assertEquals(t1.getNoArgumentDependency(), d1); + DependencyTerm t2 = new DependencyTerm(t1, d, e); + Dependency d2 = new Dependency(d1, d); + assertEquals(t2.getNoArgumentDependency(), d2); + + } + }