in meta/src/main/java/org/arend/lib/meta/linear/LinearSolver.java [172:264]
private List<BigInteger> solveEquations(List<? extends Equation<CompiledTerm>> equations, int var) {
if (equations.isEmpty()) {
return null;
}
if (var < 0) {
List<BigInteger> result = new ArrayList<>(equations.size());
boolean found = false;
for (Equation<CompiledTerm> equation : equations) {
if (!found && equation.operation == Equation.Operation.LESS) {
result.add(BigInteger.ONE);
found = true;
} else {
result.add(BigInteger.ZERO);
}
}
return found ? result : null;
}
Map<Integer, Integer> indexMap1 = new HashMap<>(); // maps an index in equations to an index in newEquations
Map<Integer, List<Pair<Integer, BigInteger>>> indexMap2 = new HashMap<>(); // maps an index in equations to a set of pairs of the form (an index in newEquations, a coefficient)
List<Equation<CompiledTerm>> newEquations = new ArrayList<>();
for (int j1 = 0; j1 < equations.size(); j1++) {
Equation<CompiledTerm> equation1 = equations.get(j1);
int cmp1 = equation1.lhsTerm.getCoef(var).compareTo(equation1.rhsTerm.getCoef(var));
if (cmp1 == 0) {
indexMap1.put(j1, newEquations.size());
newEquations.add(equation1);
continue;
}
for (int j2 = 0; j2 < j1; j2++) {
equation1 = equations.get(j1);
Equation<CompiledTerm> equation2 = equations.get(j2);
int cmp2 = equation2.lhsTerm.getCoef(var).compareTo(equation2.rhsTerm.getCoef(var));
if (cmp2 == 0) continue;
if (!(cmp1 < 0 && cmp2 > 0 || cmp1 > 0 && cmp2 < 0)) {
continue;
}
boolean swap = cmp1 > 0;
if (swap) {
Equation<CompiledTerm> tmp = equation1;
equation1 = equation2;
equation2 = tmp;
}
BigInteger c1 = equation1.rhsTerm.getCoef(var).subtract(equation1.lhsTerm.getCoef(var));
BigInteger c2 = equation2.lhsTerm.getCoef(var).subtract(equation2.rhsTerm.getCoef(var));
BigInteger gcd = c1.gcd(c2);
BigInteger d1 = c2.divide(gcd);
BigInteger d2 = c1.divide(gcd);
List<BigInteger> lhs = new ArrayList<>();
List<BigInteger> rhs = new ArrayList<>();
for (int i = 0; i < var; i++) {
lhs.add(d1.multiply(equation1.lhsTerm.getCoef(i)).add(d2.multiply(equation2.lhsTerm.getCoef(i))));
rhs.add(d1.multiply(equation1.rhsTerm.getCoef(i)).add(d2.multiply(equation2.rhsTerm.getCoef(i))));
}
indexMap2.computeIfAbsent(j1, k -> new ArrayList<>()).add(new Pair<>(newEquations.size(), swap ? d2 : d1));
indexMap2.computeIfAbsent(j2, k -> new ArrayList<>()).add(new Pair<>(newEquations.size(), swap ? d1 : d2));
newEquations.add(new Equation<>(null, equation1.operation == Equation.Operation.EQUALS && equation2.operation == Equation.Operation.EQUALS
? Equation.Operation.EQUALS
: equation1.operation == Equation.Operation.LESS || equation2.operation == Equation.Operation.LESS
? Equation.Operation.LESS
: Equation.Operation.LESS_OR_EQUALS,
new CompiledTerm(null, lhs, Collections.emptySet()), new CompiledTerm(null, rhs, Collections.emptySet())));
}
}
List<BigInteger> solution = solveEquations(newEquations, var - 1);
if (solution == null) return null;
List<BigInteger> result = new ArrayList<>(equations.size());
for (int i = 0; i < equations.size(); i++) {
Integer j = indexMap1.get(i);
if (j != null) {
result.add(solution.get(j));
} else {
List<Pair<Integer, BigInteger>> list = indexMap2.get(i);
if (list != null) {
BigInteger s = BigInteger.ZERO;
for (Pair<Integer, BigInteger> pair : list) {
s = s.add(solution.get(pair.proj1).multiply(pair.proj2));
}
result.add(s);
} else {
result.add(BigInteger.ZERO);
}
}
}
return result;
}