private List solveEquations()

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;
  }