diff --git a/src/main/java/Main.java b/src/main/java/Main.java index 85ce966..18049d3 100644 --- a/src/main/java/Main.java +++ b/src/main/java/Main.java @@ -7,6 +7,7 @@ import models.algebra.Type; import models.algebra.Variable; import models.formulas.DependencyFormula; +import models.formulas.EquationFormula; import models.terms.Dependency; import models.terms.DependencyTerm; import models.terms.EvaluatableTerm; @@ -23,7 +24,7 @@ public static void main(String[] args) { // - sandbox2(); + sandbox4(); } static void sandbox() { @@ -35,10 +36,41 @@ Resource a = new Resource("a", 1); Resource b = new Resource("b", 1); Resource c = new Resource("c", 1); + Resource d = new Resource("d", 1); DependencyFormula d1 = new DependencyFormula(a, b); DependencyFormula d2 = new DependencyFormula(b, c); - DependencyFormula d3 = new DependencyFormula(a, c); - ProofSystem ps = new ProofSystem(Set.of(d1, d2), d3); + DependencyFormula d3 = new DependencyFormula(c, d); + DependencyFormula d4 = new DependencyFormula(a, d); + ProofSystem ps = new ProofSystem(Set.of(d1, d2, d3), d4); + ps.dependencyInference(); + System.out.println(ps.getState().getHistory().getHistoryString(d4)); + } + + static void sandbox3() { + Resource a = new Resource("a", 1); + Resource b = new Resource("b", 1); + Resource c = new Resource("c", 1); + Resource d = new Resource("d", 1); + Resource e = new Resource("e", 1); + DependencyFormula d1 = new DependencyFormula(a, b); + DependencyFormula d2 = new DependencyFormula(b, c); + DependencyFormula d3 = new DependencyFormula(c, d); + DependencyFormula d4 = new DependencyFormula(d, e); + DependencyFormula d5 = new DependencyFormula(a, e); + ProofSystem ps = new ProofSystem(Set.of(d1, d2, d3, d4), d5); + ps.dependencyInference(); + System.out.println(ps.getState().getHistory().getHistoryString(d5)); + } + + static void sandbox4() { + Resource a = new Resource("a", 2); + Resource b = new Resource("b", 2); + Resource c = new Resource("c", 1); + Resource d = new Resource("d", 1); + DependencyFormula d2 = new DependencyFormula(new Dependency(a, b), c); + EquationFormula eq1 = new EquationFormula(d, d); + DependencyFormula d3 = new DependencyFormula(new DependencyTerm(a, b, d), c, d); + ProofSystem ps = new ProofSystem(Set.of(d2, eq1), d3); ps.dependencyInference(); System.out.println(ps.getState().getHistory().getHistoryString(d3)); } 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/inference/InferenceHistory.java b/src/main/java/inference/InferenceHistory.java index 95a0db3..0c8c756 100644 --- a/src/main/java/inference/InferenceHistory.java +++ b/src/main/java/inference/InferenceHistory.java @@ -26,16 +26,19 @@ } public String getHistoryString(Formula conclusion) { + if (! inferenceHistory.containsKey(conclusion)) { + return "Inference failed"; + } List result = new ArrayList<>(); Deque q = new ArrayDeque<>(); q.add(conclusion); + result.add(conclusion.toString()); while (! q.isEmpty()) { Formula formula = q.pollFirst(); if (! inferenceHistory.containsKey(formula)) { continue; } InferenceHistoryNode node = inferenceHistory.get(formula).iterator().next(); - result.add(conclusion.toString()); result.add("--------------------------------" + node.getUsedRule().getName()); result.add(node.getAssumptions().stream().map(v -> v.toString()).collect(Collectors.joining(", "))); for (Formula f: node.getAssumptions()) { diff --git a/src/main/java/inference/InferenceRule.java b/src/main/java/inference/InferenceRule.java index c7d7755..78bb131 100644 --- a/src/main/java/inference/InferenceRule.java +++ b/src/main/java/inference/InferenceRule.java @@ -9,8 +9,10 @@ import lombok.Getter; import models.formulas.Formula; import models.formulas.meta.MetaFormula; +import models.terms.RDLTerm; import models.terms.meta.MatchConstraint; import models.terms.meta.MetaVariable; +import utils.Permutation; public class InferenceRule { @@ -23,7 +25,6 @@ protected MetaFormula conclusion; protected InferenceOrderConstraint defaultOrderConstraint; - @Getter protected List missingVariables = new ArrayList<>(); protected InferenceRule(String name) { @@ -46,9 +47,30 @@ this(name, assumptions, conclusion, null); } - public Set derive(List assumptions) { - return derive(assumptions, MatchConstraint.createDefault()); + return derive(assumptions, Set.of()); + } + + 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())) { + MatchConstraint constraint = MatchConstraint.createDefault(); + boolean flg = false; + for (int i = 0; i < missingVariables.size(); i++) { + if (missingVariables.get(i).isMatchedBy(terms.get(i)).isEmpty()) { + flg = true; + break; + } + constraint.setBinding(missingVariables.get(i).getVariableName(), terms.get(i)); + } + if (flg) continue; + result.addAll(derive(assumptions, constraint)); + } + return result; + } } public Set derive(List assumptions, MatchConstraint constraint) { @@ -82,6 +104,9 @@ return matchResult; } + public List getMissingVariables(List assumptions, MatchConstraint constraint) { + return this.missingVariables; + } // public Set apply(Set formulas, Set existTerms) { // List> matchFormulas = new ArrayList<>(); diff --git a/src/main/java/inference/ProofState.java b/src/main/java/inference/ProofState.java index 880bd70..7531106 100644 --- a/src/main/java/inference/ProofState.java +++ b/src/main/java/inference/ProofState.java @@ -6,6 +6,7 @@ import java.util.Map; import java.util.Set; +import exceptions.MissingContextException; import lombok.Getter; import models.formulas.DependencyFormula; import models.formulas.EquationFormula; @@ -13,6 +14,7 @@ import models.formulas.meta.MetaEquationFormula; import models.terms.Dependency; import models.terms.EvaluatableTerm; +import models.terms.RDLTerm; import models.terms.meta.MetaRDLTerm; @Getter @@ -93,7 +95,7 @@ } } - public void addFormuals(Set existFormulas) { + public void addFormuals(Set existFormulas) { for (Formula formula: existFormulas) { formulas.add(formula); if (formula instanceof DependencyFormula df) { @@ -130,12 +132,16 @@ Set lhs = new HashSet<>(); Set rhs = new HashSet<>(); for (EvaluatableTerm term : evaluatableTerms) { - if (! conclusionLeft.isMatchedBy(term).isEmpty()) { - lhs.add(term); - } - if (! conclusionRight.isMatchedBy(term).isEmpty()) { - rhs.add(term); - } + 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++) { @@ -160,6 +166,13 @@ this.history.addHistory(conclusion, node); } + public Set getExistTerms() { + Set result = new HashSet<>(); + result.addAll(dependencies); + result.addAll(evaluatableTerms); + return result; + } + record ConclusionMatchedTerm(Set leftSideHands, Set rightSideHands) {}; } diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index f96eb7b..d6dd188 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -200,24 +200,40 @@ } } else if (conclusion instanceof DependencyFormula dep) { while((! state.getDependencyFormulas().contains(dep))) { - state.addFormuals(dependencyInferenceStep()); + Set result = dependencyInferenceStep(); + Set sizeConstraintOk = new HashSet<>(); + for (DependencyFormula df: result) { + if (dep.getMaxIndex() >= df.getMaxIndex()) { + if (! state.getFormulas().contains(df)) { + sizeConstraintOk.add(df); + } + } + } + if (sizeConstraintOk.size() == 0) { + break; + } + state.addFormuals(sizeConstraintOk); } } } - public Set dependencyInferenceStep() { - Set result = new HashSet<>(); + 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)); } for (List formulas: Product.product(matchedFormulas)) { - Set results = rule.derive(formulas); + Set results = rule.derive(formulas, state.getExistTerms()); for (Formula res: results) { state.addHistory(formulas, rule, res); } - result.addAll(results); + for (Formula f: results) { + if (f instanceof DependencyFormula df) { + result.add(df); + } + } } } return result; diff --git a/src/main/java/inference/axioms/ArgumentReduction.java b/src/main/java/inference/axioms/ArgumentReduction.java index 28b3e3d..13d89be 100644 --- a/src/main/java/inference/axioms/ArgumentReduction.java +++ b/src/main/java/inference/axioms/ArgumentReduction.java @@ -9,6 +9,7 @@ import inference.InferenceRule; 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; @@ -71,7 +72,13 @@ 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) { diff --git a/src/main/java/inference/axioms/CompositeMapping.java b/src/main/java/inference/axioms/CompositeMapping.java index 8406ca1..6263d1d 100644 --- a/src/main/java/inference/axioms/CompositeMapping.java +++ b/src/main/java/inference/axioms/CompositeMapping.java @@ -86,7 +86,7 @@ for (MatchConstraint res: matchResult) { try { int k = (Integer) res.getContext().get("k"); - int n = (Integer) res.getContext().get("n"); + 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) { diff --git a/src/main/java/inference/axioms/MapComposition.java b/src/main/java/inference/axioms/MapComposition.java index 8f024e8..5276f81 100644 --- a/src/main/java/inference/axioms/MapComposition.java +++ b/src/main/java/inference/axioms/MapComposition.java @@ -5,6 +5,7 @@ import java.util.Map; import java.util.Set; +import exceptions.MissingContextException; import exceptions.SubstituteFailedException; import inference.EquationAxiom; import models.Position; @@ -94,6 +95,12 @@ @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) { diff --git a/src/main/java/inference/axioms/UncurriedMapping.java b/src/main/java/inference/axioms/UncurriedMapping.java index 407f48e..ef26ff7 100644 --- a/src/main/java/inference/axioms/UncurriedMapping.java +++ b/src/main/java/inference/axioms/UncurriedMapping.java @@ -19,7 +19,7 @@ import models.terms.meta.MetaTermGenerator; import utils.ExpressionUtils; -public class UncurriedMapping extends InferenceRule{ +public class UncurriedMapping extends InferenceRule { public UncurriedMapping() { super("Uncurried Mapping"); @@ -73,7 +73,7 @@ } ) ); - + this.missingVariables.add(new MetaEvaluatableTermVariable(new Variable("ve"))); } @Override diff --git a/src/main/java/inference/axioms/Uncurrying.java b/src/main/java/inference/axioms/Uncurrying.java index b5d4edb..f5e8299 100644 --- a/src/main/java/inference/axioms/Uncurrying.java +++ b/src/main/java/inference/axioms/Uncurrying.java @@ -5,6 +5,7 @@ import java.util.Map; import java.util.Set; +import exceptions.MissingContextException; import exceptions.SubstituteFailedException; import inference.EquationAxiom; import models.Position; @@ -52,6 +53,9 @@ @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) { 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/test/java/inference/inferencerule/DependencyAxiomTest.java b/src/test/java/inference/inferencerule/DependencyAxiomTest.java new file mode 100644 index 0000000..61494eb --- /dev/null +++ b/src/test/java/inference/inferencerule/DependencyAxiomTest.java @@ -0,0 +1,126 @@ +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 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, f); + MatchConstraint constraint = MatchConstraint.createDefault(); + constraint.getContext().put("j", 2); + constraint.setBinding(new Variable("ue0"), 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 2ef365c..0000000 --- a/src/test/java/inferencerule/DependencyAxiomTest.java +++ /dev/null @@ -1,126 +0,0 @@ -package 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 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, f); - MatchConstraint constraint = MatchConstraint.createDefault(); - constraint.getContext().put("j", 2); - constraint.setBinding(new Variable("ue0"), 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/inferencerule/EqualityAxiomTest.java b/src/test/java/inferencerule/EqualityAxiomTest.java deleted file mode 100644 index 91955f8..0000000 --- a/src/test/java/inferencerule/EqualityAxiomTest.java +++ /dev/null @@ -1,137 +0,0 @@ -package inferencerule; -import static org.junit.jupiter.api.Assertions.*; - -import org.junit.jupiter.api.Test; - -import java.util.HashSet; -import java.util.List; -import java.util.Set; - -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/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()); +// } +// +//}