diff --git a/src/main/java/Main.java b/src/main/java/Main.java index fac8790..0959b6f 100644 --- a/src/main/java/Main.java +++ b/src/main/java/Main.java @@ -1,17 +1,15 @@ -import java.util.HashMap; -import java.util.Map; - -import com.google.common.collect.TreeMultimap; +import java.util.Set; import constants.Types; -import models.algebra.Constant; -import models.algebra.Expression; +import inference.ProofSystem; +import models.Position; import models.algebra.Type; -import models.algebra.Variable; -import models.terms.meta.MetaDynamicDependency; -import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaResource; -import models.terms.meta.MetaTermGenerator; +import models.formulas.DependencyFormula; +import models.formulas.EquationFormula; +import models.terms.DependencyTerm; +import models.terms.EvaluatableTerm; +import models.terms.Resource; +import models.terms.ResourceConstant; public class Main { @@ -19,46 +17,60 @@ public static void main(String[] args) { // - sandbox(); - sandbox2(); sandbox3(); } - static void sandbox() { - Expression tmp = utils.ExpressionUitls.parse("x"); + 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); - tmp = utils.ExpressionUitls.parse("(x + 5) * 3"); - Map nums = new HashMap<>(); - int a = utils.ExpressionUitls.getCoefficientAndConstantsFromExpression(tmp, nums, 1); - System.out.println(tmp); - System.out.println(a); - System.out.println(nums); - - int b = utils.ExpressionUitls.getConstantValue(new Constant("3")); - System.out.println(b); + for (var pos: tmp.keySet()) { + System.out.println(Position.convertPosition(pos) + ", " + tmp.get(pos)); + } } - + static void sandbox2() { - TreeMultimap tmp = TreeMultimap.create(); - tmp.put(1, 1); - tmp.put(1, 2); - tmp.put(1, 1); - tmp.put(1, 3); - System.out.println(tmp.get(1)); + 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() { - MetaDynamicDependency d1 = new MetaDynamicDependency((ci, cd, mi, md, context) -> new MetaResource(new Variable("x" + ci))); - MetaDynamicDependency d2 = new MetaDynamicDependency(new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - if (curIndex == 0 && curDepth < maxDepth) return new MetaDynamicDependency(this); - else return new MetaResource(new Variable("x" + curIndex + "_" + curDepth)); - } - }); - d2.generate(0, 2, 2, null); - System.out.println(d2.generate(0, 2, 2, null)); + 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/exceptions/MissingContextException.java b/src/main/java/exceptions/MissingContextException.java new file mode 100644 index 0000000..890565e --- /dev/null +++ b/src/main/java/exceptions/MissingContextException.java @@ -0,0 +1,13 @@ +package exceptions; + +public class MissingContextException extends RuntimeException{ + + public MissingContextException(String msg) { + super(msg); + } + + public MissingContextException() { + super("some context missing"); + } + +} diff --git a/src/main/java/exceptions/ReplaceFailedException.java b/src/main/java/exceptions/ReplaceFailedException.java new file mode 100644 index 0000000..01ce665 --- /dev/null +++ b/src/main/java/exceptions/ReplaceFailedException.java @@ -0,0 +1,5 @@ +package exceptions; + +public class ReplaceFailedException extends RuntimeException { + +} diff --git a/src/main/java/inference/AssumptionSizeCalculator.java b/src/main/java/inference/AssumptionSizeCalculator.java new file mode 100644 index 0000000..aa9e971 --- /dev/null +++ b/src/main/java/inference/AssumptionSizeCalculator.java @@ -0,0 +1,10 @@ +package inference; + +import models.terms.RDLTerm; + +@FunctionalInterface +public interface AssumptionSizeCalculator { + + public int calculate(RDLTerm rightSideHand); + +} diff --git a/src/main/java/inference/ConclusionSizeCalculator.java b/src/main/java/inference/ConclusionSizeCalculator.java new file mode 100644 index 0000000..d2cdb23 --- /dev/null +++ b/src/main/java/inference/ConclusionSizeCalculator.java @@ -0,0 +1,12 @@ +package inference; + +import java.util.List; + +import models.formulas.Formula; + +@FunctionalInterface +public interface ConclusionSizeCalculator { + + public int calculate(List assumptions); + +} diff --git a/src/main/java/inference/DependencyAxiom.java b/src/main/java/inference/DependencyAxiom.java new file mode 100644 index 0000000..720be34 --- /dev/null +++ b/src/main/java/inference/DependencyAxiom.java @@ -0,0 +1,72 @@ +package inference; + +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.Deque; +import java.util.HashSet; +import java.util.List; +import java.util.Set; + +import exceptions.SyntaxException; +import models.Position; +import models.formulas.DependencyFormula; +import models.formulas.Formula; +import models.terms.Dependency; +import models.terms.RDLTerm; +import models.terms.meta.MatchConstraint; +import utils.Permutation; + +public class DependencyAxiom extends InferenceRule{ + + protected int targetAssumptionIndex = 0; + + public DependencyAxiom(String name) { + super(name); + } + + @Override + public Set derive(List assumptions, Set existTerms) { + if (missingVariables.size() == 0) { + return recursionDerive(assumptions, MatchConstraint.createDefault()); + } else { + Set result = new HashSet<>(); + for (List terms: Permutation.permutation(existTerms, missingVariables.size())) { + for (MatchConstraint constraint: missingVariableFill(terms)) { + if (defaultOrderConstraint != null && (! defaultOrderConstraint.check(constraint.getOrderConstraint()))) continue; + result.addAll(recursionDerive(assumptions, constraint)); + } + } + return result; + } + } + + public Set recursionDerive(List assumptions, MatchConstraint constraint) { + Set result = new HashSet<>(); + Deque q = new ArrayDeque<>(); + q.add(new Position()); + Dependency baseTerm = ((DependencyFormula) assumptions.get(targetAssumptionIndex)).getDependency(); + while (! q.isEmpty()) { + Position curPos = q.pollFirst(); + RDLTerm curTerm = baseTerm; + for (int i = 1; i < curPos.size(); i++) { + curTerm = (RDLTerm) curTerm.getChild(curPos.getPath(i)); + } + if (curTerm instanceof Dependency d) { + List assumptionsCopy = new ArrayList(assumptions); + assumptionsCopy.set(targetAssumptionIndex, new DependencyFormula(d)); + for (Formula derived: derive(assumptionsCopy, constraint.clone())) { + if (derived instanceof DependencyFormula df) { + try { + result.add(new DependencyFormula((Dependency) baseTerm.replace(curPos, df.getDependency()))); + } catch (SyntaxException e) {} + } + } + } + for (int i = 0; i < curTerm.getChildren().size(); i++) { + q.add(curPos.addPath(i)); + } + } + return result; + } + +} diff --git a/src/main/java/inference/EquationAxiom.java b/src/main/java/inference/EquationAxiom.java new file mode 100644 index 0000000..0f014ef --- /dev/null +++ b/src/main/java/inference/EquationAxiom.java @@ -0,0 +1,163 @@ +package inference; +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 exceptions.SubstituteFailedException; +import models.Position; +import models.formulas.DependencyFormula; +import models.formulas.Formula; +import models.formulas.meta.MetaEquationFormula; +import models.formulas.meta.MetaFormula; +import models.terms.DependencyTerm; +import models.terms.EvaluatableTerm; +import models.terms.RDLTerm; +import models.terms.Resource; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaRDLTerm; +import utils.Permutation; + +public class EquationAxiom extends InferenceRule { + + public EquationAxiom(String name, List assumptions, MetaEquationFormula conclusion, InferenceOrderConstraint constraint) { + super(name, assumptions, conclusion, constraint); + } + + public EquationAxiom(String name, List assumptions, MetaEquationFormula conclusion) { + super(name, assumptions, conclusion); + } + + 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()); + } + + public Set apply(Listassumptions, EvaluatableTerm term, MatchConstraint constraint) { + Set result = new HashSet<>(); + if (assumptions.size() < this.assumptions.size()) { + return new HashSet<>(); + } + + Set matchResult = assumptionMatch(assumptions, constraint); + + Set conclusionLeftMatchResult = conclusionLeftSideHandMatch(term, matchResult); + for (MatchConstraint leftConst: conclusionLeftMatchResult) { + leftConst.getContext().put("isLeft", true); + } + Set conclusionRightMatchResult = conclusionRightSideHandMatch(term, matchResult); + for (MatchConstraint rightConst: conclusionRightMatchResult) { + rightConst.getContext().put("isLeft", false); + } + Set conclusionMatchResult = new HashSet<>(); + conclusionMatchResult.addAll(conclusionLeftMatchResult); + conclusionMatchResult.addAll(conclusionRightMatchResult); + + MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion; + for (MatchConstraint matchRes: conclusionMatchResult) { + boolean isLeft =(Boolean) matchRes.getContext().get("isLeft"); + if (defaultOrderConstraint != null && ! defaultOrderConstraint.check(matchRes.getOrderConstraint())) { + continue; + } + try { + if (isLeft) { + result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getRightHandSide()).substitute(matchRes.getBinding(), matchRes.getContext())); + } else { + result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getLeftHandSide()).substitute(matchRes.getBinding(), matchRes.getContext())); + } + } catch (SubstituteFailedException e) { + continue; + } + } + return result; + } + + + protected Set conclusionLeftSideHandMatch(EvaluatableTerm term, Set matchResult) { + MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion; + return ((MetaRDLTerm) metaConclusion.getLeftHandSide()).isMatchedBy(term, matchResult); + } + + protected Set conclusionRightSideHandMatch(EvaluatableTerm term, Set matchResult) { + MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion; + return ((MetaRDLTerm) metaConclusion.getRightHandSide()).isMatchedBy(term, matchResult); + } + + + protected static Set requiredAssumptions(EvaluatableTerm term) { + if (term instanceof Resource) { + return new HashSet<>(); + } + DependencyTerm depTerm = (DependencyTerm) term; + Set result = new HashSet<>(); + EvaluatableTerm dependingTerm = depTerm.getDependingTerm(); + List dependedTerms = depTerm.getDependedTerms(); + List argumentTerms = depTerm.getArgumentTerms(); + if (dependingTerm instanceof Resource) { + result.add(new DependencyFormula(dependingTerm, dependedTerms)); + } else if (dependingTerm instanceof DependencyTerm depending) { + for (Formula formula : requiredAssumptions(depending)) { + if (formula instanceof DependencyFormula dependency) { + DependencyTerm newDependingTerm = new DependencyTerm((EvaluatableTerm) dependency.getDependency().getDependingTerm(), dependedTerms, argumentTerms); + List newDependedTerms = new ArrayList<>(); + for (RDLTerm dependedTerm : dependency.getDependency().getDependedTerms()) { + newDependedTerms.add(new DependencyTerm((EvaluatableTerm) dependedTerm, dependedTerms, argumentTerms)); + } + result.add(new DependencyFormula(newDependingTerm, newDependedTerms)); + } + } + } + return result; + } + + protected static boolean conclusionCheck(EvaluatableTerm leftSideHand, Set formulas) { + for (Formula formula: requiredAssumptions(leftSideHand)) { + if (! formulas.contains(formula)) { + return false; + } + } + return true; + } + + protected static Map> savePositions(Set matchConstraint) { + Map> result = new HashMap<>(); + for (MatchConstraint constraint : matchConstraint) { + Deque posDeque = new ArrayDeque<>(); + posDeque.add(new Position()); + Map posMap = new HashMap<>(); + while (posDeque.size() != 0) { + Position pos = posDeque.pollFirst(); + if (! constraint.getContext().containsKey(pos)) { + continue; + } + int i = 0; + while (true) { + Position nextPos = pos.addPath(i); + if (! constraint.getContext().containsKey(nextPos)) { + break; + } + posMap.put(pos, (Integer) constraint.getContext().get(pos)); + posDeque.add(nextPos); + } + } + result.put(constraint, posMap); + } + return result; + } + +} diff --git a/src/main/java/inference/In.java b/src/main/java/inference/In.java new file mode 100644 index 0000000..5833adc --- /dev/null +++ b/src/main/java/inference/In.java @@ -0,0 +1,246 @@ +package inference; + +import java.util.HashSet; +import java.util.Map; +import java.util.Set; + +import lombok.Getter; +import lombok.RequiredArgsConstructor; +import models.algebra.Variable; +import models.formulas.EquationFormula; +import models.formulas.Formula; +import models.formulas.meta.MetaEquationFormula; +import models.terms.EvaluatableTerm; +import models.terms.RDLTerm; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaConstant; +import models.terms.meta.MetaDependencyTerm; +import models.terms.meta.MetaDynamicDependencyTerm; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; + + +@RequiredArgsConstructor +@Getter +public class In extends Formula { + + private final EvaluatableTerm leftSideHand; + private final EvaluatableTerm rightSideHand; + + static final MetaEquationFormula domainMembershipAssumption = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + context.put("" + curDepth, curIndex); + if (curDepth == maxDepth - 1 && curIndex == 0) { + return new MetaDependencyTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ); + } else if (curIndex == 0) { + return new MetaDynamicDependencyTerm(this); + } + curIndex -= 1; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex/2)); + } + return new MetaEvaluatableTermVariable(new Variable("ue" + curDepth + "_" + curIndex/2)); + } + } + ), + new MetaConstant(new Variable("c")) + ); + + static final MetaDependencyTerm domainMembershipConclusionLeftSideHand = new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + maxIndex = (Integer) context.get("" + curDepth); + if (curDepth == maxDepth && curIndex == 0) { + return new MetaEvaluatableTermVariable(new Variable("ue")); + } + curIndex -= 1; + if (curIndex >= maxIndex) { + return null; + } + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex/2)); + } + return new MetaEvaluatableTermVariable(new Variable("ue" + curDepth + "_" + curIndex/2)); + } + } + ); + + static final MetaDependencyTerm domainMembershipConclusionRightSideHand = new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + maxIndex = (Integer) context.get("" + curDepth); + if (curDepth == maxDepth && curIndex == 0) { + return new MetaEvaluatableTermVariable(new Variable("te")); + } + curIndex -= 1; + if (curIndex >= maxIndex) { + return null; + } + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex/2)); + } + return new MetaEvaluatableTermVariable(new Variable("ue" + curDepth + "_" + curIndex/2)); + } + } + ); + + + static final MetaEvaluatableTermVariable codomainMembershipConclusionLeftSideHand = new MetaEvaluatableTermVariable(new Variable("ve")); + static final MetaEvaluatableTermVariable codomainMembershipConclusionRightSideHand = new MetaEvaluatableTermVariable(new Variable("se")); + + static final MetaEquationFormula codomainMembershipAssumption = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")) + ), + new MetaEvaluatableTermVariable(new Variable("ve")) + ); + + public Set deriveRule() { + Set result = new HashSet<>(); +// result.addAll(deriveByDomainMemberShip()); +// result.addAll(deriveByCodomainMemberShip()); + return result; + } + + static Set deriveIn(Set equationFormulas) { + Set result = new HashSet<>(); + for (EquationFormula eq : equationFormulas) { + result.addAll(deriveByDomainMembership(eq)); + result.addAll(deriveByCodomainMembership(eq)); + } + return result; + } + + static Set deriveIn(EquationFormula equationFormula) { + return deriveIn(Set.of(equationFormula)); + } + + static Set deriveByDomainMembership(EquationFormula equationFormula) { + Set result = new HashSet<>(); + Set constraints = domainMembershipAssumption.isMatchedBy(equationFormula); + for (MatchConstraint constraint : constraints) { + 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()); + result.add(new In((EvaluatableTerm) left, (EvaluatableTerm)right)); + } + return result; + } + + static Set deriveByCodomainMembership(EquationFormula equationFormula) { + Set result = new HashSet<>(); + Set constraints = codomainMembershipAssumption.isMatchedBy(equationFormula); + for (MatchConstraint constraint : constraints) { + RDLTerm left = codomainMembershipConclusionLeftSideHand.substitute(constraint.getBinding(), constraint.getContext()); + RDLTerm right = codomainMembershipConclusionRightSideHand.substitute(constraint.getBinding(), constraint.getContext()); + result.add(new In((EvaluatableTerm) left, (EvaluatableTerm)right)); + } + return result; + } + + +// private Set deriveByDomainMemberShip() { +// Set result = new HashSet<>(); +// Set leftMatchResult = domainMembershipConclusionLeftSideHand.isMatchedBy(leftSideHand); +// Set rightMatchResult = domainMembershipConclusionRightSideHand.isMatchedBy(rightSideHand, leftMatchResult); +// for (MatchConstraint constraint: rightMatchResult) { +// int used1 = (Integer) constraint.getContext().getOrDefault("used1", 1); +// int used2 = (Integer) constraint.getContext().getOrDefault("used2", 1); +// int depth1 = (Integer) constraint.getContext().get("depth1"); +// int depth2 = (Integer) constraint.getContext().get("depth2"); +// if (used1 != used2) { +// continue; +// } +// if (depth1 != depth2) { +// continue; +// } +// boolean flg = false; +// for (int i = 1; i < depth1; i++) { +// int d1 = (Integer) constraint.getContext().get("1-" + i); +// int d2 = (Integer) constraint.getContext().get("2-" + i); +// if (d1 != d2) { +// flg = true; +// break; +// } +// } +// if (flg) continue; +// Map mapping = new HashMap<>(); +// for (Variable variable: constraint.getBinding().keySet()) { +// mapping.put(new MetaEvaluatableTermVariable(variable), constraint.getBinding().get(variable)); +// } +// MetaRDLTerm left = (MetaRDLTerm)domainMembershipAssumptionLeftSideHand.generate(10000, depth1, constraint.cloneContext()).replace(mapping); +// MetaResource right = new MetaResource(new Variable("c"), new Constant("0")); +// result.add(new MetaEquationFormula(left, right)); +// } +// return result; +// } +// +// private Set deriveByCodomainMemberShip() { +// Set result = new HashSet<>(); +// Set leftMatchResult = codomainMembershipConclusionLeftSideHand.isMatchedBy(leftSideHand); +// Set rightMatchResult = codomainMembershipConclusionRightSideHand.isMatchedBy(rightSideHand, leftMatchResult); +// for (MatchConstraint constraint : rightMatchResult) { +// Map mapping = new HashMap<>(); +// for (Variable variable: constraint.getBinding().keySet()) { +// mapping.put(new MetaEvaluatableTermVariable(variable), constraint.getBinding().get(variable)); +// } +// MetaRDLTerm left = new MetaDynamicDependencyTerm( +// new MetaTermGenerator() { +// @Override +// public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { +// curIndex -= 1; +// if (curIndex % 2 == 0) { +// return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2)); +// } +// return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); +// } +// }, +// constraint.getBinding().get(codomainMembershipConclusionRightSideHand.getVariableName()) +// ); +// result.add(new MetaEquationFormula(left, constraint.getBinding().get(codomainMembershipConclusionLeftSideHand.getVariableName()))); +// } +// return result; +// } + + + + @Override + public String toString() { + return leftSideHand.toString() + " in " + rightSideHand.toString(); + } + + @Override + public boolean equals(Object another) { + if (another instanceof In in) { + return this.leftSideHand.equals(in.getLeftSideHand()) && this.rightSideHand.equals(in.getRightSideHand()); + } + return false; + } + + @Override + public int hashCode() { + return toString().hashCode(); + } + +} diff --git a/src/main/java/inference/InferenceHistory.java b/src/main/java/inference/InferenceHistory.java new file mode 100644 index 0000000..b3c4a0a --- /dev/null +++ b/src/main/java/inference/InferenceHistory.java @@ -0,0 +1,78 @@ +package inference; + +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.Collections; +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 java.util.stream.Collectors; + +import models.formulas.Formula; + +public class InferenceHistory { + + private Map> inferenceHistory; + + public InferenceHistory() { + 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); + } + + public String getHistoryString(Formula conclusion) { + if (! inferenceHistory.containsKey(conclusion)) { + return "Inference failed"; + } + List result = new ArrayList<>(); + Deque q = new ArrayDeque<>(); + Set used = new HashSet<>(); + q.add(conclusion); + result.add(conclusion.toString()); + while (! q.isEmpty()) { + Formula formula = q.pollFirst(); + 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(", "))); + for (Formula f: node.getAssumptions()) { + q.add(f); + } + } + Collections.reverse(result); + return result.stream().collect(Collectors.joining("\n")); + } + +} diff --git a/src/main/java/inference/InferenceHistoryNode.java b/src/main/java/inference/InferenceHistoryNode.java new file mode 100644 index 0000000..7486d1d --- /dev/null +++ b/src/main/java/inference/InferenceHistoryNode.java @@ -0,0 +1,40 @@ +package inference; +import java.util.List; + +import com.google.common.base.Objects; + +import lombok.Getter; +import models.formulas.Formula; + +@Getter +public class InferenceHistoryNode { + + private final List assumptions; + private final Formula conclusion; + private final InferenceRule usedRule; + + public InferenceHistoryNode(List assumptions, InferenceRule usedRule, Formula conclusion) { + this.assumptions = assumptions; + this.usedRule = usedRule; + this.conclusion = conclusion; + } + + @Override + public boolean equals(Object another) { + if (another instanceof InferenceHistoryNode node) { + return Objects.equal(node.assumptions, this.assumptions) && Objects.equal(node.usedRule, this.usedRule) && Objects.equal(this.conclusion, node.conclusion); + } + return false; + } + + @Override + public int hashCode() { + return Objects.hashCode(assumptions, conclusion, usedRule); + } + + @Override + public String toString() { + return assumptions + "---(" + usedRule.getName() + ")--->" + conclusion; + } + +} diff --git a/src/main/java/inference/InferenceOrderConstraint.java b/src/main/java/inference/InferenceOrderConstraint.java index e74b9dc..e255d63 100644 --- a/src/main/java/inference/InferenceOrderConstraint.java +++ b/src/main/java/inference/InferenceOrderConstraint.java @@ -46,6 +46,9 @@ } public boolean check(Map orderConstraints) { + if (!variableCheck(orderConstraints)) { + return false; + } switch(this.operator) { case EQ: return getLeftValue(orderConstraints) == getRightValue(orderConstraints); @@ -71,6 +74,16 @@ } } + private boolean variableCheck(Map orderConstraints) { + if (this.leftSideHandVariable != null && ! orderConstraints.containsKey(this.leftSideHandVariable)) { + return false; + } + if (this.rightSideHandVariable != null && ! orderConstraints.containsKey(this.rightSideHandVariable)) { + return false; + } + return true; + } + private int getRightValue(Map orderConstraints) { if (this.rightSideHandVariable != null) { OrderVariableConstraint constraint = orderConstraints.get(this.rightSideHandVariable); diff --git a/src/main/java/inference/InferenceRule.java b/src/main/java/inference/InferenceRule.java index 6abbded..c9a7ecd 100644 --- a/src/main/java/inference/InferenceRule.java +++ b/src/main/java/inference/InferenceRule.java @@ -1,18 +1,13 @@ package inference; import java.util.ArrayList; -import java.util.Collection; -import java.util.HashMap; import java.util.HashSet; import java.util.List; -import java.util.Map; import java.util.Set; import exceptions.SubstituteFailedException; import lombok.Getter; -import models.algebra.Variable; import models.formulas.Formula; -import models.formulas.meta.MetaEquationFormula; import models.formulas.meta.MetaFormula; import models.terms.RDLTerm; import models.terms.meta.MatchConstraint; @@ -22,213 +17,191 @@ public class InferenceRule { @Getter - private final String name; + protected String name; @Getter - private final List assumptions; + protected List assumptions = new ArrayList<>(); @Getter - private final MetaFormula conclusion; - protected final InferenceOrderConstraint defaultOrderConstraint; + protected MetaFormula conclusion; + protected InferenceOrderConstraint defaultOrderConstraint; - private final boolean hasDynamicAssumption; - private final AssumptionGenerator generator; + protected List missingVariables = new ArrayList<>(); + protected InferenceRule(String name) { + this.name = name; + } public InferenceRule(String name, List assumptions, MetaFormula conclusion, InferenceOrderConstraint constraint) { this.name = name; this.assumptions = assumptions; this.conclusion = conclusion; this.defaultOrderConstraint = constraint; - this.hasDynamicAssumption = false; - this.generator = null; - } - - public InferenceRule(String name, List assumptions, AssumptionGenerator generator, MetaFormula conclusion, InferenceOrderConstraint constraint) { - this.name = name; - this.assumptions = assumptions; - this.conclusion = conclusion; - this.defaultOrderConstraint = constraint; - this.hasDynamicAssumption = true; - this.generator = generator; - } - - public InferenceRule( List assumptions, MetaFormula conclusion, InferenceOrderConstraint constraint) { - this("undefined", assumptions, conclusion, constraint); + Set missingVariables = conclusion.getAllVariables(); + for (MetaFormula assumption: assumptions) { + missingVariables.removeAll(assumption.getAllVariables()); + } + this.missingVariables = new ArrayList<>(missingVariables); } public InferenceRule(String name, List assumptions, MetaFormula conclusion) { this(name, assumptions, conclusion, null); } - public InferenceRule(String name, List assumptions, AssumptionGenerator generator, MetaFormula conclusion) { - this(name, assumptions, generator, conclusion, null); + public Set derive(List assumptions) { + return derive(assumptions, Set.of()); } - public InferenceRule(List assumptions, MetaFormula conclusion) { - this("undefined", assumptions, conclusion, null); - } - - public boolean check(Collection assumptions, Formula conclusion) { - - if (this.assumptions.size() > assumptions.size()) { - return false; - } - - for(List assumption : Permutation.permutation(assumptions, this.assumptions.size())) { - if (check(assumption, conclusion)) { - return true; - } - } - return false; - } - - private boolean check(List assumptions, Formula conclusion) { - Set matchResult = this.assumptions.get(0).isMatchedBy(assumptions.get(0)); - for (int i = 1; i < assumptions.size(); i++) { - matchResult = this.assumptions.get(i).isMatchedBy(assumptions.get(i), matchResult); - if (matchResult.isEmpty()) { - return false; - } - } - - if (this.conclusion.isMatchedBy(conclusion, matchResult).isEmpty()) { - return false; - } - if (this.defaultOrderConstraint != null) { - for (MatchConstraint constraint: matchResult) { - if (defaultOrderConstraint.check(constraint.getOrderConstraint())) { - return true; + public Set derive(List assumptions, Set existTerms) { + if (missingVariables.size() == 0) { + return derive(assumptions, MatchConstraint.createDefault()); + } else { + Set result = new HashSet<>(); + for (List terms: Permutation.permutation(existTerms, missingVariables.size())) { + for (MatchConstraint constraint: missingVariableFill(terms)) { + if (defaultOrderConstraint != null && (! defaultOrderConstraint.check(constraint.getOrderConstraint()))) continue; + result.addAll(derive(assumptions, constraint)); } } - return false; + return result; } - return true; } - - public Set apply(List assumptions, Set existTerms) { + public Set derive(List assumptions, MatchConstraint constraint) { Set result = new HashSet<>(); - Set assumptionVariables = new HashSet<>(); - Set conclusionVariables = new HashSet<>(); - for (MetaFormula assumption: this.assumptions) { - assumptionVariables.addAll(assumption.getSubTerms(MetaVariable.class)); + if (this.assumptions.size() != assumptions.size()) { + return new HashSet<>(); } - conclusionVariables.addAll(conclusion.getSubTerms(MetaVariable.class)); + Set matchResult = assumptionMatch(assumptions, constraint); - conclusionVariables.removeAll(assumptionVariables); - List leftVariables = new ArrayList<>(conclusionVariables); - - if (! conclusionVariables.isEmpty()) { - for (List variables: Permutation.permutation(existTerms, leftVariables.size())) { - Map binding = new HashMap<>(); - for (int i = 0; i < variables.size(); i++) { - binding.put(leftVariables.get(i).getVariableName(), variables.get(i)); - } - try { - Formula res = apply(assumptions, new MatchConstraint(binding, new HashMap<>())); - if (res != null) { - // ??? - Set constraints = conclusion.isMatchedBy(res); - boolean flg = true; - for (MatchConstraint constraint : constraints) { - if (defaultOrderConstraint != null && ! defaultOrderConstraint.check(constraint.getOrderConstraint())) { - flg = false; - break; - } - } - if (flg) { - result.add(res); - } - } - } catch (SubstituteFailedException e) { - continue; - } - } - } - return result; - } - - public Formula apply(Formula ...assumptions) { - return apply(Set.of(assumptions)); - } - - public Formula apply(Collection assumptions) { - if (assumptions.size() < getAssumptionSize()) { - return null; - } - for (List assumptionList : Permutation.permutation(assumptions, assumptions.size())) { - Formula result = apply(assumptionList); - if (result != null) { - return result; - } - } - return null; - } - - protected Formula apply(List assumptions) { - return apply(assumptions, MatchConstraint.createDefault()); - } - - protected Formula apply(List assumptions, MatchConstraint constraint) { - if (assumptions.size() < getAssumptionSize()) { - return null; - } - - Set result = new HashSet<>(); - result.add(constraint); - for (int i = 0; i < getAssumptionSize(); i++) { - result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result); - if (result.isEmpty()) { - return null; - } - } - if (hasDynamicAssumption) { - for (int i = 0; i < assumptions.size() - getAssumptionSize(); i++) { - int j = getAssumptionSize() + i; - result = this.generator.generate(i).isMatchedBy(assumptions.get(j), result); - if (result.isEmpty()) { - return null; - } - } - } - Formula subRes = null; - for (MatchConstraint con: result) { + for (MatchConstraint res: matchResult) { try { - subRes = conclusion.substitution(con.getBinding()); + result.add(this.conclusion.substitution(res.getBinding(), res.getContext())); } catch (SubstituteFailedException e) { continue; } } - return subRes; + return result; } + protected Set missingVariableFill(List terms) { + Set constraints = new HashSet<>(); + constraints.add(MatchConstraint.createDefault()); + for (int i = 0; i < missingVariables.size(); i++) { + constraints = missingVariables.get(i).isMatchedBy(terms.get(i), constraints); + if (constraints.isEmpty()) return new HashSet<>(); + } + return constraints; + } - public RDLTerm generateRightSideHand(List assumptions, RDLTerm leftSideHand) { - if (! (this.conclusion instanceof MetaEquationFormula)) return null; - if (this.assumptions.size() > assumptions.size()) return null; - MetaEquationFormula metaFormula = (MetaEquationFormula) this.conclusion; - Set constraints = metaFormula.getLeftSideHand().isMatchedBy(leftSideHand); - for (List assumptionList: Permutation.permutation(assumptions, assumptions.size())) { - for (int i = 0; i < getAssumptionSize(); i++) { - constraints = this.assumptions.get(i).isMatchedBy(assumptionList.get(i), constraints); - } - if (hasDynamicAssumption) { - for (int i = 0; i < assumptions.size() - getAssumptionSize(); i++) { - int j = getAssumptionSize() + i; - constraints = this.generator.generate(i).isMatchedBy(assumptions.get(j), constraints); - } - } - for (MatchConstraint constraint: constraints) { - try { - return metaFormula.getRightSideHand().substitute(constraint.getBinding()); - } catch (SubstituteFailedException e) { - continue; - } + protected Set assumptionMatch(Listassumptions, MatchConstraint constraint) { + Set matchResult = new HashSet<>(); + matchResult.add(constraint); + for (int i = 0; i < assumptions.size(); i++) { + Formula assumption = assumptions.get(i); + MetaFormula metaAssumption = this.assumptions.get(i); + matchResult = metaAssumption.isMatchedBy(assumption, matchResult); + if (matchResult.isEmpty()) { + return new HashSet<>(); } } - return null; + return matchResult; } + public List getMissingVariables(List assumptions, MatchConstraint constraint) { + return this.missingVariables; + } + +// public Set apply(Set formulas, Set existTerms) { +// List> matchFormulas = new ArrayList<>(); +// List> matchTerms = new ArrayList<>(); +// Set result = new HashSet<>(); +// for (int i = 0; i < assumptions.size(); i++) { +// matchFormulas.add(new ArrayList<>()); +// for (Formula formula: formulas) { +// if (! assumptions.get(i).isMatchedBy(formula).isEmpty()) { +// matchFormulas.get(i).add(formula); +// } +// } +// if (matchFormulas.get(i).isEmpty()) { +// return new HashSet<>(); +// } +// } +// for (int i = 0; i < missingVariables.size(); i++) { +// matchTerms.add(new ArrayList<>()); +// for (RDLTerm term : existTerms) { +// if (! missingVariables.get(i).isMatchedBy(term).isEmpty()) { +// matchTerms.get(i).add(term); +// } +// } +// if (matchTerms.get(i).isEmpty()) { +// return new HashSet<>(); +// } +// } +// if (matchFormulas.size() == 0) { +// for (List terms : Product.product(matchTerms)) { +// MatchConstraint constraint = MatchConstraint.createDefault(); +// for (int i = 0; i < terms.size(); i++) { +// MetaVariable variable = missingVariables.get(i); +// RDLTerm term = terms.get(i); +// constraint.setBinding(variable.getVariableName(), term); +// Formula conclusion = this.conclusion.substitution(constraint.getBinding(), constraint.getContext()); +// if (conclusionCheck(conclusion, constraint, formulas)) { +// result.add(conclusion); +// } +// } +// } +// } +// for (List assumptions: Product.product(matchFormulas)) { +// Set matchResult = matchCheck(assumptions); +// if (matchResult.isEmpty()) { +// continue; +// } +// for (MatchConstraint constraint: matchResult) { +// if (missingVariables.size() == 0) { +// try { +// Formula conclusion = this.conclusion.substitution(constraint.getBinding(), constraint.getContext()); +// if (conclusionCheck(conclusion, constraint, formulas)) { +// result.add(conclusion); +// } +// } catch (SubstituteFailedException e) { +// continue; +// } +// } +// for (List terms : Product.product(matchTerms)) { +// for (int i = 0; i < terms.size(); i++) { +// MetaVariable variable = missingVariables.get(i); +// RDLTerm term = terms.get(i); +// constraint.setBinding(variable.getVariableName(), term); +// try { +// Formula conclusion = this.conclusion.substitution(constraint.getBinding(), constraint.getContext()); +// if (conclusionCheck(conclusion, constraint, formulas)) { +// result.add(conclusion); +// } +// } catch (SubstituteFailedException e) { +// continue; +// } +// +// } +// } +// } +// } +// return result; +// } +// +// protected Set matchCheck(List assumptions) { +// Set matchResult = new HashSet<>(); +// matchResult.add(MatchConstraint.createDefault()); +// for (int i = 0; i < assumptions.size(); i++) { +// Formula assumption = assumptions.get(i); +// MetaFormula metaAssumption = this.assumptions.get(i); +// matchResult = metaAssumption.isMatchedBy(assumption, matchResult); +// if (matchResult.isEmpty()) { +// return new HashSet<>(); +// } +// } +// return matchResult; +// } + public int getAssumptionSize() { return this.assumptions.size(); } diff --git a/src/main/java/inference/ProofState.java b/src/main/java/inference/ProofState.java new file mode 100644 index 0000000..f52ac1b --- /dev/null +++ b/src/main/java/inference/ProofState.java @@ -0,0 +1,208 @@ +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 exceptions.MissingContextException; +import lombok.Getter; +import models.formulas.DependencyFormula; +import models.formulas.EquationFormula; +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; + +@Getter +public class ProofState { + + private Set dependencies = new HashSet<>(); + private Set evaluatableTerms = new HashSet<>(); + private Set formulas = new HashSet<>(); + private Set dependencyFormulas = new HashSet<>(); + private Set equationFormulas = new HashSet<>(); + private Map>> matchedFormulas = new HashMap<>(); + private Map matchedTerms = new HashMap<>(); + private InferenceHistory history = new InferenceHistory(); + + 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) { + this.dependencyFormulas.add(df); + this.dependencies.add(df.getDependency()); + this.evaluatableTerms.addAll(df.getDependency().getSubTerms(EvaluatableTerm.class).values()); + } else if (formula instanceof EquationFormula eq) { + this.equationFormulas.add(eq); + 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++) { + terms.add(new HashSet<>()); + for (DependencyFormula dep : dependencyFormulas) { + if (! rule.getAssumptions().get(i).isMatchedBy(dep).isEmpty()) { + terms.get(i).add(dep); + } + } + for (EquationFormula eq : equationFormulas) { + if (! rule.getAssumptions().get(i).isMatchedBy(eq).isEmpty()) { + terms.get(i).add(eq); + } + } + } + matchedFormulas.put(rule, terms); + } + for (EquationAxiom rule: ProofSystem.equationAxioms) { + List> formulas = new ArrayList<>(); + 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) { + try { + if (! conclusionLeft.isMatchedBy(term).isEmpty()) { + lhs.add(term); + } + } catch (RuntimeException e) {} + try { + if (! conclusionRight.isMatchedBy(term).isEmpty()) { + rhs.add(term); + } + } catch(RuntimeException e) {} + } + matchedTerms.put(rule, new ConclusionMatchedTerm(lhs, rhs)); + for (int i = 0; i < rule.getAssumptionSize(); i++) { + formulas.add(new HashSet<>()); + for (DependencyFormula dep : dependencyFormulas) { + if (! rule.getAssumptions().get(i).isMatchedBy(dep).isEmpty()) { + formulas.get(i).add(dep); + } + } + for (EquationFormula eq : equationFormulas) { + if (! rule.getAssumptions().get(i).isMatchedBy(eq).isEmpty()) { + formulas.get(i).add(eq); + } + } + } + matchedFormulas.put(rule, formulas); + } + } + + public void addFormuals(Set existFormulas) { + for (Formula formula: existFormulas) { + formulas.add(formula); + if (formula instanceof DependencyFormula df) { + this.dependencyFormulas.add(df); + this.dependencies.add(df.getDependency()); + this.evaluatableTerms.addAll(df.getDependency().getSubTerms(EvaluatableTerm.class).values()); + } else if (formula instanceof EquationFormula eq) { + this.equationFormulas.add(eq); + 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) { + List> terms = new ArrayList<>(); + for (int i = 0; i < rule.getAssumptionSize(); i++) { + terms.add(new HashSet<>()); + for (DependencyFormula dep : dependencyFormulas) { + if (! rule.getAssumptions().get(i).isMatchedBy(dep).isEmpty()) { + terms.get(i).add(dep); + } + } + for (EquationFormula eq : equationFormulas) { + if (! rule.getAssumptions().get(i).isMatchedBy(eq).isEmpty()) { + terms.get(i).add(eq); + } + } + } + matchedFormulas.put(rule, terms); + } + for (EquationAxiom rule: ProofSystem.equationAxioms) { + List> formulas = new ArrayList<>(); + 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) { + try { + if (! conclusionLeft.isMatchedBy(term).isEmpty()) { + lhs.add(term); + } + } catch (MissingContextException e) {} + try { + if (! conclusionRight.isMatchedBy(term).isEmpty()) { + rhs.add(term); + } + } catch (MissingContextException e) {} + } + matchedTerms.put(rule, new ConclusionMatchedTerm(lhs, rhs)); + for (int i = 0; i < rule.getAssumptionSize(); i++) { + formulas.add(new HashSet<>()); + for (DependencyFormula dep : dependencyFormulas) { + if (! rule.getAssumptions().get(i).isMatchedBy(dep).isEmpty()) { + formulas.get(i).add(dep); + } + } + for (EquationFormula eq : equationFormulas) { + if (! rule.getAssumptions().get(i).isMatchedBy(eq).isEmpty()) { + formulas.get(i).add(eq); + } + } + } + matchedFormulas.put(rule, formulas); + } + } + + public void addHistory(List assumptions, InferenceRule usedAxiom, Formula conclusion) { + if (formulaExist(conclusion)) return; + InferenceHistoryNode node = new InferenceHistoryNode(assumptions, usedAxiom, conclusion); + this.history.addHistory(conclusion, node); + } + + public Set getExistTerms() { + Set result = new HashSet<>(); + result.addAll(dependencies); + result.addAll(evaluatableTerms); + return result; + } + + public boolean formulaExist(Formula formula) { + if (formula instanceof EquationFormula eq) { + return this.equationFormulas.contains(eq); + } else if (formula instanceof DependencyFormula df) { + return this.dependencyFormulas.contains(df); + } + return false; + } + + record ConclusionMatchedTerm(Set leftSideHands, Set rightSideHands) {}; + +} diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index 26eaad3..0cfd112 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -1,32 +1,49 @@ package inference; -import java.util.ArrayDeque; import java.util.ArrayList; -import java.util.Collection; -import java.util.Deque; import java.util.HashMap; import java.util.HashSet; import java.util.List; import java.util.Map; -import java.util.Queue; import java.util.Set; -import java.util.stream.Collectors; +import inference.axioms.ArgumentConstraint; +import inference.axioms.ArgumentExtension; +import inference.axioms.ArgumentReduction; +import inference.axioms.CompositeMapping; +import inference.axioms.ConstantMapping; +import inference.axioms.Constantness; +import inference.axioms.DependencyExtension; +import inference.axioms.Identity; +import inference.axioms.LeftSubstitution; +import inference.axioms.MapComposition; +import inference.axioms.PseudoConstantness; +import inference.axioms.RightSubstitution; +import inference.axioms.UncurriedMapping; +import inference.axioms.Uncurrying; +import lombok.Getter; import models.algebra.Variable; import models.formulas.DependencyFormula; import models.formulas.EquationFormula; import models.formulas.Formula; +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 { //======================Equality Axioms============================= - public static final InferenceRule reflexivity = new InferenceRule( + public static final EquationAxiom reflexivity = new EquationAxiom( "Reflexivity", List.of(), new MetaEquationFormula( @@ -35,7 +52,7 @@ ) ); - public static final InferenceRule symmetry = new InferenceRule( + public static final EquationAxiom symmetry = new EquationAxiom( "Symmetry", List.of( new MetaEquationFormula( @@ -49,7 +66,7 @@ ) ); - public static final InferenceRule transitivity = new InferenceRule( + public static final EquationAxiom transitivity = new EquationAxiom( "Transitivity", List.of( new MetaEquationFormula( @@ -68,219 +85,328 @@ ); + public static final EquationAxiom rightSubstitution = new RightSubstitution(); + + + + public static final EquationAxiom leftSubstitution = new LeftSubstitution(); + + + public static final EquationAxiom identity = new Identity(); + + public static final EquationAxiom mapComposition = new MapComposition(); +// + public static final EquationAxiom constantness = new Constantness(); +// +// public static final InferenceRule rightNormalization = new RightNormalization(); +// + + public static final EquationAxiom pseudoConstantness = new PseudoConstantness(); + + public static final EquationAxiom uncurrying = new Uncurrying(); + + // // //======================Dependency Axioms============================= // - - private static final List axioms = List.of( -// reflexivity, -// symmetry, -// transitivity, -// rightSubstitution, -// leftSubstitution, -// identity, -// mapComposition, -// constantness, -// rightNormalization, -// pseudoConstantness, -// identityMapping, -// compositeMapping, -// constantMapping, -// slicedMapping, -// memberSubstitution, -// membershipChain, -// collectionSubstitution, -// setEquivelence, -// setHomomorphism, -// leftProjection, -// rightProjection, -// domainMembership, -// codomainMembership, -// codomainMembership2 + public static final InferenceRule identityMapping = new InferenceRule( + "Identity Mapping", + List.of( + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("se")) + ) + ), + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("se")) + ) ); - public static void debug() { - for (var axiom : axioms) { - System.out.println(axiom); - System.out.println("=================================================================================================="); - } + public static final InferenceRule argumentExtension = new ArgumentExtension(); + + public static final InferenceRule argumentReduction = new ArgumentReduction(); + + public static final InferenceRule argumentConstraint = new ArgumentConstraint(); + + public static final InferenceRule compositeMapping = new CompositeMapping(); + + public static final InferenceRule constantMapping = new ConstantMapping(); + + public static final InferenceRule constantMapping1 = new InferenceRule( + "Constant Mapping", + List.of(), + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("te"), new Variable("m")) + ), + new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")) + ); + + public static final InferenceRule uncurriedMapping = new UncurriedMapping(); + + public static final InferenceRule dependencyExtension = new DependencyExtension(); + + public static final List axioms = List.of( + reflexivity, + symmetry, + transitivity, + rightSubstitution, + leftSubstitution, + identity, + mapComposition, + constantness, + pseudoConstantness, + uncurrying, + identityMapping, + argumentExtension, + argumentReduction, + compositeMapping, + constantMapping1, + uncurriedMapping, + dependencyExtension + ); + + public static final List equationAxioms = List.of( + reflexivity, + symmetry, + transitivity, + rightSubstitution, + leftSubstitution, + identity, + mapComposition, + constantness, + pseudoConstantness, + uncurrying + ); + + public static final List dependencyAxioms = List.of( + identityMapping, + argumentExtension, + argumentReduction, + compositeMapping, + constantMapping1, + uncurriedMapping, + dependencyExtension + ); + + private Set assumptions; + private Formula conclusion; + @Getter + private ProofState state; + + + public ProofSystem(Set assumptions, Formula conclusion) { + this(assumptions, conclusion, Set.of()); } - record AxiomResult(InferenceRule axiom, List formulas) {} - - public static boolean check(Collection assumptions, Formula conclusion) { - - Map proofGraph = new HashMap<>(); - Map>> appliedFormulas = new HashMap<>(); - - for (InferenceRule axiom : axioms) { - appliedFormulas.put(axiom, new HashSet<>()); - } - - Set appearFormulas = new HashSet<>(assumptions); - Set existTerms = new HashSet<>(); - for (Formula assumption : assumptions) { - addExistTerms(assumption, existTerms); - } - int prevAppearFormulasSize = appearFormulas.size(); - while (! appearFormulas.contains(conclusion)) { - Set derivedFormulas = new HashSet<>(); - for(InferenceRule axiom : axioms) { - derivedFormulas.addAll(applyAxiom(axiom, appearFormulas, appliedFormulas.get(axiom), existTerms, proofGraph)); - } - if (derivedFormulas.size() == 0) { - return false; - } - appearFormulas.addAll(derivedFormulas); - if (appearFormulas.size() == prevAppearFormulasSize) { - return false; - } - prevAppearFormulasSize = appearFormulas.size(); - } - - Queue formulaQueue = new ArrayDeque<>(); - Queue depthQueue = new ArrayDeque<>(); - List formulaResult = new ArrayList<>(); - List depthResult = new ArrayList<>(); - Set used = new HashSet<>(); - Map> usedAxioms = new HashMap<>(); - - formulaQueue.add(conclusion); - depthQueue.add(0); - - System.out.println("proof finish"); - System.out.println(); - - while (formulaQueue.size() != 0) { - Formula currentFormula = formulaQueue.poll(); -// if (used.contains(currentFormula)) { -// continue; -// } - used.add(currentFormula); - int currentDepth = depthQueue.poll(); - formulaResult.add(currentFormula); - depthResult.add(currentDepth); - if (! proofGraph.containsKey(currentFormula)) continue; - for (Formula nextFormula : proofGraph.get(currentFormula).formulas) { -// if (used.contains(nextFormula)) { -// continue; -// } - formulaQueue.add(nextFormula); - depthQueue.add(currentDepth + 1); - if (! usedAxioms.containsKey(currentDepth + 1)) { - usedAxioms.put(currentDepth + 1, new HashSet<>()); - } - usedAxioms.get(currentDepth + 1).add(proofGraph.get(currentFormula).axiom); - } - } - int prevDepth = depthResult.get(depthResult.size() - 1); - Set sameDepthFormulas = new HashSet<>(); - for (int i = formulaResult.size() - 1; i >= 0; i--) { - int currentDepth = depthResult.get(i); - Formula currentFormula = formulaResult.get(i); - if (currentDepth != prevDepth) { - String out = sameDepthFormulas.stream().map(String::valueOf).collect(Collectors.joining(", ")); - String axioms = usedAxioms.get(prevDepth).stream().map(InferenceRule::getName).collect(Collectors.joining(", ")); - System.out.println(out); - System.out.println("==============================================================(" + axioms + ")"); - sameDepthFormulas.clear(); - } - prevDepth = currentDepth; - sameDepthFormulas.add(currentFormula); - - } - String out = sameDepthFormulas.stream().map(String::valueOf).collect(Collectors.joining(",")); - System.out.println(out); - return true; + public ProofSystem(Set assumptions, Formula conclusion, Set existResources) { + state = new ProofState(assumptions); + this.assumptions = assumptions; + this.conclusion = conclusion; + state.getEvaluatableTerms().addAll(existResources); + checkDefinitionFormulaFormat(); } - private static Set applyAxiom(InferenceRule axiom, Set formulas, Set> appliedFormulas, Set existTerms, Map proofGraph) { - Set result = new HashSet<>(); - List> matchedFormulas = new ArrayList<>(); - for (int i = 0; i < axiom.getAssumptionSize(); i++) { - matchedFormulas.add(new ArrayList<>()); - for (Formula formula : formulas) { - if (! axiom.getAssumptions().get(i).isMatchedBy(formula).isEmpty()) { - matchedFormulas.get(i).add(formula); - } + 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."); } - } - for(List applyFormulas : Product.product(matchedFormulas)) { - if (appliedFormulas.contains(applyFormulas)) continue; - Set applied = axiom.apply(applyFormulas, existTerms); - if (applied != null) { - for (Formula formula : applied) { - if (! formulas.contains(formula)) { - addExistTerms(formula, existTerms); - proofGraph.put(formula, new AxiomResult(axiom, applyFormulas)); + 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."); } } - result.addAll(applied); - appliedFormulas.add(applyFormulas); + } + } + } + + 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() { + return state.getHistory().getHistoryString(conclusion); + } + + public boolean dependencyInference() { + return dependencyInference(this.conclusion); + } + + public boolean dependencyInference(Formula conclusion) { + if (conclusion instanceof EquationFormula eq) { + 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))) { + state.addFormuals(dependencyInferenceStep()); + } + return true; + } else if (conclusion instanceof DependencyFormula dep) { + while((! state.getDependencyFormulas().contains(dep))) { + Set result = dependencyInferenceStep(); + Set sizeConstraintOk = new HashSet<>(); + for (DependencyFormula df: result) { + if (dep.getDependency().getSize() >= df.getDependency().getSize()) { + if (! state.getFormulas().contains(df)) { + sizeConstraintOk.add(df); + } + } + } + if (sizeConstraintOk.size() == 0) { + return false; + } + state.addFormuals(sizeConstraintOk); + } + return true; + } + return false; + } + + public Set dependencyInferenceStep() { + Set result = new HashSet<>(); + for (InferenceRule rule: dependencyAxioms) { + List> matchedFormulas = new ArrayList<>(); + for (Set formulas: state.getMatchedFormulas().get(rule)) { + matchedFormulas.add(new ArrayList<>(formulas)); + } + if (rule.getAssumptions().size() == 0) { + result.addAll(dependencyDerive(List.of(), rule)); + } else { + for (List formulas: Product.product(matchedFormulas)) { + result.addAll(dependencyDerive(formulas, rule)); + } } } return result; } - private static void addExistTerms(Formula formula, Set existTerms) { - if (formula instanceof EquationFormula) { - RDLTerm leftSideHand = ((EquationFormula) formula).getLeftSideHand(); - RDLTerm rightSideHand = ((EquationFormula) formula).getRightSideHand(); - existTerms.addAll(leftSideHand.getSubTerms(RDLTerm.class).values()); - existTerms.addAll(rightSideHand.getSubTerms(RDLTerm.class).values()); - } else if (formula instanceof DependencyFormula) { - RDLTerm dependency = ((DependencyFormula) formula).getDependency(); - existTerms.addAll(dependency.getSubTerms(RDLTerm.class).values()); - } + private Set dependencyDerive(List assumptions, InferenceRule rule) { + Set result = new HashSet<>(); + for (Formula res: rule.derive(assumptions, state.getExistTerms())) { + if (state.formulaExist(res)) continue; + state.addHistory(assumptions, rule, res); + if (res instanceof DependencyFormula df) { + result.add(df); + } + } + return result; } - private static boolean equationTransitionCheck(Collection assumptions, Formula conclusion) { - if (! (conclusion instanceof EquationFormula)) { - return false; - } - EquationFormula equationConclusion = (EquationFormula) conclusion; - Map> graph = constructEquationGraph(assumptions); - Deque que = new ArrayDeque<>(); - Set visited = new HashSet<>(); - que.add(equationConclusion.getLeftSideHand()); - while (! que.isEmpty()) { - EvaluatableTerm curNode = que.pollFirst(); - if (curNode.equals(equationConclusion.getRightSideHand())) { - return true; + public Set equationInferenceStep() { + Set result = new HashSet<>(); + for (EquationAxiom rule: equationAxioms) { + List> matchedFormulas = new ArrayList<>(); + for (Set formulas: state.getMatchedFormulas().get(rule)) { + matchedFormulas.add(new ArrayList<>(formulas)); } - for (EvaluatableTerm nextNode : graph.getOrDefault(curNode, new ArrayList<>())) { - if (visited.contains(nextNode)) { - continue; + for (EvaluatableTerm left: state.getMatchedTerms().get(rule).leftSideHands()) { + for (List formulas: Product.product(matchedFormulas)) { + for (EvaluatableTerm right: rule.apply(formulas, left)) { + result.add(new EquationFormula(left, right)); + state.addHistory(formulas, rule, new EquationFormula(left, right)); + } } - visited.add(nextNode); - que.add(nextNode); + } + for (EvaluatableTerm right: state.getMatchedTerms().get(rule).rightSideHands()) { + for (List formulas: Product.product(matchedFormulas)) { + for (EvaluatableTerm left: rule.apply(formulas, right)) { + result.add(new EquationFormula(left, right)); + state.addHistory(formulas, rule, new EquationFormula(left, right)); + } + } } } - return false; + return result; } - private static Map> constructEquationGraph(Collection assumptions) { - List equations = new ArrayList<>(); - for (Formula assumption : assumptions) { - if (assumption instanceof EquationFormula) { - equations.add((EquationFormula) assumption); - } - } - - Map> graph = new HashMap<>(); - for (EquationFormula equation : equations) { - EvaluatableTerm lsh = equation.getLeftSideHand(); - EvaluatableTerm rsh = equation.getRightSideHand(); - if (! graph.containsKey(lsh)) { - graph.put(lsh, new ArrayList<>()); - } - if (! graph.containsKey(rsh)) { - graph.put(rsh, new ArrayList<>()); - } - graph.get(lsh).add(rsh); - graph.get(rsh).add(lsh); - } - return graph; + 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/ArgumentConstraint.java b/src/main/java/inference/axioms/ArgumentConstraint.java new file mode 100644 index 0000000..46ccd6e --- /dev/null +++ b/src/main/java/inference/axioms/ArgumentConstraint.java @@ -0,0 +1,97 @@ +package inference.axioms; + +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import exceptions.SubstituteFailedException; +import inference.InferenceRule; +import models.Position; +import models.algebra.Variable; +import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.formulas.meta.MetaEquationFormula; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaConstant; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaDynamicDependencyTerm; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; + +public class ArgumentConstraint extends InferenceRule { + + public ArgumentConstraint() { + super("Argument Constraint"); + + assumptions.add(new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 3; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("xe" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("ye")) + ), + new MetaConstant(new Variable("c")) + )); + + assumptions.add(new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex)); + } + }, + new MetaEvaluatableTermVariable(new Variable("te")) + ) + )); + + conclusion = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("xe" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("te")) + ), + new MetaEvaluatableTermVariable(new Variable("ye")) + ); + } + + @Override + public Set derive(List assumptions, MatchConstraint constraint) { + Set result = new HashSet<>(); + if (this.assumptions.size() != assumptions.size()) { + return new HashSet<>(); + } + Set matchResult = assumptionMatch(assumptions, constraint); + + for (MatchConstraint res: matchResult) { + try { + res.getContext().put(new Position(), (Integer) res.getContext().get(new Position()) * 2 - 1); + result.add(this.conclusion.substitution(res.getBinding(), res.getContext())); + } catch (SubstituteFailedException e) { + continue; + } + } + return result; + } + +} diff --git a/src/main/java/inference/axioms/ArgumentExtension.java b/src/main/java/inference/axioms/ArgumentExtension.java new file mode 100644 index 0000000..9a89d16 --- /dev/null +++ b/src/main/java/inference/axioms/ArgumentExtension.java @@ -0,0 +1,72 @@ +package inference.axioms; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import exceptions.SubstituteFailedException; +import inference.DependencyAxiom; +import models.Position; +import models.algebra.Variable; +import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaRDLTermVariable; +import models.terms.meta.MetaTermGenerator; + +public class ArgumentExtension extends DependencyAxiom { + + public ArgumentExtension() { + super("Argument Extension"); + assumptions.add(new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + return new MetaEvaluatableTermVariable(new Variable("te" + curIndex)); + } + }, + new MetaRDLTermVariable(new Variable("se")) + ) + )); + + conclusion = new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 2; + return new MetaEvaluatableTermVariable(new Variable("te" + curIndex)); + } + }, + new MetaRDLTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ) + ); + this.missingVariables.add(new MetaEvaluatableTermVariable(new Variable("ue"))); + } + + + public Set derive(List assumptions, MatchConstraint constraint) { + Set result = new HashSet<>(); + if (this.assumptions.size() != assumptions.size()) { + return new HashSet<>(); + } + Set matchResult = assumptionMatch(assumptions, constraint); + + for (MatchConstraint res: matchResult) { + try { + res.getContext().put(new Position(), (Integer) res.getContext().get(new Position()) + 1); + result.add(this.conclusion.substitution(res.getBinding(), res.getContext())); + } catch (SubstituteFailedException e) { + continue; + } + } + return result; + } + +} diff --git a/src/main/java/inference/axioms/ArgumentReduction.java b/src/main/java/inference/axioms/ArgumentReduction.java new file mode 100644 index 0000000..f19260c --- /dev/null +++ b/src/main/java/inference/axioms/ArgumentReduction.java @@ -0,0 +1,98 @@ +package inference.axioms; + +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import exceptions.SubstituteFailedException; +import inference.DependencyAxiom; +import models.Position; +import models.algebra.Variable; +import models.formulas.DependencyFormula; +import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaRDLTermVariable; +import models.terms.meta.MetaTermGenerator; + +public class ArgumentReduction extends DependencyAxiom { + + public ArgumentReduction() { + super("Argument Reduction"); + + assumptions.add(new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + context.put("k", curIndex); + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex)); + } + }, + new MetaEvaluatableTermVariable(new Variable("te")) + ) + )); + + assumptions.add(new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 2; + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex)); + } + }, + new MetaRDLTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + )); + + conclusion = new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex)); + } + }, + new MetaRDLTermVariable(new Variable("se")) + ) + ); + + this.targetAssumptionIndex = 1; + + } + + + public Set derive(List assumptions, MatchConstraint constraint) { + Set result = new HashSet<>(); + if (this.assumptions.size() != assumptions.size()) { + return new HashSet<>(); + } + if (assumptions.get(0) instanceof DependencyFormula dep1 && assumptions.get(1) instanceof DependencyFormula dep2) { + if (dep1.getDependency().getMaxIndex() >= dep2.getDependency().getMaxIndex()) { + return new HashSet<>(); + } + } else { + return new HashSet<>(); + } + Set matchResult = assumptionMatch(assumptions, constraint); + + for (MatchConstraint res: matchResult) { + try { + res.getContext().put(new Position(), (Integer) res.getContext().get(new Position()) - 1); + result.add(this.conclusion.substitution(res.getBinding(), res.getContext())); + } catch (SubstituteFailedException e) { + continue; + } + } + return result; + } + +} diff --git a/src/main/java/inference/axioms/CompositeMapping.java b/src/main/java/inference/axioms/CompositeMapping.java new file mode 100644 index 0000000..9d62770 --- /dev/null +++ b/src/main/java/inference/axioms/CompositeMapping.java @@ -0,0 +1,102 @@ +package inference.axioms; + +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import exceptions.SubstituteFailedException; +import inference.DependencyAxiom; +import models.Position; +import models.algebra.Variable; +import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaRDLTermVariable; +import models.terms.meta.MetaTermGenerator; + +public class CompositeMapping extends DependencyAxiom { + + public CompositeMapping() { + super("Composite Mapping"); + + assumptions.add( + new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + context.put("k", curIndex + 1); + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex)); + } + }, + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ) + ); + + assumptions.add( + new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 2; + context.put("n", curIndex + 1); + return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex)); + } + }, + new MetaRDLTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ) + ); + + conclusion = new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + int k = (Integer) context.get("k"); + if (curIndex < k) { + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex)); + } + curIndex -= k; + return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex)); + } + }, + new MetaRDLTermVariable(new Variable("se")) + ) + ); + + this.targetAssumptionIndex = 1; + } + + @Override + public Set derive(List assumptions, MatchConstraint constraint) { + Set result = new HashSet<>(); + if (this.assumptions.size() != assumptions.size()) { + return new HashSet<>(); + } + + Set matchResult = assumptionMatch(assumptions, constraint); + + for (MatchConstraint res: matchResult) { + try { + int k = (Integer) res.getContext().get("k"); + int n = (Integer) res.getContext().getOrDefault("n", 0); + res.getContext().put(new Position(), k + n + 1); + result.add(this.conclusion.substitution(res.getBinding(), res.getContext())); + } catch (SubstituteFailedException e) { + continue; + } + } + return result; + } + +} diff --git a/src/main/java/inference/axioms/ConstantMapping.java b/src/main/java/inference/axioms/ConstantMapping.java new file mode 100644 index 0000000..ec6aa6f --- /dev/null +++ b/src/main/java/inference/axioms/ConstantMapping.java @@ -0,0 +1,35 @@ +package inference.axioms; + +import java.util.Map; + +import inference.InferenceOrderConstraint; +import inference.InferenceRule; +import models.algebra.Variable; +import models.formulas.meta.MetaDependencyFormula; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaRDLTermVariable; +import models.terms.meta.MetaTermGenerator; +import models.terms.meta.OrderConstraint; + +public class ConstantMapping extends InferenceRule { + + public ConstantMapping() { + super("Constant Mapping"); + defaultOrderConstraint = new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")); + conclusion = new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + return new MetaEvaluatableTermVariable(new Variable("te" + curIndex), new Variable("m")); + } + }, + new MetaRDLTermVariable(new Variable("se"), new Variable("n")) + ) + ); + } + +} diff --git a/src/main/java/inference/axioms/Constantness.java b/src/main/java/inference/axioms/Constantness.java new file mode 100644 index 0000000..e7c0724 --- /dev/null +++ b/src/main/java/inference/axioms/Constantness.java @@ -0,0 +1,44 @@ +package inference.axioms; + +import java.util.Map; + +import inference.EquationAxiom; +import inference.InferenceOrderConstraint; +import models.algebra.Variable; +import models.formulas.meta.MetaEquationFormula; +import models.terms.meta.MetaDynamicDependencyTerm; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; +import models.terms.meta.OrderConstraint; +import utils.ExpressionUtils; + +public class Constantness extends EquationAxiom{ + + public Constantness() { + super("Constantness"); + defaultOrderConstraint = new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")); + + conclusion = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + 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"), new Variable("n")); + } else if (curIndex == 0) { + return new MetaDynamicDependencyTerm(this); + } + curIndex -= 1; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("m-" + (maxDepth - curDepth))); + } + return new MetaEvaluatableTermVariable(new Variable("ue" + curDepth + "_" + curIndex / 2)); + } + } + ), + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) + ); + } + +} diff --git a/src/main/java/inference/axioms/DependencyExtension.java b/src/main/java/inference/axioms/DependencyExtension.java new file mode 100644 index 0000000..cf63345 --- /dev/null +++ b/src/main/java/inference/axioms/DependencyExtension.java @@ -0,0 +1,81 @@ +package inference.axioms; + +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import exceptions.SubstituteFailedException; +import inference.InferenceRule; +import models.Position; +import models.algebra.Variable; +import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDependency; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; +import utils.ExpressionUtils; + +public class DependencyExtension extends InferenceRule { + + public DependencyExtension() { + super("Dependency Extension"); + + assumptions.add(new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + return new MetaEvaluatableTermVariable(new Variable("te" + curIndex), new Variable("n")); + } + }, + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) + ) + )); + + conclusion = new MetaDependencyFormula( + new MetaDependency( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + return new MetaEvaluatableTermVariable(new Variable("te" + curIndex), new Variable("n")); + } + }, + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) + ), + new MetaEvaluatableTermVariable(new Variable("ue"), ExpressionUtils.parse("n-1")) + ) + ); + missingVariables.add(new MetaEvaluatableTermVariable(new Variable("ue"))); + } + + @Override + public Set derive(List assumptions, MatchConstraint constraint) { + Set result = new HashSet<>(); + if (this.assumptions.size() != assumptions.size()) { + return new HashSet<>(); + } + Set matchResult = assumptionMatch(assumptions, constraint); + + for (MatchConstraint res: matchResult) { + try { + res.getContext().put(new Position(List.of(0, 0)), (Integer) res.getContext().get(new Position())); + if (res.getContext().containsKey("j")) { + res.getContext().put(new Position(), (Integer) res.getContext().get("j") + 1); + } + res.getContext().put("maxDepth", 2); + result.add(this.conclusion.substitution(res.getBinding(), res.getContext())); + } catch (SubstituteFailedException e) { + continue; + } + } + return result; + } + +} diff --git a/src/main/java/inference/axioms/Identity.java b/src/main/java/inference/axioms/Identity.java new file mode 100644 index 0000000..0b72c61 --- /dev/null +++ b/src/main/java/inference/axioms/Identity.java @@ -0,0 +1,76 @@ +package inference.axioms; + +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import exceptions.SubstituteFailedException; +import inference.EquationAxiom; +import models.algebra.Variable; +import models.formulas.Formula; +import models.formulas.meta.MetaEquationFormula; +import models.terms.EvaluatableTerm; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDynamicDependencyTerm; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; + +public class Identity extends EquationAxiom{ + + public Identity() { + super("Identity"); + this.conclusion = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 2; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + ), + new MetaEvaluatableTermVariable(new Variable("te")) + ); + } + + @Override + public Set apply(Listassumptions, EvaluatableTerm term, MatchConstraint constraint) { + Set result = new HashSet<>(); + boolean isLeft = true; + if (assumptions.size() < this.assumptions.size()) { + return new HashSet<>(); + } + Set matchResult = assumptionMatch(assumptions, constraint); + + Set conclusionMatchResult = conclusionLeftSideHandMatch(term, matchResult); + if (conclusionMatchResult.isEmpty()) { + isLeft = false; + conclusionMatchResult = conclusionRightSideHandMatch(term, matchResult); + if (conclusionMatchResult.isEmpty()) { + return new HashSet<>(); + } + } + MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion; + for (MatchConstraint matchRes: conclusionMatchResult) { + try { + if (isLeft) { + result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getRightHandSide()).substitute(matchRes.getBinding(), matchRes.getContext())); + } else { + result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getLeftHandSide()).substitute(matchRes.getBinding(), matchRes.getContext())); + } + } catch (SubstituteFailedException e) { + continue; + } + } + return result; + } + +} diff --git a/src/main/java/inference/axioms/LeftSubstitution.java b/src/main/java/inference/axioms/LeftSubstitution.java new file mode 100644 index 0000000..131a1bf --- /dev/null +++ b/src/main/java/inference/axioms/LeftSubstitution.java @@ -0,0 +1,64 @@ +package inference.axioms; + +import java.util.List; +import java.util.Map; +import java.util.Set; + +import inference.EquationAxiom; +import models.algebra.Variable; +import models.formulas.Formula; +import models.formulas.meta.MetaEquationFormula; +import models.terms.EvaluatableTerm; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDynamicDependencyTerm; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; + +public class LeftSubstitution extends EquationAxiom { + + public LeftSubstitution() { + super("Left Substitution"); + assumptions.add(new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + )); + conclusion = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")) + ), + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ); + } + + @Override + public Set apply(Listassumptions, EvaluatableTerm term) { + MatchConstraint constraint = MatchConstraint.createDefault(); + constraint.getContext().put("maxIndex", term.getMaxIndex()); + constraint.getContext().put("maxDepth", term.getMaxDepth()); + return apply(assumptions, term, constraint); + } + +} diff --git a/src/main/java/inference/axioms/MapComposition.java b/src/main/java/inference/axioms/MapComposition.java new file mode 100644 index 0000000..e279a92 --- /dev/null +++ b/src/main/java/inference/axioms/MapComposition.java @@ -0,0 +1,180 @@ +package inference.axioms; + +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import exceptions.MissingContextException; +import exceptions.SubstituteFailedException; +import inference.EquationAxiom; +import models.Position; +import models.algebra.Variable; +import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.formulas.meta.MetaEquationFormula; +import models.terms.EvaluatableTerm; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaDynamicDependencyTerm; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; + +public class MapComposition extends EquationAxiom { + + public MapComposition() { + super("Map Composition"); + assumptions.add(new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 2; + context.put("tIndex", curIndex + 1); + return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + )); + + assumptions.add(new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + context.put("uIndex", curIndex + 1); + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex)); + } + }, + new MetaEvaluatableTermVariable(new Variable("te")) + ) + )); + + conclusion = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 3; + int tIndex = (Integer) context.getOrDefault("tIndex", 0); + if (curIndex >= tIndex * 2) { + return null; + } + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("v" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + if (! context.containsKey("uIndex")) { + throw new MissingContextException(); + } + int uIndex = (Integer) context.get("uIndex"); + if (curIndex >= uIndex * 2) { + return null; + } + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("u" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ), + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + if (! context.containsKey("uIndex")) { + throw new MissingContextException("uIndex is missing from context"); + } + if (! context.containsKey("tIndex")) { + throw new MissingContextException("tIndex is missing from context"); + } + int uIndex = (Integer) context.get("uIndex"); + int tIndex = (Integer) context.get("tIndex"); + if (curIndex >= uIndex * 2 + tIndex * 2) { + return null; + } + if (curIndex % 2 == 0 && curIndex < uIndex * 2) { + return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); + } else if (curIndex < uIndex * 2) { + return new MetaEvaluatableTermVariable(new Variable("u" + curIndex / 2)); + } + curIndex -= uIndex * 2; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("v" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")) + ) + ); + } + + @Override + public Set apply(Listassumptions, EvaluatableTerm term, MatchConstraint constraint) { + Set result = new HashSet<>(); + if (assumptions.size() < this.assumptions.size()) { + 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) { + leftConst.getContext().put("isLeft", true); + } + Set conclusionRightMatchResult = conclusionRightSideHandMatch(term, matchResult); + for (MatchConstraint rightConst: conclusionRightMatchResult) { + rightConst.getContext().put("isLeft", false); + } + Set conclusionMatchResult = new HashSet<>(); + conclusionMatchResult.addAll(conclusionLeftMatchResult); + conclusionMatchResult.addAll(conclusionRightMatchResult); + + MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion; + + for (MatchConstraint matchRes: conclusionMatchResult) { + try { + boolean isLeft = (Boolean) matchRes.getContext().get("isLeft"); + if (isLeft) { + 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.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.getLeftHandSide()).substitute(matchRes.getBinding(), matchRes.getContext()); + result.add(leftSide); + } + } catch (SubstituteFailedException e) { + continue; + } + } + return result; + } + +} diff --git a/src/main/java/inference/axioms/PseudoConstantness.java b/src/main/java/inference/axioms/PseudoConstantness.java new file mode 100644 index 0000000..c4e357d --- /dev/null +++ b/src/main/java/inference/axioms/PseudoConstantness.java @@ -0,0 +1,101 @@ +package inference.axioms; + +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import exceptions.SubstituteFailedException; +import inference.EquationAxiom; +import inference.InferenceOrderConstraint; +import models.Position; +import models.algebra.Constant; +import models.algebra.Variable; +import models.formulas.DependencyFormula; +import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.formulas.meta.MetaEquationFormula; +import models.terms.EvaluatableTerm; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaDynamicDependencyTerm; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; +import models.terms.meta.OrderConstraint; + +public class PseudoConstantness extends EquationAxiom { + + public PseudoConstantness() { + super("Pseudo-Constantness"); + assumptions.add(new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + return new MetaEvaluatableTermVariable(new Variable("te" + curIndex), new Variable("n")); + } + }, + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) + ) + )); + defaultOrderConstraint = new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")); + + conclusion = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2), new Variable("n")); + } + }, + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) + ), + new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")) + ); + } + + @Override + public Set apply(List assumptions, EvaluatableTerm term, MatchConstraint constraint) { + Set result = new HashSet<>(); + if (assumptions.size() < this.assumptions.size()) { + return new HashSet<>(); + } + + Set matchResult = assumptionMatch(assumptions, constraint); + + Set conclusionLeftMatchResult = conclusionLeftSideHandMatch(term, matchResult); + for (MatchConstraint leftConst: conclusionLeftMatchResult) { + leftConst.getContext().put("isLeft", true); + } + Set conclusionRightMatchResult = conclusionRightSideHandMatch(term, matchResult); + for (MatchConstraint rightConst: conclusionRightMatchResult) { + rightConst.getContext().put("isLeft", false); + } + Set conclusionMatchResult = new HashSet<>(); + conclusionMatchResult.addAll(conclusionLeftMatchResult); + conclusionMatchResult.addAll(conclusionRightMatchResult); + + MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion; + for (MatchConstraint matchRes: conclusionMatchResult) { + boolean isLeft =(Boolean) matchRes.getContext().get("isLeft"); + if (defaultOrderConstraint != null && ! defaultOrderConstraint.check(matchRes.getOrderConstraint())) { + continue; + } + try { + if (isLeft) { + 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.getLeftHandSide()).substitute(matchRes.getBinding(), matchRes.getContext())); + } + } catch (SubstituteFailedException e) { + continue; + } + } + return result; + } + +} diff --git a/src/main/java/inference/axioms/RightNormalization.java b/src/main/java/inference/axioms/RightNormalization.java new file mode 100644 index 0000000..b285fb4 --- /dev/null +++ b/src/main/java/inference/axioms/RightNormalization.java @@ -0,0 +1,11 @@ +package inference.axioms; + +import inference.EquationAxiom; + +public class RightNormalization extends EquationAxiom { + + public RightNormalization() { + super("Right Normalization"); + } + +} diff --git a/src/main/java/inference/axioms/RightSubstitution.java b/src/main/java/inference/axioms/RightSubstitution.java new file mode 100644 index 0000000..b8d3e53 --- /dev/null +++ b/src/main/java/inference/axioms/RightSubstitution.java @@ -0,0 +1,85 @@ +package inference.axioms; + +import java.util.List; +import java.util.Map; +import java.util.Set; + +import inference.EquationAxiom; +import models.algebra.Variable; +import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.formulas.meta.MetaEquationFormula; +import models.terms.EvaluatableTerm; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaDynamicDependencyTerm; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; + +public class RightSubstitution extends EquationAxiom { + + public RightSubstitution() { + super("Right Substitution"); + assumptions.add(new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("ue")), + new MetaEvaluatableTermVariable(new Variable("ve")) + )); + assumptions.add(new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 2; + return new MetaEvaluatableTermVariable(new Variable("xe" + curIndex)); + } + + }, + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + )); + this.conclusion = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 3; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("xe" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ), + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 3; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("xe" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("ve")) + ) + ); + } + + + @Override + public Set apply(Listassumptions, EvaluatableTerm term) { + MatchConstraint constraint = MatchConstraint.createDefault(); + constraint.getContext().put("maxIndex", term.getMaxIndex()); + constraint.getContext().put("maxDepth", term.getMaxDepth()); + return apply(assumptions, term, constraint); + } + +} diff --git a/src/main/java/inference/axioms/UncurriedMapping.java b/src/main/java/inference/axioms/UncurriedMapping.java new file mode 100644 index 0000000..ee174da --- /dev/null +++ b/src/main/java/inference/axioms/UncurriedMapping.java @@ -0,0 +1,100 @@ +package inference.axioms; + +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import exceptions.SubstituteFailedException; +import inference.DependencyAxiom; +import models.Position; +import models.algebra.Variable; +import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDependencyTerm; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaRDLTermVariable; +import models.terms.meta.MetaTermGenerator; +import utils.ExpressionUtils; + +public class UncurriedMapping extends DependencyAxiom { + + public UncurriedMapping() { + super("Uncurried Mapping"); + assumptions.add(new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + int i = maxDepth - curDepth; + context.put("i", Math.max(i, (Integer) context.getOrDefault("i", 0))); + if (curDepth == maxDepth) { + if (curIndex == 0) { + return new MetaRDLTermVariable(new Variable("se"), new Variable("n")); + } else if (curIndex == 1) { + return new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")); + } + curIndex -= 1; + } else if (curIndex == 0) { + return new MetaDynamicDependency(this); + } + curIndex -= 1; + return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex), ExpressionUtils.parse("n-" + i)); + } + } + ) + )); + + conclusion = new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + int i = (Integer) context.get("i"); + if (curDepth == maxDepth - 1 && curIndex == 0) { + return new MetaDependencyTerm( + new MetaRDLTermVariable(new Variable("se"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("ve"), ExpressionUtils.parse("n-" + i)) + ); + } else if (curIndex == 0) { + return new MetaDynamicDependency(this); + } if (curDepth == 1) { + if (curIndex == 1) { + return new MetaEvaluatableTermVariable(new Variable("ve"), ExpressionUtils.parse("n-" + i)); + } + curIndex -= 1; + } + curIndex -= 1; + return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex), ExpressionUtils.parse("n-" + i)); + } + } + ) + ); + this.missingVariables.add(new MetaEvaluatableTermVariable(new Variable("ve"))); + } + + @Override + public Set derive(List assumptions, MatchConstraint constraint) { + Set result = new HashSet<>(); + if (this.assumptions.size() != assumptions.size()) { + return new HashSet<>(); + } + Set matchResult = assumptionMatch(assumptions, constraint); + + for (MatchConstraint res: matchResult) { + try { + int maxDepth = (Integer) res.getContext().get("maxDepth"); + res.getContext().put(new Position(), (Integer) res.getContext().get(new Position()) + 1); + result.add(this.conclusion.substitution(res.getBinding(), res.getContext())); + } catch (SubstituteFailedException e) { + continue; + } + } + return result; + } + +} diff --git a/src/main/java/inference/axioms/Uncurrying.java b/src/main/java/inference/axioms/Uncurrying.java new file mode 100644 index 0000000..9f073f7 --- /dev/null +++ b/src/main/java/inference/axioms/Uncurrying.java @@ -0,0 +1,158 @@ +package inference.axioms; + +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import exceptions.MissingContextException; +import exceptions.SubstituteFailedException; +import inference.EquationAxiom; +import models.Position; +import models.algebra.Variable; +import models.formulas.Formula; +import models.formulas.meta.MetaDependencyFormula; +import models.formulas.meta.MetaEquationFormula; +import models.terms.EvaluatableTerm; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaDynamicDependencyTerm; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; +import utils.ExpressionUtils; + +public class Uncurrying extends EquationAxiom { + + public Uncurrying() { + super("Uncurrying"); + + assumptions.add(new MetaDependencyFormula( + new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + context.put("" + curDepth, maxIndex + 1); + context.put("i", Math.max(maxDepth - curDepth, (Integer) context.getOrDefault("i", 0))); + if (curDepth == maxDepth && curIndex == 0) { + return new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")); + } else if (curDepth == maxDepth && curIndex == 1) { + return new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")); + } else if (curIndex == 0) { + return new MetaDynamicDependency(this); + } + return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex), ExpressionUtils.parse("n-" + (maxDepth - curDepth))); + } + } + ) + )); + + conclusion = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { +// maxIndex = (Integer) context.get(""+curDepth); + if (! context.containsKey("i")) { + throw new MissingContextException("i is missing from the context"); + } + int i = (Integer) context.get("i"); + if (curDepth == maxDepth) { + if (curIndex == 0) { + return new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")); + } else if (curIndex == 1) { + return new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")); + } else if (curIndex == 2) { + return new MetaEvaluatableTermVariable(new Variable("ve"), ExpressionUtils.parse("n-" + i)); + } + } else if (curIndex == 0) { + return new MetaDynamicDependencyTerm(this); + } + if (i == maxDepth - curDepth && curIndex == maxIndex - 2) { + return new MetaEvaluatableTermVariable(new Variable("ve"), ExpressionUtils.parse("n-" + i)); + } else if (i == maxDepth - curDepth && curIndex == maxIndex - 1) { + return new MetaEvaluatableTermVariable(new Variable("we")); + } + curIndex -= 1; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n-" + (maxDepth - curDepth))); + } + return new MetaEvaluatableTermVariable(new Variable("ue" + curDepth + "_" + curIndex / 2)); + } + } + ), + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { +// maxIndex = (Integer) context.get(""+curDepth); + if (curDepth == maxDepth) { + if (curIndex == 0) { + return new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")); + } else if (curIndex == 1) { + return new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")); + } else if (curIndex == 2) { + return new MetaEvaluatableTermVariable(new Variable("we")); + } + } else if (curIndex == 0) { + return new MetaDynamicDependencyTerm(this); + } + curIndex -= 1; + if (curIndex >= maxIndex) { + return null; + } + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n-" + (maxDepth - curDepth))); + } + return new MetaEvaluatableTermVariable(new Variable("ue" + curDepth + "_" + curIndex / 2)); + } + } + ) + ); + } + + @Override + public Set apply(List assumptions, EvaluatableTerm term, MatchConstraint constraint) { + Set result = new HashSet<>(); + if (assumptions.size() < this.assumptions.size()) { + return new HashSet<>(); + } + + Set matchResult = assumptionMatch(assumptions, constraint); + + Set conclusionLeftMatchResult = conclusionLeftSideHandMatch(term, matchResult); + for (MatchConstraint leftConst: conclusionLeftMatchResult) { + leftConst.getContext().put("isLeft", true); + } + Set conclusionRightMatchResult = conclusionRightSideHandMatch(term, matchResult); + for (MatchConstraint rightConst: conclusionRightMatchResult) { + rightConst.getContext().put("isLeft", false); + } + Set conclusionMatchResult = new HashSet<>(); + conclusionMatchResult.addAll(conclusionLeftMatchResult); + conclusionMatchResult.addAll(conclusionRightMatchResult); + + MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion; + for (MatchConstraint matchRes: conclusionMatchResult) { + boolean isLeft =(Boolean) matchRes.getContext().get("isLeft"); + if (defaultOrderConstraint != null && ! defaultOrderConstraint.check(matchRes.getOrderConstraint())) { + continue; + } + try { + if (isLeft) { + matchRes.getContext().put(new Position(), (Integer) matchRes.getContext().get(new Position()) - 2); + 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.getLeftHandSide()).substitute(matchRes.getBinding(), matchRes.getContext())); + } + } catch (SubstituteFailedException e) { + continue; + } + } + return result; + } + + + +} 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/Position.java b/src/main/java/inference/rewrite/Position.java deleted file mode 100644 index 61755b5..0000000 --- a/src/main/java/inference/rewrite/Position.java +++ /dev/null @@ -1,68 +0,0 @@ -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 index cfe6929..69a7db5 100644 --- a/src/main/java/inference/rewrite/ResourceTree.java +++ b/src/main/java/inference/rewrite/ResourceTree.java @@ -8,9 +8,9 @@ import java.util.stream.Collectors; import lombok.Getter; +import models.Position; import models.terms.DependencyTerm; import models.terms.EvaluatableTerm; -import models.terms.PrimedTerm; import models.terms.Resource; public class ResourceTree { @@ -79,37 +79,6 @@ } } 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; } diff --git a/src/main/java/inference/rewrite/RewriteInferenceSystem.java b/src/main/java/inference/rewrite/RewriteInferenceSystem.java index 0f214b0..bd24b1d 100644 --- a/src/main/java/inference/rewrite/RewriteInferenceSystem.java +++ b/src/main/java/inference/rewrite/RewriteInferenceSystem.java @@ -9,12 +9,12 @@ import java.util.Map; import java.util.Set; +import models.Position; import models.formulas.EquationFormula; import models.formulas.Formula; import models.formulas.Then; import models.terms.DependencyTerm; import models.terms.EvaluatableTerm; -import models.terms.PrimedTerm; import models.terms.Resource; public class RewriteInferenceSystem { @@ -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,55 +536,34 @@ 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; } 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; - } + 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; - } + 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 false; } } return true; @@ -594,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; @@ -608,14 +587,6 @@ if (! (formula instanceof EquationFormula equation)) { return false; } - EvaluatableTerm leftSideHand = equation.getLeftSideHand(); - EvaluatableTerm rightSideHand = equation.getRightSideHand(); - - if (leftSideHand instanceof PrimedTerm) { - return ((PrimedTerm) leftSideHand).getPrimedTerm().equals(rightSideHand); - } else if (rightSideHand instanceof PrimedTerm) { - return ((PrimedTerm) rightSideHand).getPrimedTerm().equals(leftSideHand); - } return false; } diff --git a/src/main/java/models/Position.java b/src/main/java/models/Position.java new file mode 100644 index 0000000..4ee3236 --- /dev/null +++ b/src/main/java/models/Position.java @@ -0,0 +1,84 @@ +package models; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Collections; +import java.util.List; +import java.util.stream.Collectors; + +import lombok.Getter; + +public class Position { + + @Getter + private List paths; + + public Position(List paths) { + this.paths = Collections.unmodifiableList(paths); + } + + public Position(Integer ...paths) { + this(Arrays.asList(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(); + } + + public int getPath(int index) { + if (index >= size()) { + return -1; + } + 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) { + 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.stream().map(String::valueOf).collect(Collectors.joining(", ")) + "]"; + } + + public static Position toPosition(String pathString) { + return new Position(Arrays.stream(pathString.substring(1, pathString.length() - 1).split(", ")).map(Integer::parseInt).toList()); + } + +} 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/DependencyFormula.java b/src/main/java/models/formulas/DependencyFormula.java index 989125c..602d6a7 100644 --- a/src/main/java/models/formulas/DependencyFormula.java +++ b/src/main/java/models/formulas/DependencyFormula.java @@ -25,6 +25,10 @@ this.dependency = new Dependency(dependingTerm, dependedTerms); } + public int getMaxIndex() { + return this.dependency.getMaxIndex(); + } + @Override public String toString() { return dependency.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/MetaDependencyFormula.java b/src/main/java/models/formulas/meta/MetaDependencyFormula.java index 04407e2..55191e6 100644 --- a/src/main/java/models/formulas/meta/MetaDependencyFormula.java +++ b/src/main/java/models/formulas/meta/MetaDependencyFormula.java @@ -19,6 +19,7 @@ import models.terms.meta.MetaDynamicDependency; import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaTermGenerator; +import models.terms.meta.MetaVariable; @Getter public class MetaDependencyFormula extends MetaFormula { @@ -36,15 +37,15 @@ this.dependency = dependency; } - public MetaDependencyFormula(MetaRDLTerm dependingTerm, List dependedTerms) { + public MetaDependencyFormula(RDLTerm dependingTerm, List dependedTerms) { this.dependency = new MetaDependency(dependingTerm, dependedTerms); } - public MetaDependencyFormula(MetaRDLTerm dependingTerm, MetaRDLTerm ...dependedTerms) { + public MetaDependencyFormula(RDLTerm dependingTerm, RDLTerm ...dependedTerms) { this(dependingTerm, Arrays.asList(dependedTerms)); } - public MetaDependencyFormula(MetaRDLTerm dependingTerm, MetaTermGenerator generator) { + public MetaDependencyFormula(RDLTerm dependingTerm, MetaTermGenerator generator) { this.dependency = new MetaDynamicDependency(generator, dependingTerm); } @@ -59,10 +60,19 @@ @Override - public DependencyFormula substitution(Map binding) { - return new DependencyFormula((Dependency) dependency.substitute(binding)); + public DependencyFormula substitution(Map binding, Map context) { + return new DependencyFormula((Dependency) dependency.substitute(binding, context)); } + @Override + public MetaDependencyFormula replace(Map mapping) { + return new MetaDependencyFormula(this.dependency.replace(mapping)); + } + + @Override + public Set getAllVariables() { + return this.dependency.getAllVariables(); + } public String toString() { diff --git a/src/main/java/models/formulas/meta/MetaEquationFormula.java b/src/main/java/models/formulas/meta/MetaEquationFormula.java index e061866..ce00bdf 100644 --- a/src/main/java/models/formulas/meta/MetaEquationFormula.java +++ b/src/main/java/models/formulas/meta/MetaEquationFormula.java @@ -13,23 +13,23 @@ import models.terms.RDLTerm; import models.terms.meta.MatchConstraint; import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaVariable; @Getter public class MetaEquationFormula extends MetaFormula { - private MetaRDLTerm leftSideHand; - private MetaRDLTerm rightSideHand; + private RDLTerm leftHandSide; + private RDLTerm rightHandSide; - public MetaEquationFormula(MetaRDLTerm left, MetaRDLTerm right) { + public MetaEquationFormula(RDLTerm left, RDLTerm right) { if (! left.isEvaluatableTerm()) { throw new IllegalTypeException(); } if (! right.isEvaluatableTerm()) { throw new IllegalTypeException(); } - - this.leftSideHand = left; - this.rightSideHand = right; + this.leftHandSide = left; + this.rightHandSide = right; } @Override @@ -38,18 +38,65 @@ if (! (formula instanceof EquationFormula)) { return result; } + result.add(constraint); EquationFormula eq = (EquationFormula) formula; - result = leftSideHand.isMatchedBy(eq.getLeftSideHand(), constraint); - return rightSideHand.isMatchedBy(eq.getRightSideHand(), result); + if (leftHandSide instanceof MetaRDLTerm metaLeft) { + result = metaLeft.isMatchedBy(eq.getLeftHandSide(), result); + } else { + if (! leftHandSide.equals(eq.getLeftHandSide())) { + return new HashSet<>(); + } + } + if (rightHandSide instanceof MetaRDLTerm metaRight) { + result = metaRight.isMatchedBy(eq.getRightHandSide(), result); + } else { + if (! rightHandSide.equals(eq.getRightHandSide())) { + return new HashSet<>(); + } + } + return result; } @Override - public EquationFormula substitution(Map binding) { - return new EquationFormula((EvaluatableTerm) leftSideHand.substitute(binding), (EvaluatableTerm) rightSideHand.substitute(binding)); + public EquationFormula substitution(Map binding, Map context) { + RDLTerm left = leftHandSide; + RDLTerm right = rightHandSide; + if (leftHandSide instanceof MetaRDLTerm metaLeft) { + left = metaLeft.substitute(binding, context); + } + if (rightHandSide instanceof MetaRDLTerm metaRight) { + right = metaRight.substitute(binding, context); + } + return new EquationFormula((EvaluatableTerm) left, (EvaluatableTerm) right); + } + + @Override + public MetaEquationFormula replace(Map mapping) { + RDLTerm left = leftHandSide; + RDLTerm right = rightHandSide; + if (leftHandSide instanceof MetaRDLTerm metaLeft) { + left = metaLeft.replace(mapping); + } + if (rightHandSide instanceof MetaRDLTerm metaRight) { + right = metaRight.replace(mapping); + } + return new MetaEquationFormula(left, right); + } + + @Override + public Set getAllVariables() { + Set result = new HashSet<>(); + if (leftHandSide instanceof MetaRDLTerm metaLeft) { + result.addAll(metaLeft.getAllVariables()); + } + 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) { @@ -57,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() { @@ -67,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/formulas/meta/MetaFormula.java b/src/main/java/models/formulas/meta/MetaFormula.java index bb54cc0..5ea1c17 100644 --- a/src/main/java/models/formulas/meta/MetaFormula.java +++ b/src/main/java/models/formulas/meta/MetaFormula.java @@ -1,6 +1,5 @@ package models.formulas.meta; -import java.util.HashMap; import java.util.HashSet; import java.util.Map; import java.util.Set; @@ -9,15 +8,18 @@ import models.formulas.Formula; import models.terms.RDLTerm; import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaVariable; -public abstract class MetaFormula { +public abstract class MetaFormula extends Formula { public Set isMatchedBy(Formula formula) { - return isMatchedBy(formula, new MatchConstraint(new HashMap<>(), new HashMap<>())); + return isMatchedBy(formula, MatchConstraint.createDefault()); } public abstract Set isMatchedBy(Formula formula, MatchConstraint constraint); + public Set isMatchedBy(Formula formula, Set constraints) { Set result = new HashSet<>(); for (MatchConstraint constraint: constraints) { @@ -26,12 +28,11 @@ return result; } - public abstract Formula substitution(Map binding); + public abstract Formula substitution(Map binding, Map context); public abstract Set getSubTerms(Class clazz); - - public abstract String toString(); - public abstract boolean equals(Object another); - public abstract int hashCode(); + + public abstract MetaFormula replace(Map mapping); + public abstract Set getAllVariables(); } diff --git a/src/main/java/models/terms/Dependency.java b/src/main/java/models/terms/Dependency.java index d454a08..af88546 100644 --- a/src/main/java/models/terms/Dependency.java +++ b/src/main/java/models/terms/Dependency.java @@ -1,15 +1,15 @@ package models.terms; -import com.google.common.collect.TreeMultiset; - import java.util.ArrayList; import java.util.Arrays; import java.util.List; import java.util.stream.Collectors; +import com.google.common.collect.TreeMultiset; + import exceptions.SyntaxException; import lombok.Getter; -import models.algebra.Symbol; +import models.Position; @Getter public class Dependency extends RDLTerm{ @@ -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); @@ -33,11 +33,63 @@ } } + public Dependency(RDLTerm dependingTerm, TreeMultiset dependedTerms) { + this(dependingTerm, new ArrayList<>(dependedTerms)); + } + public Dependency(RDLTerm dependingTerm, EvaluatableTerm ...dependedTerms) { this(dependingTerm, Arrays.asList(dependedTerms)); } @Override + public Dependency getDependency() { + return this; + } + + @Override + public RDLTerm replace(Position targetPosition, RDLTerm term, Position curPosition) { + if (targetPosition.equals(curPosition)) { + return term; + } else { + int nextPath = targetPosition.getPath(curPosition.size()); + if (nextPath == 0) { + return new Dependency(dependingTerm.replace(targetPosition, term, curPosition.addPath(nextPath)), this.dependedTerms); + } else { + List dependedTerms = new ArrayList<>(); + for (int i = 1; i < getChildren().size(); i++) { + if (i == nextPath) { + dependedTerms.add((EvaluatableTerm) ((RDLTerm) getChild(i)).replace(targetPosition, term, curPosition.addPath(i))); + } else { + dependedTerms.add((EvaluatableTerm) getChild(i)); + } + } + return new Dependency(dependingTerm, dependedTerms); + } + } + } + + @Override + public int getMaxIndex() { + return 1 + dependedTerms.size(); + } + + @Override + public int getMaxDepth() { + int result = dependingTerm.getMaxDepth(); + if (! (dependingTerm instanceof Resource || dependingTerm instanceof ResourceConstant)) { + result++; + } + for (RDLTerm dependedTerm : dependedTerms) { + int dependedTermDepth = dependedTerm.getMaxDepth(); + if (! (dependedTerm instanceof Resource || dependedTerm instanceof ResourceConstant)) { + dependedTermDepth++; + } + result = Math.max(result, dependedTermDepth); + } + return result; + } + + @Override public int getTermOrder() { return getOrder() - 1; } diff --git a/src/main/java/models/terms/DependencyTerm.java b/src/main/java/models/terms/DependencyTerm.java index 5387e41..c3e4721 100644 --- a/src/main/java/models/terms/DependencyTerm.java +++ b/src/main/java/models/terms/DependencyTerm.java @@ -1,14 +1,17 @@ package models.terms; -import com.google.common.collect.TreeMultiset; - 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; + import exceptions.SyntaxException; import lombok.Getter; +import models.Position; @Getter public class DependencyTerm extends EvaluatableTerm{ @@ -93,6 +96,105 @@ } @Override + public Dependency getDependency() { + 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 { + 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)); + } + + } + + return result; + } + + @Override + public RDLTerm replace(Position targetPosition, RDLTerm term, Position curPosition) { + if (targetPosition.equals(curPosition)) { + return term; + } else { + int nextPath = targetPosition.getPath(curPosition.size()); + List children = new ArrayList<>(); + for (int i = 1; i < getChildren().size(); i++) { + children.add((EvaluatableTerm) getChild(i)); + } + if (nextPath == 0) { + return new DependencyTerm((EvaluatableTerm) dependingTerm.replace(targetPosition, term, curPosition.addPath(nextPath)), children); + } else { + children.set(nextPath - 1, (EvaluatableTerm) children.get(nextPath - 1).replace(targetPosition, term, curPosition.addPath(nextPath))); + return new DependencyTerm(dependingTerm, children); + } + } + } + + @Override + public int getMaxIndex() { + int result = 1; + for (EvaluatableTerm dependedTerm : termPairs.keySet()) { + for (EvaluatableTerm argTerm : termPairs.get(dependedTerm)) { + result += 2; + } + } + return result; + } + + @Override + public int getMaxDepth() { + int result = 0; + if (dependingTerm instanceof Resource || dependingTerm instanceof ResourceConstant) { + result = dependingTerm.getMaxDepth(); + } else { + result = dependingTerm.getMaxDepth() + 1; + } + for (EvaluatableTerm dependedTerm : termPairs.keySet()) { + int dependedTermDepth = dependedTerm.getMaxDepth(); + if (! (dependedTerm instanceof Resource || dependedTerm instanceof ResourceConstant)) { + dependedTermDepth++; + } + result = Math.max(result, dependedTermDepth); + for (EvaluatableTerm argTerm : termPairs.get(dependedTerm)) { + int argTermDepth = dependedTerm.getMaxDepth(); + if (! (argTerm instanceof Resource || argTerm instanceof ResourceConstant)) { + argTermDepth++; + } + result = Math.max(result, argTermDepth); + } + } + + return result; + } + + @Override public boolean isLinearRightNormalized() { return isLinearRightNormaled(0); } diff --git a/src/main/java/models/terms/PrimedTerm.java b/src/main/java/models/terms/PrimedTerm.java deleted file mode 100644 index 40ebd68..0000000 --- a/src/main/java/models/terms/PrimedTerm.java +++ /dev/null @@ -1,64 +0,0 @@ -package models.terms; - -import lombok.Getter; - -@Getter -public class PrimedTerm extends EvaluatableTerm { - - private EvaluatableTerm primedTerm; - private boolean isResource; - - public PrimedTerm(EvaluatableTerm term) { - super(term.getOrder(), term.getSize()); - this.primedTerm = term; - this.isResource = term instanceof Resource; - } - - @Override - public String toString() { - return primedTerm.toString() + "'"; - } - - @Override - public String toStringWithOrder() { - return toString() + "(" + primedTerm.getOrder() + ")"; - } - - @Override - 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() { - return new PrimedTerm(primedTerm); - } - - @Override - public boolean isLinearRightNormalized() { - return primedTerm.isLinearRightNormalized(); - } - - @Override - public EvaluatableTerm linearRightNormalize() { - return new PrimedTerm(primedTerm.linearRightNormalize()); - } - - @Override - public void selfLinearRightNormalize() { - primedTerm.selfLinearRightNormalize(); - } - - - -} diff --git a/src/main/java/models/terms/RDLTerm.java b/src/main/java/models/terms/RDLTerm.java index 536230d..4eb68b5 100644 --- a/src/main/java/models/terms/RDLTerm.java +++ b/src/main/java/models/terms/RDLTerm.java @@ -1,6 +1,7 @@ package models.terms; import lombok.Getter; +import models.Position; import models.algebra.Symbol; import models.algebra.Term; @@ -11,7 +12,7 @@ protected int size; protected RDLTerm(int order, int size) { - super(new Symbol("")); + super(new Symbol("", -1)); this.order = order; this.size = size; } @@ -20,6 +21,39 @@ return getOrder(); } + public abstract Dependency getDependency(); + + public abstract RDLTerm replace(Position targetPosition, RDLTerm term, Position curPosition); + + public RDLTerm replace(Position targetPosition, RDLTerm term) { + return replace(targetPosition, term, new Position()); + } + + public abstract int getMaxIndex(); + + public abstract int getMaxDepth(); + + public boolean isVariable() { + return false; + } + + public boolean isDependency() { + return this instanceof Dependency; + } + + public boolean isEvaluatableTerm() { + return this instanceof EvaluatableTerm; + } + + public boolean isDependencyTerm() { + return this instanceof DependencyTerm; + } + + public boolean isResource() { + return this instanceof Resource; + } + + @Override public abstract String toString(); diff --git a/src/main/java/models/terms/Resource.java b/src/main/java/models/terms/Resource.java index cd487d7..51f08a0 100644 --- a/src/main/java/models/terms/Resource.java +++ b/src/main/java/models/terms/Resource.java @@ -1,8 +1,8 @@ package models.terms; +import exceptions.ReplaceFailedException; import lombok.Getter; -import models.algebra.Symbol; -import models.algebra.Type; +import models.Position; @Getter public class Resource extends EvaluatableTerm { @@ -15,6 +15,29 @@ } @Override + public Dependency getDependency() { + return null; + } + + @Override + public RDLTerm replace(Position targetPosition, RDLTerm term, Position curPosition) { + if (targetPosition.equals(curPosition)) { + return term; + } + throw new ReplaceFailedException(); + } + + @Override + public int getMaxIndex() { + return 1; + } + + @Override + public int getMaxDepth() { + return 1; + } + + @Override public EvaluatableTerm linearRightNormalize() { return (Resource) clone(); } diff --git a/src/main/java/models/terms/ResourceConstant.java b/src/main/java/models/terms/ResourceConstant.java index bf1567c..bb9b72b 100644 --- a/src/main/java/models/terms/ResourceConstant.java +++ b/src/main/java/models/terms/ResourceConstant.java @@ -1,7 +1,8 @@ package models.terms; +import exceptions.ReplaceFailedException; import lombok.Getter; -import models.algebra.Symbol; +import models.Position; import models.algebra.Type; @Getter @@ -23,6 +24,29 @@ } @Override + public Dependency getDependency() { + return null; + } + + @Override + public RDLTerm replace(Position targetPosition, RDLTerm term, Position curPosition) { + if (targetPosition.equals(curPosition)) { + return term; + } + throw new ReplaceFailedException(); + } + + @Override + public int getMaxIndex() { + return 1; + } + + @Override + public int getMaxDepth() { + return 1; + } + + @Override public boolean isLinearRightNormalized() { return true; } diff --git a/src/main/java/models/terms/meta/MatchConstraint.java b/src/main/java/models/terms/meta/MatchConstraint.java index 5d40446..f78f5cc 100644 --- a/src/main/java/models/terms/meta/MatchConstraint.java +++ b/src/main/java/models/terms/meta/MatchConstraint.java @@ -15,10 +15,12 @@ private final Map binding; private final Map orderConstraint; + private final Map context; public MatchConstraint(MatchConstraint constraint) { this.binding = constraint.getBinding(); this.orderConstraint = constraint.getOrderConstraint(); + this.context = constraint.cloneContext(); } public Map getBinding() { @@ -44,9 +46,21 @@ public void setOrderConstraint(Variable key, OrderConstraint constraint, int value) { this.orderConstraint.get(key).setConstraint(value, constraint); } + + public Map getContext() { + return this.context; + } + + public Map cloneContext() { + return new HashMap<>(this.context); + } + + public MatchConstraint clone() { + return new MatchConstraint(this); + } public static MatchConstraint createDefault() { - return new MatchConstraint(new HashMap<>(), new HashMap<>()); + return new MatchConstraint(new HashMap<>(), new HashMap<>(), new HashMap<>()); } } diff --git a/src/main/java/models/terms/meta/MetaConstant.java b/src/main/java/models/terms/meta/MetaConstant.java new file mode 100644 index 0000000..b2659ef --- /dev/null +++ b/src/main/java/models/terms/meta/MetaConstant.java @@ -0,0 +1,17 @@ +package models.terms.meta; + +import models.algebra.Constant; +import models.algebra.Variable; + +public class MetaConstant extends MetaVariable { + + public MetaConstant(Variable name) { + super(TermType.MEAT_CONSTANT_VARIABLE, name, OrderConstraint.EQ, new Constant("0")); + } + + @Override + public MetaVariable cloneWithName(String name) { + return new MetaConstant(new Variable(name)); + } + +} diff --git a/src/main/java/models/terms/meta/MetaDependency.java b/src/main/java/models/terms/meta/MetaDependency.java index 031bf73..f6016d3 100644 --- a/src/main/java/models/terms/meta/MetaDependency.java +++ b/src/main/java/models/terms/meta/MetaDependency.java @@ -6,10 +6,12 @@ import java.util.List; import java.util.Map; import java.util.Set; +import java.util.stream.Collectors; import exceptions.SubstituteFailedException; import exceptions.SyntaxException; -import models.algebra.Symbol; +import models.Position; +import models.algebra.Expression; import models.algebra.Variable; import models.terms.Dependency; import models.terms.EvaluatableTerm; @@ -19,7 +21,7 @@ public class MetaDependency extends MetaRDLTerm{ protected RDLTerm dependingTerm; - protected List dependedTerms; + protected List dependedTerms = new ArrayList<>(); protected MetaDependency() { super(TermType.META_DEPENDENCY, -1); @@ -43,7 +45,7 @@ } @Override - protected Set isMatchedBy(RDLTerm another, MatchConstraint constraint, int depth) { + public Set isMatchedBy(RDLTerm another, MatchConstraint constraint, Position position) { Set result = new HashSet<>(); if (! another.getClass().isAssignableFrom(this.termType.getBaseTermClass())) { return result; @@ -51,25 +53,28 @@ if (isDependencyTerm() && (! islinearRightNormalizedMatchedBy(another))) { return result; } - result = dependingTermMatch(another, constraint, depth); - return dependedTermsMatch(another, result, depth); + if (another.getChildren().size() != this.getChildren().size()) { + return result; + } + result = dependingTermMatch(another, constraint, position); + return dependedTermsMatch(another, result, position); } - private Set dependingTermMatch(RDLTerm another, MatchConstraint constraint, int depth) { + private Set dependingTermMatch(RDLTerm another, MatchConstraint constraint, Position position) { RDLTerm dependingChild = (RDLTerm) this.getChild(0); RDLTerm anotherDependingChild = (RDLTerm) another.getChild(0); if (dependingChild instanceof MetaRDLTerm) { MetaRDLTerm metaChild = (MetaRDLTerm) dependingChild; - return metaChild.isMatchedBy(anotherDependingChild, constraint, depth + 1); + return metaChild.isMatchedBy(anotherDependingChild, constraint, position.addPath(0)); } else { - if (!(dependingChild.equals(anotherDependingChild))) { - return new HashSet<>(); + if (dependingChild.equals(anotherDependingChild)) { + return new HashSet<>(Set.of(constraint)); } } return new HashSet<>(); } - private Set dependedTermsMatch(RDLTerm another, Set constraint, int depth) { + private Set dependedTermsMatch(RDLTerm another, Set constraint, Position position) { Set result = new HashSet<>(); for (List perm : Permutation.permutation(another.getChildren().size() - 1)) { Set localResult = new HashSet<>(constraint); @@ -79,7 +84,7 @@ RDLTerm metaDependedTerm = (RDLTerm) getChild(metaTermIndex + 1); RDLTerm anotherDependedTerm = (RDLTerm) another.getChild(anotherTermIndex + 1); if (metaDependedTerm instanceof MetaRDLTerm metaTerm) { - localResult = metaTerm.isMatchedBy(anotherDependedTerm, localResult, depth + 1); + localResult = metaTerm.isMatchedBy(anotherDependedTerm, localResult, position.addPath(metaTermIndex + 1)); if (localResult.isEmpty()) { flg = false; break; @@ -99,16 +104,16 @@ } @Override - protected RDLTerm substitute(Map binding, int depth) { + public RDLTerm substitute(Map binding, Map context, Position position) { RDLTerm dependingTerm = (RDLTerm) getChild(0); if (dependingTerm instanceof MetaRDLTerm) { - dependingTerm = ((MetaRDLTerm) dependingTerm).substitute(binding, depth + 1); + dependingTerm = ((MetaRDLTerm) dependingTerm).substitute(binding, context, position.addPath(0)); } List dependedTerms = new ArrayList<>(); for (int i = 1; i < getChildren().size(); i++) { RDLTerm dependedTerm = (RDLTerm) getChild(i); if (dependedTerm instanceof MetaRDLTerm metaTerm) { - dependedTerm = metaTerm.substitute(binding, depth + 1); + dependedTerm = metaTerm.substitute(binding, context, position.addPath(i)); } if (dependedTerm instanceof EvaluatableTerm te) { dependedTerms.add(te); @@ -123,4 +128,25 @@ } } + @Override + public MetaRDLTerm replace(Map mapping) { + RDLTerm dependingTerm = this.dependingTerm; + List dependedTerms = new ArrayList<>(); + if (dependingTerm instanceof MetaRDLTerm metaTerm) { + dependingTerm = metaTerm.replace(mapping); + } + for (RDLTerm term : this.dependedTerms) { + if (term instanceof MetaRDLTerm metaTerm) { + term = metaTerm.replace(mapping); + } + dependedTerms.add(term); + } + return new MetaDependency(dependingTerm, dependedTerms); + } + + @Override + public String toString() { + return "[" + getChild(0).toString() + " : " + getChildren().stream().skip(1).map(Expression::toString).collect(Collectors.joining(",")) + "]"; + } + } diff --git a/src/main/java/models/terms/meta/MetaDependencyTerm.java b/src/main/java/models/terms/meta/MetaDependencyTerm.java index 8825dc8..db16619 100644 --- a/src/main/java/models/terms/meta/MetaDependencyTerm.java +++ b/src/main/java/models/terms/meta/MetaDependencyTerm.java @@ -9,10 +9,12 @@ import java.util.Map; import java.util.Set; import java.util.TreeMap; +import java.util.stream.Collectors; +import java.util.stream.IntStream; import exceptions.SubstituteFailedException; import exceptions.SyntaxException; -import models.algebra.Symbol; +import models.Position; import models.algebra.Variable; import models.terms.DependencyTerm; import models.terms.EvaluatableTerm; @@ -21,9 +23,17 @@ public class MetaDependencyTerm extends MetaRDLTerm{ + protected RDLTerm dependingTerm; + protected Map> termPairs = new TreeMap<>(); + + protected MetaDependencyTerm() { + super(TermType.META_DEPENDENCY_TERM, -1); + } + public MetaDependencyTerm(RDLTerm dependingTerm, List terms) { super(TermType.META_DEPENDENCY_TERM, -1); TreeMap> sortedMap = new TreeMap<>(); + this.dependingTerm = dependingTerm; addChild(dependingTerm); int size = dependingTerm.getSize(); for (int i = 0; i < terms.size() / 2; i++) { @@ -33,6 +43,7 @@ } for (RDLTerm dependedTerm: sortedMap.keySet()) { for (RDLTerm argTerm: sortedMap.get(dependedTerm)) { + termPairs.computeIfAbsent(dependedTerm, k -> TreeMultiset.create()).add(argTerm); addChild(dependedTerm); addChild(argTerm); size += dependedTerm.getSize(); @@ -47,7 +58,7 @@ } @Override - protected Set isMatchedBy(RDLTerm another, MatchConstraint constraint, int depth) { + public Set isMatchedBy(RDLTerm another, MatchConstraint constraint, Position position) { Set result = new HashSet<>(); if (! another.getClass().isAssignableFrom(this.termType.getBaseTermClass())) { return result; @@ -55,25 +66,28 @@ if (isDependencyTerm() && (! islinearRightNormalizedMatchedBy(another))) { return result; } - result = dependingTermMatch(another, constraint, depth); - return termPairsMatch(another, result, depth); + if (another.getChildren().size() != this.getChildren().size()) { + return new HashSet<>(); + } + result = dependingTermMatch(another, constraint, position); + return termPairsMatch((DependencyTerm) another, result, position); } - private Set dependingTermMatch(RDLTerm another, MatchConstraint constraint, int depth) { + private Set dependingTermMatch(RDLTerm another, MatchConstraint constraint, Position position) { RDLTerm dependingChild = (RDLTerm) this.getChild(0); RDLTerm anotherDependingChild = (RDLTerm) another.getChild(0); if (dependingChild instanceof MetaRDLTerm) { MetaRDLTerm metaChild = (MetaRDLTerm) dependingChild; - return metaChild.isMatchedBy(anotherDependingChild, constraint, depth + 1); + return metaChild.isMatchedBy(anotherDependingChild, constraint, position.addPath(0)); } else { - if (!(dependingChild.equals(anotherDependingChild))) { - return new HashSet<>(); + if (dependingChild.equals(anotherDependingChild)) { + return new HashSet<>(List.of(constraint)); } } return new HashSet<>(); } - private Set termPairsMatch(RDLTerm another, Set constraint, int depth) { + private Set termPairsMatch(DependencyTerm another, Set constraint, Position position) { Set result = new HashSet<>(); for (List perm : Permutation.permutation((another.getChildren().size() - 1) / 2)) { Set localResult = new HashSet<>(constraint); @@ -85,7 +99,7 @@ RDLTerm metaArgTerm = (RDLTerm) getChild(2 * metaTermIndex + 2); RDLTerm anotherArgTerm = (RDLTerm) another.getChild(2 * anotherTermIndex + 2); if (metaDependedTerm instanceof MetaRDLTerm metaTerm) { - localResult = metaTerm.isMatchedBy(anotherDependedTerm, localResult, depth + 1); + localResult = metaTerm.isMatchedBy(anotherDependedTerm, localResult, position.addPath(2 * metaTermIndex + 1)); if (localResult.isEmpty()) { flg = false; break; @@ -97,7 +111,7 @@ } } if (metaArgTerm instanceof MetaRDLTerm metaTerm) { - localResult = metaTerm.isMatchedBy(anotherArgTerm, localResult, depth + 1); + localResult = metaTerm.isMatchedBy(anotherArgTerm, localResult, position.addPath(2 * metaTermIndex + 2)); if (localResult.isEmpty()) { flg = false; break; @@ -117,20 +131,20 @@ } @Override - protected RDLTerm substitute(Map binding, int depth) { + public RDLTerm substitute(Map binding, Map context, Position position) { RDLTerm dependingTerm = (RDLTerm) getChild(0); if (dependingTerm instanceof MetaRDLTerm) { - dependingTerm = ((MetaRDLTerm) dependingTerm).substitute(binding, depth + 1); + dependingTerm = ((MetaRDLTerm) dependingTerm).substitute(binding, context, position.addPath(0)); } List termPairs = new ArrayList<>(); for (int i = 0; i < (getChildren().size() - 1) / 2; i++) { RDLTerm dependedTerm = (RDLTerm) getChild(i * 2 + 1); RDLTerm argTerm = (RDLTerm) getChild(i * 2 + 2); if (dependedTerm instanceof MetaRDLTerm metaTerm) { - dependedTerm = metaTerm.substitute(binding, depth + 1); + dependedTerm = metaTerm.substitute(binding, context, position.addPath(i * 2 + 1)); } if (argTerm instanceof MetaRDLTerm metaTerm) { - argTerm = metaTerm.substitute(binding, depth + 1); + argTerm = metaTerm.substitute(binding, context, position.addPath(i * 2 + 2)); } termPairs.add((EvaluatableTerm) dependedTerm); termPairs.add((EvaluatableTerm) argTerm); @@ -141,5 +155,35 @@ throw new SubstituteFailedException(e.getMessage()); } } + + @Override + public MetaRDLTerm replace(Map mapping) { + RDLTerm dependingTerm = this.dependingTerm; + List termPairs = new ArrayList<>(); + if (dependingTerm instanceof MetaRDLTerm metaTerm) { + dependingTerm = metaTerm.replace(mapping); + } + for (RDLTerm dependedTerm : this.termPairs.keySet()) { + RDLTerm nextDependedTerm = dependedTerm; + if (nextDependedTerm instanceof MetaRDLTerm metaTerm) { + nextDependedTerm = metaTerm.replace(mapping); + } + for (RDLTerm argTerm : this.termPairs.get(dependedTerm)) { + if (argTerm instanceof MetaRDLTerm metaTerm) { + argTerm = metaTerm.replace(mapping); + } + termPairs.add(nextDependedTerm); + termPairs.add(argTerm); + } + } + return new MetaDependencyTerm(dependingTerm, termPairs); + } + + + @Override + public String toString() { + return "[" + getChild(0).toString() + " : " + IntStream.range(0, (getChildren().size() - 1) / 2) + .mapToObj(i -> getChild(i * 2 + 1).toString() + " -> " + getChild(i * 2 + 2)).collect(Collectors.joining(", ")) + "]"; + } } diff --git a/src/main/java/models/terms/meta/MetaDependencyTermVariable.java b/src/main/java/models/terms/meta/MetaDependencyTermVariable.java index ab5291b..6a6a0a7 100644 --- a/src/main/java/models/terms/meta/MetaDependencyTermVariable.java +++ b/src/main/java/models/terms/meta/MetaDependencyTermVariable.java @@ -3,7 +3,6 @@ import lombok.Getter; import models.algebra.Constant; import models.algebra.Expression; -import models.algebra.Symbol; import models.algebra.Variable; @Getter @@ -21,4 +20,9 @@ super(MetaRDLTerm.TermType.META_DEPENDENCY_TERM_VARIABLE, variableName, OrderConstraint.EQ, order); } + @Override + public MetaDependencyTermVariable cloneWithName(String name) { + return new MetaDependencyTermVariable(new Variable(name), constraint, orderExpression); + } + } diff --git a/src/main/java/models/terms/meta/MetaDependencyVariable.java b/src/main/java/models/terms/meta/MetaDependencyVariable.java index b59886a..07765e6 100644 --- a/src/main/java/models/terms/meta/MetaDependencyVariable.java +++ b/src/main/java/models/terms/meta/MetaDependencyVariable.java @@ -3,7 +3,6 @@ import lombok.Getter; import models.algebra.Constant; import models.algebra.Expression; -import models.algebra.Symbol; import models.algebra.Variable; @Getter @@ -21,4 +20,9 @@ super(MetaRDLTerm.TermType.META_DEPENDENCY_VARIABLE, variableName, OrderConstraint.EQ, order); } + @Override + public MetaDependencyVariable cloneWithName(String name) { + return new MetaDependencyVariable(new Variable(name), constraint, orderExpression); + } + } diff --git a/src/main/java/models/terms/meta/MetaDynamicDependency.java b/src/main/java/models/terms/meta/MetaDynamicDependency.java index 97b02d3..c9e342c 100644 --- a/src/main/java/models/terms/meta/MetaDynamicDependency.java +++ b/src/main/java/models/terms/meta/MetaDynamicDependency.java @@ -2,10 +2,15 @@ import java.util.ArrayList; import java.util.Arrays; +import java.util.HashSet; import java.util.List; import java.util.Map; import java.util.Set; +import java.util.stream.Collectors; +import exceptions.SubstituteFailedException; +import models.Position; +import models.algebra.Expression; import models.algebra.Variable; import models.terms.RDLTerm; @@ -21,6 +26,9 @@ this.termGenerator = termGenerator; this.dependingTerm = terms.size() > 0 ? terms.get(0) : null; this.dependedTerms = terms.size() > 1 ? terms.stream().skip(1).toList() : List.of(); + for (RDLTerm term : terms) { + addChild(term); + } } public MetaDynamicDependency(MetaTermGenerator termGenerator, RDLTerm ...terms) { @@ -28,17 +36,60 @@ } @Override - public MetaRDLTerm generate(int depth, Map context) { - // TODO 自動生成されたメソッド・スタブ - return null; + public Set isMatchedBy(RDLTerm another, MatchConstraint constraint, Position position) { + int maxIndex = another.getMaxIndex(); + if (! another.isDependency()) { + return new HashSet<>(); + } + Set result = new HashSet<>(); + constraint.getContext().put(position, maxIndex); + if (! (Boolean) constraint.getContext().getOrDefault("isDynamicStarted", false)) { + int maxDepth = another.getMaxDepth(); + constraint.getContext().put("isDynamicStarted", true); + for (int i = maxDepth; i >= 1; i--) { + MatchConstraint newConstraint = new MatchConstraint(constraint); + newConstraint.getContext().put("maxDepth", i); + MetaRDLTerm metaDep = generate(position.size(), maxIndex, i, newConstraint.getContext()); + Set res = metaDep.isMatchedBy(another, newConstraint, position); + result.addAll(res); + } + } else { + int maxDepth = (Integer) constraint.getContext().get("maxDepth"); + MetaRDLTerm metaDep = generate(position.size(), maxIndex, maxDepth, constraint.getContext()); + Set res = metaDep.isMatchedBy(another, constraint, position); + result.addAll(res); + } + return result; } + @Override - public MetaDependency generate(int depth, int maxIndex, int maxDepth, Map context) { + public MetaDependency generate(int depth, int maxIndex, int maxDepth, Map context) { if (maxIndex < 2) return null; + if (depth > maxDepth) return null; + RDLTerm dependingTerm = this.dependingTerm == null ? termGenerator.generate(0, depth, maxIndex, maxDepth, context) : this.dependingTerm; + List dependedTerms = new ArrayList<>(); + int staticSize = this.dependedTerms == null ? 0 : this.dependedTerms.size(); + for (int i = 0; i < Math.min(maxIndex - 1, staticSize); i++) { + dependedTerms.add(this.dependedTerms.get(i)); + } + for (int i = staticSize; i < maxIndex - 1; i++) { + RDLTerm generatedTerm = termGenerator.generate(i + 1, depth, maxIndex, maxDepth, context); + if (generatedTerm == null) { + break; + } + dependedTerms.add(generatedTerm); + } + return new MetaDependency(dependingTerm, dependedTerms); + } + + @Override + public MetaDependency allGenerate(int depth, int maxIndex, int maxDepth, Map context) { + if (maxIndex < 2) return null; + if (depth > maxDepth) return null; RDLTerm dependingTerm = this.dependingTerm == null ? termGenerator.generate(0, depth, maxIndex, maxDepth, context) : this.dependingTerm; while (dependingTerm instanceof MetaDynamicTerm dynamicTerm) { - dependingTerm = dynamicTerm.generate(depth + 1, maxIndex, maxDepth, context); + dependingTerm = dynamicTerm.allGenerate(depth + 1, maxIndex, maxDepth, context); } List dependedTerms = new ArrayList<>(); int staticSize = this.dependedTerms == null ? 0 : this.dependedTerms.size(); @@ -47,8 +98,11 @@ } for (int i = staticSize; i < maxIndex - 1; i++) { RDLTerm generatedTerm = termGenerator.generate(i + 1, depth, maxIndex, maxDepth, context); + if (generatedTerm == null) { + break; + } while (generatedTerm instanceof MetaDynamicTerm dynamicTerm) { - generatedTerm = dynamicTerm.generate(depth + 1, maxIndex, maxDepth, context); + generatedTerm = dynamicTerm.allGenerate(depth + 1, maxIndex, maxDepth, context); } dependedTerms.add(generatedTerm); } @@ -57,16 +111,23 @@ @Override - protected Set isMatchedBy(RDLTerm another, MatchConstraint constraint, int depth) { - // TODO 自動生成されたメソッド・スタブ - return null; - } - - @Override - protected RDLTerm substitute(Map binding, int depth) { - // TODO 自動生成されたメソッド・スタブ - return null; + public RDLTerm substitute(Map binding, Map context, Position position) { + if (! context.containsKey(position)) throw new SubstituteFailedException(); + if (! context.containsKey("maxDepth")) throw new SubstituteFailedException(); + int maxIndex = (int) context.get(position); + int maxDepth = (int) context.get("maxDepth"); + return generate(position.size(), maxIndex, maxDepth, context).substitute(binding, context, position); } + @Override + public String toString() { + if (dependingTerm != null) { + return "[" + + getChild(0).toString() + " : " + + getChildren().stream().skip(1).map(Expression::toString).collect(Collectors.joining(",")) + + " ...? ]"; + } + return "[ ...? ]"; + } } diff --git a/src/main/java/models/terms/meta/MetaDynamicDependencyTerm.java b/src/main/java/models/terms/meta/MetaDynamicDependencyTerm.java new file mode 100644 index 0000000..1303e88 --- /dev/null +++ b/src/main/java/models/terms/meta/MetaDynamicDependencyTerm.java @@ -0,0 +1,183 @@ +package models.terms.meta; + +import com.google.common.collect.TreeMultiset; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; +import java.util.stream.Collectors; +import java.util.stream.IntStream; + +import exceptions.SubstituteFailedException; +import exceptions.SyntaxException; +import models.Position; +import models.algebra.Variable; +import models.terms.RDLTerm; + +public class MetaDynamicDependencyTerm extends MetaDependencyTerm implements MetaDynamicTerm{ + + private final MetaTermGenerator generator; + + public MetaDynamicDependencyTerm (MetaTermGenerator generator) { + this.generator = generator; + } + + public MetaDynamicDependencyTerm(MetaTermGenerator generator, List terms) { + this.generator = generator; + if (terms.size() != 0 && terms.size() % 2 != 1) { + throw new SyntaxException(""); + } + this.dependingTerm = terms.size() > 0 ? terms.get(0) : null; + addChild(dependingTerm); + for (int i = 0; i < (terms.size() - 1) / 2; i++) { + RDLTerm dependedTerm = terms.get(i * 2 + 1); + RDLTerm argTerm = terms.get(i * 2 + 2); + this.termPairs.computeIfAbsent(dependedTerm, k -> TreeMultiset.create()).add(argTerm); + addChild(dependedTerm); + addChild(argTerm); + } + } + + public MetaDynamicDependencyTerm(MetaTermGenerator generator, RDLTerm ...terms) { + this(generator, Arrays.asList(terms)); + } + + @Override + public MetaRDLTerm generate(int depth, int maxIndex, int maxDepth, Map context) { + if (maxIndex % 2 == 0 && maxIndex <= 2) return null; + RDLTerm dependingTerm; + List termPairs = new ArrayList<>(); + if (this.dependingTerm != null) { + dependingTerm = this.dependingTerm; + } else { + dependingTerm = generator.generate(0, depth, maxIndex, maxDepth, context); + } + if (maxIndex == 1) { + return (MetaRDLTerm) dependingTerm; + } + int index = 1; + for (RDLTerm dependedTerm : this.termPairs.keySet()) { + for (RDLTerm argTerm : this.termPairs.get(dependedTerm)) { + termPairs.add(dependedTerm); + termPairs.add(argTerm); + index+=2; + } + } + for (int i = 0; i < (maxIndex - index) / 2; i++) { + RDLTerm dependedTerm = generator.generate(i * 2 + index, depth, maxIndex, maxDepth, context); + if (dependedTerm == null) { + break; + } + RDLTerm argTerm = generator.generate(i * 2 + index + 1, depth, maxIndex, maxDepth, context); + if (argTerm == null) { + break; + } + termPairs.add(dependedTerm); + termPairs.add(argTerm); + } + if (termPairs.isEmpty()) { + return (MetaRDLTerm) dependingTerm; + } + return new MetaDependencyTerm(dependingTerm, termPairs); + } + + @Override + public MetaRDLTerm allGenerate(int depth, int maxIndex, int maxDepth, Map context) { + if (maxIndex % 2 == 0 && maxIndex <= 2) return null; + RDLTerm dependingTerm; + List termPairs = new ArrayList<>(); + if (this.dependingTerm != null) { + dependingTerm = this.dependingTerm; + } else { + dependingTerm = generator.generate(0, depth, maxIndex, maxDepth, context); + } + while (dependingTerm instanceof MetaDynamicTerm dynamicTerm) { + dependingTerm = dynamicTerm.allGenerate(depth + 1, maxIndex, maxDepth, context); + } + if (maxIndex == 1) { + return (MetaRDLTerm) dependingTerm; + } + int index = 1; + for (RDLTerm dependedTerm : this.termPairs.keySet()) { + for (RDLTerm argTerm : this.termPairs.get(dependedTerm)) { + while (dependedTerm instanceof MetaDynamicTerm dynamicTerm) { + dependedTerm = dynamicTerm.allGenerate(depth + 1, maxIndex, maxDepth, context); + } + while (argTerm instanceof MetaDynamicTerm dynamicTerm) { + argTerm = dynamicTerm.allGenerate(depth + 1, maxIndex, maxDepth, context); + } + termPairs.add(dependedTerm); + termPairs.add(argTerm); + index+=2; + } + } + for (int i = 0; i < (maxIndex - index) / 2; i++) { + RDLTerm dependedTerm = generator.generate(i * 2 + index, depth, maxIndex, maxDepth, context); + if (dependedTerm == null) { + break; + } + RDLTerm argTerm = generator.generate(i * 2 + index + 1, depth, maxIndex, maxDepth, context); + if (argTerm == null) { + break; + } + while (dependedTerm instanceof MetaDynamicTerm dynamicTerm) { + dependedTerm = dynamicTerm.generate(depth + 1, maxIndex, maxDepth, context); + } + while (argTerm instanceof MetaDynamicTerm dynamicTerm) { + argTerm = dynamicTerm.generate(depth + 1, maxIndex, maxDepth, context); + } + termPairs.add(dependedTerm); + termPairs.add(argTerm); + } + if (termPairs.isEmpty()) { + return (MetaRDLTerm) dependingTerm; + } + return new MetaDependencyTerm(dependingTerm, termPairs); + } + + @Override + public Set isMatchedBy(RDLTerm another, MatchConstraint constraint, Position position) { + int maxIndex = another.getMaxIndex(); + Set result = new HashSet<>(); + constraint.getContext().put(position, maxIndex); + if (! (Boolean) constraint.getContext().getOrDefault("isDynamicStarted", false)) { + int maxDepth = another.getMaxDepth(); + constraint.getContext().put("isDynamicStarted", true); + for (int i = maxDepth; i > 0; i--) { + MatchConstraint newConstraint = new MatchConstraint(constraint); + newConstraint.getContext().put("maxDepth", i); + MetaRDLTerm metaTerm = generate(position.size(), maxIndex, i, newConstraint.getContext()); + result.addAll(metaTerm.isMatchedBy(another, newConstraint, position)); + } + } else { + int maxDepth = (Integer) constraint.getContext().get("maxDepth"); + MetaRDLTerm metaTerm = generate(position.size(), maxIndex, maxDepth, constraint.getContext()); + result.addAll(metaTerm.isMatchedBy(another, constraint, position)); + } + + return result; + } + + @Override + public RDLTerm substitute(Map binding, Map context, Position position) { + if (! context.containsKey(position)) throw new SubstituteFailedException(); + if (! context.containsKey("maxDepth")) throw new SubstituteFailedException(); + int maxIndex = (int) context.get(position); + int maxDepth = (int) context.get("maxDepth"); + return generate(position.size(), maxIndex, maxDepth, context).substitute(binding, context, position); + } + + + @Override + public String toString() { + if (dependingTerm != null) { + return "[" + getChild(0).toString() + " : " + IntStream.range(0, (getChildren().size() - 1) / 2) + .mapToObj(i -> getChild(i * 2 + 1).toString() + " -> " + getChild(i * 2 + 2)).collect(Collectors.joining(", ")) + " ...? ]"; + } + return "[ ...? ]"; + } + +} diff --git a/src/main/java/models/terms/meta/MetaDynamicTerm.java b/src/main/java/models/terms/meta/MetaDynamicTerm.java index db8f017..17b302a 100644 --- a/src/main/java/models/terms/meta/MetaDynamicTerm.java +++ b/src/main/java/models/terms/meta/MetaDynamicTerm.java @@ -2,11 +2,14 @@ import java.util.Map; -import models.algebra.Variable; - public interface MetaDynamicTerm { - public MetaRDLTerm generate(int depth, Map context); - public MetaRDLTerm generate(int depth, int maxIndex, int maxDepth, Map context); + public MetaRDLTerm generate(int depth, int maxIndex, int maxDepth, Map context); + + public MetaRDLTerm allGenerate(int depht, int maxIndex, int maxDepth, Map context); + + default MetaRDLTerm allGenerate(int maxIndex, int maxDepth, Map context) { + return allGenerate(1, maxIndex, maxDepth, context); + } } diff --git a/src/main/java/models/terms/meta/MetaEvaluatableTermVariable.java b/src/main/java/models/terms/meta/MetaEvaluatableTermVariable.java index 8c19328..9dbaaad 100644 --- a/src/main/java/models/terms/meta/MetaEvaluatableTermVariable.java +++ b/src/main/java/models/terms/meta/MetaEvaluatableTermVariable.java @@ -2,7 +2,6 @@ import models.algebra.Constant; import models.algebra.Expression; -import models.algebra.Symbol; import models.algebra.Variable; import models.terms.LinearRightNormalizedType; @@ -32,4 +31,9 @@ super(MetaRDLTerm.TermType.META_EVALUATABLE_TERM_VARIABLE, variableName, OrderConstraint.EQ, order, linearRIghtNormalizedType); } + @Override + public MetaEvaluatableTermVariable cloneWithName(String name) { + return new MetaEvaluatableTermVariable(new Variable(name), constraint, orderExpression); + } + } diff --git a/src/main/java/models/terms/meta/MetaRDLTerm.java b/src/main/java/models/terms/meta/MetaRDLTerm.java index c1e6b35..edfa5fe 100644 --- a/src/main/java/models/terms/meta/MetaRDLTerm.java +++ b/src/main/java/models/terms/meta/MetaRDLTerm.java @@ -1,15 +1,13 @@ package models.terms.meta; -import java.util.Collection; +import java.util.HashMap; import java.util.HashSet; import java.util.Map; import java.util.Set; -import java.util.stream.Collectors; -import java.util.stream.IntStream; +import exceptions.ReplaceFailedException; import lombok.Getter; -import models.algebra.Expression; -import models.algebra.Symbol; +import models.Position; import models.algebra.Variable; import models.terms.Dependency; import models.terms.DependencyTerm; @@ -17,6 +15,7 @@ import models.terms.LinearRightNormalizedType; import models.terms.RDLTerm; import models.terms.Resource; +import models.terms.ResourceConstant; @Getter public abstract class MetaRDLTerm extends RDLTerm { @@ -33,33 +32,56 @@ public Set isMatchedBy(RDLTerm another) { - return isMatchedBy(another, MatchConstraint.createDefault(), 0); - } - - public Set isMatchedBy(RDLTerm another, MatchConstraint constraint) { - return isMatchedBy(another, constraint, 0); - } - - public Set isMatchedBy(RDLTerm another, Set constraints) { - return isMatchedBy(another, constraints, 0); - } - - protected Set isMatchedBy(RDLTerm another, Set constraints, int depth) { - Set result = new HashSet<>(); - for (MatchConstraint constraint : constraints) { - result.addAll(isMatchedBy(another, constraint, depth + 1)); + Set result = isMatchedBy(another, MatchConstraint.createDefault(), new Position()); + for (MatchConstraint constraint: result) { + constraint.getContext().put("isDynamicStarted", false); } return result; } - abstract protected Set isMatchedBy(RDLTerm another, MatchConstraint constraint, int depth); - - - public RDLTerm substitute(Map binding) { - return substitute(binding, 0); + public Set isMatchedBy(RDLTerm another, Set constraints) { + Set result = new HashSet<>(); + for (MatchConstraint constraint : constraints) { + result.addAll(isMatchedBy(another, constraint, new Position())); + } + for (MatchConstraint constraint: result) { + constraint.getContext().put("isDynamicStarted", false); + } + return result; } - abstract protected RDLTerm substitute(Map binding, int depth); + public Set isMatchedBy(RDLTerm another, MatchConstraint constraint) { + Set result = isMatchedBy(another, constraint, new Position()); + for (MatchConstraint res: result) { + res.getContext().put("isDynamicStarted", false); + } + return result; + } + + protected Set isMatchedBy(RDLTerm another, Set constraints, Position position) { + Set result = new HashSet<>(); + for (MatchConstraint constraint : constraints) { + result.addAll(isMatchedBy(another, constraint, position)); + } + return result; + } + + protected abstract Set isMatchedBy(RDLTerm another, MatchConstraint constraint, Position position); + + @Override + public RDLTerm replace(Position targetPosition, RDLTerm term, Position curPosition) { + throw new ReplaceFailedException(); + } + + public RDLTerm substitute(Map binding) { + return substitute(binding, new HashMap<>(), new Position()); + } + + public RDLTerm substitute(Map binding, Map context) { + return substitute(binding, context, new Position()); + } + + abstract public RDLTerm substitute(Map binding, Map context, Position position); public boolean checkTermType(Class clazz) { @@ -93,8 +115,8 @@ this.linearRightNormalizedType = next; } - public Collection getAllVariables() { - return getSubTerms(MetaVariable.class).values(); + public Set getAllVariables() { + return new HashSet<>(getSubTerms(MetaVariable.class).values()); } protected boolean islinearRightNormalizedMatchedBy(RDLTerm another) { @@ -113,20 +135,24 @@ return true; } + @Override + public Dependency getDependency() { + return null; + } + @Override - public String toString() { - switch(termType) { - case META_DEPENDENCY: - return "[" + getChild(0).toString() + " : " + getChildren().stream().skip(1).map(Expression::toString).collect(Collectors.joining(",")) + "]"; - case META_DEPENDENCY_TERM: - return "[" + getChild(0).toString() + " : " + IntStream.range(0, (getChildren().size() - 1) / 2) - .mapToObj(i -> getChild(i * 2 + 1).toString() + " -> " + getChild(i * 2 + 2)).collect(Collectors.joining(",")) + "]"; - default: - return ""; - } + public int getMaxIndex() { + return -1; } - + + @Override + public int getMaxDepth() { + return -1; + } + + public abstract RDLTerm replace(Map mapping); + @Override public String toStringWithOrder() { switch(termType) { @@ -153,7 +179,7 @@ @Override public int hashCode() { - return (termType.toString() + toStringWithOrder()).hashCode(); + return (termType.toString() + toString()).hashCode(); } @Override @@ -170,7 +196,8 @@ META_DEPENDENCY_TERM(DependencyTerm.class), META_DEPENDENCY_TERM_VARIABLE(DependencyTerm.class), META_EVALUATABLE_TERM_VARIABLE(EvaluatableTerm.class), - META_RESOURCE_VARIABLE(Resource.class); + META_RESOURCE_VARIABLE(Resource.class), + MEAT_CONSTANT_VARIABLE(ResourceConstant.class); @Getter private Class baseTermClass; diff --git a/src/main/java/models/terms/meta/MetaRDLTermVariable.java b/src/main/java/models/terms/meta/MetaRDLTermVariable.java index 75bdeea..0148aef 100644 --- a/src/main/java/models/terms/meta/MetaRDLTermVariable.java +++ b/src/main/java/models/terms/meta/MetaRDLTermVariable.java @@ -2,7 +2,6 @@ import models.algebra.Constant; import models.algebra.Expression; -import models.algebra.Symbol; import models.algebra.Variable; public class MetaRDLTermVariable extends MetaVariable { @@ -19,4 +18,9 @@ super(MetaRDLTerm.TermType.META_RDL_TERM, variableName, OrderConstraint.EQ, order); } + @Override + public MetaRDLTermVariable cloneWithName(String name) { + return new MetaRDLTermVariable(new Variable(name), constraint, orderExpression); + } + } diff --git a/src/main/java/models/terms/meta/MetaResource.java b/src/main/java/models/terms/meta/MetaResource.java index fbdc3c3..6602702 100644 --- a/src/main/java/models/terms/meta/MetaResource.java +++ b/src/main/java/models/terms/meta/MetaResource.java @@ -1,17 +1,9 @@ package models.terms.meta; -import java.util.HashSet; -import java.util.Map; -import java.util.Set; - import lombok.Getter; import models.algebra.Constant; import models.algebra.Expression; -import models.algebra.Symbol; import models.algebra.Variable; -import models.terms.RDLTerm; -import models.terms.Resource; -import models.terms.ResourceConstant; @Getter public class MetaResource extends MetaVariable { @@ -28,30 +20,36 @@ super(MetaRDLTerm.TermType.META_RESOURCE_VARIABLE, variableName, OrderConstraint.EQ, order); } +// @Override +// public Set isMatchedBy(RDLTerm another, MatchConstraint constraint) { +// Set result = new HashSet<>(); +// Map binding = constraint.getBinding(); +// Map orderConstraint = constraint.getOrderConstraint(); +// if ((! (another instanceof Resource)) && (! (another instanceof ResourceConstant))) { +// return result; +// } +// +// if (! orderConstraintCheck(another, orderConstraint)) { +// return result; +// } +// +// if (! islinearRightNormalizedMatchedBy(another)) { +// return result; +// } +// +// if (! binding.containsKey(this.variableName)) { +// binding.put(this.variableName, another); +// result.add(new MatchConstraint(binding, orderConstraint, constraint.cloneContext())); +// } +// else if (binding.get(this.variableName).equals(another)) { +// result.add(new MatchConstraint(binding, orderConstraint, constraint.cloneContext())); +// } +// return result; +// } + @Override - public Set isMatchedBy(RDLTerm another, MatchConstraint constraint) { - Set result = new HashSet<>(); - Map binding = constraint.getBinding(); - Map orderConstraint = constraint.getOrderConstraint(); - if ((! (another instanceof Resource)) && (! (another instanceof ResourceConstant))) { - return result; - } - - if (! orderConstraintCheck(another, orderConstraint)) { - return result; - } - - if (! islinearRightNormalizedMatchedBy(another)) { - return result; - } - - if (! binding.containsKey(this.variableName)) { - binding.put(this.variableName, another); - result.add(new MatchConstraint(binding, orderConstraint)); - } - else if (binding.get(this.variableName).equals(another)) { - result.add(new MatchConstraint(binding, orderConstraint)); - } - return result; + public MetaResource cloneWithName(String name) { + return new MetaResource(new Variable(name), constraint, orderExpression); } + } diff --git a/src/main/java/models/terms/meta/MetaTermGenerator.java b/src/main/java/models/terms/meta/MetaTermGenerator.java index 44a5c36..9ba6fe6 100644 --- a/src/main/java/models/terms/meta/MetaTermGenerator.java +++ b/src/main/java/models/terms/meta/MetaTermGenerator.java @@ -2,11 +2,9 @@ import java.util.Map; -import models.algebra.Variable; - @FunctionalInterface public interface MetaTermGenerator { - MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context); + MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context); } diff --git a/src/main/java/models/terms/meta/MetaTermPairGenerator.java b/src/main/java/models/terms/meta/MetaTermPairGenerator.java deleted file mode 100644 index d8837eb..0000000 --- a/src/main/java/models/terms/meta/MetaTermPairGenerator.java +++ /dev/null @@ -1,10 +0,0 @@ -package models.terms.meta; - -@FunctionalInterface -public interface MetaTermPairGenerator { - - record TermPair(MetaRDLTerm dependedTerm, MetaRDLTerm argTerm) {}; - - TermPair generate(int index, int depth, boolean isLast); - -} diff --git a/src/main/java/models/terms/meta/MetaVariable.java b/src/main/java/models/terms/meta/MetaVariable.java index 89a4bbe..08f043a 100644 --- a/src/main/java/models/terms/meta/MetaVariable.java +++ b/src/main/java/models/terms/meta/MetaVariable.java @@ -9,12 +9,12 @@ import exceptions.SubstituteFailedException; import exceptions.TooManyVariablesException; import lombok.Getter; +import models.Position; import models.algebra.Expression; -import models.algebra.Symbol; import models.algebra.Variable; import models.terms.LinearRightNormalizedType; import models.terms.RDLTerm; -import utils.ExpressionUitls; +import utils.ExpressionUtils; @Getter public abstract class MetaVariable extends MetaRDLTerm { @@ -31,7 +31,7 @@ this.constraint = constraint; this.orderExpression = order; Map coefficients = new HashMap<>(); - int constant = ExpressionUitls.getCoefficientAndConstantsFromExpression(order, coefficients, 1); + int constant = ExpressionUtils.getCoefficientAndConstantsFromExpression(order, coefficients, 1); if (coefficients.size() > 1) { // todo: create exception throw new TooManyVariablesException("Too many variables"); @@ -53,7 +53,7 @@ this.constraint = constraint; this.orderExpression = order; Map coefficients = new HashMap<>(); - int constant = ExpressionUitls.getCoefficientAndConstantsFromExpression(order, coefficients, 1); + int constant = ExpressionUtils.getCoefficientAndConstantsFromExpression(order, coefficients, 1); if (coefficients.size() > 1) { // todo: create exception throw new TooManyVariablesException("Too many variables"); @@ -76,7 +76,7 @@ } @Override - public Set isMatchedBy(RDLTerm another, MatchConstraint constraint, int depth) { + public Set isMatchedBy(RDLTerm another, MatchConstraint constraint, Position position) { Set result = new HashSet<>(); Map binding = constraint.getBinding(); Map orderConstraint = constraint.getOrderConstraint(); @@ -94,16 +94,16 @@ if (! binding.containsKey(this.variableName)) { binding.put(this.variableName, another); - result.add(new MatchConstraint(binding, orderConstraint)); + result.add(new MatchConstraint(binding, orderConstraint, constraint.cloneContext())); } else if (binding.get(this.variableName).equals(another)) { - result.add(new MatchConstraint(binding, orderConstraint)); + result.add(new MatchConstraint(binding, orderConstraint, constraint.cloneContext())); } return result; } @Override - public RDLTerm substitute(Map binding, int depth) { + public RDLTerm substitute(Map binding, Map context, Position position) { if (binding.containsKey(variableName)) { return binding.get(variableName); } @@ -136,7 +136,19 @@ return false; } + public abstract MetaVariable cloneWithName(String name); + @Override + public RDLTerm replace(Map mapping) { + RDLTerm v = this; + if (mapping.containsKey(v)) { + v = mapping.get(v); + if (v instanceof MetaRDLTerm metaTerm) { + v = metaTerm.replace(mapping); + } + } + return v; + } @Override diff --git a/src/main/java/utils/ExpressionUitls.java b/src/main/java/utils/ExpressionUitls.java deleted file mode 100644 index d223bcf..0000000 --- a/src/main/java/utils/ExpressionUitls.java +++ /dev/null @@ -1,81 +0,0 @@ -package utils; - -import java.util.Map; - -import constants.Symbols; -import exceptions.NonLinearExpressionException; -import models.algebra.Constant; -import models.algebra.Expression; -import models.algebra.Symbol; -import models.algebra.Term; -import models.algebra.Variable; -import parser.Parser; -import parser.Parser.TokenStream; - -public class ExpressionUitls { - - - public static int getCoefficientAndConstantsFromExpression(Expression expression, Map coefficients, int curWeight) { - int res = 0; - if(expression instanceof Constant) { - return getConstantValue((Constant) expression) * curWeight; - } else if(expression instanceof Variable) { - coefficients.put((Variable) expression, coefficients.getOrDefault((Variable) expression, 0) + curWeight); - return 0; - } - Term term = (Term) expression; - Symbol symbol = term.getSymbol(); - if(symbol.equals(Symbols.add)) { - Expression c1 = term.getChild(0); - Expression c2 = term.getChild(1); - res += getCoefficientAndConstantsFromExpression(c1, coefficients, curWeight); - res += getCoefficientAndConstantsFromExpression(c2, coefficients, curWeight); - } else if(symbol.equals(Symbols.sub)) { - Expression c1 = term.getChild(0); - Expression c2 = term.getChild(1); - res += getCoefficientAndConstantsFromExpression(c1, coefficients, curWeight); - res += getCoefficientAndConstantsFromExpression(c2, coefficients, -curWeight); - } else if(symbol.equals(Symbols.mul)) { - Expression c1 = term.getChild(0); - Expression c2 = term.getChild(1); - if(c1.getVariables().size() == 0 && c2.getVariables().size() == 0) { - res += getCoefficientAndConstantsFromExpression(c1, coefficients, curWeight) * - getCoefficientAndConstantsFromExpression(c2, coefficients, curWeight); - } else if(c1.getVariables().size() == 0) { - res += getCoefficientAndConstantsFromExpression( - c2, - coefficients, - getCoefficientAndConstantsFromExpression(c1, coefficients, curWeight) - ); - } else if(c2.getVariables().size() == 0){ - res += getCoefficientAndConstantsFromExpression( - c1, - coefficients, - getCoefficientAndConstantsFromExpression(c2, coefficients, curWeight) - ); - } else { - throw new NonLinearExpressionException("Order expression must be linear expression."); - } - } else if(symbol.equals(Symbols.minus)) { - Expression c1 = term.getChild(0); - res += getCoefficientAndConstantsFromExpression(c1, coefficients, -curWeight); - } else { - throw new NonLinearExpressionException("Order expression must be linear expression."); - } - return res; - - } - - public static int getConstantValue(Constant constant) { - return Integer.parseInt((String) constant.getValue()); - } - - private static TokenStream stream = new Parser.TokenStream(); - private static Parser parser = new Parser(stream); - - public static Expression parse(String expr) { - stream.addLine(expr); - return parser.parseTerm(stream); - } - -} diff --git a/src/main/java/utils/ExpressionUtils.java b/src/main/java/utils/ExpressionUtils.java new file mode 100644 index 0000000..0277794 --- /dev/null +++ b/src/main/java/utils/ExpressionUtils.java @@ -0,0 +1,81 @@ +package utils; + +import java.util.Map; + +import constants.Symbols; +import exceptions.NonLinearExpressionException; +import models.algebra.Constant; +import models.algebra.Expression; +import models.algebra.Symbol; +import models.algebra.Term; +import models.algebra.Variable; +import parser.Parser; +import parser.Parser.TokenStream; + +public class ExpressionUtils { + + + public static int getCoefficientAndConstantsFromExpression(Expression expression, Map coefficients, int curWeight) { + int res = 0; + if(expression instanceof Constant) { + return getConstantValue((Constant) expression) * curWeight; + } else if(expression instanceof Variable) { + coefficients.put((Variable) expression, coefficients.getOrDefault((Variable) expression, 0) + curWeight); + return 0; + } + Term term = (Term) expression; + Symbol symbol = term.getSymbol(); + if(symbol.equals(Symbols.add)) { + Expression c1 = term.getChild(0); + Expression c2 = term.getChild(1); + res += getCoefficientAndConstantsFromExpression(c1, coefficients, curWeight); + res += getCoefficientAndConstantsFromExpression(c2, coefficients, curWeight); + } else if(symbol.equals(Symbols.sub)) { + Expression c1 = term.getChild(0); + Expression c2 = term.getChild(1); + res += getCoefficientAndConstantsFromExpression(c1, coefficients, curWeight); + res += getCoefficientAndConstantsFromExpression(c2, coefficients, -curWeight); + } else if(symbol.equals(Symbols.mul)) { + Expression c1 = term.getChild(0); + Expression c2 = term.getChild(1); + if(c1.getVariables().size() == 0 && c2.getVariables().size() == 0) { + res += getCoefficientAndConstantsFromExpression(c1, coefficients, curWeight) * + getCoefficientAndConstantsFromExpression(c2, coefficients, curWeight); + } else if(c1.getVariables().size() == 0) { + res += getCoefficientAndConstantsFromExpression( + c2, + coefficients, + getCoefficientAndConstantsFromExpression(c1, coefficients, curWeight) + ); + } else if(c2.getVariables().size() == 0){ + res += getCoefficientAndConstantsFromExpression( + c1, + coefficients, + getCoefficientAndConstantsFromExpression(c2, coefficients, curWeight) + ); + } else { + throw new NonLinearExpressionException("Order expression must be linear expression."); + } + } else if(symbol.equals(Symbols.minus)) { + Expression c1 = term.getChild(0); + res += getCoefficientAndConstantsFromExpression(c1, coefficients, -curWeight); + } else { + throw new NonLinearExpressionException("Order expression must be linear expression."); + } + return res; + + } + + public static int getConstantValue(Constant constant) { + return Integer.parseInt((String) constant.getValue()); + } + + private static TokenStream stream = new Parser.TokenStream(); + private static Parser parser = new Parser(stream); + + public static Expression parse(String expr) { + stream.addLine(expr); + return parser.parseTerm(stream); + } + +} diff --git a/src/test/java/inference/DependencyInferenceTest.java b/src/test/java/inference/DependencyInferenceTest.java new file mode 100644 index 0000000..172d382 --- /dev/null +++ b/src/test/java/inference/DependencyInferenceTest.java @@ -0,0 +1,124 @@ +package inference; + +import static org.junit.jupiter.api.Assertions.*; + +import java.util.Set; + +import org.junit.jupiter.api.Test; + +import models.formulas.DependencyFormula; +import models.formulas.EquationFormula; +import models.terms.Dependency; +import models.terms.DependencyTerm; +import models.terms.Resource; + +public class DependencyInferenceTest { + + 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); + + @Test + void IdentityMappingInferenceTest() { + EquationFormula eq1 = new EquationFormula(a, b); + DependencyFormula d1 = new DependencyFormula(a, b); + ProofSystem ps = new ProofSystem(Set.of(eq1), d1); + assertTrue(ps.dependencyInference()); + } + + @Test + void ArgumentExtensionInferenceTest() { + DependencyFormula d1 = new DependencyFormula(a, b); + DependencyFormula d2 = new DependencyFormula(a, b, c); + DependencyFormula d3 = new DependencyFormula(a, b, c, d, e); + ProofSystem ps = new ProofSystem(Set.of(d1), d2); + assertFalse(ps.dependencyInference()); + ProofSystem ps2 = new ProofSystem(Set.of(d1), d2, Set.of(c)); + assertTrue(ps2.dependencyInference()); + ProofSystem ps3 = new ProofSystem(Set.of(d1), d3, Set.of(c, d, e)); + assertTrue(ps3.dependencyInference()); + } + + @Test + void ArgumentReductionInferenceTest() { + DependencyFormula d1 = new DependencyFormula(a, b, c); + DependencyFormula d2 = new DependencyFormula(b, c); + DependencyFormula d3 = new DependencyFormula(a, c); + ProofSystem ps = new ProofSystem(Set.of(d1, d2), d3); + assertTrue(ps.dependencyInference()); + + DependencyFormula d4 = new DependencyFormula(a, b, b); + EquationFormula eq1 = new EquationFormula(b, b); + DependencyFormula d5 = new DependencyFormula(a, b); + ProofSystem ps2 = new ProofSystem(Set.of(d4, eq1), d5); + assertTrue(ps2.dependencyInference()); + + DependencyFormula d6 = new DependencyFormula(new Dependency(a, b, b), c, d); + ProofSystem ps3 = new ProofSystem(Set.of(d6, eq1), new DependencyFormula(new Dependency(a, b), c, d)); + assertTrue(ps3.dependencyInference()); + System.out.println(ps3.getInferenceHistoryString()); + + } + + @Test + void CompositeMappingInferenceTest() { + DependencyFormula d1 = new DependencyFormula(a, b); + DependencyFormula d2 = new DependencyFormula(b, c, d); + DependencyFormula d3 = new DependencyFormula(a, c, d); + ProofSystem ps = new ProofSystem(Set.of(d1, d2), d3); + assertTrue(ps.dependencyInference()); + + DependencyFormula d4 = new DependencyFormula(new Dependency(a, b), c); + DependencyFormula d5 = new DependencyFormula(b, d); + ProofSystem ps2 = new ProofSystem(Set.of(d4, d5), new DependencyFormula(new Dependency(a, d), c)); + assertTrue(ps2.dependencyInference()); + + } + + @Test + void ConstantMappingInferenceTest() { + DependencyFormula d1 = new DependencyFormula(a, f); + ProofSystem ps = new ProofSystem(Set.of(), d1, Set.of(a, f)); + assertTrue(ps.dependencyInference()); + + DependencyFormula d2 = new DependencyFormula(a, f, g); + ProofSystem ps2 = new ProofSystem(Set.of(), d2, Set.of(a, b, f, g)); + assertTrue(ps2.dependencyInference()); + } + + @Test + void UncurriedMappingInferenceTest() { + DependencyFormula d1 = new DependencyFormula(new Dependency(f, g), a); + DependencyFormula d2 = new DependencyFormula(new DependencyTerm(f, g, b), a, b); + ProofSystem ps = new ProofSystem(Set.of(d1), d2, Set.of(b)); + assertTrue(ps.dependencyInference()); + + DependencyFormula d3 = new DependencyFormula(new Dependency(new Dependency(h, i), f, g), a); + DependencyFormula d4 = new DependencyFormula(new Dependency(new DependencyTerm(h, i, b), f, g), a, b); + ProofSystem ps2 = new ProofSystem(Set.of(d3), d4, Set.of(b)); + assertTrue(ps2.dependencyInference()); + + DependencyFormula d5 = new DependencyFormula(new Dependency(new Dependency(h, i), f), a); + DependencyFormula d6 = new DependencyFormula(new Dependency(new DependencyTerm(h, i, g), f, g), a); + ProofSystem ps3 = new ProofSystem(Set.of(d5), d6, Set.of(g)); + assertTrue(ps3.dependencyInference()); + } + + @Test + void DependencyExtensionInferenceTest() { + DependencyFormula d1 = new DependencyFormula(f, g); + ProofSystem ps1 = new ProofSystem(Set.of(d1), new DependencyFormula(new Dependency(f, g), a), Set.of(a)); + assertTrue(ps1.dependencyInference()); + + ProofSystem ps2 = new ProofSystem(Set.of(d1), new DependencyFormula(new Dependency(f, g), a, b, c), Set.of(a, b, c, d)); + assertTrue(ps2.dependencyInference()); + + } + +} 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/inference/inferencerule/DependencyAxiomTest.java b/src/test/java/inference/inferencerule/DependencyAxiomTest.java new file mode 100644 index 0000000..56cdaf5 --- /dev/null +++ b/src/test/java/inference/inferencerule/DependencyAxiomTest.java @@ -0,0 +1,134 @@ +package inference.inferencerule; +import static org.junit.jupiter.api.Assertions.*; + +import java.util.List; +import java.util.Set; + +import org.junit.jupiter.api.Test; + +import inference.ProofSystem; +import models.Position; +import models.algebra.Variable; +import models.formulas.DependencyFormula; +import models.formulas.EquationFormula; +import models.formulas.Formula; +import models.terms.Dependency; +import models.terms.DependencyTerm; +import models.terms.Resource; +import models.terms.ResourceConstant; +import models.terms.meta.MatchConstraint; + +public class DependencyAxiomTest { + + 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); + Resource h = new Resource("h", 1); + Resource i = new Resource("i", 1); + Resource j = new Resource("j", 1); + Resource k = new Resource("k", 1); + Resource l = new Resource("l", 2); + Resource m = new Resource("m", 2); + + @Test + void IdentityMappingTest() { + Set res = ProofSystem.identityMapping.derive(List.of(new EquationFormula(a, b))); + assertTrue(res.contains(new DependencyFormula(a, b))); + } + + @Test + void ArgumentExtensionTest() { + MatchConstraint constraint = MatchConstraint.createDefault(); + constraint.setBinding(new Variable("ue"), d); + Set res = ProofSystem.argumentExtension.derive(List.of(new DependencyFormula(a, b, c)), constraint); + assertTrue(res.contains(new DependencyFormula(a, b, c, d))); + } + + @Test + void ArgumentReductionTest() { + DependencyFormula d1 = new DependencyFormula(a, b, c); + DependencyFormula d2 = new DependencyFormula(d, a, b, c, e, f); + Set res = ProofSystem.argumentReduction.derive(List.of(d1, d2)); + assertTrue(res.contains(new DependencyFormula(d, b, c, e, f))); + } + + @Test + void ArgumentConstraintTest() { + DependencyTerm t1 = new DependencyTerm(a, b, c, d, e, f, g, h, i); + EquationFormula eq1 = new EquationFormula(t1, new ResourceConstant("0")); + DependencyFormula d1 = new DependencyFormula(b, d, f); + Set res = ProofSystem.argumentConstraint.derive(List.of(eq1, d1)); + DependencyTerm t2 = new DependencyTerm(b, d, e, f, g); + assertTrue(res.contains(new EquationFormula(t2, c))); + } + + @Test + void CompositeMappingTest() { + DependencyFormula d1 = new DependencyFormula(a, b, c, d); + DependencyFormula d2 = new DependencyFormula(e, a, f, g, h); + Set res = ProofSystem.compositeMapping.derive(List.of(d1, d2)); + assertTrue(res.contains(new DependencyFormula(e, b, c, d, f, g, h))); + } + + @Test + void ConstantMappingTest() { + MatchConstraint constraint = MatchConstraint.createDefault(); + constraint.getContext().put(new Position(), 3); + constraint.setBinding(new Variable("se"), a); + constraint.setBinding(new Variable("te0"), l); + constraint.setBinding(new Variable("te1"), m); + constraint.getContext().put("maxDepth", 1); + Set res = ProofSystem.constantMapping.derive(List.of(), constraint); + assertTrue(res.contains(new DependencyFormula(a, l, m))); + } + + @Test + void ConstantMapping1Test() { + Set res = ProofSystem.constantMapping1.derive(List.of(), Set.of(a, m)); + assertTrue(res.contains(new DependencyFormula(a, m))); + Set res2 = ProofSystem.constantMapping1.derive(List.of(), Set.of(a, b)); + assertFalse(res2.contains(new DependencyFormula(a, b))); + } + + @Test + void UncurriedMappingTest() { + Resource a = new Resource("a", 4); + Resource b = new Resource("b", 4); + Resource d = new Resource("d", 3); + Resource e = new Resource("e", 3); + Resource f = new Resource("f", 3); + Resource g = new Resource("g", 3); + Resource h = new Resource("h", 2); + Resource i = new Resource("i", 2); + Resource x = new Resource("x", 2); + DependencyFormula d1 = new DependencyFormula(new Dependency(new Dependency(new Dependency(a, b), d, e, f, g), h, i)); + MatchConstraint constraint = MatchConstraint.createDefault(); + constraint.setBinding(new Variable("ve"), x); + Set res = ProofSystem.uncurriedMapping.derive(List.of(d1), constraint); + DependencyFormula d2 = new DependencyFormula(new Dependency(new Dependency(new DependencyTerm(a, b, x), d, e, f, g), h, i, x)); + assertTrue(res.contains(d2)); + } + + @Test + void DependencyExtensionTest() { + Resource a = new Resource("a", 4); + Resource b = new Resource("b", 4); + Resource d = new Resource("d", 4); + Resource e = new Resource("e", 3); + Resource f = new Resource("f", 3); + DependencyFormula d1 = new DependencyFormula(a, b, d); + DependencyFormula d2 = new DependencyFormula(d1.getDependency(), e); + MatchConstraint constraint = MatchConstraint.createDefault(); + constraint.getContext().put("j", 1); + constraint.setBinding(new Variable("ue"), e); + constraint.setBinding(new Variable("ue1"), f); + Set res = ProofSystem.dependencyExtension.derive(List.of(d1), constraint); + assertTrue(res.contains(d2)); + } + + +} diff --git a/src/test/java/inference/inferencerule/EqualityAxiomTest.java b/src/test/java/inference/inferencerule/EqualityAxiomTest.java new file mode 100644 index 0000000..87e0ea9 --- /dev/null +++ b/src/test/java/inference/inferencerule/EqualityAxiomTest.java @@ -0,0 +1,137 @@ +package inference.inferencerule; +import static org.junit.jupiter.api.Assertions.*; + +import java.util.HashSet; +import java.util.List; +import java.util.Set; + +import org.junit.jupiter.api.Test; + +import inference.ProofSystem; +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.RDLTerm; +import models.terms.Resource; +import models.terms.meta.MatchConstraint; + +public class EqualityAxiomTest { + + 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); + Resource h = new Resource("h", 1); + Resource i = new Resource("i", 1); + Resource j = new Resource("j", 1); + Resource k = new Resource("k", 1); + Resource l = new Resource("l", 1); + Resource m = new Resource("m", 2); + Resource n = new Resource("n", 2); + Resource o = new Resource("o", 3); + Resource p = new Resource("p", 3); + Resource q = new Resource("q", 3); + + @Test + void ReflexivityTest() { + Set terms = new HashSet<>(); + terms.add(a); + terms.add(b); + Set formulas = ProofSystem.reflexivity.apply(List.of(), a); + assertTrue(formulas.contains(a)); + } + + @Test + void SymmetryTest() { + Set formulas = ProofSystem.symmetry.apply(List.of(new EquationFormula(a, b)), a); + assertTrue(formulas.contains(b)); + formulas = ProofSystem.symmetry.apply(List.of(new EquationFormula(a, b)), b); + assertTrue(formulas.contains(a)); + } + + @Test + void TransitivityTest() { + Set formulas = ProofSystem.transitivity.apply(List.of(new EquationFormula(a, b), new EquationFormula(b, c)), c); + assertTrue(formulas.contains(a)); + } + + @Test + void RightSubTest() { + EquationFormula eq1 = new EquationFormula(a, b); + DependencyFormula d1 = new DependencyFormula(c, d); + Set formulas = ProofSystem.rightSubstitution.apply(List.of(eq1, d1), new DependencyTerm(c, d, a)); + assertTrue(formulas.contains(new DependencyTerm(c, d, b))); + } + + @Test + void LeftSubTest() { + EquationFormula eq1 = new EquationFormula(a, b); + Set formulas = ProofSystem.leftSubstitution.apply(List.of(eq1), new DependencyTerm(a, c, d)); + assertTrue(formulas.contains(new DependencyTerm(b, c, d))); + formulas = ProofSystem.leftSubstitution.apply(List.of(eq1), new DependencyTerm(b, c, d)); + assertTrue(formulas.contains(new DependencyTerm(a, c, d))); + + } + + @Test + void IdentityTest() { + Set terms = ProofSystem.identity.apply(List.of(), new DependencyTerm(a, a, b)); + assertTrue(terms.contains(b)); + } + + @Test + void MapCompositionTest() { + DependencyFormula d1 = new DependencyFormula(a, b, c); + DependencyFormula d2 = new DependencyFormula(b, d, e); + DependencyTerm dt1 = new DependencyTerm(a, d, f, e, g, c, h); + DependencyTerm dt2 = new DependencyTerm(a, b, new DependencyTerm(b, d, f, e, g), c, h); + Set terms = ProofSystem.mapComposition.apply(List.of(d1, d2), dt1); + assertTrue(terms.contains(dt2)); + terms = ProofSystem.mapComposition.apply(List.of(d1, d2), dt2); + assertTrue(terms.contains(dt1)); + } + + @Test + void ConstantnessTest() { + DependencyTerm dt1 = new DependencyTerm(new DependencyTerm(a, o, b), m, c); + DependencyTerm dt2 = new DependencyTerm(a, m, b); + Set terms = ProofSystem.constantness.apply(List.of(), dt1); + assertTrue(terms.contains(a)); + terms = ProofSystem.constantness.apply(List.of(), dt2); + assertTrue(terms.contains(a)); + } + + @Test + void RightNormalizationTest() { + } + + @Test + void PseudoConstantnessTest() { + DependencyFormula d1 = new DependencyFormula(a, b, c); + DependencyTerm dt1 = new DependencyTerm(a, b, b, c, c); + Set terms = ProofSystem.pseudoConstantness.apply(List.of(d1), dt1); + assertTrue(terms.contains(a)); + terms = ProofSystem.pseudoConstantness.apply(List.of(d1), a); + assertTrue(terms.contains(dt1)); + } + + @Test + void UncurryingTest() { + DependencyFormula d1 = new DependencyFormula(new Dependency(new Dependency(o, p, q), n, m), a, b, c); + DependencyTerm dt1 = new DependencyTerm(new DependencyTerm(new DependencyTerm(o, p, d, q, e), n, f, m ,g), a, h, b, i, c, j); + DependencyTerm dt2 = new DependencyTerm(new DependencyTerm(new DependencyTerm(o, p, k, q, e), n, f, m ,g), a, h, b, i, c, j, k, d); + MatchConstraint constraint = MatchConstraint.createDefault(); + constraint.setBinding(new Variable("ve"), k); + Set terms = ProofSystem.uncurrying.apply(List.of(d1), dt1, constraint); + assertTrue(terms.contains(dt2)); + terms = ProofSystem.uncurrying.apply(List.of(d1), dt2); + assertTrue(terms.contains(dt1)); + } + +} diff --git a/src/test/java/inferencerule/DependencyAxiomTest.java b/src/test/java/inferencerule/DependencyAxiomTest.java deleted file mode 100644 index 9b62347..0000000 --- a/src/test/java/inferencerule/DependencyAxiomTest.java +++ /dev/null @@ -1,16 +0,0 @@ -package inferencerule; -import models.terms.Resource; -import utils.Utils; - -public class DependencyAxiomTest { - - 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", 2); - -} diff --git a/src/test/java/inferencerule/EqualityAxiomTest.java b/src/test/java/inferencerule/EqualityAxiomTest.java deleted file mode 100644 index a3e0efa..0000000 --- a/src/test/java/inferencerule/EqualityAxiomTest.java +++ /dev/null @@ -1,20 +0,0 @@ -package inferencerule; -import models.terms.Resource; -import utils.Utils; - -public class EqualityAxiomTest { - - 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); - Resource h = new Resource("h", 2); - Resource i = new Resource("i", 2); - Resource j = new Resource("j", 2); - Resource k = new Resource("k", 2); - Resource l = new Resource("l", 1); - -} diff --git a/src/test/java/inferencerule/InferenceRuleTest.java b/src/test/java/inferencerule/InferenceRuleTest.java deleted file mode 100644 index 57deb71..0000000 --- a/src/test/java/inferencerule/InferenceRuleTest.java +++ /dev/null @@ -1,5 +0,0 @@ -package inferencerule; - -public class InferenceRuleTest { - -} diff --git a/src/test/java/rewrite/RewriteInferenceTest.java b/src/test/java/rewrite/RewriteInferenceTest.java index d0d9adb..74d708a 100644 --- a/src/test/java/rewrite/RewriteInferenceTest.java +++ b/src/test/java/rewrite/RewriteInferenceTest.java @@ -1,107 +1,107 @@ -package rewrite; -import static org.junit.jupiter.api.Assertions.*; - -import org.junit.jupiter.api.Test; - -import java.util.List; - -import inference.rewrite.RewriteInferenceSystem; -import models.formulas.EquationFormula; -import models.formulas.Then; -import models.terms.DependencyTerm; -import models.terms.PrimedTerm; -import models.terms.Resource; -import utils.Utils; - -public class RewriteInferenceTest { - - @Test - void RewriteInferenceTest1() { - Resource totalAmount = new Resource("totalAmount", 1); - Resource quantity = new Resource("quantity", 1); - Resource unitPrice = new Resource("unitPrice", 1); - Resource productId = new Resource("productID", 1); - Resource productName = new Resource("productName", 1); - Resource soledProductId = new Resource("soledProductId", 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", 0); - Resource b = new Resource("b", 0); - Resource c = new Resource("c", 0); - Resource d = new Resource("d", 0); - Resource e = new Resource("e", 0); - Resource salesId = new Resource("salesId", 1); - PrimedTerm salesIdP = new PrimedTerm(salesId); - Resource mul = new Resource("mul", 1); - Resource mul1= new Resource("mul1", 1); - Resource mul2 = new Resource("mul2", 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); - - //value copy change value - RewriteInferenceSystem ris = new RewriteInferenceSystem(List.of(eq9, eq10, eq11, eq12, eq13, eq14), eq15); - assertTrue(ris.inference()); - - //reference conclusion - DependencyTerm te13 = new DependencyTerm(soledProductId, salesId, a); - EquationFormula eq16 = new EquationFormula(d, te13); - Then th1 = new Then(eq16, eq15); - - //reference change value - RewriteInferenceSystem ris2 = new RewriteInferenceSystem(List.of(eq1, eq2, eq9, eq10, eq11, eq12, eq13), th1); - - assertFalse(ris2.inference()); - } - -} +//package rewrite; +//import static org.junit.jupiter.api.Assertions.*; +// +//import org.junit.jupiter.api.Test; +// +//import java.util.List; +// +//import inference.rewrite.RewriteInferenceSystem; +//import models.formulas.EquationFormula; +//import models.formulas.Then; +//import models.terms.DependencyTerm; +//import models.terms.PrimedTerm; +//import models.terms.Resource; +//import utils.Utils; +// +//public class RewriteInferenceTest { +// +// @Test +// void RewriteInferenceTest1() { +// Resource totalAmount = new Resource("totalAmount", 1); +// Resource quantity = new Resource("quantity", 1); +// Resource unitPrice = new Resource("unitPrice", 1); +// Resource productId = new Resource("productID", 1); +// Resource productName = new Resource("productName", 1); +// Resource soledProductId = new Resource("soledProductId", 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", 0); +// Resource b = new Resource("b", 0); +// Resource c = new Resource("c", 0); +// Resource d = new Resource("d", 0); +// Resource e = new Resource("e", 0); +// Resource salesId = new Resource("salesId", 1); +// PrimedTerm salesIdP = new PrimedTerm(salesId); +// Resource mul = new Resource("mul", 1); +// Resource mul1= new Resource("mul1", 1); +// Resource mul2 = new Resource("mul2", 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); +// +// //value copy change value +// RewriteInferenceSystem ris = new RewriteInferenceSystem(List.of(eq9, eq10, eq11, eq12, eq13, eq14), eq15); +// assertTrue(ris.inference()); +// +// //reference conclusion +// DependencyTerm te13 = new DependencyTerm(soledProductId, salesId, a); +// EquationFormula eq16 = new EquationFormula(d, te13); +// Then th1 = new Then(eq16, eq15); +// +// //reference change value +// RewriteInferenceSystem ris2 = new RewriteInferenceSystem(List.of(eq1, eq2, eq9, eq10, eq11, eq12, eq13), th1); +// +// assertFalse(ris2.inference()); +// } +// +//} diff --git a/src/test/java/terms/DependencyTermTest.java b/src/test/java/terms/DependencyTermTest.java index 13a9fb4..114c288 100644 --- a/src/test/java/terms/DependencyTermTest.java +++ b/src/test/java/terms/DependencyTermTest.java @@ -5,9 +5,10 @@ import org.junit.jupiter.api.Test; import exceptions.SyntaxException; +import models.Position; +import models.terms.Dependency; import models.terms.DependencyTerm; import models.terms.Resource; -import utils.Utils; public class DependencyTermTest { @@ -75,6 +76,64 @@ DependencyTerm t5 = new DependencyTerm(a, b, c, b, c); assertEquals(t5.toString(), "[a : b -> c, b -> c]"); + } + + @Test + void MaxIndexAndMaxDepthTest() { + DependencyTerm t1 = new DependencyTerm(a, b, c); + assertEquals(t1.getMaxIndex(), 3); + assertEquals(t1.getMaxDepth(), 1); + + DependencyTerm t2 = new DependencyTerm(a, b, c, d, e); + assertEquals(t2.getMaxIndex(), 5); + assertEquals(t2.getMaxDepth(), 1); + + DependencyTerm t3 = new DependencyTerm(t2, f, g); + assertEquals(t3.getMaxIndex(), 3); + assertEquals(t3.getMaxDepth(), 2); + + DependencyTerm t4 = new DependencyTerm(t3, t1, t2); + assertEquals(t4.getMaxIndex(), 3); + assertEquals(t4.getMaxDepth(), 3); + + } + + @Test + void ReplaceTest() { + DependencyTerm t1 = new DependencyTerm(a, b, c); + assertEquals(t1.replace(new Position(0, 1), d), new DependencyTerm(a, d, c)); + + DependencyTerm t2 = new DependencyTerm(t1, d, e); + 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); } diff --git a/src/test/java/terms/DependencyTest.java b/src/test/java/terms/DependencyTest.java index c146330..e7c8200 100644 --- a/src/test/java/terms/DependencyTest.java +++ b/src/test/java/terms/DependencyTest.java @@ -4,9 +4,9 @@ import org.junit.jupiter.api.Test; import exceptions.SyntaxException; +import models.Position; import models.terms.Dependency; import models.terms.Resource; -import utils.Utils; public class DependencyTest { @@ -75,4 +75,35 @@ assertEquals(d4.toString(), "a : b, b, c, e"); } + @Test + void MaxIndexAndMaxDepthTest() { + Dependency d1 = new Dependency(a, b); + assertEquals(d1.getMaxIndex(), 2); + assertEquals(d1.getMaxDepth(), 1); + + Dependency d2 = new Dependency(d1, c); + assertEquals(d2.getMaxIndex(), 2); + assertEquals(d2.getMaxDepth(), 2); + + Dependency d3 = new Dependency(d2, e, f); + assertEquals(d3.getMaxIndex(), 3); + assertEquals(d3.getMaxDepth(), 3); + + } + + @Test + void ReplaceTest() { + Dependency d1 = new Dependency(a, b); + Dependency d2 = (Dependency) d1.replace(new Position(0, 0), c); + assertEquals(d2, new Dependency(c, b)); + + Dependency d3 = new Dependency(d1, c); + Dependency d4 = (Dependency) d3.replace(new Position(0, 0, 1), d); + assertEquals(d4, new Dependency(new Dependency(a, d), c)); + + assertEquals(d3.replace(new Position(0, 1), c), new Dependency(d1, c)); + assertEquals(d3.replace(new Position(0, 0), c), new Dependency(c, c)); + + } + } diff --git a/src/test/java/terms/meta/MetaDependencyTermTest.java b/src/test/java/terms/meta/MetaDependencyTermTest.java index 46fc0d8..1824c8b 100644 --- a/src/test/java/terms/meta/MetaDependencyTermTest.java +++ b/src/test/java/terms/meta/MetaDependencyTermTest.java @@ -1,25 +1,21 @@ package terms.meta; import static org.junit.jupiter.api.Assertions.*; -import org.junit.jupiter.api.Test; - import java.util.HashMap; import java.util.Map; import java.util.Set; +import org.junit.jupiter.api.Test; + import models.algebra.Variable; import models.terms.DependencyTerm; import models.terms.RDLTerm; import models.terms.Resource; import models.terms.meta.MatchConstraint; import models.terms.meta.MetaDependencyTerm; -import models.terms.meta.MetaDynamicTerm; import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaResource; -import models.terms.meta.MetaTermPairGenerator; -import models.terms.meta.MetaTermPairGenerator.TermPair; import models.terms.meta.OrderVariableConstraint; -import utils.Utils; public class MetaDependencyTermTest { @@ -55,7 +51,7 @@ correctBinding.put(w.getVariableName(), b); correctBinding.put(p.getVariableName(), c); mt4.toString(); - Set tmp = mt1.isMatchedBy(t1, new MatchConstraint(binding, orderConstraint)); + Set tmp = mt1.isMatchedBy(t1, new MatchConstraint(binding, orderConstraint, new HashMap<>())); assertTrue(! tmp.isEmpty()); tmp = mt2.isMatchedBy(t1, tmp); assertTrue(! tmp.isEmpty()); @@ -81,7 +77,7 @@ MetaRDLTerm mt2 = new MetaDependencyTerm(x, v, w, y, z); Map binding = new HashMap<>(); Map orderConstraint = new HashMap<>(); - Set tmp = mt1.isMatchedBy(t1, new MatchConstraint(binding, orderConstraint)); + Set tmp = mt1.isMatchedBy(t1, new MatchConstraint(binding, orderConstraint, new HashMap<>())); assertTrue(! tmp.isEmpty()); tmp = mt2.isMatchedBy(t2, tmp); assertTrue(! tmp.isEmpty()); @@ -107,13 +103,48 @@ } @Test - void DynamicMatchTest2() { + void MetaDependencyTermReplaceTest() { MetaResource x = new MetaResource(new Variable("x")); - MetaDynamicTerm mt1 = new MetaDynamicTerm(x, (MetaTermPairGenerator) (i, depth, isLast) -> new TermPair(new MetaResource(new Variable("x" + i)), new MetaResource(new Variable("y"+i)))); - DependencyTerm d1 = new DependencyTerm(a, b, c); - DependencyTerm d2 = new DependencyTerm(a, b, c, d, e); - assertTrue(! mt1.isMatchedBy(d1).isEmpty()); - assertTrue(! mt1.isMatchedBy(d2).isEmpty()); + MetaResource y = new MetaResource(new Variable("y")); + MetaResource z = new MetaResource(new Variable("z")); + MetaResource w = new MetaResource(new Variable("w")); + MetaResource p = new MetaResource(new Variable("p")); + MetaResource q = new MetaResource(new Variable("q")); + MetaResource r = new MetaResource(new Variable("r")); + MetaResource s = new MetaResource(new Variable("s")); + + MetaDependencyTerm t1 = new MetaDependencyTerm(x, y, z); + MetaDependencyTerm t2 = new MetaDependencyTerm(p, q, r); + assertEquals(t1.replace(Map.of(x, p, y, q, z, r)), t2); + + MetaDependencyTerm t3 = new MetaDependencyTerm(t1, w, z); + MetaDependencyTerm t4 = new MetaDependencyTerm(t2, s, r); + assertEquals(t3.replace(Map.of(x, p, y, q, z, r, w, s)), t4); + } + + @Test + void SpecificTermMatchTest() { + 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); + MetaResource x = new MetaResource(new Variable("x")); + MetaResource y = new MetaResource(new Variable("y")); + + MetaDependencyTerm mdt = new MetaDependencyTerm(a, b, c); + DependencyTerm dt1 = new DependencyTerm(a, b, c); + DependencyTerm dt2 = new DependencyTerm(d, e, f); + DependencyTerm dt3 = new DependencyTerm(d, e, c); + MetaDependencyTerm mdt2 = new MetaDependencyTerm(x, y, c); + + assertFalse(mdt.isMatchedBy(dt1).isEmpty()); + assertTrue(mdt.isMatchedBy(dt2).isEmpty()); + + assertFalse(mdt2.isMatchedBy(dt1).isEmpty()); + assertTrue(mdt2.isMatchedBy(dt2).isEmpty()); + assertFalse(mdt2.isMatchedBy(dt3).isEmpty()); } } diff --git a/src/test/java/terms/meta/MetaDependencyTest.java b/src/test/java/terms/meta/MetaDependencyTest.java index 236202c..cc60e00 100644 --- a/src/test/java/terms/meta/MetaDependencyTest.java +++ b/src/test/java/terms/meta/MetaDependencyTest.java @@ -2,13 +2,13 @@ import static org.junit.jupiter.api.Assertions.*; import static utils.Utils.*; -import org.junit.jupiter.api.Test; - import java.util.HashMap; import java.util.HashSet; import java.util.Map; import java.util.Set; +import org.junit.jupiter.api.Test; + import models.algebra.Constant; import models.algebra.Variable; import models.terms.Dependency; @@ -19,12 +19,10 @@ import models.terms.meta.MetaDependency; import models.terms.meta.MetaDependencyTerm; import models.terms.meta.MetaDependencyTermVariable; -import models.terms.meta.MetaDynamicTerm; +import models.terms.meta.MetaDependencyVariable; import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaResource; -import models.terms.meta.MetaTermGenerator; import models.terms.meta.OrderVariableConstraint; -import utils.Utils; public class MetaDependencyTest { @@ -60,11 +58,11 @@ Map binding = new HashMap<>(); Map orderConst = new HashMap<>(); Set tmp = new HashSet<>(); - tmp = mt1.isMatchedBy(d1, new MatchConstraint(binding, orderConst)); + tmp = mt1.isMatchedBy(d1, new MatchConstraint(binding, orderConst, new HashMap<>())); assertTrue(! tmp.isEmpty()); assertEquals(tmp.iterator().next().getBinding().get(p.getVariableName()), a); assertEquals(tmp.iterator().next().getBinding().get(q.getVariableName()), b); - tmp = mt2.isMatchedBy(d2, new MatchConstraint(binding, orderConst)); + tmp = mt2.isMatchedBy(d2, new MatchConstraint(binding, orderConst, new HashMap<>())); assertTrue(!tmp.isEmpty()); tmp = mt3.isMatchedBy(d2, tmp); assertTrue(!tmp.isEmpty()); @@ -155,26 +153,54 @@ } @Test - void DynamicMatchTest() { + void MatchTest2() { + MetaDependencyVariable md1 = new MetaDependencyVariable(new Variable("md1"), new Variable("n")); + Dependency d = new Dependency(new Resource("a", 2), new Resource("b", 2), new Resource("c", 2)); + Set result = md1.isMatchedBy(d); + assertEquals(2, result.iterator().next().getOrderConstraint().get(new Variable("n")).getOrder()); + } + + @Test + void MetaDependencyReplaceTest() { MetaResource x = new MetaResource(new Variable("x")); - MetaDynamicTerm md1 = new MetaDynamicTerm(x, new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int index, int depth, boolean isLast) { - if (index != 0) { - return new MetaResource(new Variable("r" + index)); - } else { - return new MetaResource(new Variable("y")); - } - }}); - MetaRDLTerm md2 = new MetaDependency(new MetaResource(new Variable("y")), new MetaResource(new Variable("z"))); - Dependency d1 = new Dependency(a, b, c); - Dependency d2 = new Dependency(c, d); - Dependency d3 = new Dependency(b, d); + MetaResource y = new MetaResource(new Variable("y")); + MetaResource z = new MetaResource(new Variable("z")); + MetaResource w = new MetaResource(new Variable("w")); - Set tmp = md1.isMatchedBy(d1); - assertTrue(!tmp.isEmpty()); - assertTrue(! md2.isMatchedBy(d2, tmp).isEmpty()); - assertTrue(! md2.isMatchedBy(d3, tmp).isEmpty()); + MetaDependency md1 = new MetaDependency(x, y); + MetaDependency md2 = new MetaDependency(z, y); + assertEquals(md1.replace(Map.of(x, z)), md2); + + MetaDependency md3 = new MetaDependency(md1, y); + MetaDependency md4 = new MetaDependency(new MetaDependency(w, z), z); + assertEquals(md3.replace(Map.of(x, w, y, z)), md4); + + MetaDependency md5 = new MetaDependency(x, y, z); + MetaDependency md6 = new MetaDependency(x, y, w); + assertEquals(md5.replace(Map.of(z, w)), md6); + } + + @Test + void SpecificTermMatchTest() { + Resource a = new Resource("a", 1); + Resource b = new Resource("b", 1); + Resource c = new Resource("c", 1); + Resource d = new Resource("d", 1); + MetaResource x = new MetaResource(new Variable("x")); + + MetaDependency md1 = new MetaDependency(a, b); + MetaDependency md2 = new MetaDependency(a, x); + Dependency d1 = new Dependency(a, b); + Dependency d2 = new Dependency(a, c); + Dependency d3 = new Dependency(c, d); + + assertFalse(md1.isMatchedBy(d1).isEmpty()); + assertTrue(md1.isMatchedBy(d2).isEmpty()); + assertTrue(md1.isMatchedBy(d3).isEmpty()); + assertFalse(md2.isMatchedBy(d1).isEmpty()); + assertFalse(md2.isMatchedBy(d2).isEmpty()); + assertTrue(md2.isMatchedBy(d3).isEmpty()); + } } diff --git a/src/test/java/terms/meta/MetaDynamicDependencyTermTest.java b/src/test/java/terms/meta/MetaDynamicDependencyTermTest.java new file mode 100644 index 0000000..697a60e --- /dev/null +++ b/src/test/java/terms/meta/MetaDynamicDependencyTermTest.java @@ -0,0 +1,55 @@ +package terms.meta; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.jupiter.api.Test; + +import java.util.Map; + +import models.algebra.Variable; +import models.terms.DependencyTerm; +import models.terms.Resource; +import models.terms.meta.MetaDynamicDependencyTerm; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaTermGenerator; + +public class MetaDynamicDependencyTermTest { + + 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); + Resource h = new Resource("h", 1); + + @Test + void DynamicMatchTest() { + MetaDynamicDependencyTerm mdt1 = new MetaDynamicDependencyTerm( + 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("t")); + } + if (curIndex == 0) { + return new MetaDynamicDependencyTerm(this); + } + curIndex -= 1; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("s" + curDepth + "_" + curIndex)); + } + return new MetaEvaluatableTermVariable(new Variable("u" + curDepth + "_" + curIndex)); + } + } + ); + DependencyTerm t1 = new DependencyTerm(a, b, c); + DependencyTerm t2 = new DependencyTerm(t1, b, c, d, e); + assertFalse(mdt1.isMatchedBy(t1).isEmpty()); + assertFalse(mdt1.isMatchedBy(t2).isEmpty()); + } + + +} diff --git a/src/test/java/terms/meta/MetaDynamicDependencyTest.java b/src/test/java/terms/meta/MetaDynamicDependencyTest.java new file mode 100644 index 0000000..bada6d7 --- /dev/null +++ b/src/test/java/terms/meta/MetaDynamicDependencyTest.java @@ -0,0 +1,138 @@ +package terms.meta; +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.jupiter.api.Test; + +import java.util.HashMap; +import java.util.Map; +import java.util.Set; + +import models.algebra.Variable; +import models.terms.Dependency; +import models.terms.RDLTerm; +import models.terms.Resource; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDependency; +import models.terms.meta.MetaDependencyVariable; +import models.terms.meta.MetaDynamicDependency; +import models.terms.meta.MetaEvaluatableTermVariable; +import models.terms.meta.MetaRDLTerm; +import models.terms.meta.MetaRDLTermVariable; +import models.terms.meta.MetaResource; +import models.terms.meta.MetaTermGenerator; + +public class MetaDynamicDependencyTest { + + 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 DynamicDependencyMatchTest() { + MetaDynamicDependency md1 = new MetaDynamicDependency((ci, cd, mi, md, context) -> new MetaResource(new Variable("x" + ci))); + Dependency d1 = new Dependency(a, b, c, d); + assertFalse(md1.isMatchedBy(d1).isEmpty()); + + Dependency d2 = new Dependency(new Dependency(a, b), c); + Dependency d3 = new Dependency(d2, d, e); + MetaDynamicDependency md2 = 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 MetaDynamicDependency(this); + } + return new MetaResource(new Variable("x" + curDepth + "_" + curIndex)); + } + }); + assertFalse(md2.isMatchedBy(d2).isEmpty()); + assertFalse(md2.isMatchedBy(d3).isEmpty()); + + MetaResource x = new MetaResource(new Variable("x")); + MetaResource y = new MetaResource(new Variable("y")); + Dependency d4 = new Dependency(a, b); + MetaDynamicDependency md3 = new MetaDynamicDependency((ci, cd, mi, md, context) -> new MetaResource(new Variable("x" + ci)), x, y); + Set constraint = new MetaDependency(x, y).isMatchedBy(d4); + Dependency d5 = new Dependency(a, b, c); + constraint = md3.isMatchedBy(d5, constraint); + assertFalse(constraint.isEmpty()); + Map binding = new HashMap<>(); + binding.put(new Variable("x"), a); + binding.put(new Variable("y"), b); + binding.put(new Variable("x2"), c); + assertEquals(constraint.iterator().next().getBinding(), binding); + } + + @Test + void DynamicSubstituteTest() { + MetaDynamicDependency md1 = new MetaDynamicDependency((ci, cd, mi, md, context) -> new MetaResource(new Variable("x" + ci))); + Dependency d1 = new Dependency(a, b, c, d); + MatchConstraint result = md1.isMatchedBy(d1).iterator().next(); + RDLTerm generated = md1.substitute(result.getBinding(), result.getContext()); + assertEquals(generated, d1); + + Dependency d2 = new Dependency(new Dependency(a, b), c); + Dependency d3 = new Dependency(d2, d, e); + MetaDynamicDependency md2 = 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 MetaDynamicDependency(this); + } + return new MetaResource(new Variable("x" + curDepth + "_" + curIndex)); + } + }); + result = md2.isMatchedBy(d2).iterator().next(); + generated = md2.substitute(result.getBinding(), result.getContext()); + assertEquals(generated, d2); + } + + @Test + void DynamiMatchTest() { + MetaDynamicDependency md1 = 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 MetaDependencyVariable(new Variable("d")); + } + if (curIndex == 0) { + return new MetaDynamicDependency(this); + } + return new MetaRDLTermVariable(new Variable("x")); + } + } + ); + + Dependency d1 = new Dependency(a, b); + Dependency d2 = new Dependency(d1, b); + Dependency d3 = new Dependency(d2, b); + assertFalse(md1.isMatchedBy(d2).isEmpty()); + assertFalse(md1.isMatchedBy(d3).isEmpty()); + } + + @Test + void DynamicMatchTest2() { + MetaDynamicDependency md1 = new MetaDynamicDependency( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + if (curIndex == 0 && curDepth == maxDepth) { + return new MetaEvaluatableTermVariable(new Variable("se")); + } else if (curIndex == 0) { + return new MetaDynamicDependency(this); + } + return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex)); + } + } + ); + Dependency d1 = new Dependency(new Dependency(a, b, c), d, e); + assertFalse(md1.isMatchedBy(d1).isEmpty()); + Dependency d2 = new Dependency(new Dependency(a, b, c, d), e); + assertFalse(md1.isMatchedBy(d2).isEmpty()); + } + +} diff --git a/src/test/java/terms/meta/MetaDynamicTermTest.java b/src/test/java/terms/meta/MetaDynamicTermTest.java deleted file mode 100644 index 33be890..0000000 --- a/src/test/java/terms/meta/MetaDynamicTermTest.java +++ /dev/null @@ -1,160 +0,0 @@ -package terms.meta; -import static org.junit.jupiter.api.Assertions.*; - -import org.junit.jupiter.api.Test; - -import models.algebra.Constant; -import models.algebra.Variable; -import models.terms.Dependency; -import models.terms.DependencyTerm; -import models.terms.Resource; -import models.terms.meta.MatchConstraint; -import models.terms.meta.MetaDynamicTerm; -import models.terms.meta.MetaRDLTerm; -import models.terms.meta.MetaResource; -import models.terms.meta.MetaTermGenerator; -import utils.Utils; - -public class MetaDynamicTermTest { - - 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); - Resource h = new Resource("h", 1); - Resource i = new Resource("i", 3); - Resource j = new Resource("j", 2); - Resource k = new Resource("k", 2); - Resource l = new Resource("l", 1); - Resource m = new Resource("m", 1); - Resource n = new Resource("n", 0); - Resource o = new Resource("o", 0); - - @Test - void GenerateTest1() { - MetaDynamicTerm mt1 = new MetaDynamicTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int index, int depth, boolean isLast) { - if (isLast) { - return new MetaResource(new Variable("x")); - } - return new MetaDynamicTerm(this, new MetaResource(new Variable("y" + depth))); - } - }, - new MetaResource(new Variable("y")) - ); - Dependency d1 = new Dependency(a, b); - Dependency d2 = new Dependency(d1, c); - Dependency d3 = new Dependency(d2, d); - assertTrue(! mt1.isMatchedBy(d1).isEmpty()); - assertTrue(! mt1.isMatchedBy(d2).isEmpty()); - assertTrue(! mt1.isMatchedBy(d3).isEmpty()); - - MatchConstraint result = mt1.isMatchedBy(d3).iterator().next(); - MetaRDLTerm mt2 = mt1.dependencyGenerate(result.getBinding()); - assertTrue(mt2.isMatchedBy(d3, result).contains(result)); - - assertEquals(mt1.substitute(result.getBinding()), d3); - } - - @Test - void GenerateTest2() { - MetaDynamicTerm mt1 = new MetaDynamicTerm( - new MetaResource(new Variable("x")), - (MetaTermGenerator) (i, d, l) -> new MetaResource(new Variable("y" + i)) - ); - Dependency d1 = new Dependency(a, b); - Dependency d2 = new Dependency(a, b, c); - Dependency d3 = new Dependency(a, b, c, d); - - assertTrue(! mt1.isMatchedBy(d1).isEmpty()); - assertTrue(! mt1.isMatchedBy(d2).isEmpty()); - assertTrue(! mt1.isMatchedBy(d3).isEmpty()); - } - - @Test - void GenerateTest3() { - MetaDynamicTerm mt1 = new MetaDynamicTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int index, int depth, boolean isLast) { - if (isLast) { - return new MetaResource(new Variable("x")); - } - return new MetaDynamicTerm(this, (MetaTermGenerator) (i, d, l) -> new MetaResource(new Variable("y" + (d+1) + "," + i))); - } - }, - (MetaTermGenerator) (i, d, l) -> new MetaResource(new Variable("y0," + i)) - ); - Dependency d1 = new Dependency(a, b, c, d); - Dependency d2 = new Dependency(d1, c, d); - assertTrue(! mt1.isMatchedBy(d1).isEmpty()); - assertTrue(! mt1.isMatchedBy(d2).isEmpty()); - - MatchConstraint result = mt1.isMatchedBy(d2).iterator().next(); - MetaRDLTerm mt2 = mt1.dependencyGenerate(result.getBinding()); - assertTrue(mt2.isMatchedBy(d2, result).contains(result)); - - assertEquals(mt1.substitute(result.getBinding()), d2); - } - - @Test - void GenerateTest4() { - MetaDynamicTerm mt1 = new MetaDynamicTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int index, int depth, boolean isLast) { - if (isLast) { - return new MetaResource(new Variable("x")); - } - return new MetaDynamicTerm(this, new MetaResource(new Variable("y" + depth)), new MetaResource(new Variable("z" + depth))); - } - }, - new MetaResource(new Variable("y")), - new MetaResource(new Variable("z")) - ); - - DependencyTerm t1 = new DependencyTerm(a, b, c); - DependencyTerm t2 = new DependencyTerm(t1, d, e); - DependencyTerm t3 = new DependencyTerm(t2, d, e); - assertTrue(! mt1.isMatchedBy(t1).isEmpty()); - assertTrue(! mt1.isMatchedBy(t2).isEmpty()); - assertTrue(! mt1.isMatchedBy(t3).isEmpty()); - - MatchConstraint result = mt1.isMatchedBy(t3).iterator().next(); - assertTrue(! mt1.dependencyTermGenerate(result.getBinding()).isMatchedBy(t3, result).isEmpty()); - assertEquals(mt1.substitute(result.getBinding()), t3); - - } - - @Test - void GenerateTest5() { - MetaDynamicTerm mt1 = new MetaDynamicTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int index, int depth, boolean isLast) { - if (isLast) { - return new MetaResource(new Variable("x"), new Variable("m")); - } - return new MetaDynamicTerm(this, new MetaResource(new Variable("y" + depth), new Variable("m-" + (depth+1))), new MetaResource(new Variable("z" + depth), new Variable("m-" + (depth+1)))); - } - }, - new MetaResource(new Variable("y"), new Constant("0")), - new MetaResource(new Variable("z"), new Constant("0")) - ); - - DependencyTerm t1 = new DependencyTerm(i, j, k); - DependencyTerm t2 = new DependencyTerm(t1, l, m); - DependencyTerm t3 = new DependencyTerm(t2, n, o); - assertTrue(! mt1.isMatchedBy(t3).isEmpty()); - - MatchConstraint result = mt1.isMatchedBy(t3).iterator().next(); - assertTrue(! mt1.dependencyTermGenerate(result.getBinding()).isMatchedBy(t3, result).isEmpty()); - assertEquals(mt1.substitute(result.getBinding()), t3); - } - -} diff --git a/src/test/java/terms/meta/MetaResourceVariableTest.java b/src/test/java/terms/meta/MetaResourceVariableTest.java index eed180b..ff7c7c4 100644 --- a/src/test/java/terms/meta/MetaResourceVariableTest.java +++ b/src/test/java/terms/meta/MetaResourceVariableTest.java @@ -3,6 +3,8 @@ import static org.junit.jupiter.api.Assertions.*; import static utils.Utils.*; +import java.util.Map; + import org.junit.jupiter.api.Test; import models.algebra.Variable; @@ -159,4 +161,12 @@ assertTrue(! x.isMatchedBy(a).isEmpty()); } + @Test + void MetaResourceReplaceTest() { + MetaResource x = new MetaResource(new Variable("x")); + MetaResource y = new MetaResource(new Variable("y")); + assertEquals(x.replace(Map.of(x, y)), y); + } + + } diff --git a/src/test/java/utils/Utils.java b/src/test/java/utils/Utils.java index 95ed96f..5500ed6 100644 --- a/src/test/java/utils/Utils.java +++ b/src/test/java/utils/Utils.java @@ -1,15 +1,18 @@ package utils; -import constants.Types; +import java.util.Random; + import models.algebra.Expression; -import models.algebra.Type; +import models.formulas.EquationFormula; +import models.terms.DependencyTerm; +import models.terms.EvaluatableTerm; +import models.terms.Resource; import parser.Parser; import parser.Parser.TokenStream; public class Utils { - public static Type INT = Types.typeInt; private static TokenStream stream = new Parser.TokenStream(); private static Parser parser = new Parser(stream); @@ -18,4 +21,10 @@ return parser.parseTerm(stream); } + public static EquationFormula in(EvaluatableTerm x, EvaluatableTerm y) { + Random random = new Random(); + int n = random.nextInt(900) + 100; + return new EquationFormula(new DependencyTerm(y, new Resource("zzz1" + n, y.getOrder()), new Resource("zzz2" + n, y.getOrder() )), x); + } + }