public ConcreteExpression solve()

in meta/src/main/java/org/arend/lib/meta/equation/RingSolver.java [294:384]
53 lines of code
5 McCabe index (conditional complexity)

    public ConcreteExpression solve(TermCompiler.CompiledTerm term1, TermCompiler.CompiledTerm term2, List<Equality> axioms) {
      int numVariables = Integer.max(numVarsInNF(term1.nf), numVarsInNF(term2.nf));
      for (Equality axiom : axioms) {
        numVariables = Integer.max(numVarsInNF(axiom.lhsTerm.nf), numVariables);
        numVariables = Integer.max(numVarsInNF(axiom.rhsTerm.nf), numVariables);
      }

      var p = termToPoly(term1, numVariables).subtr(termToPoly(term2, numVariables));
      var idealGen = new ArrayList<Poly<BigInteger>>();

      for (Equality axiom : axioms) {
        idealGen.add(termToPoly(axiom.lhsTerm, numVariables).subtr(termToPoly(axiom.rhsTerm, numVariables)));
      }

      var idealCoeffs = new GroebnerIM(new Buchberger()).computeGenDecomposition(p, idealGen);

      if (idealCoeffs == null) {
        return null;
      }

      var genCoeffs = new ArrayList<ConcreteExpression>();
      var axiomDiffs = new ArrayList<ConcreteExpression>();

      for (int i = 0;i < axioms.size(); ++i) {
        var axiom = axioms.get(i);
        var axiomDiff = minusRingElement(axiom.lhsTerm.originalExpr, axiom.rhsTerm.originalExpr);
        var axDiffIsZero = factory.appBuilder(factory.ref(meta.toZero.getRef()))
          .app(factory.core(instance), false)
          .app(axiom.lhsTerm.originalExpr, false)
          .app(axiom.rhsTerm.originalExpr, false)
          .app(axiom.bindingExpr)
          .build();
        var coeffTerm = nfToRingTerm(polyToNF(idealCoeffs.get(i)));

        coeffTerm = factory.appBuilder(factory.ref(meta.ringInterpret.getRef()))
          .app(factory.ref(dataRef), false)
          .app(coeffTerm).build();
        axiomDiffs.add(minusRingTerm(axiom.lhsTerm.concrete, axiom.rhsTerm.concrete));
        genCoeffs.add(factory.tuple(coeffTerm, axiomDiff, axDiffIsZero));
      }

      /*
      var axDiffIsZeroPrf = new ArrayList<ConcreteExpression>();

      for (Equality axiom : axioms) {
        axiomDiffs.add(minusRingTerm(axiom.lhsTerm.concrete, axiom.rhsTerm.concrete));
        axDiffIsZeroPrf.add(factory.appBuilder(factory.ref(meta.toZero.getRef()))
                .app(factory.core(instance), false)
                .app(axiom.lhsTerm.originalExpr)
                .app(axiom.rhsTerm.originalExpr)
                .app(axiom.binding)
                .build());
      }

       */

      // term1 - term2 = sum_i idealCoeffs(i) * (axiom(i).L - axiom(i).R)
      var decompositionProof = factory.appBuilder(factory.ref(meta.commRingTermsEq.getRef()))
        .app(factory.ref(dataRef), false)
        .app(minusRingTerm(term1.concrete, term2.concrete))
        .app(idealGenDecompRingTerm(idealCoeffs, axiomDiffs))
        .app(factory.ref(meta.ext.prelude.getIdp().getRef()))
        .build();

      /*
      // term1 - term2 = 0
      var isZeroProof = factory.appBuilder(factory.ref(meta.ext.concat.getRef()))
              .app(decompositionProof)
              .app(idealGenDecompEqZero(idealCoeffs, axDiffIsZeroPrf))
              .build();

       */

      // sum_i idealCoeffs(i) * (axiom(i).L - axiom(i).R) = 0
      var idealGenDecompEqZero = factory.appBuilder(factory.ref(meta.gensZeroToIdealZero.getRef()))
        .app(MonoidSolver.formList(genCoeffs, factory, meta.ext.nil, meta.ext.cons))
        .build();

      // term1 - term2 = 0
      var isZeroProof = factory.appBuilder(factory.ref(meta.ext.concat.getRef()))
        .app(decompositionProof)
        .app(idealGenDecompEqZero)
        .build();

      return factory.appBuilder(factory.ref(meta.fromZero.getRef()))
        .app(factory.core(instance), false)
        .app(term1.originalExpr, false)
        .app(term2.originalExpr, false)
        .app(isZeroProof)
        .build();
    }