diff --git a/src/main/java/inference/In.java b/src/main/java/inference/In.java index f8bee34..520120a 100644 --- a/src/main/java/inference/In.java +++ b/src/main/java/inference/In.java @@ -1,24 +1,23 @@ package inference; -import java.util.HashMap; import java.util.HashSet; import java.util.Map; import java.util.Set; import lombok.Getter; import lombok.RequiredArgsConstructor; -import models.algebra.Constant; 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.MetaResource; import models.terms.meta.MetaTermGenerator; @@ -29,134 +28,78 @@ private final EvaluatableTerm leftSideHand; private final EvaluatableTerm rightSideHand; - private static final MetaDependencyTerm domainMembershipConclusionLeftSideHand = new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - context.put("1-" + curDepth, curIndex); - context.put("depth1", maxDepth); - if (curDepth == maxDepth && curIndex == 0) { - return new MetaEvaluatableTermVariable(new Variable("ue1")); - } else if (curIndex == 0) { - return new MetaDynamicDependencyTerm(this); - } - int used = (Integer) context.getOrDefault("used1", 4); - context.put("used1", used + 1); - curIndex -= 1; - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("te" + used / 2)); + 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)); + } } - return new MetaEvaluatableTermVariable(new Variable("ue" + used / 2)); - } - } + ), + new MetaConstant(new Variable("c")) ); - private static final MetaDependencyTerm domainMembershipConclusionRightSideHand = new MetaDynamicDependencyTerm( + static final MetaDependencyTerm domainMembershipConclusionLeftSideHand = new MetaDynamicDependencyTerm( new MetaTermGenerator() { @Override public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - context.put("2-" + curDepth, curIndex); - context.put("depth2", maxDepth); + maxIndex = (Integer) context.get("" + curDepth); if (curDepth == maxDepth && curIndex == 0) { - return new MetaEvaluatableTermVariable(new Variable("te1")); - } else if (curIndex == 0) { - return new MetaDynamicDependencyTerm(this); - } - int used = (Integer) context.getOrDefault("used2", 4); - context.put("used2", used + 1); - curIndex -= 1; - if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("te" + used / 2)); + return new MetaEvaluatableTermVariable(new Variable("ue")); } - return new MetaEvaluatableTermVariable(new Variable("ue" + used / 2)); - } - } - ); - - private static final MetaDynamicDependencyTerm domainMembershipAssumptionLeftSideHand = new MetaDynamicDependencyTerm( - new MetaTermGenerator() { - @Override - public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { - if (curIndex - 1 >= (Integer) context.get("1-" + curDepth)) { + curIndex -= 1; + if (curIndex >= maxIndex) { return null; } - if (curIndex == 0 && curDepth == maxDepth) { - return new MetaDependencyTerm( - new MetaEvaluatableTermVariable(new Variable("se")), - new MetaEvaluatableTermVariable(new Variable("te1")), - new MetaEvaluatableTermVariable(new Variable("ue1")) - ); - } - else if (curIndex == 0) { - return new MetaDynamicDependencyTerm(this); - } - curIndex -= 1; - int used = (Integer) context.getOrDefault("used3", 4); - context.put("used3", used + 1); if (curIndex % 2 == 0) { - return new MetaEvaluatableTermVariable(new Variable("te" + used / 2)); + return new MetaEvaluatableTermVariable(new Variable("te" + curDepth + "_" + curIndex/2)); } - return new MetaEvaluatableTermVariable(new Variable("ue" + used / 2)); + return new MetaEvaluatableTermVariable(new Variable("ue" + curDepth + "_" + curIndex/2)); } } ); - private static final MetaEvaluatableTermVariable codomainMembershipConclusionLeftSideHand = new MetaEvaluatableTermVariable(new Variable("ve")); - private static final MetaEvaluatableTermVariable codomainMembershipConclusionRightSideHand = new MetaEvaluatableTermVariable(new Variable("se")); - - public Set deriveRule() { - Set result = new HashSet<>(); - result.addAll(deriveByDomainMemberShip()); - result.addAll(deriveByCodomainMemberShip()); - 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; + 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)); } } - 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( + + 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) { @@ -167,13 +110,121 @@ return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2)); } }, - constraint.getBinding().get(codomainMembershipConclusionRightSideHand.getVariableName()) - ); - result.add(new MetaEquationFormula(left, constraint.getBinding().get(codomainMembershipConclusionLeftSideHand.getVariableName()))); + 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.getLeftSideHand().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(); diff --git a/src/main/java/inference/InferenceRule.java b/src/main/java/inference/InferenceRule.java index e47a0a6..c8c1ffc 100644 --- a/src/main/java/inference/InferenceRule.java +++ b/src/main/java/inference/InferenceRule.java @@ -5,6 +5,7 @@ import java.util.List; import java.util.Set; +import exceptions.SubstituteFailedException; import lombok.Getter; import models.formulas.DependencyFormula; import models.formulas.EquationFormula; @@ -99,9 +100,13 @@ } for (MatchConstraint constraint: matchResult) { if (missingVariables.size() == 0) { - Formula conclusion = this.conclusion.substitution(constraint.getBinding(), constraint.getContext()); - if (conclusionCheck(conclusion, constraint, formulas)) { - result.add(conclusion); + 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)) { @@ -109,10 +114,15 @@ 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); + try { + Formula conclusion = this.conclusion.substitution(constraint.getBinding(), constraint.getContext()); + if (conclusionCheck(conclusion, constraint, formulas)) { + result.add(conclusion); + } + } catch (SubstituteFailedException e) { + continue; } + } } } diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index 85cda79..99f8f3e 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -1,25 +1,28 @@ 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 com.google.common.collect.BoundType; 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.EvaluatableTerm; import models.terms.RDLTerm; +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 ProofSystem { @@ -67,7 +70,60 @@ ); -// public static final InferenceRule rightSubstitution = new RightSubstitution(); + public static final InferenceRule rightSubstitution = new InferenceRule( + "Right Substitution", + List.of( + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("ue")), + new MetaEvaluatableTermVariable(new Variable("ve")) + ), + 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 MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ) + ), + 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("te" + 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("te" + 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")) + ) + ) + ); // // public static final InferenceRule leftSubstitution = new EquationAxiom( // "Left Substitution", @@ -266,6 +322,7 @@ ); */ + private static final List axioms = List.of( // reflexivity, // symmetry, @@ -293,187 +350,62 @@ // codomainMembership2 ); - public static void debug() { - for (var axiom : axioms) { - System.out.println(axiom); - System.out.println("=================================================================================================="); + + private Set dependencyFormulas = new HashSet<>(); + private Set equationFormulas = new HashSet<>(); + private Map>> dependencyInMap = new HashMap<>(); + private Map> ins = new HashMap<>(); + private Set terms = new HashSet<>(); + + public void addDependency(Dependency dependency) { + addDependency(new DependencyFormula(dependency)); + } + + public void addDependency(DependencyFormula dependency) { + dependencyFormulas.add(dependency); + addExistTerms(dependency); + Dependency dep = dependency.getDependency(); + dependencyInMap.put(dependency, new ArrayList<>()); + for (EvaluatableTerm dependedTerm : dep.getDependedTerms()) { + if (ins.containsKey(dependedTerm)) { + dependencyInMap.get(dependency).add(new HashSet<>(ins.get(dependedTerm))); + } else { + dependencyInMap.get(dependency).add(new HashSet<>()); + } } } - 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<>()); + public void addEquationFormula(EquationFormula eq) { + addExistTerms(eq); + equationFormulas.add(eq); + Set ins = In.deriveIn(eq); + for (In in : ins) { + this.ins.computeIfAbsent(in.getRightSideHand(), t -> new HashSet<>()).add(in); + for (DependencyFormula depFormula : dependencyInMap.keySet()) { + int startIndex = depFormula.getDependency().getDependedTerms().headMultiset(in.getRightSideHand(), BoundType.OPEN).size(); + int count = depFormula.getDependency().getDependedTerms().count(in.getRightSideHand()); + for (int i = 0; i < count; i++) { + dependencyInMap.get(depFormula).get(startIndex + i).add(in); } - 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; } - 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); -// } -// } -// } -// for(List applyFormulas : Product.product(matchedFormulas)) { -// if (appliedFormulas.contains(applyFormulas)) continue; -// Set applied = axiom.apply(applyFormulas); -// if (applied != null) { -// for (Formula formula : applied) { -// if (! formulas.contains(formula)) { -// addExistTerms(formula, existTerms); -// proofGraph.put(formula, new AxiomResult(axiom, applyFormulas)); -// } -// } -// result.addAll(applied); -// appliedFormulas.add(applyFormulas); -// } -// } - return result; + private void dependencyInMap(DependencyFormula key, int index, In in) { + } - private static void addExistTerms(Formula formula, Set existTerms) { + + private void addExistTerms(Formula formula) { 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()); + terms.addAll(leftSideHand.getSubTerms(RDLTerm.class).values()); + terms.addAll(rightSideHand.getSubTerms(RDLTerm.class).values()); } else if (formula instanceof DependencyFormula) { RDLTerm dependency = ((DependencyFormula) formula).getDependency(); - existTerms.addAll(dependency.getSubTerms(RDLTerm.class).values()); + terms.addAll(dependency.getSubTerms(RDLTerm.class).values()); } } - 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; - } - for (EvaluatableTerm nextNode : graph.getOrDefault(curNode, new ArrayList<>())) { - if (visited.contains(nextNode)) { - continue; - } - visited.add(nextNode); - que.add(nextNode); - } - } - return false; - } - - 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; - } } 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/MetaRDLTerm.java b/src/main/java/models/terms/meta/MetaRDLTerm.java index 7167e81..e1d4968 100644 --- a/src/main/java/models/terms/meta/MetaRDLTerm.java +++ b/src/main/java/models/terms/meta/MetaRDLTerm.java @@ -13,6 +13,7 @@ import models.terms.LinearRightNormalizedType; import models.terms.RDLTerm; import models.terms.Resource; +import models.terms.ResourceConstant; @Getter public abstract class MetaRDLTerm extends RDLTerm { @@ -157,7 +158,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/MetaResource.java b/src/main/java/models/terms/meta/MetaResource.java index f98039d..6602702 100644 --- a/src/main/java/models/terms/meta/MetaResource.java +++ b/src/main/java/models/terms/meta/MetaResource.java @@ -1,16 +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.Variable; -import models.terms.RDLTerm; -import models.terms.Resource; -import models.terms.ResourceConstant; @Getter public class MetaResource extends MetaVariable { @@ -27,32 +20,32 @@ 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, constraint.cloneContext())); +// } +// else if (binding.get(this.variableName).equals(another)) { +// result.add(new MatchConstraint(binding, orderConstraint, constraint.cloneContext())); +// } +// return result; +// } @Override public MetaResource cloneWithName(String name) { diff --git a/src/test/java/inferencerule/EqualityAxiomTest.java b/src/test/java/inferencerule/EqualityAxiomTest.java index 21af142..abb46b3 100644 --- a/src/test/java/inferencerule/EqualityAxiomTest.java +++ b/src/test/java/inferencerule/EqualityAxiomTest.java @@ -7,11 +7,13 @@ import org.junit.jupiter.api.Test; import inference.ProofSystem; +import models.formulas.DependencyFormula; import models.formulas.EquationFormula; import models.formulas.Formula; import models.terms.DependencyTerm; import models.terms.RDLTerm; import models.terms.Resource; +import utils.Utils; public class EqualityAxiomTest { @@ -57,6 +59,13 @@ @Test void RightSubTest() { + EquationFormula eq1 = new EquationFormula(a, b); + DependencyFormula d1 = new DependencyFormula(c, d); + Set formulas = ProofSystem.rightSubstitution.apply(Set.of(eq1, d1), Set.of(e, f)); + assertTrue(formulas.isEmpty()); + EquationFormula eq2 = Utils.in(e, d); + formulas = ProofSystem.rightSubstitution.apply(Set.of(eq1, d1, eq2), Set.of(e, f)); + assertEquals(formulas.size(), 1); } @Test diff --git a/src/test/java/utils/Utils.java b/src/test/java/utils/Utils.java index 4de8f2c..5500ed6 100644 --- a/src/test/java/utils/Utils.java +++ b/src/test/java/utils/Utils.java @@ -3,9 +3,7 @@ import java.util.Random; -import constants.Types; import models.algebra.Expression; -import models.algebra.Type; import models.formulas.EquationFormula; import models.terms.DependencyTerm; import models.terms.EvaluatableTerm; @@ -15,7 +13,6 @@ public class Utils { - public static Type INT = Types.typeInt; private static TokenStream stream = new Parser.TokenStream(); private static Parser parser = new Parser(stream);