diff --git a/src/main/java/inference/EquationAxiom.java b/src/main/java/inference/EquationAxiom.java index 64a89b0..c330507 100644 --- a/src/main/java/inference/EquationAxiom.java +++ b/src/main/java/inference/EquationAxiom.java @@ -6,7 +6,6 @@ import exceptions.SubstituteFailedException; import models.formulas.DependencyFormula; -import models.formulas.EquationFormula; import models.formulas.Formula; import models.formulas.meta.MetaEquationFormula; import models.formulas.meta.MetaFormula; @@ -35,30 +34,37 @@ return apply(assumptions, term, MatchConstraint.createDefault()); } - public Set apply(Listassumptions, EvaluatableTerm leftSideHand, MatchConstraint constraint) { + 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); - MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion; - Set conclusionMatchResult = conclusionLeftSideHandMatch(leftSideHand, matchResult); - if (conclusionMatchResult.isEmpty()) { - isLeft = false; - conclusionMatchResult = conclusionRightSideHandMatch(leftSideHand, matchResult); - if (conclusionMatchResult.isEmpty()) { - return new HashSet<>(); - } + 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 { - EquationFormula eq = metaConclusion.substitution(matchRes.getBinding(), matchRes.getContext()); if (isLeft) { - result.add(eq.getRightSideHand()); + result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getRightSideHand()).substitute(matchRes.getBinding(), matchRes.getContext())); } else { - result.add(eq.getLeftSideHand()); + result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getLeftSideHand()).substitute(matchRes.getBinding(), matchRes.getContext())); } } catch (SubstituteFailedException e) { continue; 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/ProofSystem.java b/src/main/java/inference/ProofSystem.java index 5ab033f..369868b 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -4,6 +4,7 @@ import java.util.List; import java.util.Set; +import inference.axioms.Constantness; import inference.axioms.Identity; import inference.axioms.LeftSubstitution; import inference.axioms.MapComposition; @@ -73,7 +74,7 @@ public static final EquationAxiom mapComposition = new MapComposition(); // -// public static final InferenceRule constantness = new Constantness(); + public static final EquationAxiom constantness = new Constantness(); // // public static final InferenceRule rightNormalization = new RightNormalization(); // diff --git a/src/main/java/inference/axioms/Identity.java b/src/main/java/inference/axioms/Identity.java index 8566314..dc24c39 100644 --- a/src/main/java/inference/axioms/Identity.java +++ b/src/main/java/inference/axioms/Identity.java @@ -42,22 +42,30 @@ } @Override - public Set apply(Listassumptions, EvaluatableTerm term) { + 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 = new HashSet<>(); - matchResult.add(MatchConstraint.createDefault()); + Set matchResult = assumptionMatch(assumptions, constraint); + Set conclusionMatchResult = conclusionLeftSideHandMatch(term, matchResult); if (conclusionMatchResult.isEmpty()) { - return new HashSet<>(); + isLeft = false; + conclusionMatchResult = conclusionRightSideHandMatch(term, matchResult); + if (conclusionMatchResult.isEmpty()) { + return new HashSet<>(); + } } MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion; - MetaEvaluatableTermVariable right = (MetaEvaluatableTermVariable) metaConclusion.getRightSideHand(); for (MatchConstraint matchRes: conclusionMatchResult) { try { - result.add((EvaluatableTerm) right.substitute(matchRes.getBinding(), matchRes.getContext())); + if (isLeft) { + result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getRightSideHand()).substitute(matchRes.getBinding(), matchRes.getContext())); + } else { + result.add((EvaluatableTerm)((MetaRDLTerm) metaConclusion.getLeftSideHand()).substitute(matchRes.getBinding(), matchRes.getContext())); + } } catch (SubstituteFailedException e) { continue; } diff --git a/src/main/java/inference/axioms/LeftSubstitution.java b/src/main/java/inference/axioms/LeftSubstitution.java index 8588ecd..a06c4bd 100644 --- a/src/main/java/inference/axioms/LeftSubstitution.java +++ b/src/main/java/inference/axioms/LeftSubstitution.java @@ -1,14 +1,11 @@ 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.EquationFormula; import models.formulas.Formula; import models.formulas.meta.MetaEquationFormula; import models.terms.EvaluatableTerm; @@ -58,37 +55,10 @@ @Override public Set apply(Listassumptions, EvaluatableTerm term) { - Set result = new HashSet<>(); - boolean isLeft = true; - if (assumptions.size() < this.assumptions.size()) { - return new HashSet<>(); - } - Set matchResult = assumptionMatch(assumptions); - - MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion; - Set conclusionMatchResult = conclusionLeftSideHandMatch(term, matchResult); - if (conclusionMatchResult.isEmpty()) { - isLeft = false; - conclusionMatchResult = conclusionRightSideHandMatch(term, matchResult); - if (conclusionMatchResult.isEmpty()) { - return new HashSet<>(); - } - } - for (MatchConstraint matchRes: conclusionMatchResult) { - matchRes.getContext().put("maxIndex", term.getMaxIndex()); - matchRes.getContext().put("maxDepth", term.getMaxDepth()); - try { - EquationFormula eq = metaConclusion.substitution(matchRes.getBinding(), matchRes.getContext()); - if (isLeft) { - result.add(eq.getRightSideHand()); - } else { - result.add(eq.getLeftSideHand()); - } - } catch (SubstituteFailedException e) { - continue; - } - } - return result; + 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 index f8a3ce3..1a36bc1 100644 --- a/src/main/java/inference/axioms/MapComposition.java +++ b/src/main/java/inference/axioms/MapComposition.java @@ -117,13 +117,13 @@ } @Override - public Set apply(Listassumptions, EvaluatableTerm term) { + 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); + Set matchResult = assumptionMatch(assumptions, constraint); MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion; Set conclusionMatchResult = conclusionLeftSideHandMatch(term, matchResult); diff --git a/src/main/java/inference/axioms/RightSubstitution.java b/src/main/java/inference/axioms/RightSubstitution.java index 41c7d01..6868fd8 100644 --- a/src/main/java/inference/axioms/RightSubstitution.java +++ b/src/main/java/inference/axioms/RightSubstitution.java @@ -1,14 +1,11 @@ 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.EquationFormula; import models.formulas.Formula; import models.formulas.meta.MetaDependencyFormula; import models.formulas.meta.MetaEquationFormula; @@ -79,37 +76,10 @@ @Override public Set apply(Listassumptions, EvaluatableTerm term) { - Set result = new HashSet<>(); - boolean isLeft = true; - if (assumptions.size() < this.assumptions.size()) { - return new HashSet<>(); - } - Set matchResult = assumptionMatch(assumptions); - - MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion; - Set conclusionMatchResult = conclusionLeftSideHandMatch(term, matchResult); - if (conclusionMatchResult.isEmpty()) { - isLeft = false; - conclusionMatchResult = conclusionRightSideHandMatch(term, matchResult); - if (conclusionMatchResult.isEmpty()) { - return new HashSet<>(); - } - } - for (MatchConstraint matchRes: conclusionMatchResult) { - matchRes.getContext().put("maxIndex", term.getMaxIndex()); - matchRes.getContext().put("maxDepth", term.getMaxDepth()); - try { - EquationFormula eq = metaConclusion.substitution(matchRes.getBinding(), matchRes.getContext()); - if (isLeft) { - result.add(eq.getRightSideHand()); - } else { - result.add(eq.getLeftSideHand()); - } - } catch (SubstituteFailedException e) { - continue; - } - } - return result; + 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/test/java/inferencerule/EqualityAxiomTest.java b/src/test/java/inferencerule/EqualityAxiomTest.java index eca1496..1985275 100644 --- a/src/test/java/inferencerule/EqualityAxiomTest.java +++ b/src/test/java/inferencerule/EqualityAxiomTest.java @@ -31,6 +31,7 @@ Resource l = new Resource("l", 1); Resource m = new Resource("m", 2); Resource n = new Resource("n", 2); + Resource o = new Resource("o", 3); @Test void ReflexivityTest() { @@ -93,7 +94,12 @@ @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