diff --git a/src/main/java/Main.java b/src/main/java/Main.java index 1f2f61e..5aad8dd 100644 --- a/src/main/java/Main.java +++ b/src/main/java/Main.java @@ -32,16 +32,16 @@ static void sandbox() { - Expression tmp = utils.ExpressionUitls.parse("x"); + Expression tmp = utils.ExpressionUtils.parse("x"); System.out.println(tmp); - tmp = utils.ExpressionUitls.parse("(x + 5) * 3"); + tmp = utils.ExpressionUtils.parse("(x + 5) * 3"); Map nums = new HashMap<>(); - int a = utils.ExpressionUitls.getCoefficientAndConstantsFromExpression(tmp, nums, 1); + int a = utils.ExpressionUtils.getCoefficientAndConstantsFromExpression(tmp, nums, 1); System.out.println(tmp); System.out.println(a); System.out.println(nums); - int b = utils.ExpressionUitls.getConstantValue(new Constant("3")); + int b = utils.ExpressionUtils.getConstantValue(new Constant("3")); System.out.println(b); } diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index 61391fb..4677ca7 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -38,7 +38,7 @@ import models.terms.meta.MetaRDLTerm; import models.terms.meta.MetaTermGenerator; import models.terms.meta.OrderConstraint; -import utils.ExpressionUitls; +import utils.ExpressionUtils; import utils.Product; public class ProofSystem { @@ -181,7 +181,7 @@ (assumptions) -> 1, (conclusion) -> (conclusion.getMaxIndex() - 1) / 2 ); - + public static final InferenceRule mapComposition = new MapComposition(); public static final InferenceRule constantness = new Constantness(); @@ -264,7 +264,7 @@ new MetaDependencyFormula(new MetaDependencyVariable(new Variable("d"), new Variable("n"))) ), List.of(), - new MetaDependencyFormula(new MetaDependencyVariable(new Variable("d"), new Variable("n")), new MetaEvaluatableTermVariable(new Variable("p"), ExpressionUitls.parse("n - 1"))), + new MetaDependencyFormula(new MetaDependencyVariable(new Variable("d"), new Variable("n")), new MetaEvaluatableTermVariable(new Variable("p"), ExpressionUtils.parse("n - 1"))), null, null, null, diff --git a/src/main/java/inference/axioms/Constantness.java b/src/main/java/inference/axioms/Constantness.java index 7f5380f..47a3c0d 100644 --- a/src/main/java/inference/axioms/Constantness.java +++ b/src/main/java/inference/axioms/Constantness.java @@ -1,11 +1,135 @@ package inference.axioms; +import java.util.HashMap; +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.Constant; +import models.algebra.Variable; +import models.formulas.EquationFormula; +import models.formulas.Formula; +import models.formulas.meta.MetaEquationFormula; +import models.terms.DependencyTerm; +import models.terms.meta.MatchConstraint; +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; public class Constantness extends EquationAxiom { public Constantness() { super("Constantness"); - } + + @Override + protected Set apply(List assumptions, MatchConstraint constraint) { + Set result = new HashSet<>(); + Map context = new HashMap<>(); + result.add(constraint); + int prevOrder = 0; + int m = 0; + int n = 1; + if (assumptions.get(0) instanceof EquationFormula eq) { + if (eq.getLeftSideHand() instanceof DependencyTerm dt) { + prevOrder = dt.getDependingTerm().getOrder(); + m = prevOrder; + } else { + return new HashSet<>(); + } + } else { + return new HashSet<>(); + } + + for (int i = 1; i < assumptions.size(); i++) { + if (assumptions.get(i) instanceof EquationFormula eq2) { + if (eq2.getLeftSideHand() instanceof DependencyTerm dt) { + int order = dt.getDependingTerm().getOrder(); + n = order; + if (prevOrder - order != 1) { + return new HashSet<>(); + } + prevOrder = order; + } else { + return new HashSet<>(); + } + } else { + return new HashSet<>(); + } + } + + if (n >= m) { + return new HashSet<>(); + } + + if (m - n != assumptions.size()) { + return new HashSet<>(); + } + + for (int i = 0; i < assumptions.size(); i++) { + Formula assumption = assumptions.get(i); + MetaDependencyTerm mdt = new MetaDependencyTerm( + new MetaEvaluatableTermVariable(new Variable("r" + i), new Constant("" + (m + i))), + new MetaEvaluatableTermVariable(new Variable("xxx" + i)), + new MetaEvaluatableTermVariable(new Variable("yyy" + i)) + ); + MetaEquationFormula mef = new MetaEquationFormula(mdt, new MetaEvaluatableTermVariable(new Variable("t" + i))); + result = mef.isMatchedBy(assumption, result); + if (result.isEmpty()) { + return new HashSet<>(); + } + } + + MetaEquationFormula conclusion = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + int n = (Integer) context.get("n"); + int m = (Integer) context.get("m"); + int i = maxDepth - curDepth - 1; + if (curDepth == maxDepth - 1) { + return new MetaDependencyTerm( + new MetaEvaluatableTermVariable(new Variable("se"), new Constant("" + n)), + new MetaEvaluatableTermVariable(new Variable("r" + i), new Constant("" + (m + i))), + new MetaEvaluatableTermVariable(new Variable("t" + i)) + ); + } + if (curIndex == 0) { + return new MetaDynamicDependencyTerm(this); + } else if (curIndex == 1) { + return new MetaEvaluatableTermVariable(new Variable("r" + i), new Constant("" + (m + i))); + } + return new MetaEvaluatableTermVariable(new Variable("t" + i)); + } + } + ), + new MetaEvaluatableTermVariable(new Variable("se"), new Constant("" + n)) + ); + + Set subRes = new HashSet<>(); + for (MatchConstraint con: result) { + try { + int maxIndex = 3; + int maxDepth = m - n; + context.put("maxIndex", maxIndex); + context.put("maxDepth", maxDepth); + context.put("n", n); + context.put("m", m); + subRes.add(conclusion.substitution(con.getBinding(), context)); + } catch (SubstituteFailedException e) { + continue; + } + } + + return super.apply(assumptions, constraint); + } + + + } diff --git a/src/main/java/inference/axioms/MapComposition.java b/src/main/java/inference/axioms/MapComposition.java index 78296f1..e6f30b0 100644 --- a/src/main/java/inference/axioms/MapComposition.java +++ b/src/main/java/inference/axioms/MapComposition.java @@ -1,10 +1,182 @@ package inference.axioms; +import java.util.HashMap; +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.MetaDependencyFormula; +import models.formulas.meta.MetaEquationFormula; +import models.terms.meta.MatchConstraint; +import models.terms.meta.MetaDependencyTerm; +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 -= 1; + context.put("firstAssumptionIndex", curIndex + 1); + return new MetaEvaluatableTermVariable(new Variable("v" + curIndex)); + } + }, + new MetaEvaluatableTermVariable(new Variable("t")) + ) + ) + ); + 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("secondAssumptionIndex", curIndex + 1); + return new MetaEvaluatableTermVariable(new Variable("u" + curIndex)); + } + + }, + new MetaEvaluatableTermVariable(new Variable("s")), + new MetaEvaluatableTermVariable(new Variable("t")) + ) + ) + ); + this.conclusion = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 3; + int secondAssumptionIndex = (Integer)context.get("secondAssumptionIndex"); + if (curIndex >= secondAssumptionIndex * 2) { + return null; + } + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("u" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("y" + curIndex / 2)); + } + }, + new MetaEvaluatableTermVariable(new Variable("s")), + new MetaEvaluatableTermVariable(new Variable("t")), + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + int firstAssumptionIndex = (Integer)context.get("firstAssumptionIndex"); + if (curIndex >= firstAssumptionIndex * 2) { + return null; + } + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("v" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2)); + }}, + new MetaEvaluatableTermVariable(new Variable("t")) + ) + ), + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + int firstAssumptionIndex = (Integer)context.get("firstAssumptionIndex"); + int secondAssumptionIndex = (Integer)context.get("secondAssumptionIndex"); + if (curIndex >= firstAssumptionIndex * 2 + secondAssumptionIndex * 2) { + return null; + } + if (curIndex < firstAssumptionIndex * 2) { + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("v" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2)); + } + curIndex -= firstAssumptionIndex * 2; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("u" + curIndex / 2)); + } + return new MetaEvaluatableTermVariable(new Variable("y" + curIndex / 2)); + }}, + new MetaEvaluatableTermVariable(new Variable("s")) + ) + ); } + @Override + protected Set apply(List assumptions, MatchConstraint constraint) { + Map context = new HashMap<>(); + Set matchResult = new HashSet<>(); + matchResult.add(constraint); + if (assumptions.size() < 2) { + return new HashSet<>(); + } + for (int i = 0; i < 2; i++) { + matchResult = this.assumptions.get(i).isMatchedBy(assumptions.get(i), matchResult, context); + if (matchResult.isEmpty()) { + return new HashSet<>(); + } + } + int firstAssumptionIndex = (Integer)context.get("firstAssumptionIndex"); + int secondAssumptionIndex = (Integer)context.get("secondAssumptionIndex"); + if (assumptions.size() < 2 + firstAssumptionIndex + secondAssumptionIndex) { + return new HashSet<>(); + } + for (int i = 0; i < firstAssumptionIndex; i++) { + Formula assumption = assumptions.get(i + 2); + MetaDependencyTerm mdt = new MetaDependencyTerm( + new MetaEvaluatableTermVariable(new Variable("v" + i)), + new MetaEvaluatableTermVariable(new Variable("xxx" + i)), + new MetaEvaluatableTermVariable(new Variable("yyy" + i)) + ); + MetaEquationFormula mef = new MetaEquationFormula(mdt, new MetaEvaluatableTermVariable(new Variable("x" + i))); + matchResult = mef.isMatchedBy(assumption, matchResult); + if (matchResult.isEmpty()) { + return new HashSet<>(); + } + } + for (int i = 0; i < secondAssumptionIndex; i++) { + Formula assumption = assumptions.get(i + 2 + firstAssumptionIndex); + MetaDependencyTerm mdt = new MetaDependencyTerm( + new MetaEvaluatableTermVariable(new Variable("u" + i)), + new MetaEvaluatableTermVariable(new Variable("xxxx" + i)), + new MetaEvaluatableTermVariable(new Variable("yyyy" + i)) + ); + MetaEquationFormula mef = new MetaEquationFormula(mdt, new MetaEvaluatableTermVariable(new Variable("y" + i))); + matchResult = mef.isMatchedBy(assumption, matchResult); + if (matchResult.isEmpty()) { + return new HashSet<>(); + } + } + Set subRes = new HashSet<>(); + for (MatchConstraint con: matchResult) { + try { + int maxIndex = 10000; + int maxDepth = 1; + context.put("maxIndex", maxIndex); + context.put("maxDepth", maxDepth); + subRes.add(conclusion.substitution(con.getBinding(), context)); + } catch (SubstituteFailedException e) { + continue; + } + } + return subRes; + } + + + } diff --git a/src/main/java/inference/axioms/RightNormalization.java b/src/main/java/inference/axioms/RightNormalization.java index 5d6f893..f3b5427 100644 --- a/src/main/java/inference/axioms/RightNormalization.java +++ b/src/main/java/inference/axioms/RightNormalization.java @@ -1,12 +1,218 @@ package inference.axioms; +import java.util.HashMap; +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.Expression; +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.MetaDependency; +import models.terms.meta.MetaDependencyTerm; +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 RightNormalization extends EquationAxiom { + private final Expression n1 = ExpressionUtils.parse("n-1"); + public RightNormalization() { super("RIght Normalization"); + 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("firstAssumptionIndex", curIndex + 1); + return new MetaEvaluatableTermVariable(new Variable("v" + curIndex), n1); + } + }, + new MetaDependency( + new MetaEvaluatableTermVariable(new Variable("s"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")) + ) + ) + ) + ); + 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("secondAssumptionIndex", curIndex + 1); + return new MetaEvaluatableTermVariable(new Variable("w" + curIndex), n1); + } + }, + new MetaEvaluatableTermVariable(new Variable("u"), n1) + ) + ) + ); + assumptions.add( + new MetaEquationFormula( + new MetaDependencyTerm( + new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("xxx")), + new MetaEvaluatableTermVariable(new Variable("yyy")) + ), + new MetaEvaluatableTermVariable(new Variable("u"), n1) + ) + ); + + conclusion = new MetaEquationFormula( + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + int firstAssumptionIndex = (Integer) context.get("firstAssumptionIndex"); + int secondAssumptionIndex = (Integer) context.get("secondAssumptionIndex"); + if (curIndex >= (firstAssumptionIndex + secondAssumptionIndex) * 2) { + return null; + } + if (curIndex < firstAssumptionIndex * 2) { + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("v" + curIndex / 2), n1); + } + return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2)); + } + curIndex -= firstAssumptionIndex * 2; + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("w" + curIndex / 2), n1); + } + return new MetaEvaluatableTermVariable(new Variable("y" + curIndex / 2)); + } + }, + new MetaDependencyTerm( + new MetaEvaluatableTermVariable(new Variable("s"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("u"), n1) + ) + ), + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + int firstAssumptionIndex = (Integer) context.get("firstAssumptionIndex"); + if (curIndex >= firstAssumptionIndex * 2) { + return null; + } + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("v" + curIndex / 2), n1); + } + return new MetaEvaluatableTermVariable(new Variable("x" + curIndex / 2)); + } + + }, + new MetaDependencyTerm( + new MetaEvaluatableTermVariable(new Variable("s"), new Variable("n")), + new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")), + new MetaDynamicDependencyTerm( + new MetaTermGenerator() { + @Override + public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map context) { + curIndex -= 1; + int secondAssumptionIndex = (Integer) context.get("secondAssumptionIndex"); + if (curIndex >= secondAssumptionIndex * 2) { + return null; + } + if (curIndex % 2 == 0) { + return new MetaEvaluatableTermVariable(new Variable("w" + curIndex / 2), n1); + } + return new MetaEvaluatableTermVariable(new Variable("y" + curIndex / 2)); + } + + }, + new MetaEvaluatableTermVariable(new Variable("u"), n1) + ) + ) + ) + ); } + + @Override + protected Set apply(List assumptions, MatchConstraint constraint) { + if (assumptions.size() < 3) { + return new HashSet<>(); + } + Set result = new HashSet<>(); + result.add(constraint); + Map context = new HashMap<>(); + for (int i = 0; i < 3; i++) { + result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result, context); + if (result.isEmpty()) { + return new HashSet<>(); + } + } + + int firstAssumptionIndex = (Integer) context.get("firstAssumptionIndex"); + int secondAssumptionIndex = (Integer) context.get("secondAssumptionIndex"); + if (assumptions.size() < 3 + firstAssumptionIndex + secondAssumptionIndex) { + return new HashSet<>(); + } + for (int i = 0; i < firstAssumptionIndex; i++) { + Formula assumption = assumptions.get(i + 3); + MetaEquationFormula mef = new MetaEquationFormula( + new MetaDependencyTerm( + new MetaEvaluatableTermVariable(new Variable("v" + i), n1), + new MetaEvaluatableTermVariable(new Variable("xxxx" + i)), + new MetaEvaluatableTermVariable(new Variable("yyyy" + i)) + ), + new MetaEvaluatableTermVariable(new Variable("x" + i)) + ); + result = mef.isMatchedBy(assumption, result); + if (result.isEmpty()) { + return new HashSet<>(); + } + } + + for(int i = 0; i < secondAssumptionIndex; i++) { + Formula assumption = assumptions.get(i + 3 + firstAssumptionIndex); + MetaEquationFormula mef = new MetaEquationFormula( + new MetaDependencyTerm( + new MetaEvaluatableTermVariable(new Variable("w" + i), n1), + new MetaEvaluatableTermVariable(new Variable("xxyy" + i)), + new MetaEvaluatableTermVariable(new Variable("yyxx" + i)) + ), + new MetaEvaluatableTermVariable(new Variable("y" + i)) + ); + result = mef.isMatchedBy(assumption, result); + if (result.isEmpty()) { + return new HashSet<>(); + } + } + + Set subRes = new HashSet<>(); + for (MatchConstraint con: result) { + try { + int maxIndex = 10000; + int maxDepth = 1; + context.put("maxIndex", maxIndex); + context.put("maxDepth", maxDepth); + subRes.add(conclusion.substitution(con.getBinding(), context)); + } catch (SubstituteFailedException e) { + continue; + } + } + return subRes; + } + + } diff --git a/src/main/java/models/terms/meta/MetaDynamicDependencyTerm.java b/src/main/java/models/terms/meta/MetaDynamicDependencyTerm.java index bf0f69e..4a5217a 100644 --- a/src/main/java/models/terms/meta/MetaDynamicDependencyTerm.java +++ b/src/main/java/models/terms/meta/MetaDynamicDependencyTerm.java @@ -1,7 +1,5 @@ package models.terms.meta; -import com.google.common.collect.TreeMultiset; - import java.util.ArrayList; import java.util.Arrays; import java.util.List; @@ -10,6 +8,8 @@ import java.util.stream.Collectors; import java.util.stream.IntStream; +import com.google.common.collect.TreeMultiset; + import exceptions.SubstituteFailedException; import exceptions.SyntaxException; import models.algebra.Variable; @@ -29,6 +29,7 @@ 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); diff --git a/src/main/java/models/terms/meta/MetaVariable.java b/src/main/java/models/terms/meta/MetaVariable.java index 34fa8b6..56f3237 100644 --- a/src/main/java/models/terms/meta/MetaVariable.java +++ b/src/main/java/models/terms/meta/MetaVariable.java @@ -13,7 +13,7 @@ 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 { @@ -30,7 +30,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"); @@ -52,7 +52,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"); 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/inferencerule/EqualityAxiomTest.java b/src/test/java/inferencerule/EqualityAxiomTest.java index 70c3a8a..8536cd6 100644 --- a/src/test/java/inferencerule/EqualityAxiomTest.java +++ b/src/test/java/inferencerule/EqualityAxiomTest.java @@ -1,19 +1,21 @@ package inferencerule; import static org.junit.jupiter.api.Assertions.*; -import org.junit.jupiter.api.Test; - import java.util.List; import java.util.Set; +import org.junit.jupiter.api.Test; + import inference.ProofSystem; import inference.axioms.RightSubstitution; 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 utils.Utils; public class EqualityAxiomTest { @@ -29,6 +31,8 @@ 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); @Test void ReflexivityTest() { @@ -93,6 +97,57 @@ } @Test + void MapCompositionTest() { + DependencyFormula df1 = new DependencyFormula(a, b, c); + DependencyFormula df2 = new DependencyFormula(b, d, e); + EquationFormula eq1 = Utils.in(f, c); + EquationFormula eq2 = Utils.in(g, d); + EquationFormula eq3 = Utils.in(h, e); + Set result = ProofSystem.mapComposition.apply(df2, df1, eq2, eq3, eq1); + EquationFormula conc1 = new EquationFormula( + new DependencyTerm( + a, b, new DependencyTerm(b, d, g, e, h), c, f + ), + new DependencyTerm(a, d, g, e, h, c, f) + ); + assertTrue(result.contains(conc1)); + } + + @Test + void ConstantnessTest() { + + } + + @Test + void RightNormalizationTest() { + DependencyFormula d1 = new DependencyFormula(new Dependency(m, n), a, b); + DependencyFormula d2 = new DependencyFormula(c, d, e); + EquationFormula eq1 = Utils.in(c, n); + EquationFormula eq2 = Utils.in(f, a); + EquationFormula eq3 = Utils.in(g, b); + EquationFormula eq4 = Utils.in(h, d); + EquationFormula eq5 = Utils.in(j, e); + Set result = ProofSystem.rightNormalization.apply(d1, d2, eq1, eq2, eq3, eq4, eq5); + EquationFormula conc1 = new EquationFormula( + new DependencyTerm( + new DependencyTerm( + m, n, c + ), + a, f, b, g, d, h, e, j + ), + new DependencyTerm( + new DependencyTerm( + m ,n, new DependencyTerm( + c, d, h, e, j + ) + ), + a, f, b, g + ) + ); + assertTrue(result.contains(conc1)); + } + + @Test void PseudoConstantnessTest() { Set result = ProofSystem.pseudoConstantness.apply(new DependencyFormula(a, b)); assertTrue(result.contains(new EquationFormula(new DependencyTerm(a, b, b), a))); diff --git a/src/test/java/utils/Utils.java b/src/test/java/utils/Utils.java index 95ed96f..4de8f2c 100644 --- a/src/test/java/utils/Utils.java +++ b/src/test/java/utils/Utils.java @@ -1,9 +1,15 @@ package utils; +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; +import models.terms.Resource; import parser.Parser; import parser.Parser.TokenStream; @@ -18,4 +24,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); + } + }